notation & some delaborators & minor renamings

GroundZero/Algebra/EilenbergMacLane.lean

@@ -87,7 +87,7 @@ namespace K1
   noncomputable def KΩ (G : Group) : Group :=
   @Group.intro (Ω¹(K1 G)) (grpd _ _) KΩ.mul KΩ.inv KΩ.one
     (λ _ _ _, Id.inv (Id.assoc _ _ _))
-    Id.reflLeft Id.reflRight Id.invComp
+    Id.lid Id.rid Id.invComp
 
   noncomputable def homomorphism : Group.Hom G (KΩ G) :=
   Group.mkhomo loop loop.mul
@@ -163,7 +163,7 @@ namespace K1
       transitivity; apply ap (· ⬝ loop x); apply loop.mul;
       transitivity; symmetry; apply Id.assoc;
       transitivity; apply ap; apply ap (· ⬝ loop x); apply loop.inv;
-      transitivity; apply ap; apply Id.invComp; apply Id.reflRight };
+      transitivity; apply ap; apply Id.invComp; apply Id.rid };
     { apply zeroEqvSet.forward; apply piRespectsNType 0;
       intro; apply zeroEqvSet.left; apply grpd };
     { apply oneEqvGroupoid.forward;

GroundZero/Algebra/Group/Z.lean

@@ -9,7 +9,7 @@ namespace GroundZero.Algebra
 
 noncomputable def ZΩ : Group :=
 Group.intro (Circle.isGroupoid Circle.base Circle.base) Id.trans Id.inv Id.refl
-  (λ a b c, (Id.assoc a b c)⁻¹) Id.reflLeft Id.reflRight Id.invComp
+  (λ a b c, (Id.assoc a b c)⁻¹) Id.lid Id.rid Id.invComp
 
 noncomputable def ZΩ.abelian : ZΩ.isCommutative := Circle.comm
 

GroundZero/Algebra/Ring.lean

@@ -284,19 +284,19 @@ hott def field.mulRightInv (T : Prering) [field T] {x : T.carrier}
   (p : T.isproper x) : x * x⁻¹ = 1 :=
 ap Sigma.fst (Tˣ.mulRightInv ⟨x, p⟩)
 
-class lid (T : Prering) [ring T] (φ : T⁺.subgroup) :=
+class Lid (T : Prering) [ring T] (φ : T⁺.subgroup) :=
 (ideal : Π r i, i ∈ φ.set → T.ψ r i ∈ φ.set)
 
-class rid (T : Prering) [ring T] (φ : T⁺.subgroup) :=
+class Rid (T : Prering) [ring T] (φ : T⁺.subgroup) :=
 (ideal : Π i r, i ∈ φ.set → T.ψ i r ∈ φ.set)
 
 class ideal (T : Prering) [ring T] (φ : T⁺.subgroup) :=
 (left  : Π r i, i ∈ φ.set → T.ψ r i ∈ φ.set)
 (right : Π i r, i ∈ φ.set → T.ψ i r ∈ φ.set)
 
 instance ideal.auto (T : Prering) [ring T]
-  (φ : T⁺.subgroup) [lid T φ] [rid T φ] : ideal T φ :=
-⟨lid.ideal, rid.ideal⟩
+  (φ : T⁺.subgroup) [Lid T φ] [Rid T φ] : ideal T φ :=
+⟨Lid.ideal, Rid.ideal⟩
 
 namespace Ring
   variable (T : Prering) [ring T] (φ : T⁺.subgroup) [ideal T φ]

GroundZero/Exercises/Chap2.lean

@@ -233,4 +233,4 @@ begin induction p; reflexivity end
 
 hott def transportSquare {A : Type u} {B : A → Type v} {f g : Π x, B x} (H : f ~ g) {x y : A} (p : x = y) :
   ap (transport B p) (H x) ⬝ apd g p = apd f p ⬝ H y :=
-begin induction p; transitivity; apply Id.reflRight; apply Equiv.idmap end
+begin induction p; transitivity; apply Id.rid; apply Equiv.idmap end

GroundZero/Exercises/Chap4.lean

@@ -140,7 +140,7 @@ namespace «4.3»
       apply ap (·⁻¹⁻¹); symmetry; apply e.2.2.2;
       apply ap (_ ⬝ · ⬝ _); apply Equiv.mapOverComp };
     { intro p; induction p; transitivity; apply ap (· ⬝ _);
-      apply Id.reflRight; apply Id.invComp }
+      apply Id.rid; apply Id.invComp }
   end
 
   hott lemma embdOfQinv : qinv f → isEmbedding f :=
@@ -222,7 +222,7 @@ namespace «4.4»
     apply transport (@Sigma _ · ≃ _); apply Theorems.funext;
     intro e; symmetry; apply ap (fib idfun);
     transitivity; apply Equiv.transportOverContrMap;
-    transitivity; apply Id.reflRight; apply ap (ap g); apply Id.invInv;
+    transitivity; apply Id.rid; apply ap (ap g); apply Id.invInv;
     apply Equiv.trans; apply Sigma.respectsEquiv;
     { intro; apply Equiv.trans; apply Sigma.hmtpyInvEqv;
       apply Structures.contrEquivUnit.{_, 0}; apply singl.contr };

GroundZero/HITs/Interval.lean

@@ -31,7 +31,7 @@ namespace Interval
   rec (φ false) (φ true) (H _ _)
 
   hott def contrLeft : Π i, i₀ = i :=
-  Interval.ind (idp i₀) seg (begin apply pathoverFromTrans; apply Id.reflLeft end)
+  Interval.ind (idp i₀) seg (begin apply pathoverFromTrans; apply Id.lid end)
 
   hott def contrRight : Π i, i₁ = i :=
   Interval.ind seg⁻¹ (idp i₁) (begin apply pathoverFromTrans; apply Id.invComp end)
@@ -108,7 +108,7 @@ namespace Interval
             apply recβrule end
     ... = seg⁻¹ ⬝ seg :
       begin apply ap (· ⬝ seg);
-            apply Id.reflRight end
+            apply Id.rid end
     ... = idp i₁ : by apply Id.invComp)
 
   hott def negNeg' (x : I) : neg (neg x) = x :=
@@ -124,7 +124,7 @@ namespace Interval
     reflexivity; reflexivity; change _ = _;
     transitivity; apply Equiv.transportOverHmtpy;
     transitivity; apply ap (· ⬝ ap p seg);
-    transitivity; apply Id.reflRight;
+    transitivity; apply Id.rid;
     transitivity; apply Id.mapInv; apply ap;
     apply recβrule; apply Id.invComp
   end

GroundZero/HITs/Merely.lean

@@ -89,7 +89,7 @@ namespace Merely
     glue⁻¹ ⬝ ap incl (ap (Generalized.dep A n) p) ⬝ glue = ap incl p :=
   begin
     induction p; transitivity; { symmetry; apply Id.assoc };
-    apply Equiv.rewriteComp; symmetry; apply Id.reflRight
+    apply Equiv.rewriteComp; symmetry; apply Id.rid
   end
 
   hott def congOverPath {A : Type u} {n : ℕ} {a b : Generalized.rep A n}

GroundZero/HITs/Quotient.lean

@@ -10,19 +10,19 @@ open GroundZero
 namespace GroundZero.HITs
 universe u v w u' v'
 
-hott def Quot {A : Type u} (R : A → A → propset.{v}) := ∥Graph (λ x y, (R x y).1)∥₀
+hott def Quot {A : Type u} (R : A → A → Prop v) := ∥Graph (λ x y, (R x y).1)∥₀
 
-hott def Quot.elem {A : Type u} {R : A → A → propset.{v}} : A → Quot R :=
+hott def Quot.elem {A : Type u} {R : A → A → Prop v} : A → Quot R :=
 Trunc.elem ∘ Graph.elem
 
-hott def Quot.sound {A : Type u} {R : A → A → propset.{v}} {a b : A} :
+hott def Quot.sound {A : Type u} {R : A → A → Prop v} {a b : A} :
   (R a b).1 → @Id (Quot R) (Quot.elem a) (Quot.elem b) :=
 begin intro H; apply ap Trunc.elem; apply Graph.line; assumption end
 
-noncomputable hott def Quot.set {A : Type u} {R : A → A → propset.{v}} : hset (Quot R) :=
+noncomputable hott def Quot.set {A : Type u} {R : A → A → Prop v} : hset (Quot R) :=
 zeroEqvSet.forward (Trunc.uniq 0)
 
-hott def Quot.ind {A : Type u} {R : A → A → propset.{u'}} {π : Quot R → Type v}
+hott def Quot.ind {A : Type u} {R : A → A → Prop u'} {π : Quot R → Type v}
   (elemπ : Π x, π (Quot.elem x))
   (lineπ : Π x y H, elemπ x =[Quot.sound H] elemπ y)
   (set   : Π x, hset (π x)) : Π x, π x :=
@@ -37,11 +37,11 @@ end
 
 attribute [eliminator] Quot.ind
 
-hott def Quot.rec {A : Type u} {R : A → A → propset.{u'}} {B : Type v}
+hott def Quot.rec {A : Type u} {R : A → A → Prop u'} {B : Type v}
   (elemπ : A → B) (lineπ : Π x y, (R x y).fst → elemπ x = elemπ y) (set : hset B) : Quot R → B :=
 @Quot.ind A R (λ _, B) elemπ (λ x y H, Equiv.pathoverOfEq (Quot.sound H) (lineπ x y H)) (λ _, set)
 
-hott def Quot.lift₂ {A : Type u} {R₁ : A → A → propset.{u'}} {B : Type v} {R₂ : B → B → propset.{v'}}
+hott def Quot.lift₂ {A : Type u} {R₁ : A → A → Prop u'} {B : Type v} {R₂ : B → B → Prop v'}
   {γ : Type w} (R₁refl : Π x, (R₁ x x).fst) (R₂refl : Π x, (R₂ x x).fst) (f : A → B → γ)
   (h : hset γ) (p : Π a₁ a₂ b₁ b₂, (R₁ a₁ b₁).fst → (R₂ a₂ b₂).fst → f a₁ a₂ = f b₁ b₂) : Quot R₁ → Quot R₂ → γ :=
 begin

GroundZero/HITs/Reals.lean

@@ -82,7 +82,7 @@ namespace Reals
     induction n using Nat.casesOn; apply Id.invComp;
     { transitivity; symmetry; apply Id.assoc;
       transitivity; apply ap; apply Id.invComp;
-      apply Id.reflRight }
+      apply Id.rid }
   end)⟩
 
   hott def dist : Π (u v : R), u = v :=

GroundZero/Meta/Notation.lean

@@ -4,6 +4,12 @@ open Lean.PrettyPrinter.Delaborator
 
 namespace GroundZero.Meta.Notation
 
+open Lean in def delabCustomSort (t₀ : Delab) (t : Syntax.Level → Delab) : Delab :=
+whenPPOption Lean.getPPNotation do {
+  let ε ← SubExpr.getExpr; let n := ε.constLevels!.get! 0;
+  if n.isZero then t₀ else t (n.quote max_prec)
+}
+
 @[app_unexpander Nat.succ]
 def natSuccUnexpander : Lean.PrettyPrinter.Unexpander
 | `($_ $n) => `($n + 1)

GroundZero/Modal/Disc.lean

@@ -71,7 +71,7 @@ begin
     transitivity; apply Id.ap (· ⬝ _); apply Id.assoc;
     transitivity; symmetry; apply Id.assoc;
     transitivity; apply Id.ap; apply Id.invComp;
-    transitivity; apply Id.reflRight; apply bimap;
+    transitivity; apply Id.rid; apply bimap;
     { transitivity; apply Id.ap; apply Id.mapInv; apply Id.invInv };
     { apply Id.invInv } }
 end

GroundZero/Structures.lean

@@ -16,17 +16,31 @@ namespace Structures
 hott def isLoop {A : Type u} {a : A} (p : a = a) := ¬(p = idp a)
 
 hott def prop (A : Type u) := Π (a b : A), a = b
+hott def hset (A : Type u) := Π (a b : A) (p q : a = b), p = q
+
+hott def groupoid (A : Type u) :=
+Π (a b : A) (p q : a = b) (A B : p = q), A = B
 
 hott def propset := Σ (A : Type u), prop A
+hott def hsetset := Σ (A : Type u), hset A
 
 macro (priority := high) "Prop" : term => `(propset)
-macro (priority := high) "Prop" n:level : term => `(propset.{$n})
+macro (priority := high) "Prop" n:(ppSpace level:max) : term => `(propset.{$n})
 
-hott def hset (A : Type u) := Π (a b : A) (p q : a = b), p = q
-hott def Ens := Σ A, hset A
+macro "Set" : term => `(hsetset)
+macro "Set" n:(ppSpace level:max) : term => `(hsetset.{$n})
 
-hott def groupoid (A : Type u) :=
-Π (a b : A) (p q : a = b) (A B : p = q), A = B
+section
+  open Lean Lean.PrettyPrinter.Delaborator
+
+  @[delab app.GroundZero.Structures.propset]
+  def delabPropSet : Delab :=
+  Meta.Notation.delabCustomSort `(Prop) (λ n, `(Prop $n))
+
+  @[delab app.GroundZero.Structures.hsetset]
+  def delabHSetSet : Delab :=
+  Meta.Notation.delabCustomSort `(Set) (λ n, `(Set $n))
+end
 
 hott def dec (A : Type u) := A + ¬A
 
@@ -413,7 +427,7 @@ begin
   apply Types.Id.transCancelLeft (f a a (ρ a));
   transitivity; symmetry; apply Types.Equiv.transportComposition;
   transitivity; apply Types.Equiv.liftedHapply (R a); apply Types.Equiv.apd (f a) p;
-  transitivity; apply ap (f a a) (h _ _ _ (ρ a)); symmetry; apply Types.Id.reflRight
+  transitivity; apply ap (f a a) (h _ _ _ (ρ a)); symmetry; apply Types.Id.rid
 end
 
 hott def doubleNegEq {A : Type u} (h : Π (x y : A), ¬¬(x = y) → x = y) : hset A :=
@@ -448,8 +462,6 @@ end
 hott corollary boolIsSet : hset 𝟐 :=
 Hedberg boolDecEq
 
-
-
 section
   open GroundZero.Types.Not (univ)
   open GroundZero.Types.Coproduct
@@ -583,7 +595,7 @@ namespace Theorems
   begin
     induction p; symmetry; transitivity; apply Types.Equiv.transportOverHmtpy;
     transitivity; apply ap (· ⬝ ap (λ (h : A → B), h a) (funext q));
-    apply Id.reflRight; transitivity; symmetry; apply mapFunctoriality (λ (h : A → B), h a);
+    apply Id.rid; transitivity; symmetry; apply mapFunctoriality (λ (h : A → B), h a);
     transitivity; apply ap; apply Id.invComp; reflexivity
   end
 
@@ -700,7 +712,7 @@ hott def Finite := iter 𝟏 𝟎
 @[match_pattern] def Finite.succ {n : ℕ} : Finite n → Finite (n + 1) := Sum.inl
 
 open Structures (prop propset)
-hott def hrel (A : Type u) := A → A → propset.{v}
+hott def hrel (A : Type u) := A → A → Prop v
 
 def LEMinf := Π (A : Type u), A + ¬A
 macro "LEM∞" : term => `(LEMinf)
@@ -758,7 +770,7 @@ begin
     apply Theorems.funext; intro;
     apply (R _ _).2 };
   { intros f g;
-     apply Theorems.funext; intro;
+    apply Theorems.funext; intro;
     apply Theorems.funext; intro;
     apply Theorems.funext; intro;
     apply Theorems.funext; intro;
@@ -883,14 +895,14 @@ namespace Types.Id
     α^p = conjugateΩ (apd idp p) (apΩ (transport (λ x, x = x) p) α) :=
   begin induction p; symmetry; apply idmapΩ end
 
-  hott def higherTransportIdfun {A : Type u} {a : A} (ε : idp a = idp a) :
+  hott lemma transportAbelian {A : Type u} {a : A} (ε : idp a = idp a) :
     transport (λ x, x = x) ε ~ λ x, x :=
   λ _, transportInvCompComp _ _ ⬝ cancelHigherConjLeft _ _
 
-  hott def abelianΩ {A : Type u} {a : A} (p : idp a = idp a) :
+  hott theorem abelianΩ {A : Type u} {a : A} (p : idp a = idp a) :
     Π (n : ℕ) (α : Ω[n + 1](a = a, idp a)), α^p = α
-  | Nat.zero,   _ => higherTransportIdfun _ _
-  | Nat.succ n, _ => conjugateSuccΩ _ _ _ ⬝ ap (conjugateΩ (apd idp p)) (apWithHomotopyΩ (higherTransportIdfun _) _ _) ⬝
+  | Nat.zero,   _ => transportAbelian _ _
+  | Nat.succ n, _ => conjugateSuccΩ _ _ _ ⬝ ap (conjugateΩ (apd idp p)) (apWithHomotopyΩ (transportAbelian _) _ _) ⬝
                      (conjugateTransΩ _ _ (n + 1) _)⁻¹ ⬝ abelianΩ _ _ _ ⬝ idmapΩ _ _
 
   hott def comApΩ {A : Type u} {B : Type v} {C : Type w} (f : B → C) (g : A → B) {a : A} :

GroundZero/Theorems/Classical.lean

@@ -16,7 +16,7 @@ axiom choice {A : Type u} (B : A → Type v) (η : Π x, B x → Type w) :
   ∥(Σ (φ : Π x, B x), Π x, η x (φ x))∥
 
 noncomputable hott def choiceOfRel {A : Type u} {B : Type v}
-  (R : A → B → propset.{w}) (H : hset A) (G : hset B) :
+  (R : A → B → Prop w) (H : hset A) (G : hset B) :
   (Π x, ∥(Σ y, (R x y).fst)∥) → ∥(Σ (φ : A → B), Π x, (R x (φ x)).fst)∥ :=
 begin
   apply @choice A (λ _, B) (λ x y, (R x y).1);

GroundZero/Theorems/Equiv.lean

@@ -309,7 +309,7 @@ begin
     { transitivity; apply transportOverPi; apply Theorems.funext; intro;
       transitivity; apply transportOverPi; apply Theorems.funext; intro;
       transitivity; apply transportOverContrMap;
-      transitivity; apply Id.reflRight;
+      transitivity; apply Id.rid;
       transitivity; apply Id.mapInv;
       transitivity; apply ap Id.inv;
       transitivity; apply mapToHapply₄;

GroundZero/Theorems/Hopf.lean

@@ -65,7 +65,7 @@ namespace Real
   begin
     fapply Suspension.ind; reflexivity; apply Suspension.merid true;
     intro (b : 𝟐); apply Id.trans; apply Equiv.transportOverHmtpy;
-    transitivity; apply ap (· ⬝ _); transitivity; apply Id.reflRight;
+    transitivity; apply ap (· ⬝ _); transitivity; apply Id.rid;
     transitivity; apply Id.mapInv; apply ap; transitivity; apply Equiv.mapOverComp;
     apply ap (ap map); apply Suspension.recβrule; induction b;
     { transitivity; apply ap (· ⬝ _); transitivity; apply ap; apply Sigma.mapFstOverProd;

GroundZero/Types/Ens.lean

@@ -87,7 +87,7 @@ begin
   { intro; apply propIsSet; apply s.2 }
 end
 
-hott def predicate (A : Type u) := A → propset.{v}
+hott def predicate (A : Type u) := A → Prop v
 
 hott def Ens.eqvPredicate {A : Type u} : Ens A ≃ predicate A :=
 begin
@@ -112,4 +112,4 @@ hott def Ens.singletonInh {A : Type u} (H : Structures.hset A) (x : A) : Ens.inh
 HITs.Merely.elem ⟨x, Id.refl⟩
 
 end Types
-end GroundZero
+end GroundZero