Merge remote-tracking branch 'Saizan/dev' into dev

src/Cat/Category.agda

@@ -348,7 +348,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
           coe refl f ≡⟨ id-coe ⟩
           f ≡⟨ sym rightIdentity ⟩
           f <<< identity ≡⟨ cong (f <<<_) (sym subst-neutral) ⟩
-          f <<< _ ≡⟨ {!!} ⟩ _ ∎) a' p
+          f <<< _ ≡⟨⟩ _ ∎) a' p
 
       module _ {b' : Object} (p : b ≡ b') where
         private
@@ -525,9 +525,9 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
     groupoidObject : isGrpd Object
     groupoidObject A B = res
       where
-      open import Data.Nat using (_≤_ ; z≤n ; s≤s)
+      open import Data.Nat using (_≤_ ; ≤′-refl ; ≤′-step)
       setIso : ∀ x → isSet (Isomorphism x)
-      setIso x = ntypeCommulative ((s≤s {n = 1} z≤n)) (propIsomorphism x)
+      setIso x = ntypeCumulative {n = 1} (≤′-step ≤′-refl) (propIsomorphism x)
       step : isSet (A ≊ B)
       step = setSig {sA = arrowsAreSets} {sB = setIso}
       res : isSet (A ≡ B)

src/Cat/Category/NaturalTransformation.agda

@@ -20,7 +20,7 @@
 {-# OPTIONS --allow-unsolved-metas --cubical #-}
 open import Cat.Prelude
 
-open import Data.Nat using (_≤_ ; z≤n ; s≤s)
+open import Data.Nat using (_≤′_ ; ≤′-refl ; ≤′-step)
 module Nat = Data.Nat
 
 open import Cat.Category
@@ -112,8 +112,8 @@ module Properties where
 
     naturalIsSet : (θ : Transformation F G) → isSet (Natural F G θ)
     naturalIsSet θ =
-      ntypeCommulative
-      (s≤s {n = Nat.suc Nat.zero} z≤n)
+      ntypeCumulative {n = 1}
+      (Data.Nat.≤′-step Data.Nat.≤′-refl)
       (naturalIsProp θ)
 
     naturalTransformationIsSet : isSet (NaturalTransformation F G)

src/Cat/Wishlist.agda

@@ -1,42 +1,16 @@
 {-# OPTIONS --allow-unsolved-metas #-}
 module Cat.Wishlist where
 
-open import Level hiding (suc)
+open import Level hiding (suc; zero)
 open import Cubical
 open import Cubical.NType
-open import Data.Nat using (_≤_ ; z≤n ; s≤s ; zero ; suc)
+open import Data.Nat using (_≤′_ ;  ≤′-refl ;  ≤′-step ; zero ; suc)
 open import Agda.Builtin.Sigma
 
 open import Cubical.NType.Properties
 
-private
-  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 = {!!}
+  ntypeCumulative : ∀ {n m} → n ≤′ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A
+  ntypeCumulative {m}         ≤′-refl      lvl = lvl
+  ntypeCumulative {n} {suc m} (≤′-step le) lvl = HasLevel+1 ⟨ m ⟩₋₂ (ntypeCumulative le lvl)