Rely on global cubical again

cat.agda-lib

@@ -2,13 +2,11 @@ name: cat
 -- version: 0.0.1
 -- description:
 --   A formalization of category theory in Agda using cubical type theory.
--- depend:
+depend:
---   standard-library
+  standard-library
---   cubical
+  cubical
 include:
   src
-  libs/agda-stdlib/src
-  libs/cubical/src
 -- libraries:
 --   libs/agda-stdlib
 --   libs/cubical

libs/agda-stdlib

@@ -1 +1 @@
-Subproject commit b5bfbc3c170b0bd0c9aaac1b4d4b3f9b06832bf6
+Subproject commit 157497a5335ad0069c7aaffbc65932c40a28ee68

libs/cubical

@@ -1 +1 @@
-Subproject commit 1d6730c4999daa2b04e9dd39faa0791d0b5c3b48
+Subproject commit 12c2c628e9e202f1698a4c32e0356d5ca8cb6151

src/Cat/Categories/Fun.agda

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

src/Cat/Category.agda

@@ -12,7 +12,7 @@ open import Data.Product renaming
 open import Data.Empty
 import Function
 open import Cubical
-open import Cubical.GradLemma using ( propIsEquiv )
+open import Cubical.NType.Properties using ( propIsEquiv )
 
 ∃! : ∀ {a b} {A : Set a}
   → (A → Set b) → Set (a ⊔ b)

src/Cat/Category/Functor.agda

@@ -83,7 +83,7 @@ module _
   IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻}
     (\ F → IsFunctorIsProp {F = F}) (\ i → F i)
     where
-      open import Cubical.GradLemma using (lemPropF)
+      open import Cubical.NType.Properties using (lemPropF)
 
 module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
   Functor≡ : {F G : Functor ℂ 𝔻}