From 2f0b50a94c33d3e6466622a137e38df23541668a Mon Sep 17 00:00:00 2001
From: Siegmentation Fault <siegmentationfault@yandex.ru>
Date: Fri, 15 Dec 2023 19:10:38 +0700
Subject: [PATCH] lemmas & minor changes

---
 GroundZero/Meta/HottTheory.lean |  7 +++++--
 GroundZero/Structures.lean      | 20 +++++++++++++++-----
 GroundZero/Types/Equiv.lean     |  6 +++++-
 3 files changed, 25 insertions(+), 8 deletions(-)

diff --git a/GroundZero/Meta/HottTheory.lean b/GroundZero/Meta/HottTheory.lean
index 3bbf2c5..fa4760e 100644
--- a/GroundZero/Meta/HottTheory.lean
+++ b/GroundZero/Meta/HottTheory.lean
@@ -34,8 +34,11 @@ section
   @[inline] def guardb {f : Type → Type u} [Alternative f] (b : Bool) : f Unit :=
   if b then pure () else failure
 
-  run_cmd { let ns := [``Eq, ``HEq, ``False]; liftTermElabM <|
-            ns.forM (λ n => hasLargeElim n >>= guardb) }
+  run_cmd { let xs := [``Eq, ``HEq, ``False, ``True, ``And, ``Iff, ``Acc, ``Subsingleton];
+            liftTermElabM <| xs.forM (λ n => hasLargeElim n >>= guardb) }
+
+  run_cmd { let ys := [``Or, ``Exists, ``Subtype, ``Quot];
+            liftTermElabM <| ys.forM (λ n => hasLargeElim n >>= guardb ∘ not) }
 end
 
 def renderChain : List Name → String :=
diff --git a/GroundZero/Structures.lean b/GroundZero/Structures.lean
index 7c7abcd..f167da7 100644
--- a/GroundZero/Structures.lean
+++ b/GroundZero/Structures.lean
@@ -49,7 +49,9 @@ hott def decEq (A : Type u) := Π (a b : A), dec (a = b)
 
 notation "dec⁼" => decEq
 
-hott def contr (A : Type u) := Σ (a : A), Π b, a = b
+hott definition contr (A : Type u) := Σ (a : A), Π b, a = b
+
+hott remark inhContr {A : Type u} : contr A → A := Sigma.fst
 
 inductive hlevel
 | minusTwo : hlevel
@@ -100,6 +102,7 @@ namespace hlevel
   succ (succ (predPred n))
 
   instance (n : ℕ) : OfNat ℕ₋₂ n := ⟨ofNat n⟩
+  instance : Coe ℕ ℕ₋₂ := ⟨ofNat⟩
 end hlevel
 
 hott definition isNType : hlevel → Type u → Type u
@@ -937,10 +940,6 @@ namespace Types.Id
   | Nat.zero,   _ => idp _
   | Nat.succ _, _ => apWithHomotopyΩ (mapOverComp _ _) _ _ ⬝ comApΩ (ap f) (ap g) _ _
 
-  hott lemma apdDiag {A : Type u} {B : A → Type v} {C : A → Type w} (f : Π x, B x) (φ : Π x, B x → C x)
-    {a b : A} (p : a = b) : apd (λ x, φ x (f x)) p = biapd φ p (apd f p) :=
-  begin induction p; reflexivity end
-
   hott lemma apdDiagΩ {A : Type u} {B : A → Type v} {C : A → Type w} (f : Π x, B x) (φ : Π x, B x → C x) {x : A} :
     Π (n : ℕ) (α : Ωⁿ(A, x)), apdΩ (λ x, φ x (f x)) α = biapdΩ φ n α (apdΩ f α)
   | Nat.zero,   _ => idp _
@@ -1088,6 +1087,17 @@ namespace Types.Id
                           apWithHomotopyΩ Product.apSnd _ _ ⬝
                           apSndΩ _ _
   end
+
+  open GroundZero.Structures
+
+  hott lemma levelStableΩ {A : Type u} {a : A} (k : ℕ₋₂) : Π {n : ℕ}, is-k-type A → is-k-type Ωⁿ(A, a)
+  | Nat.zero,   H => H
+  | Nat.succ n, H => @levelStableΩ (a = a) (idp a) k n (hlevel.cumulative k H a a)
+
+  hott lemma levelOverΩ {A : Type u} {B : A → Type v} {a : A} {b : B a} (k : ℕ₋₂) :
+    Π {n : ℕ}, (Π x, is-k-type (B x)) → Π (α : Ωⁿ(A, a)), is-k-type Ωⁿ(B, b, α)
+  | Nat.zero,   H, x => H x
+  | Nat.succ n, H, α => @levelOverΩ (a = a) (λ p, b =[B, p] b) (idp a) (idp b) k n (λ p, hlevel.cumulative k (H a) _ _) α
 end Types.Id
 
 end GroundZero
diff --git a/GroundZero/Types/Equiv.lean b/GroundZero/Types/Equiv.lean
index d6f930f..12a3c2e 100644
--- a/GroundZero/Types/Equiv.lean
+++ b/GroundZero/Types/Equiv.lean
@@ -296,7 +296,7 @@ namespace Equiv
 
   hott definition depTrans {A : Type u} {B : A → Type v}
     {a b c : A} {p : a = b} {q : b = c} {u : B a} {v : B b} {w : B c}
-    (r : u =[p] v) (s : v =[q] w): u =[p ⬝ q] w :=
+    (r : u =[p] v) (s : v =[q] w) : u =[p ⬝ q] w :=
   transportcom p q u ⬝ ap (transport B q) r ⬝ s
 
   infix:60 " ⬝′ " => depTrans
@@ -685,6 +685,10 @@ namespace Equiv
     (p : a = b) (q : u =[B₁, p] v) : biapd (λ x, ψ x ∘ φ x) p q = biapd ψ p (biapd φ p q) :=
   begin induction p; apply mapOverComp end
 
+  hott lemma apdDiag {A : Type u} {B : A → Type v} {C : A → Type w} (f : Π x, B x) (φ : Π x, B x → C x)
+    {a b : A} (p : a = b) : apd (λ x, φ x (f x)) p = biapd φ p (apd f p) :=
+  begin induction p; reflexivity end
+
   hott definition bimapΩ {A : Type u} {B : Type v} {C : Type w} (f : A → B → C) {a : A} {b : B} :
     Π {n : ℕ}, Ωⁿ(A, a) → Ωⁿ(B, b) → Ωⁿ(C, f a b)
   | Nat.zero   => f