Trying to prove cummulativity of homotopy levels

src/Cat/Category/Monad/Voevodsky.agda

@@ -175,12 +175,12 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         where
         lem : Monoidal→Kleisli ∘ Kleisli→Monoidal ≡ Function.id
         lem = {!!} -- verso-recto Monoidal≃Kleisli
-        t : {ℓ : Level} {A B : Set ℓ} {a : _ → A} {b : B → _}
+        t : (§2-fromMonad ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad)
-          → a ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ b ≡ a ∘ b
+          ≡ (§2-fromMonad ∘ §2-3.§2.toMonad)
-        t {a = a} {b} = cong (λ φ → a ∘ φ ∘ b) lem
+        t = cong (λ φ → §2-fromMonad ∘ (λ{ {ω} → φ {{!????!}}}) ∘ §2-3.§2.toMonad) {!lem!}
-        u : {ℓ : Level} {A B : Set ℓ} {a : _ → A} {b : B → _}
+        u : (§2-fromMonad ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad) m
-          → {m : _} → (a ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ b) m ≡ (a ∘ b) m
+          ≡ (§2-fromMonad ∘ §2-3.§2.toMonad) m
-        u {m = m} = cong (λ φ → φ m) t
+        u = cong (λ φ → φ m) t
 
       backEq : ∀ m → (back ∘ forth) m ≡ m
       backEq m = begin

src/Cat/Wishlist.agda

@@ -1,9 +1,41 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module Cat.Wishlist where
 
-open import Level
+open import Level hiding (suc)
+open import Cubical
 open import Cubical.NType
-open import Data.Nat using (_≤_ ; z≤n ; s≤s)
+open import Data.Nat using (_≤_ ; z≤n ; s≤s ; zero ; suc)
+open import Agda.Builtin.Sigma
 
 open import Cubical.NType.Properties
 
-postulate ntypeCommulative : ∀ {ℓ n m} {A : Set ℓ} → n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A
+step : ∀ {ℓ} {A : Set ℓ} → isContr A → (x y : A) → isContr (x ≡ y)
+step (a , contr) x y = {!p , c!}
+  -- where
+  -- p : x ≡ y
+  -- p = begin
+  --   x ≡⟨ sym (contr x) ⟩
+  --   a ≡⟨ contr y ⟩
+  --   y ∎
+  -- c : (q : x ≡ y) → p ≡ q
+  -- c q i j = contr (p {!!}) {!!}
+
+-- Contractible types have any given homotopy level.
+contrInitial : {ℓ : Level} {A : Set ℓ} → ∀ n → isContr A → HasLevel n A
+contrInitial ⟨-2⟩ contr = contr
+-- lem' (S ⟨-2⟩) (a , contr) = {!step!}
+contrInitial (S ⟨-2⟩) (a , contr) x y = begin
+  x ≡⟨ sym (contr x) ⟩
+  a ≡⟨ contr y ⟩
+  y ∎
+contrInitial (S (S n)) contr x y = {!lvl!} -- Why is this not well-founded?
+  where
+  c : isContr (x ≡ y)
+  c = step contr x y
+  lvl : HasLevel (S n) (x ≡ y)
+  lvl = contrInitial {A = x ≡ y} (S n) c
+
+module _ {ℓ : Level} {A : Set ℓ} where
+  ntypeCommulative : ∀ {n m} → n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A
+  ntypeCommulative {n = zero} {m} z≤n lvl = {!contrInitial ⟨ m ⟩₋₂ lvl!}
+  ntypeCommulative {n = .(suc _)} {.(suc _)} (s≤s x) lvl = {!!}