Use arrowIsSet to simplify equality constructor for functors

src/Cat/Categories/Fun.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --allow-unsolved-metas --cubical #-}
 module Cat.Categories.Fun where
 
 open import Agda.Primitive
@@ -9,6 +9,9 @@ open import Data.Product
 open import Cat.Category
 open import Cat.Category.Functor
 
+open import Cat.Equality
+open Equality.Data.Product
+
 module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where
   open Category hiding ( _∘_ ; Arrow )
   open Functor
@@ -86,12 +89,20 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
     NatComp = _:⊕:_
 
   private
+    module _ {F G : Functor ℂ 𝔻} where
+      naturalTransformationIsSets : IsSet (NaturalTransformation F G)
+      naturalTransformationIsSets {θ , θNat} {η , ηNat} p q i j
+        = (λ C →  𝔻.arrowIsSet (λ l → proj₁ (p l) C) (λ l → proj₁ (q l) C) i j)
+        , λ f k → 𝔻.arrowIsSet (λ l → proj₂ (p l) f {!!}) (λ l → proj₂ (p l) f {!!}) {!!} {!!}
+        where
+          module 𝔻 = IsCategory (isCategory 𝔻)
+
     module _ {A B C D : Functor ℂ 𝔻} {f : NaturalTransformation A B}
       {g : NaturalTransformation B C} {h : NaturalTransformation C D} where
       _g⊕f_ = _:⊕:_ {A} {B} {C}
       _h⊕g_ = _:⊕:_ {B} {C} {D}
       :assoc: : (_:⊕:_ {A} {C} {D} h (_:⊕:_ {A} {B} {C} g f)) ≡ (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} h g) f)
-      :assoc: = {!!}
+      :assoc: = Σ≡ (funExt λ x → {!Fun.arrowIsSet!}) {!!}
     module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
       ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
       ident-r = {!!}
@@ -116,7 +127,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
     :isCategory: = record
       { assoc = λ {A B C D} → :assoc: {A} {B} {C} {D}
       ; ident = λ {A B} → :ident: {A} {B}
-      ; arrowIsSet = {!!}
+      ; arrowIsSet = λ {F} {G} → naturalTransformationIsSets {F} {G}
       ; univalent = {!!}
       }
 

src/Cat/Category.agda

@@ -26,6 +26,10 @@ syntax ∃!-syntax (λ x → B) = ∃![ x ] B
 IsSet   : {ℓ : Level} (A : Set ℓ) → Set ℓ
 IsSet A = {x y : A} → (p q : x ≡ y) → p ≡ q
 
+-- This follows from [HoTT-book: §7.1.10]
+-- Andrea says the proof is in `cubical` but I can't find it.
+postulate isSetIsProp : {ℓ : Level} → {A : Set ℓ} → isProp (IsSet A)
+
 record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
   -- adding no-eta-equality can speed up type-checking.
   -- ONLY IF you define your categories with copatterns though.
@@ -53,6 +57,7 @@ record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
 -- (univalent).
 record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
   open RawCategory ℂ
+  module Raw = RawCategory ℂ
   field
     assoc : {A B C D : Object} { f : Arrow A B } { g : Arrow B C } { h : Arrow C D }
       → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
@@ -91,22 +96,40 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
   -- This lemma will be useful to prove the equality of two categories.
   IsCategory-is-prop : isProp (IsCategory ℂ)
   IsCategory-is-prop x y i = record
+    -- Why choose `x`'s `arrowIsSet`?
     { assoc = x.arrowIsSet x.assoc y.assoc i
     ; ident =
       ( x.arrowIsSet (fst x.ident) (fst y.ident) i
       , x.arrowIsSet (snd x.ident) (snd y.ident) i
       )
-    ; arrowIsSet = λ p q →
-      let
-        golden : x.arrowIsSet p q ≡ y.arrowIsSet p q
-        golden = {!!}
-      in
-        golden i
-      ; univalent = λ y₁ → {!!}
+    ; arrowIsSet = isSetIsProp x.arrowIsSet y.arrowIsSet i
+    ; univalent = {!!}
     }
     where
       module x = IsCategory x
       module y = IsCategory y
+      xuni : x.Univalent
+      xuni = x.univalent
+      yuni : y.Univalent
+      yuni = y.univalent
+      open RawCategory ℂ
+      T :  I → Set (ℓa ⊔ ℓb)
+      T i = {A B : Object} →
+        isEquiv (A ≡ B) (A x.≅ B)
+          (λ A≡B →
+            transp
+            (λ j →
+            Σ-syntax (Arrow A (A≡B j))
+            (λ f → Σ-syntax (Arrow (A≡B j) A) (λ g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙)))
+            ( 𝟙
+            , 𝟙
+            , x.arrowIsSet (fst x.ident) (fst y.ident) i
+            , x.arrowIsSet (snd x.ident) (snd y.ident) i
+            )
+          )
+      eqUni : T [ xuni ≡ yuni ]
+      eqUni = {!!}
+
 
 record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   field

src/Cat/Category/Functor.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --cubical #-}
 module Cat.Category.Functor where
 
 open import Agda.Primitive
@@ -78,14 +79,11 @@ module _
   IsProp' : {ℓ : Level} (A : I → Set ℓ) → Set ℓ
   IsProp' A = (a0 : A i0) (a1 : A i1) → A [ a0 ≡ a1 ]
 
-  postulate IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i)
-  -- IsFunctorIsProp' isF0 isF1 i = record
-  --   { ident = {!𝔻.arrowIsSet {!isF0.ident!} {!isF1.ident!} i!}
-  --   ; distrib = {!𝔻.arrowIsSet {!isF0.distrib!} {!isF1.distrib!} i!}
-  --   }
-  --   where
-  --     module isF0 = IsFunctor isF0
-  --     module isF1 = IsFunctor isF1
+  IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i)
+  IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻}
+    (\ F → IsFunctorIsProp {F = F}) (\ i → F i)
+    where
+      open import Cubical.GradLemma using (lemPropF)
 
 module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
   Functor≡ : {F G : Functor ℂ 𝔻}
@@ -95,14 +93,13 @@ module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
     → F ≡ G
   Functor≡ {F} {G} eq* eq→ i = record
     { raw = eqR i
-    ; isFunctor = f i
+    ; isFunctor = eqIsF i
     }
     where
       eqR : raw F ≡ raw G
       eqR i = record { func* = eq* i ; func→ = eq→ i }
-      postulate T : isSet (IsFunctor _ _ (raw F))
-      f : (λ i →  IsFunctor ℂ 𝔻 (eqR i)) [ isFunctor F ≡ isFunctor G ]
-      f = IsFunctorIsProp' (isFunctor F) (isFunctor G)
+      eqIsF : (λ i →  IsFunctor ℂ 𝔻 (eqR i)) [ isFunctor F ≡ isFunctor G ]
+      eqIsF = IsFunctorIsProp' (isFunctor F) (isFunctor G)
 
 module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where
   private