Show that objects are groupoids

src/Cat/Category.agda

@@ -496,6 +496,20 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
         res : Xi ≡ Yi
         res = lemSig propIsInitial _ _ (isoToId iso)
 
+    groupoidObject : isGrpd Object
+    groupoidObject A B = res
+      where
+      open import Data.Nat using (_≤_ ; z≤n ; s≤s)
+      setIso : ∀ x → isSet (Isomorphism x)
+      setIso x = ntypeCommulative ((s≤s {n = 1} z≤n)) (propIsomorphism x)
+      step : isSet (A ≅ B)
+      step = setSig {sA = arrowsAreSets} {sB = setIso}
+      res : isSet (A ≡ B)
+      res = equivPreservesNType
+        {A = A ≅ B} {B = A ≡ B} {n = ⟨0⟩}
+        (Equivalence.symmetry (univalent≃ {A = A} {B}))
+        step
+
 module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
   open RawCategory ℂ
   open Univalence

src/Cat/Category/Product.agda

@@ -216,8 +216,14 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
           )
       step1
         = symIso
-            (isoSigFst {A = (X ℂ.≅ Y)} {B = (X ≡ Y)} {!!} {Q = \ p → (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb)} ℂ.isoToId
-                           (symIso (_ , ℂ.asTypeIso {X} {Y}) .snd))
+            (isoSigFst
+              {A = (X ℂ.≅ Y)}
+              {B = (X ≡ Y)}
+              (ℂ.groupoidObject _ _)
+              {Q = \ p → (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb)}
+              ℂ.isoToId
+              (symIso (_ , ℂ.asTypeIso {X} {Y}) .snd)
+            )
 
       step2
         : Σ (X ℂ.≅ Y) (λ iso

src/Cat/Prelude.agda

@@ -21,7 +21,7 @@ open import Cubical.GradLemma
   using (gradLemma)
   public
 open import Cubical.NType
-  using (⟨-2⟩ ; ⟨-1⟩ ; ⟨0⟩ ; TLevel ; HasLevel)
+  using (⟨-2⟩ ; ⟨-1⟩ ; ⟨0⟩ ; TLevel ; HasLevel ; isGrpd)
   public
 open import Cubical.NType.Properties
   using
@@ -96,3 +96,5 @@ module _ {ℓ : Level} {A : Set ℓ} {a : A} where
     pathJ (λ y x → A) _ A refl ≡⟨ pathJprop {x = a} (λ y x → A) _ ⟩
     _ ≡⟨ pathJprop {x = a} (λ y x → A) _ ⟩
     a ∎
+
+open import Cat.Wishlist public

src/Cat/Wishlist.agda

@@ -9,8 +9,9 @@ open import Agda.Builtin.Sigma
 
 open import Cubical.NType.Properties
 
-step : ∀ {ℓ} {A : Set ℓ} → isContr A → (x y : A) → isContr (x ≡ y)
-step (a , contr) x y = {!p , c!}
+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
@@ -20,15 +21,15 @@ step (a , contr) x y = {!p , c!}
     -- 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
+  -- 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?
+  contrInitial (S (S n)) contr x y = {!lvl!} -- Why is this not well-founded?
     where
     c : isContr (x ≡ y)
     c = step contr x y