Try to show that natural transformations are sets

src/Cat/Categories/Free.agda

@@ -44,7 +44,7 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
       --   ident-r : concatenate {A} {A} {B} p (lift 𝟙) ≡ p
       --   ident-l : concatenate {A} {B} {B} (lift 𝟙) p ≡ p
     module _ {A B : Object ℂ} where
-      isSet : IsSet (Path A B)
+      isSet : Cubical.isSet (Path A B)
       isSet = {!!}
   RawFree : RawCategory ℓ (ℓ ⊔ ℓ')
   RawFree = record

src/Cat/Categories/Fun.agda

@@ -5,6 +5,7 @@ open import Agda.Primitive
 open import Cubical
 open import Function
 open import Data.Product
+import Cubical.GradLemma
 
 open import Cat.Category
 open import Cat.Category.Functor
@@ -30,6 +31,9 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
       → (f : ℂ [ A , B ])
       → 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ]
 
+    -- naturalIsProp : ∀ θ → isProp (Natural θ)
+    -- naturalIsProp θ x y = {!funExt!}
+
     NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
     NaturalTransformation = Σ Transformation Natural
 
@@ -90,19 +94,67 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
 
   private
     module _ {F G : Functor ℂ 𝔻} where
-      naturalTransformationIsSets : IsSet (NaturalTransformation F G)
+      module 𝔻 = IsCategory (isCategory 𝔻)
-      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}
+      transformationIsSet : isSet (Transformation F G)
-      {g : NaturalTransformation B C} {h : NaturalTransformation C D} where
+      transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l → p l C)   (λ l → q l C) i j
+      IsSet'   : {ℓ : Level} (A : Set ℓ) → Set ℓ
+      IsSet' A = {x y : A} → (p q : (λ _ → A) [ x ≡ y ]) → p ≡ q
+
+      -- Example 3.1.6. in HoTT states that
+      -- If `B a` is a set for all `a : A` then `(a : A) → B a` is a set.
+      -- In the case below `B = Natural F G`.
+
+      -- naturalIsSet : (θ : Transformation F G) → IsSet' (Natural F G θ)
+      -- naturalIsSet = {!!}
+
+      -- isS : IsSet' ((θ : Transformation F G) → Natural F G θ)
+      -- isS = {!!}
+
+      naturalIsProp : (θ : Transformation F G) → isProp (Natural F G θ)
+      naturalIsProp θ θNat θNat' = lem
+        where
+          lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ]
+          lem = λ i f → 𝔻.arrowIsSet _ _ (θNat f) (θNat' f) i
+
+      naturalTransformationIsSets : isSet (NaturalTransformation F G)
+      naturalTransformationIsSets (θ , θNat) (η , ηNat) p q i j
+        = θ-η
+        -- `i or `j - `p'` or `q'`?
+        , refl {x = t} i
+        -- naturalIsSet i (λ i → {!!} i) {!!} {!!} i j
+        -- naturalIsSet {!p''!} {!p''!} {!!} i j
+        -- λ f k → 𝔻.arrowIsSet (λ l → proj₂ (p l) f k) (λ l → proj₂ (p l) f k) {!!} {!!}
+        where
+          θ≡η θ≡η' : θ ≡ η
+          θ≡η  i = proj₁ (p i)
+          θ≡η' i = proj₁ (q i)
+          θ-η : Transformation F G
+          θ-η = transformationIsSet _ _ θ≡η θ≡η' i j
+          θNat≡ηNat  : (λ i → Natural F G (θ≡η  i)) [ θNat ≡ ηNat ]
+          θNat≡ηNat  i = proj₂ (p i)
+          θNat≡ηNat' : (λ i → Natural F G (θ≡η' i)) [ θNat ≡ ηNat ]
+          θNat≡ηNat' i = proj₂ (q i)
+          k  : Natural F G (θ≡η  i)
+          k  = θNat≡ηNat  i
+          k' : Natural F G (θ≡η' i)
+          k' = θNat≡ηNat' i
+          t : Natural F G θ-η
+          t = naturalIsProp {!θ!} {!!} {!!} {!!}
+
+    module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B}
+      {η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where
+      private
+        θ = proj₁ θ'
+        η = proj₁ η'
+        ζ = proj₁ ζ'
       _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: : (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ')) ≡ (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ')
-      :assoc: = Σ≡ (funExt λ x → {!Fun.arrowIsSet!}) {!!}
+      :assoc: = Σ≡ (funExt (λ _ → assoc)) {!!}
+        where
+          open IsCategory (isCategory 𝔻)
+
     module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
       ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
       ident-r = {!!}

src/Cat/Category.agda

@@ -11,7 +11,7 @@ open import Data.Product renaming
   )
 open import Data.Empty
 import Function
-open import Cubical hiding (isSet)
+open import Cubical
 open import Cubical.GradLemma using ( propIsEquiv )
 
 ∃! : ∀ {a b} {A : Set a}
@@ -23,12 +23,9 @@ open import Cubical.GradLemma using ( propIsEquiv )
 
 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)
+postulate isSetIsProp : {ℓ : Level} → {A : Set ℓ} → isProp (isSet A)
 
 record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
   -- adding no-eta-equality can speed up type-checking.
@@ -63,7 +60,7 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
       → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
     ident : {A B : Object} {f : Arrow A B}
       → f ∘ 𝟙 ≡ f × 𝟙 ∘ f ≡ f
-    arrowIsSet : ∀ {A B : Object} → IsSet (Arrow A B)
+    arrowIsSet : ∀ {A B : Object} → isSet (Arrow A B)
 
   Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb
   Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙
@@ -97,10 +94,10 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
   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
+    { assoc = x.arrowIsSet _ _ x.assoc y.assoc i
     ; ident =
-      ( x.arrowIsSet (fst x.ident) (fst y.ident) i
+      ( x.arrowIsSet _ _ (fst x.ident) (fst y.ident) i
-      , x.arrowIsSet (snd x.ident) (snd y.ident) i
+      , x.arrowIsSet _ _ (snd x.ident) (snd y.ident) i
       )
     ; arrowIsSet = isSetIsProp x.arrowIsSet y.arrowIsSet i
     ; univalent = {!!}
@@ -123,8 +120,8 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
             (λ f → Σ-syntax (Arrow (A≡B j) A) (λ g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙)))
             ( 𝟙
             , 𝟙
-            , x.arrowIsSet (fst x.ident) (fst y.ident) i
+            , x.arrowIsSet _ _ (fst x.ident) (fst y.ident) i
-            , x.arrowIsSet (snd x.ident) (snd y.ident) i
+            , x.arrowIsSet _ _ (snd x.ident) (snd y.ident) i
             )
           )
       eqUni : T [ xuni ≡ yuni ]

src/Cat/Category/Functor.agda

@@ -61,14 +61,14 @@ module _
 
   IsFunctorIsProp : isProp (IsFunctor _ _ F)
   IsFunctorIsProp isF0 isF1 i = record
-    { ident = 𝔻.arrowIsSet isF0.ident isF1.ident i
+    { ident = 𝔻.arrowIsSet _ _ isF0.ident isF1.ident i
-    ; distrib = 𝔻.arrowIsSet isF0.distrib isF1.distrib i
+    ; distrib = 𝔻.arrowIsSet _ _ isF0.distrib isF1.distrib i
     }
     where
       module isF0 = IsFunctor isF0
       module isF1 = IsFunctor isF1
 
--- Alternate version of above where `F` is a path in 
+-- Alternate version of above where `F` is indexed by an interval
 module _
     {ℓa ℓb : Level}
     {ℂ 𝔻 : Category ℓa ℓb}

src/Cat/Equality.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --cubical #-}
 -- Defines equality-principles for data-types from the standard library.
 
 module Cat.Equality where
@@ -19,3 +20,28 @@ module Equality where
         Σ≡ : a ≡ b
         proj₁ (Σ≡ i) = proj₁≡ i
         proj₂ (Σ≡ i) = proj₂≡ i
+
+        -- Remark 2.7.1: This theorem:
+        --
+        --   (x , u) ≡ (x , v) → u ≡ v
+        --
+        -- does *not* hold! We can only conclude that there *exists* `p : x ≡ x`
+        -- such that
+        --
+        --   p* u ≡ v
+        -- thm : isSet A → (∀ {a} → isSet (B a)) → isSet (Σ A B)
+        -- thm sA sB (x , y) (x' , y') p q = res
+        --   where
+        --     x≡x'0 : x ≡ x'
+        --     x≡x'0 = λ i → proj₁ (p i)
+        --     x≡x'1 : x ≡ x'
+        --     x≡x'1 = λ i → proj₁ (q i)
+        --     someP : x ≡ x'
+        --     someP = {!!}
+        --     tricky : {!y!} ≡ y'
+        --     tricky = {!!}
+        --     -- res' : (λ _ → Σ A B) [ (x , y) ≡ (x' , y') ]
+        --     res' : ({!!} , {!!}) ≡ ({!!} , {!!})
+        --     res' = {!!}
+        --     res : p ≡ q
+        --     res i = {!res'!}