Library HoTT.Utf8

Require Export Coq.Unicode.Utf8.
Require Export HoTT.Basics.Utf8.
Require Import HoTT.Basics HoTT.Types.Arrow HoTT.Types.Prod HoTT.Types.Sum.
Require Import Modalities.Identity.
Require Import HIT.Circle HIT.TwoSphere HoTT.Truncations Homotopy.Suspension.

Notation Type₀ := Type0.
Notation pr₁ := pr1.
Notation pr₂ := pr2.
Local Open Scope fibration_scope.
Notation "x ₁" := (x.1) : fibration_scope.
Notation "x ₂" := (x.2) : fibration_scope.
Notation "g ∘ f" := (g o f)%function : function_scope.
Notation "g ∘ᴱ f" := (g oE f)%equiv : equiv_scope.
Notation "f *ᴱ g" := (f ×E g)%equiv : equiv_scope.
Notation "f ×ᴱ g" := (f ×E g)%equiv : equiv_scope.
Notation "A × B" := (A × B)%type : type_scope.
Notation "f +ᴱ g" := (f +E g)%equiv : equiv_scope.
We copy the HoTT-Agda library with regard to path concatenation.
Notation "p • q" := (p @ q)%path : path_scope.
Notation "p '⁻¹'" := (p^)%path : path_scope.
Notation "p •' q" := (p @ q)%path : long_path_scope.
Add error messages so people aren't intensely confused by using an almost identical character.
Infix "∙" := ltac:(fail "You used '∙' (BULLET OPERATOR, #x2219) when you probably meant to use '•' (BULLET, #x2022)") (only parsing) : path_scope.
Notation "A ≃ B" := (A <~> B) : type_scope.
Notation "f '⁻¹'" := (f^-1)%function : function_scope.
Notation "f '⁻¹'" := (f^-1)%equiv : equiv_scope.
Notation "¬ x" := (¬x) : type_scope.
Notation "x ≠ y" := (x y) : type_scope.

Notation "m ≤ n" := (m n)%trunc : trunc_scope.


Notation "'S¹'" := S1.
Notation "'S²'" := S2.

Notation "∥ A ∥₋₂" := (Trunc (-2) A).
Notation "❘ a ❘₋₂" := (@tr (-2) _ a) : trunc_scope.

Notation "∥ A ∥" := (Trunc (-1) A) (only parsing).
Notation "∥ A ∥₋₁" := (Trunc (-1) A).
Notation "❘ a ❘₋₁" := (@tr (-1) _ a) : trunc_scope.

Notation "x ∨ y" := (hor x y) : type_scope.
Notation "x ⊔ y" := (sum x y) : type_scope.

Notation "∥ A ∥₀" := (Trunc 0 A).
Notation "❘ a ❘₀" := (@tr 0 _ a) : trunc_scope.

Notation "∥ A ∥₁" := (Trunc 1 A).
Notation "❘ a ❘₁" := (@tr 1 _ a) : trunc_scope.

Notation "∥ A ∥₂" := (Trunc 2 A).
Notation "❘ a ❘₂" := (@tr 2 _ a) : trunc_scope.

Notation "∞" := purely.

Notation Σ := Susp.