From 92fb53098abc56db1bf056daf3a815ae1ae08adc Mon Sep 17 00:00:00 2001
From: Andrea Vezzosi <sanzhiyan@gmail.com>
Date: Sun, 15 Apr 2018 13:49:46 +0200
Subject: [PATCH] Implemented ntypeCumulative

---
 src/Cat/Category.agda                       |  4 +--
 src/Cat/Category/NaturalTransformation.agda |  6 ++--
 src/Cat/Wishlist.agda                       | 36 +++------------------
 3 files changed, 10 insertions(+), 36 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 3cc5068..a821a37 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -497,9 +497,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)
diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda
index 01eff6d..d8b20a8 100644
--- a/src/Cat/Category/NaturalTransformation.agda
+++ 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)
diff --git a/src/Cat/Wishlist.agda b/src/Cat/Wishlist.agda
index a0c8a26..37b8c87 100644
--- a/src/Cat/Wishlist.agda
+++ b/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)