From 7b45b5cdc36afdc1871a3d830c3dd156fc360e61 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 13 Apr 2018 15:22:13 +0200
Subject: [PATCH] Show that objects are groupoids

---
 src/Cat/Category.agda         | 14 ++++++++++
 src/Cat/Category/Product.agda | 10 +++++--
 src/Cat/Prelude.agda          |  4 ++-
 src/Cat/Wishlist.agda         | 49 ++++++++++++++++++-----------------
 4 files changed, 50 insertions(+), 27 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 9e51447..aa77c28 100644
--- a/src/Cat/Category.agda
+++ b/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
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index e738a16..5286976 100644
--- a/src/Cat/Category/Product.agda
+++ b/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
diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda
index 409549c..55f031c 100644
--- a/src/Cat/Prelude.agda
+++ b/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
diff --git a/src/Cat/Wishlist.agda b/src/Cat/Wishlist.agda
index 8385afd..a0c8a26 100644
--- a/src/Cat/Wishlist.agda
+++ b/src/Cat/Wishlist.agda
@@ -9,31 +9,32 @@ 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!}
-  -- 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 {!!}) {!!}
+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
+  -- 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