Relative monad

Cubical/Categories/Displayed/Constructions/PresheafElements.agda

@@ -0,0 +1,34 @@
+{-
+
+  The category of elements of a presheaf is naturally formulated as a
+  total category of a displayed category.
+
+-}
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Displayed.Constructions.PresheafElements where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Instances.Sets
+open import Cubical.Categories.Functor.Base
+open import Cubical.Categories.Presheaf hiding (Elements)
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Properties
+open import Cubical.Categories.Displayed.Instances.Sets.Elements
+  renaming (Element to SetElement)
+
+private
+  variable
+    ℓB ℓB' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓP : Level
+
+module _ {C : Category ℓC ℓC'}
+         (P : Presheaf C ℓP) where
+  Elemento : Categoryᴰ C ℓP ℓP
+  Elemento = reindex (SetElement _) P ^opᴰ
+
+module _ {C : Category ℓC ℓC'}
+         (P : Functor C (SET ℓP)) where
+  Element* : Categoryᴰ C ℓP ℓP
+  Element* = reindex (SetElement _) P

Cubical/Categories/Displayed/Instances/Functor.agda

@@ -14,10 +14,10 @@ open import Cubical.Categories.Displayed.NaturalTransformation
 
 private
   variable
-    ℓC ℓC' ℓD ℓD' : Level
+    ℓC ℓC' ℓD ℓD' ℓCᴰ ℓCᴰ' ℓDᴰ ℓDᴰ' : Level
 
 module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}
-  (Cᴰ : Categoryᴰ C ℓC ℓC')(Dᴰ : Categoryᴰ D ℓD ℓD') where
+  (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ')(Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ') where
 
   open Category
   open Functorᴰ

Cubical/Categories/Displayed/Instances/Sets/Elements.agda

@@ -0,0 +1,37 @@
+{-
+
+  The category of elements of a presheaf is naturally formulated as a
+  total category of a displayed category.
+
+-}
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Displayed.Instances.Sets.Elements where
+
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Structure
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Instances.Sets
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Functor
+open import Cubical.Categories.Displayed.Constructions.StructureOver
+
+private
+  variable
+    ℓB ℓB' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓP : Level
+
+module _ (ℓ : Level) where
+  Element : Categoryᴰ (SET ℓ) ℓ ℓ
+  Element = StructureOver→Catᴰ S where
+    open StructureOver
+    S : StructureOver _ _ _
+    S .ob[_] X = ⟨ X ⟩
+    S .Hom[_][_,_] f x y = f x ≡ y
+    S .idᴰ = refl
+    S ._⋆ᴰ_ {g = g} fx≡y gy≡z = cong g fx≡y ∙ gy≡z
+    S .isPropHomᴰ {y = Y} = Y .snd _ _

Cubical/Categories/Displayed/Limits/BinProduct.agda

@@ -5,11 +5,9 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Data.Sigma
 
 open import Cubical.Categories.Category.Base
-open import Cubical.Categories.Adjoint.UniversalElements
 open import Cubical.Categories.Limits.BinProduct.More
 open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.Adjoint.More
-open import Cubical.Categories.Displayed.Constructions.Slice
 open import Cubical.Categories.Displayed.Constructions.BinProduct.More
 
 private

Cubical/Categories/Displayed/Limits/Limits.agda

@@ -0,0 +1,106 @@
+{-
+  Displayed limits, aka lifted limits.
+-}
+
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Displayed.Limits.Limits where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Functor
+open import Cubical.Categories.NaturalTransformation
+open import Cubical.Categories.Instances.Functors
+open import Cubical.Categories.Adjoint.UniversalElements
+open import Cubical.Categories.Limits.AsRepresentable
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Section.Base
+open import Cubical.Categories.Displayed.Functor
+open import Cubical.Categories.Displayed.Instances.Terminal
+open import Cubical.Categories.Displayed.Instances.Terminal.More
+open import Cubical.Categories.Displayed.NaturalTransformation
+open import Cubical.Categories.Displayed.Adjoint.More
+-- TODO: fix this naming to be Functors
+open import Cubical.Categories.Displayed.Instances.Functor
+
+private
+  variable
+    ℓC ℓC' ℓCᴰ ℓCᴰ' ℓJ ℓJ' ℓJᴰ ℓJᴰ' : Level
+
+open Functor
+open Functorᴰ
+open NatTrans
+open NatTransᴰ
+
+module _ {C : Category ℓC ℓC'} {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'}
+         {J : Category ℓJ ℓJ'} {Jᴰ : Categoryᴰ J ℓJᴰ ℓJᴰ'}
+       where
+  private
+    import Cubical.Categories.Displayed.Reasoning as HomᴰReasoning
+    module R = HomᴰReasoning Cᴰ
+    module C = Category C
+    module Cᴰ = Categoryᴰ Cᴰ
+  ΔFᴰ : Functorᴰ ΔF Cᴰ (FUNCTORᴰ Jᴰ Cᴰ)
+  ΔFᴰ .F-obᴰ c .F-obᴰ _ = c
+  ΔFᴰ .F-obᴰ c .F-homᴰ _ = Cᴰ.idᴰ
+  ΔFᴰ .F-obᴰ c .F-idᴰ = refl
+  ΔFᴰ .F-obᴰ c .F-seqᴰ _ _ = R.≡[]-rectify (symP (Cᴰ.⋆IdLᴰ _))
+  ΔFᴰ .F-homᴰ fᴰ .N-obᴰ _ = fᴰ
+  ΔFᴰ .F-homᴰ fᴰ .N-homᴰ _ = R.≡[]-rectify (R.≡[]∙ (C.⋆IdL _) (sym (C.⋆IdR _))
+    (Cᴰ.⋆IdLᴰ _)
+    (symP (Cᴰ.⋆IdRᴰ _)))
+  ΔFᴰ .F-idᴰ = makeNatTransPathᴰ _ _ _ refl
+  ΔFᴰ .F-seqᴰ fᴰ gᴰ = makeNatTransPathᴰ _ _ _ refl
+
+  limitᴰ : {F : Functor J C} → limit F → Functorᴰ F Jᴰ Cᴰ → Type _
+  limitᴰ = RightAdjointAtᴰ ΔFᴰ
+
+limitsᴰOfShape :
+  {C : Category ℓC ℓC'} {J : Category ℓJ ℓJ'}
+  → limitsOfShape C J
+  → Categoryᴰ C ℓCᴰ ℓCᴰ'
+  → Categoryᴰ J ℓJᴰ ℓJᴰ'
+  → Type _
+limitsᴰOfShape lims Cᴰ Jᴰ = RightAdjointᴰ (ΔFᴰ {Cᴰ = Cᴰ}{Jᴰ = Jᴰ}) lims
+
+liftedLimit :
+  {C : Category ℓC ℓC'}
+  {J : Category ℓJ ℓJ'}
+  {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'}
+  → {cⱼ : Functor J C}
+  → limit cⱼ
+  → (cᴰⱼ : Section cⱼ Cᴰ)
+  → Type _
+liftedLimit lim⟨cⱼ⟩ cᴰⱼ = limitᴰ lim⟨cⱼ⟩ (recᴰ cᴰⱼ)
+
+-- A displayed category Cᴰ lifts a limit lim⟨cⱼ⟩ when every lift of cⱼ
+-- has a limᴰ
+liftsLimit :
+  {C : Category ℓC ℓC'}
+  {J : Category ℓJ ℓJ'}
+  → {cⱼ : Functor J C}
+  → (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ')
+  → limit cⱼ
+  → Type _
+liftsLimit {cⱼ = cⱼ} Cᴰ lim =
+  ∀ (cᴰⱼ : Section cⱼ Cᴰ) → liftedLimit lim cᴰⱼ
+
+liftsLimitsOfShape :
+  {C : Category ℓC ℓC'}
+  → Category ℓJ ℓJ'
+  → Categoryᴰ C ℓCᴰ ℓCᴰ'
+  → Type _
+liftsLimitsOfShape {C = C} J Cᴰ =
+  ∀ (cⱼ : Functor J _)
+    (lim⟨cⱼ⟩ : limit cⱼ)
+  → liftsLimit Cᴰ lim⟨cⱼ⟩
+
+liftsLimitsOfSize : {C : Category ℓC ℓC'} (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ')
+  → ∀ (ℓJ ℓJ' : Level) → Type _
+liftsLimitsOfSize {C = C} Cᴰ ℓJ ℓJ' =
+  ∀ (J : Category ℓJ ℓJ')
+  → liftsLimitsOfShape J Cᴰ
+
+liftsLimits : {C : Category ℓC ℓC'} (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') → Typeω
+liftsLimits Cᴰ = ∀ ℓJ ℓJ' → liftsLimitsOfSize Cᴰ ℓJ ℓJ'

Cubical/Categories/Limits/AsRepresentable.agda

@@ -3,6 +3,7 @@
 module Cubical.Categories.Limits.AsRepresentable where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
 open import Cubical.Categories.Category renaming (isIso to isIsoC)
 open import Cubical.Categories.Constructions.BinProduct
 open import Cubical.Categories.Functor.Base
@@ -18,19 +19,56 @@ open import Cubical.Categories.Adjoint.UniversalElements
 
 open import Cubical.Categories.Instances.Functors.More
 open import Cubical.Categories.Profunctor.General
+open import Cubical.Tactics.FunctorSolver.Reflection
 
 private
   variable
-    ℓj ℓj' ℓc ℓc' : Level
+    ℓj ℓj' ℓc ℓc' ℓd ℓd' : Level
+
+ΔF : {C : Category ℓc ℓc'}{J : Category ℓj ℓj'}
+   → Functor C (FUNCTOR J C)
+ΔF = λFR Bif.Fst
+
+CONE : (C : Category ℓc ℓc')(J : Category ℓj ℓj')
+     → Profunctor (FUNCTOR J C) C (ℓ-max (ℓ-max ℓc' ℓj) ℓj')
+CONE C J = RightAdjointProf (ΔF {C = C} {J = J})
 
 limit : {C : Category ℓc ℓc'}{J : Category ℓj ℓj'}
         (D : Functor J C)
       → Type _
-limit {C = C}{J = J} = RightAdjointAt (λFR Bif.Fst)
+limit {C = C}{J = J} = RightAdjointAt ΔF
 
 limitsOfShape : (C : Category ℓc ℓc') (J : Category ℓj ℓj')
               → Type _
-limitsOfShape C J = RightAdjoint {C = C} {D = (FUNCTOR J C)} (λFR Bif.Fst)
+limitsOfShape C J = RightAdjoint {C = C} {D = (FUNCTOR J C)} ΔF
+
+-- Limit preservation
+module _ {C : Category ℓc ℓc'}{D : Category ℓd ℓd'}
+         (F : Functor C D)
+       where
+  -- the simplest one is to preserve a *particular* limit, meaning the
+  -- limit cone is mapped to a limiting cone.
+  module _ {J : Category ℓj ℓj'} where
+    open Functor
+    open NatTrans
+    open UniversalElement
+    pushCone : ∀ (cⱼ : Functor J C)
+      → PshHom F (CONE C J ⟅ cⱼ ⟆) (CONE D J ⟅ F ∘F cⱼ ⟆)
+    pushCone cⱼ .N-ob c' (lift α) .lower .N-ob = (F ∘ʳ α) .N-ob
+    pushCone cⱼ .N-ob c' (lift α) .lower .N-hom f =
+      cong₂ (seq' D) (sym (F .F-id)) refl
+      ∙ (F ∘ʳ α) .N-hom f
+    pushCone cⱼ .N-hom f = funExt (λ (lift α) →
+      cong lift (makeNatTransPath (funExt (λ j → F .F-seq _ _))))
+
+    preservesLimit : ∀ {cⱼ : Functor J C}
+      → (lim : UniversalElement C (CONE C J ⟅ cⱼ ⟆))
+      → Type _
+    preservesLimit {cⱼ} =
+      preservesRepresentation F (CONE C J ⟅ cⱼ ⟆) (CONE D J ⟅ F ∘F cⱼ ⟆)
+        (pushCone cⱼ)
+
+    -- todo: preservesLimitsOfShape, preservesLimits
 
 -- TODO: All functors preserve cones
 --       Functors with left adjoints preserve limiting cones