[WIP] natural transformations are sets

src/Cat/Categories/Fun.agda

@@ -6,6 +6,7 @@ open import Cubical
 open import Function
 open import Data.Product
 import Cubical.GradLemma
+module UIP = Cubical.GradLemma
 
 open import Cat.Category
 open import Cat.Category.Functor
@@ -117,11 +118,29 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
           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 f : isSet (NaturalTransformation F G)
+      f a b p q i = res
+        where
+          k : (θ : Transformation F G) → (xx yy : Natural F G θ) → xx ≡ yy
+          k θ x y = let kk = naturalIsProp θ x y in {!!}
+          res : a ≡ b
+          res j = {!!} , {!!}
+      -- naturalTransformationIsSets σa σb p q
+        -- where
+          -- -- In Andrea's proof `lemSig` he proves something very similiar to
+          -- -- what I'm doing here, just for `Cubical.FromPathPrelude.Σ` rather
+          -- -- than `Σ`. In that proof, he just needs *one* proof that the first
+          -- -- components are equal - hence the arbitrary usage of `p` here.
+          -- secretSauce : proj₁ σa ≡ proj₁ σb
+          -- secretSauce i = proj₁ (p i)
+          -- lemSig : σa ≡ σb
+          -- lemSig i = (secretSauce i) , (UIP.lemPropF naturalIsProp secretSauce) {proj₂ σa} {proj₂ σb} i
+          -- res : p ≡ q
+          -- res = {!!}
       naturalTransformationIsSets (θ , θNat) (η , ηNat) p q i j
         = θ-η
         -- `i or `j - `p'` or `q'`?
-        , refl {x = t} i
+        , {!!} -- UIP.lemPropF {B = Natural F G} (λ x → {!!}) {(θ , θNat)} {(η , ηNat)} {!!} 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) {!!} {!!}