currying as equivalence of functors categories, also moved to new mod…

…ule to avoid circular dep.

Cubical/Categories/Category/Base.agda

@@ -38,6 +38,10 @@ open Category
 _[_,_] : (C : Category ℓ ℓ') → (x y : C .ob) → Type ℓ'
 _[_,_] = Hom[_,_]
 
+_Endo[_] : (C : Category ℓ ℓ') → (x : C .ob) → Type ℓ'
+C Endo[ x ] = C [ x , x ]
+
+
 -- Needed to define this in order to be able to make the subsequence syntax declaration
 seq' : ∀ (C : Category ℓ ℓ') {x y z} (f : C [ x , y ]) (g : C [ y , z ]) → C [ x , z ]
 seq' = _⋆_

Cubical/Categories/Equivalence/AdjointEquivalence.agda

@@ -8,6 +8,9 @@ open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
 open import Cubical.Categories.NaturalTransformation
 
+open import Cubical.Categories.Equivalence.Base
+open import Cubical.HITs.PropositionalTruncation
+
 module Cubical.Categories.Equivalence.AdjointEquivalence
   {ℓC ℓ'C : Level} {ℓD ℓ'D : Level}
   where
@@ -72,6 +75,11 @@ module _ (C : Category ℓC ℓ'C) (D : Category ℓD ℓ'D) where
       η : 𝟙⟨ C ⟩ ≅ᶜ inv ∘F fun
       ε : fun ∘F inv ≅ᶜ 𝟙⟨ D ⟩
       triangleIdentities : TriangleIdentities fun inv (NatIso.trans η) (NatIso.trans ε)
+
+    to≃ᶜ : C ≃ᶜ D
+    _≃ᶜ_.func to≃ᶜ = fun
+    _≃ᶜ_.isEquiv to≃ᶜ = ∣ record { invFunc = inv ; η = η ; ε = ε } ∣₁
+
 module _
   {C : Category ℓC ℓ'C} {D : Category ℓD ℓ'D}
   (adj-equiv : AdjointEquivalence C D)

Cubical/Categories/Instances/Functors.agda

@@ -6,7 +6,6 @@
    Includes the following
    - isos in FUNCTOR are precisely the pointwise isos
    - FUNCTOR C D is univalent when D is
-   - Isomorphism of functors currying
 
 -}
 
@@ -24,7 +23,6 @@ open import Cubical.Categories.Functor.Base
 open import Cubical.Categories.Morphism
 open import Cubical.Categories.NaturalTransformation.Base
 open import Cubical.Categories.NaturalTransformation.Properties
-open import Cubical.Foundations.Function renaming (_∘_ to _∘→_)
 
 private
   variable
@@ -139,57 +137,4 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where
     β .N-ob e ∘⟨ D ⟩ (G .F-hom g ∘⟨ D ⟩ (α .N-ob d ∘⟨ D ⟩ F .F-hom f))
       ≡⟨ D .⋆Assoc _ _ _ ⟩
     (β .N-ob e ∘⟨ D ⟩ G .F-hom g) ∘⟨ D ⟩ (α .N-ob d ∘⟨ D ⟩ F .F-hom f) ∎
-  module _ (E : Category ℓE ℓE') where
-    λF : Functor (E ×C C) D → Functor E FUNCTOR
-    λF F .F-ob e .F-ob c = F ⟅ e , c ⟆
-    λF F .F-ob e .F-hom f = F ⟪ (E .id) , f ⟫
-    λF F .F-ob e .F-id = F .F-id
-    λF F .F-ob e .F-seq f g =
-      F ⟪ E .id , g ∘⟨ C ⟩ f ⟫
-        ≡⟨ (λ i → F ⟪ (E .⋆IdL (E .id) (~ i)) , (g ∘⟨ C ⟩ f) ⟫) ⟩
-      (F ⟪ (E .id ∘⟨ E ⟩ E .id) , g ∘⟨ C ⟩ f ⟫)
-        ≡⟨ F .F-seq (E .id , f) (E .id , g) ⟩
-      (F ⟪ E .id , g ⟫ ∘⟨ D ⟩ F ⟪ E .id , f ⟫) ∎
-    λF F .F-hom h .N-ob c = F ⟪ h , (C .id) ⟫
-    λF F .F-hom h .N-hom f =
-      F ⟪ h , C .id ⟫ ∘⟨ D ⟩ F ⟪ E .id , f ⟫ ≡⟨ sym (F .F-seq _ _) ⟩
-      F ⟪ h ∘⟨ E ⟩ E .id , C .id ∘⟨ C ⟩ f ⟫
-        ≡⟨ (λ i → F ⟪ E .⋆IdL h i , C .⋆IdR f i  ⟫) ⟩
-      F ⟪ h , f ⟫ ≡⟨ (λ i → F ⟪ (E .⋆IdR h (~ i)) , (C .⋆IdL f (~ i)) ⟫) ⟩
-      F ⟪ E .id ∘⟨ E ⟩ h , f ∘⟨ C ⟩ C .id ⟫ ≡⟨ F .F-seq _ _ ⟩
-      F ⟪ E .id , f ⟫ ∘⟨ D ⟩ F ⟪ h , C .id ⟫ ∎
-    λF F .F-id = makeNatTransPath (funExt λ c → F .F-id)
-    λF F .F-seq f g = makeNatTransPath (funExt lem) where
-      lem : (c : C .ob) →
-            F ⟪ g ∘⟨ E ⟩ f , C .id ⟫ ≡
-            F ⟪ g , C .id ⟫ ∘⟨ D ⟩ F ⟪ f , C .id ⟫
-      lem c =
-        F ⟪ g ∘⟨ E ⟩ f , C .id ⟫
-          ≡⟨ (λ i → F ⟪ (g ∘⟨ E ⟩ f) , (C .⋆IdR (C .id) (~ i)) ⟫) ⟩
-        F ⟪ g ∘⟨ E ⟩ f , C .id ∘⟨ C ⟩ C .id ⟫
-          ≡⟨ F .F-seq (f , C .id) (g , C .id) ⟩
-        (F ⟪ g , C .id ⟫) ∘⟨ D ⟩ (F ⟪ f , C .id ⟫) ∎
-
-
-    λF⁻ : Functor E FUNCTOR → Functor (E ×C C) D
-    F-ob (λF⁻ a) = uncurry (F-ob ∘→ F-ob a)
-    F-hom (λF⁻ a) _ = N-ob (F-hom a _) _ ∘⟨ D ⟩ (F-hom (F-ob a _)) _
-    F-id (λF⁻ a) = cong₂ (seq' D) (F-id (F-ob a _))
-        (cong (flip N-ob _) (F-id a)) ∙ D .⋆IdL _
-    F-seq (λF⁻ a) _ (eG , cG) =
-     cong₂ (seq' D) (F-seq (F-ob a _) _ _) (cong (flip N-ob _)
-           (F-seq a _ _))
-          ∙ AssocCong₂⋆R {C = D} _
-              (N-hom ((F-hom a _) ●ᵛ (F-hom a _)) _ ∙
-                (⋆Assoc D _ _ _) ∙
-                  cong (seq' D _) (sym (N-hom (F-hom a eG) cG)))
-
-    isoλF : Iso (Functor (E ×C C) D) (Functor E FUNCTOR)
-    fun isoλF = λF
-    inv isoλF = λF⁻
-    rightInv isoλF b = Functor≡ (λ _ → Functor≡ (λ _ → refl)
-      λ _ → cong (seq' D _) (congS (flip N-ob _) (F-id b)) ∙ D .⋆IdR _)
-      λ _ → toPathP (makeNatTransPath (transportRefl _ ∙
-        funExt λ _ → cong (flip (seq' D) _) (F-id (F-ob b _)) ∙ D .⋆IdL _))
-    leftInv isoλF a = Functor≡ (λ _ → refl) λ _ → sym (F-seq a _ _)
-          ∙ cong (F-hom a) (cong₂ _,_ (E .⋆IdL _) (C .⋆IdR _))
+

Cubical/Categories/Instances/Functors/Currying.agda

@@ -0,0 +1,142 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Instances.Functors.Currying where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Transport
+
+open import Cubical.Categories.Category renaming (isIso to isIsoC)
+open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.Functor.Base
+open import Cubical.Categories.NaturalTransformation.Base
+open import Cubical.Foundations.Function renaming (_∘_ to _∘→_)
+open import Cubical.Categories.Instances.Functors
+open import Cubical.Categories.Equivalence.AdjointEquivalence
+open import Cubical.Categories.Adjoint
+
+private
+  variable
+    ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level
+
+module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where
+  open Category
+  open NatTrans
+  open Functor
+
+
+  open Iso
+
+  module _ (E : Category ℓE ℓE') where
+    λF : Functor (E ×C C) D → Functor E (FUNCTOR C D)
+    λF F .F-ob e .F-ob c = F ⟅ e , c ⟆
+    λF F .F-ob e .F-hom f = F ⟪ (E .id) , f ⟫
+    λF F .F-ob e .F-id = F .F-id
+    λF F .F-ob e .F-seq f g =
+      F ⟪ E .id , g ∘⟨ C ⟩ f ⟫
+        ≡⟨ (λ i → F ⟪ (E .⋆IdL (E .id) (~ i)) , (g ∘⟨ C ⟩ f) ⟫) ⟩
+      (F ⟪ (E .id ∘⟨ E ⟩ E .id) , g ∘⟨ C ⟩ f ⟫)
+        ≡⟨ F .F-seq (E .id , f) (E .id , g) ⟩
+      (F ⟪ E .id , g ⟫ ∘⟨ D ⟩ F ⟪ E .id , f ⟫) ∎
+    λF F .F-hom h .N-ob c = F ⟪ h , (C .id) ⟫
+    λF F .F-hom h .N-hom f =
+      F ⟪ h , C .id ⟫ ∘⟨ D ⟩ F ⟪ E .id , f ⟫ ≡⟨ sym (F .F-seq _ _) ⟩
+      F ⟪ h ∘⟨ E ⟩ E .id , C .id ∘⟨ C ⟩ f ⟫
+        ≡⟨ (λ i → F ⟪ E .⋆IdL h i , C .⋆IdR f i  ⟫) ⟩
+      F ⟪ h , f ⟫ ≡⟨ (λ i → F ⟪ (E .⋆IdR h (~ i)) , (C .⋆IdL f (~ i)) ⟫) ⟩
+      F ⟪ E .id ∘⟨ E ⟩ h , f ∘⟨ C ⟩ C .id ⟫ ≡⟨ F .F-seq _ _ ⟩
+      F ⟪ E .id , f ⟫ ∘⟨ D ⟩ F ⟪ h , C .id ⟫ ∎
+    λF F .F-id = makeNatTransPath (funExt λ c → F .F-id)
+    λF F .F-seq f g = makeNatTransPath (funExt lem) where
+      lem : (c : C .ob) →
+            F ⟪ g ∘⟨ E ⟩ f , C .id ⟫ ≡
+            F ⟪ g , C .id ⟫ ∘⟨ D ⟩ F ⟪ f , C .id ⟫
+      lem c =
+        F ⟪ g ∘⟨ E ⟩ f , C .id ⟫
+          ≡⟨ (λ i → F ⟪ (g ∘⟨ E ⟩ f) , (C .⋆IdR (C .id) (~ i)) ⟫) ⟩
+        F ⟪ g ∘⟨ E ⟩ f , C .id ∘⟨ C ⟩ C .id ⟫
+          ≡⟨ F .F-seq (f , C .id) (g , C .id) ⟩
+        (F ⟪ g , C .id ⟫) ∘⟨ D ⟩ (F ⟪ f , C .id ⟫) ∎
+
+    λFFunctor : Functor (FUNCTOR (E ×C C) D) (FUNCTOR E (FUNCTOR C D))
+    F-ob λFFunctor = λF
+    N-ob (F-hom λFFunctor x) _ =
+     natTrans (curry (N-ob x) _) (curry (N-hom x) _)
+    N-hom ((F-hom λFFunctor) x) _ =
+     makeNatTransPath (funExt λ _ → N-hom x (_ , C .id))
+    F-id λFFunctor = makeNatTransPath refl
+    F-seq λFFunctor _ _ = makeNatTransPath refl
+
+    λF⁻ : Functor E (FUNCTOR C D) → Functor (E ×C C) D
+    F-ob (λF⁻ a) = uncurry (F-ob ∘→ F-ob a)
+    F-hom (λF⁻ a) _ = N-ob (F-hom a _) _ ∘⟨ D ⟩ (F-hom (F-ob a _)) _
+    F-id (λF⁻ a) = cong₂ (seq' D) (F-id (F-ob a _))
+        (cong (flip N-ob _) (F-id a)) ∙ D .⋆IdL _
+    F-seq (λF⁻ a) _ (eG , cG) =
+     cong₂ (seq' D) (F-seq (F-ob a _) _ _) (cong (flip N-ob _)
+           (F-seq a _ _))
+          ∙ AssocCong₂⋆R {C = D} _
+              (N-hom ((F-hom a _) ●ᵛ (F-hom a _)) _ ∙
+                (⋆Assoc D _ _ _) ∙
+                  cong (seq' D _) (sym (N-hom (F-hom a eG) cG)))
+
+    λF⁻Functor : Functor (FUNCTOR E (FUNCTOR C D)) (FUNCTOR (E ×C C) D)
+    F-ob λF⁻Functor = λF⁻
+    N-ob (F-hom λF⁻Functor x) = uncurry (N-ob ∘→ N-ob x)
+    N-hom ((F-hom λF⁻Functor) {F} {F'} x) {xx} {yy} =
+     uncurry λ hh gg →
+                AssocCong₂⋆R {C = D} _ (cong N-ob (N-hom x hh) ≡$ _)
+            ∙∙ cong (comp' D _) ((N-ob x (fst xx) .N-hom) gg)
+            ∙∙ D .⋆Assoc _ _ _
+
+    F-id λF⁻Functor = makeNatTransPath refl
+    F-seq λF⁻Functor _ _ = makeNatTransPath refl
+
+    isoλF : Iso (Functor (E ×C C) D) (Functor E (FUNCTOR C D))
+    fun isoλF = λF
+    inv isoλF = λF⁻
+    rightInv isoλF b = Functor≡ (λ _ → Functor≡ (λ _ → refl)
+      λ _ → cong (seq' D _) (congS (flip N-ob _) (F-id b)) ∙ D .⋆IdR _)
+      λ _ → makeNatTransPathP _ _
+        (funExt λ _ → cong (comp' D _) (F-id (F-ob b _)) ∙ D .⋆IdL _)
+    leftInv isoλF a = Functor≡ (λ _ → refl) λ _ → sym (F-seq a _ _)
+          ∙ cong (F-hom a) (cong₂ _,_ (E .⋆IdL _) (C .⋆IdR _))
+
+    open AdjointEquivalence
+
+
+    𝟙≅ᶜλF⁻∘λF : 𝟙⟨ FUNCTOR (E ×C C) D ⟩ ≅ᶜ λF⁻Functor ∘F λFFunctor
+    𝟙≅ᶜλF⁻∘λF = pathToNatIso $
+         Functor≡ (λ x → Functor≡ (λ _ → refl)
+                  λ _ → cong (F-hom x) (cong₂ _,_ (sym (E .⋆IdL _)) (sym (C .⋆IdR _)))
+                    ∙ F-seq x _ _)
+              λ _ → makeNatTransPathP _ _ refl
+
+    λF∘λF⁻≅ᶜ𝟙 : λFFunctor ∘F λF⁻Functor ≅ᶜ 𝟙⟨ FUNCTOR E (FUNCTOR C D) ⟩
+    λF∘λF⁻≅ᶜ𝟙 = pathToNatIso $ Functor≡
+      (λ x → Functor≡
+         (λ _ → Functor≡ (λ _ → refl) λ _ → cong (D ⋆ F-hom (F-ob x _) _)
+                   (cong N-ob (F-id x) ≡$ _) ∙ D .⋆IdR _)
+         λ _ → makeNatTransPathP _ _
+                    (funExt λ _ → cong (comp' D _) (F-id (F-ob x _)) ∙ D .⋆IdL _))
+         λ _ → makeNatTransPathP _ _ (funExt λ _ → makeNatTransPathP _ _ refl)
+
+    open UnitCounit.TriangleIdentities
+
+    FunctorCurryAdjointEquivalence :
+      AdjointEquivalence (FUNCTOR (E ×C C) D) (FUNCTOR E (FUNCTOR C D))
+    fun FunctorCurryAdjointEquivalence = λFFunctor
+    inv FunctorCurryAdjointEquivalence = λF⁻Functor
+    η FunctorCurryAdjointEquivalence = 𝟙≅ᶜλF⁻∘λF
+    ε FunctorCurryAdjointEquivalence = λF∘λF⁻≅ᶜ𝟙
+    Δ₁ (triangleIdentities FunctorCurryAdjointEquivalence) c = makeNatTransPath $
+      funExt λ _ → makeNatTransPath (funExt λ _ → cong (join $ seq' D)
+        (congP₂$ (transport-fillerExt⁻ (cong (D Endo[_] ∘→ c ⟅_⟆) (transportRefl _))) λ _ → D .id)
+      ∙ D .⋆IdR _)
+
+    Δ₂ (triangleIdentities FunctorCurryAdjointEquivalence) d = makeNatTransPath $
+      funExt λ _ → cong (join $ seq' D)
+        (congP₂$ (transport-fillerExt⁻ (cong (D Endo[_] ∘→  uncurry (F-ob ∘→ F-ob d))
+              (transportRefl _))) λ _ → D .id)
+      ∙ D .⋆IdR _
+

Cubical/Foundations/Function.agda

@@ -82,6 +82,9 @@ uncurry4 f (x , y , z , w , u) = f x y z w u
 curry : ((p : Σ A B) → C (fst p) (snd p)) → (x : A) → (y : B x) → C x y
 curry f x y = f (x , y)
 
+join : {B : (x y : A) → Type ℓ} → (∀ x y → B x y) → ∀ x → B x x
+join f x = f x x
+
 module _ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} where
   -- Notions of 'coherently constant' functions for low dimensions.
   -- These are the properties of functions necessary to e.g. eliminate

Cubical/Foundations/Prelude.agda

@@ -327,6 +327,12 @@ funExt⁻ : {B : A → I → Type ℓ'}
   → ((x : A) → PathP (B x) (f x) (g x))
 funExt⁻ eq x i = eq i x
 
+congP₂$ : {A : I → Type ℓ} {B : ∀ i → A i → Type ℓ'}
+  {f : ∀ x → B i0 x} {g : ∀ y → B i1 y}
+  → (p : PathP (λ i → ∀ x → B i x) f g)
+  → ∀ {x y} (p : PathP A x y) → PathP (λ i → B i (p i)) (f x) (g y)
+congP₂$ eq x i = eq i (x i)
+
 implicitFunExt⁻ : {B : A → I → Type ℓ'}
   {f : {x : A} → B x i0} {g : {x : A} → B x i1}
   → PathP (λ i → {x : A} → B x i) f g