New profunctors (#51)

* new definition of profunctor * progress on slick functor comprehension Co-authored-by: Steven Schaefer <[email protected]> * Graph of a profunctor as a displayed category * fix the definition of Graph lol * work on Comma categories * introduction principle for Grothendieck construction * more Functor^D combinators, IsoComma functor constructor * more IsoComma stuff, use Preorder^D a bit less * more progress on Comma cat stuff, probably done for today * start porting FunctorComprehension proof to use Graph/IsoComma * hasPropHomsIsoCommaD * one more hole filled * invMoveLinv * hasPropHomsIsoCommaD1 * hasContrHomsIsoCommaᴰ₁ done * fullyfaithfulcomposition * fullcomposefull, faithfulcomposefaithful * Define new FunctorComprehension, more displayed stuff * Port Adjoints, BinProducts to new format. Better definition of BinProducts * bifunctorial construction of the product of presheaves * simplify definition of product of presheaves functor * compositional definition of BinProduct UMP, Intro rule for Redundant Prod * Define Relators, Natural Elements of Relators * whiskered pi-elt * get counit-elt from whiskering, some naming changes * A few new combinators, fixing definitions broken by changes * fix whitespace * mk\intsrfunctor * Universal Elements as structure to Representations as structure * define the natural isomorphism from representability * line lengths * line lengths but for real * make some local defs private * clean up --------- Co-authored-by: Steven Schaefer <[email protected]>
maxsnew · Feb 20, 2024 · 44f6100 · 44f6100
1 parent 05f521c
commit 44f6100
Show file tree

Hide file tree

Showing 26 changed files with 1,565 additions and 743 deletions.
diff --git a/Cubical/Categories/Adjoint/2Var.agda b/Cubical/Categories/Adjoint/2Var.agda
@@ -6,8 +6,8 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Profunctor.General
-open import Cubical.Categories.Constructions.BinProduct.Redundant.Base
-open import Cubical.Categories.Bifunctor.Redundant
+open import Cubical.Categories.Constructions.BinProduct.Redundant.Base as Prod
+open import Cubical.Categories.Bifunctor.Redundant as Bif
 open import Cubical.Categories.Constructions.BinProduct.Redundant.Assoc
 
 private
@@ -17,32 +17,38 @@ private
 open Category
 
 -- Given a Bifunctor F : C , D → E
--- A Right Adjoint in C would be a
--- Bifunctor
--- -<=[F]=- : E , D ^op → C
+-- a Right Adjoint valued in D would be
 -- -=[F]=>- : C ^op , E → D
+-- a Right Adjoint valued in C would be
+-- -<=[F]=- : E , D ^op → C
 --
 -- satisfying
 -- E [ F ⟅ c , d ⟆ , e ]
--- =~ C [ c , d <=[ F ]= e ]
+-- =~ C [ c , e <=[ F ]= d ]
 -- =~ D [ d , c =[ F ]=> e ]
+--
+-- with universal elements of the form
+-- E [ F ⟅ c , c =[ F ]=> e ⟆ , e ]
+-- E [ F ⟅ e <=[ F ]= d , d ⟆ , e ]
+
+module _ {C : Category ℓC ℓC'}
+         {D : Category ℓD ℓD'}
+         {E : Category ℓE ℓE'}
+         (F : Bifunctor C D E)
+         where
+  RightAdjointRProf : Profunctor ((C ^op) ×C E) D ℓE'
+  RightAdjointRProf =
+    CurryBifunctor (assoc-bif⁻
+      (assoc-bif (HomBif E ∘Fl rec (C ^op) (D ^op) (F ^opBif))
+      ∘Fr Prod.Sym))
+
+  RightAdjointR : Type _
+  RightAdjointR = UniversalElements RightAdjointRProf
+
+  RightAdjointLProf : Profunctor (E ×C (D ^op)) C ℓE'
+  RightAdjointLProf =
+    CurryBifunctor (assoc-bif⁻ (Bif.Sym
+      (HomBif E ∘Fl rec (D ^op) (C ^op) (Bif.Sym (F ^opBif)))))
 
-2VarRightAdjointR : (C : Category ℓC ℓC')
-               (D : Category ℓD ℓD')
-               (E : Category ℓE ℓE')
-               (F : Bifunctor C D E) → Type _
-2VarRightAdjointR C D E F =
-  UniversalElements ((C ^op) ×C E) D
-    (assoc-bif (HomBif E ∘Fl
-      (rec D C (Sym F) ^opF) ∘F
-      ×-op-commute⁻ {C = D}{D = C}))
-
-2VarRightAdjointL : (C : Category ℓC ℓC')
-               (D : Category ℓD ℓD')
-               (E : Category ℓE ℓE')
-               (F : Bifunctor C D E) → Type _
-2VarRightAdjointL C D E F =
-  UniversalElements ((D ^op) ×C E) C
-    (assoc-bif (HomBif E ∘Fl
-      (rec C D F ^opF) ∘F
-      ×-op-commute⁻ {C = C}{D = D}))
+  RightAdjointL : Type _
+  RightAdjointL = UniversalElements RightAdjointLProf
diff --git a/Cubical/Categories/Adjoint/UniversalElements.agda b/Cubical/Categories/Adjoint/UniversalElements.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe #-}
+{-# OPTIONS --safe --lossy-unification #-}
 
 module Cubical.Categories.Adjoint.UniversalElements where
 
@@ -7,26 +7,46 @@ open import Cubical.Foundations.Isomorphism
 open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Profunctor.General
+open import Cubical.Categories.Profunctor.FunctorComprehension
+open import Cubical.Categories.Presheaf.Base
 open import Cubical.Categories.Presheaf.More
 open import Cubical.Categories.Presheaf.Representable
 open import Cubical.Categories.Instances.Sets
+open import Cubical.Categories.Yoneda
 
 private
   variable
     ℓC ℓC' ℓD ℓD' : Level
 
 open Category
 
-RightAdjoint : (C : Category ℓC ℓC')
-               (D : Category ℓD ℓD')
-               (F : Functor C D) → Type _
-RightAdjoint C D F  = UniversalElements D C (Functor→Profo-* C D F)
+-- A right adjoint to F : C → D
+-- is specified by a functor RAdj F : D → 𝓟 C
+--   RAdj F d c := D [ F c , d ]
+module _ {C : Category ℓC ℓC'}
+         {D : Category ℓD ℓD'}
+         (F : Functor C D)
+         where
+  RightAdjointProf : Functor D (PresheafCategory C ℓD')
+  RightAdjointProf = precomposeF (SET _) (F ^opF) ∘F YO
+
+
+  RightAdjointAt : (d : D .ob) → Type _
+  RightAdjointAt d = UniversalElement C (RightAdjointProf ⟅ d ⟆)
+
+  RightAdjoint : Type _
+  RightAdjoint = UniversalElements RightAdjointProf
 
-RightAdjointAt : (C : Category ℓC ℓC')
-                 (D : Category ℓD ℓD')
-                 (F : Functor C D)
-                 (d : D .ob) → Type _
-RightAdjointAt C D F = UniversalElementAt D C (Functor→Profo-* C D F)
+
+module _ {C : Category ℓC ℓC'}
+         {D : Category ℓD ℓD'}
+         (F : Functor C D)
+         where
+  LeftAdjoint : Type _
+  LeftAdjoint = RightAdjoint (F ^opF)
+
+  LeftAdjointAt : (d : D .ob) → Type _
+  LeftAdjointAt = RightAdjointAt (F ^opF)
 
 -- Uh Oh
 RightAdjointAt' : (C : Category ℓC ℓC')
@@ -40,7 +60,7 @@ RightAdjointAt→Prime : (C : Category ℓC ℓC')
                  (D : Category ℓD ℓD')
                  (F : Functor C D)
                  (d : D .ob)
-                 → RightAdjointAt C D F d → RightAdjointAt' C D F d
+                 → RightAdjointAt F d → RightAdjointAt' C D F d
 RightAdjointAt→Prime C D F d x .UniversalElement.vertex =
   UniversalElement.vertex x
 RightAdjointAt→Prime C D F d x .UniversalElement.element =
@@ -61,13 +81,3 @@ IdRightAdj' C c .UniversalElement.element = id C
 IdRightAdj' C c .UniversalElement.universal c' =
   isoToIsEquiv (iso _ (λ z → z) (C .⋆IdR) (C .⋆IdR))
 
-LeftAdjoint : (C : Category ℓC ℓC')
-              (D : Category ℓD ℓD')
-              (F : Functor C D) → Type _
-LeftAdjoint C D F  = RightAdjoint (C ^op) (D ^op) (F ^opF)
-
-LeftAdjointAt : (C : Category ℓC ℓC')
-                (D : Category ℓD ℓD')
-                (F : Functor C D)
-                (d : D .ob) → Type _
-LeftAdjointAt C D F = RightAdjointAt (C ^op) (D ^op) (F ^opF)
diff --git a/Cubical/Categories/Bifunctor/Redundant.agda b/Cubical/Categories/Bifunctor/Redundant.agda
@@ -147,6 +147,25 @@ record BifunctorSep (C : Category ℓc ℓc')
                → Bif-homR c g ⋆⟨ E ⟩ Bif-homL f d'
                ≡ Bif-homL f d ⋆⟨ E ⟩ Bif-homR c' g
 
+-- A version of bifunctor that only requires the parallel action and
+-- constructs the joint acions using id. This is definitionally
+-- isomorphic to a functor out of the ordinary cartesian product of C
+-- and D.
+record BifunctorPar (C : Category ℓc ℓc')
+                  (D : Category ℓd ℓd')
+                  (E : Category ℓe ℓe')
+       : Type (ℓ-max ℓc (ℓ-max ℓc' (ℓ-max ℓd (ℓ-max ℓd' (ℓ-max ℓe ℓe'))))) where
+  field
+    Bif-ob : C .ob → D .ob → E .ob
+    Bif-hom× : ∀ {c c' d d'} (f : C [ c , c' ])(g : D [ d , d' ])
+             → E [ Bif-ob c d , Bif-ob c' d' ]
+    Bif-×-id : ∀ {c d} → Bif-hom× (C .id {c}) (D .id {d}) ≡ E .id
+    Bif-×-seq : ∀ {c c' c'' d d' d''}
+               (f : C [ c , c' ])(f' : C [ c' , c'' ])
+               (g : D [ d , d' ])(g' : D [ d' , d'' ])
+             → Bif-hom× (f ⋆⟨ C ⟩ f') (g ⋆⟨ D ⟩ g')
+             ≡ Bif-hom× f g ⋆⟨ E ⟩ Bif-hom× f' g'
+
 private
   variable
     C D E : Category ℓ ℓ'
@@ -242,9 +261,24 @@ mkBifunctorParAx {C = C}{D = D}{E = E} F = G where
     ∙ sym (F .Bif-×-seq _ _ _ _)
     ∙ cong₂ (F .Bif-hom×) (C .⋆IdL _) (D .⋆IdR _)
 
+mkBifunctorPar : BifunctorPar C D E → Bifunctor C D E
+mkBifunctorPar {C = C}{D = D}{E = E} F = mkBifunctorParAx G where
+  module F = BifunctorPar F
+  G : BifunctorParAx C D E
+  G .Bif-ob = F.Bif-ob
+  G .Bif-hom× = F.Bif-hom×
+  G .Bif-×-id = F.Bif-×-id
+  G .Bif-×-seq = F.Bif-×-seq
+  G .Bif-homL f d = F.Bif-hom× f (D .id)
+  G .Bif-homR c g = F.Bif-hom× (C .id) g
+  G .Bif-L×-agree f = refl
+  G .Bif-R×-agree g = refl
+
 open Bifunctor
 open BifunctorParAx
+open BifunctorPar
 open BifunctorSepAx
+open BifunctorSep
 -- action on objects
 infix 30 _⟅_⟆b
 _⟅_⟆b : (F : Bifunctor C D E)
@@ -438,14 +472,28 @@ compF {E = E}{E' = E'}{C = C}{D = D} F  G = mkBifunctorParAx B where
   B .Bif-L×-agree f = cong (F ⟪_⟫) (G .Bif-L×-agree f)
   B .Bif-R×-agree g = cong (F ⟪_⟫) (G .Bif-R×-agree g)
 
-infixr 30 compL
-infixr 30 compR
+infixl 30 compL
+infixl 30 compR
 infixr 30 compF
+infixl 30 compLR'
 
 syntax compL F G = F ∘Fl G
 syntax compR F G = F ∘Fr G
 syntax compF F G = F ∘Fb G
 
+-- | This includes an arbitrary choice, the action on objects should
+-- | be definitionally equal to the other order, but the proofs are
+-- | affected.
+compLR : (F : Bifunctor C' D' E) (G : Functor C C')(H : Functor D D')
+       → Bifunctor C D E
+compLR F G H = F ∘Fl G ∘Fr H
+
+compLR' : (F : Bifunctor C' D' E) (GH : Functor C C' × Functor D D')
+        → Bifunctor C D E
+compLR' F GH = compLR F (GH .fst) (GH .snd)
+
+syntax compLR' F GH = F ∘Flr GH
+
 -- For Hom we use the Seperate actions formulation because there is no
 -- "nice" way to do triple composition (at least with this definition
 -- of category).
@@ -467,6 +515,25 @@ BifunctorToParFunctor F .F-hom (f , g) = F .Bif-hom× f g
 BifunctorToParFunctor F .F-id = F .Bif-×-id
 BifunctorToParFunctor F .F-seq f g = F .Bif-×-seq _ _ _ _
 
+CurriedToBifunctor : Functor C (FUNCTOR D E) → Bifunctor C D E
+CurriedToBifunctor F = mkBifunctorSep G where
+  G : BifunctorSep _ _ _
+  G .Bif-ob c d = F ⟅ c ⟆ ⟅ d ⟆
+  G .Bif-homL f d = F ⟪ f ⟫ ⟦ d ⟧
+  G .Bif-homR c g = F ⟅ c ⟆ ⟪ g ⟫
+  G .Bif-L-id {d = d} = (cong (_⟦ d ⟧) (F .F-id))
+  G .Bif-L-seq f f' = (cong (_⟦ _ ⟧) (F .F-seq f f'))
+  G .Bif-R-id = (F ⟅ _ ⟆) .F-id
+  G .Bif-R-seq g g' = (F ⟅ _ ⟆) .F-seq g g'
+  G .SepBif-RL-commute f g = (F ⟪ f ⟫) .N-hom g
+
+CurryBifunctor : Bifunctor C D E → Functor C (FUNCTOR D E)
+CurryBifunctor F .F-ob c = appL F c
+CurryBifunctor F .F-hom f .N-ob d = appR F d .F-hom f
+CurryBifunctor F .F-hom f .N-hom g = Bif-RL-commute F f g
+CurryBifunctor F .F-id = makeNatTransPath (funExt λ d → F .Bif-L-id)
+CurryBifunctor F .F-seq _ _ = makeNatTransPath (funExt λ d → F .Bif-L-seq _ _)
+
 open Separate.Bifunctor
 ForgetPar : Bifunctor C D E → Separate.Bifunctor C D E
 ForgetPar F .Bif-ob = F .Bif-ob
@@ -477,3 +544,17 @@ ForgetPar F .Bif-idR = F .Bif-R-id
 ForgetPar F .Bif-seqL = F .Bif-L-seq
 ForgetPar F .Bif-seqR = F .Bif-R-seq
 ForgetPar F .Bif-assoc f g = sym (Bif-RL-commute F f g)
+
+_^opBif : Bifunctor C D E
+        → Bifunctor (C ^op) (D ^op) (E ^op)
+_^opBif {C = C}{D = D}{E = E} F = mkBifunctorParAx G where
+  module F = Bifunctor F
+  G : BifunctorParAx (C ^op) (D ^op) (E ^op)
+  G .Bif-ob = F.Bif-ob
+  G .Bif-homL = F.Bif-homL
+  G .Bif-homR = F.Bif-homR
+  G .Bif-hom× = F.Bif-hom×
+  G .Bif-×-id = F.Bif-×-id
+  G .Bif-×-seq f f' g g' = F.Bif-×-seq f' f g' g
+  G .Bif-L×-agree = F.Bif-L×-agree
+  G .Bif-R×-agree = F.Bif-R×-agree
diff --git a/Cubical/Categories/Comonad/ExtensionSystem.agda b/Cubical/Categories/Comonad/ExtensionSystem.agda
@@ -54,7 +54,7 @@ module _ (C : Category ℓ ℓ') where
     F = (MES.G (C ^op) E) ^opF
 
     open import Cubical.Categories.Adjoint.UniversalElements
-    G : RightAdjoint _ _ F
+    G : RightAdjoint F
     G = MES.F (C ^op) E
 
   pull : {T T' : ExtensionSystem} → ComonadMorphism T T' →

diff --git a/Cubical/Categories/Constructions/BinProduct/Redundant/Assoc.agda b/Cubical/Categories/Constructions/BinProduct/Redundant/Assoc.agda
@@ -30,3 +30,6 @@ module _ {C : Category ℓc ℓc'}
          {D : Category ℓd ℓd'}{E : Category ℓe ℓe'}{F : Category ℓf ℓf'} where
   assoc-bif : Bifunctor (C ×C D) E F → Bifunctor C (D ×C E) F
   assoc-bif G = Functor→Bifunctor (rec (C ×C D) E G ∘F ToLeft.Assoc)
+
+  assoc-bif⁻ : Bifunctor C (D ×C E) F → Bifunctor (C ×C D) E F
+  assoc-bif⁻ G = Functor→Bifunctor (rec C (D ×C E) G ∘F ToRight.Assoc)