Functor Comprehension #1106

stschaef · 2024-02-25T16:08:45Z

Adding a module called Comprehension, and associated dependencies, that provides a method for constructing functors without providing the full functorial structure up front.

That is, say you wish to define a functor F : C → D via some universal property P. Instead of manually constructing the action on objects, morphisms, and proving functoriality, one can instead just give an action on objects and prove the functoriality of the property P.

This is a pretty big PR. I have tried to integrate most of our changes into the appropriate spots so far, and I'll be marking it as a draft until I address these

Continue renaming and integrating our changes. For instance, the modules that currently end in More
Considering moving Comprehension.agda back under the Profunctor directory.
Some dangling TODOs and naming concerns

stschaef · 2024-02-25T16:16:01Z

Originially we had comprehension under Profunctor rather than Functor, but after looking at the cubical directory structure, I'm thinking it might make more sense to put comprehension underneath Functor.

I'm torn on this though. After all we are constructing a functor, even if the implementation makes use of profunctors

stschaef · 2024-02-26T15:54:29Z

Cubical/Categories/Displayed/Base.agda

+module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where
+  open Category
+  open Categoryᴰ
+  weaken : Categoryᴰ C ℓD ℓD'


is this name too similar to weakenᴰ?

Could this not be factorized as "display over *", then weaken?

If by weaken you mean "reindex" then unfortunately no as that leads to too many transports that don't reduce

stschaef · 2024-02-26T15:57:27Z

Cubical/Categories/Displayed/DisplayOverProjections.agda

@@ -0,0 +1,131 @@
+{-# OPTIONS --safe #-}
+--
+module Cubical.Categories.Displayed.DisplayOverProjections where


I don't have any good ideas for naming this module.

I had this in Displayed.Base but it got too bloated. A rough first naming was DisplayOverProjections because we turn a display over C ×C D into a display over C or D, but I don't think this is a good module name.

Maybe more principled naming for the terms here, instead of things like mk∫ᴰsrFunctorᴰ

My (biased) opinion would be to sacrifice a bit of usability for generality instead, and define the "left adjoint" of reindexation along any functor (the dependent sum if you will), and apply this to the projection. The usual ∫Cᴰ is an example of this for the terminal functor as well.

I would understand if this is a bit too annoying to add for now, but this feels way too specific.

Good idea! We'll try it out

stschaef · 2024-02-26T15:59:44Z

Cubical/Categories/Displayed/Functor.agda

+           (F : Functor D C)
+           (Fᴰ : Functorᴰ F (Unitᴰ D) Cᴰ)
+           where
+    mk∫Functor : Functor D (∫C Cᴰ)


Similar to the above comment, maybe a more descriptive naming scheme should be used for all of these mk<X> constructions? I have no current ideas, but they should all be consistent

This is a specific case of the left adjointness of "existential quantification" in Cat, but specialized to Unitᴰ, so part of the UP for ∫. Somehow this seems ok because of that, although maybe the more general version could inherit that name as well.

We were discussing maybe to call all of these principles intro as they are the dual of elim.

stschaef · 2024-02-26T16:00:28Z

Cubical/Categories/Displayed/Preorder.agda

+        → Cᴰ.Hom[ f ][ xᴰ , yᴰ ]
+        → Qᴰ.Hom[ F .F-hom f ][ F-obᴰ xᴰ , F-obᴰ yᴰ ]) where
+
+    mkP→CᴰFunctorᴰ : Functorᴰ F Cᴰ (Preorderᴰ→Catᴰ Qᴰ)


This is the same principle as detailed in HLevel, one of them has to go.

stschaef · 2024-02-26T16:00:55Z

Cubical/Categories/Displayed/HLevels.agda

+    module Cᴰ = Categoryᴰ Cᴰ
+    module Dᴰ = Categoryᴰ Dᴰ
+
+  mkFunctorᴰPropHoms :


stschaef · 2024-02-26T16:01:04Z

Cubical/Categories/Displayed/HLevels.agda

+  mkFunctorᴰPropHoms propHoms F-obᴰ F-homᴰ .Functorᴰ.F-seqᴰ _ _ =
+    isProp→PathP (λ i → propHoms _ _ _) _ _
+
+  mkFunctorᴰContrHoms : (contrHoms : hasContrHoms Dᴰ)


stschaef · 2024-02-26T16:01:15Z

Cubical/Categories/Displayed/Functor.agda

+           (Gᴰ : Functorᴰ (∫F Fᴰ) (Unitᴰ (∫C Eᴰ)) Dᴰ)
+           where
+
+    mk∫ᴰFunctorᴰ : Functorᴰ F Eᴰ (∫Cᴰ Cᴰ Dᴰ)


stschaef · 2024-02-26T16:01:26Z

Cubical/Categories/Displayed/DisplayOverProjections.agda

+
+    open Functorᴰ
+
+    mk∫ᴰsrFunctorᴰ : Functorᴰ F Eᴰ ∫Cᴰsr


stschaef · 2024-02-26T16:01:41Z

Cubical/Categories/Displayed/DisplayOverProjections.agda

+
+  -- s for "simple" because D is not dependent on C
+  -- r for "right" because D is on the right of the product
+  ∫Cᴰsr : Categoryᴰ C (ℓ-max ℓD ℓCᴰ) (ℓ-max ℓD' ℓCᴰ')


stschaef · 2024-02-26T16:02:43Z

Cubical/Categories/Equivalence/Base.agda

@@ -24,6 +24,69 @@ record WeakInverse {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
    η : 𝟙⟨ C ⟩ ≅ᶜ invFunc ∘F func
    ε : func ∘F invFunc ≅ᶜ 𝟙⟨ D ⟩

+-- Composition of weak inverses is a weak inverse


unsure if here or Properties is better

Without looking at it: We usually do not split up things enough in the library, so most of the time the good idea is to have more files. So it might also sense to have something on 'composition' or 'weak equivalences'.

felixwellen · 2024-02-26T16:02:47Z

I have no opinion on the names so far.
If you can do that git-wise, it would be great if you split the PR up by topics - I think a couple of things are happening at once and that makes it harder to review.

stschaef · 2024-02-26T16:09:24Z

@felixwellen
Yeah sorry for the spam, that was moreso to not have to comb through them later.

For splitting up the PR, would you prefer something like rebased commits by topics all in a single PR or distinct PRs?

We have written a big web of mess building up to this comprehension construction, but I think these can be decoupled roughly into

displayed category additions
bifunctor additions
profunctor additions
the comprehension construction itself

felixwellen · 2024-02-26T19:55:39Z

If it is easy for you to split it into multiple PRs by topic, that would be great.

maxsnew · 2024-02-26T20:29:50Z

Cubical/Categories/Bifunctor/Base.agda

+open Functor
+open NatTrans
+
+record Bifunctor (C : Category ℓc ℓc')


This definition is subsumed by BifunctorSep in Bifunctor.Redundant. I don't think we need this file at all, and we should just include Bifunctor.Redundant as Bifunctor.Base.

jpoiret

Overall seems okay to me, but it's hard to see at what level of generality the new categorical additions should be done. I'm wondering though, isn't the ff.ness of Yoneda enough for all this?

jpoiret · 2024-02-28T10:48:46Z

Cubical/Categories/Bifunctor/Redundant.agda

+open NatTrans
+
+-- This definition is the most convenient to use
+-- But its axioms are redundant as well as its


Isn't this comment cut short?

jpoiret · 2024-02-28T10:51:54Z

Cubical/Categories/Bifunctor/Redundant.agda

+  2. and that they agree
+
+  The full definition includes some redundant *axioms* to make it
+  convenient to use, so we include two alternative formulations to


What exactly makes it more convenient than the usual definition? I'm not criticizing the choice of definition here but I'm curious wrt. what works better here.

The convenience here relates to better definitional equality.

The quick sell is that we would like to act functorially only on one side of C ×C D without additional identities tossed in the resulting term. If you had some F : Functor (C ×C D) E, in regular math F would reduce to a functorial action on f : C [ c , c' ] via F .F-hom (f , D .id), but this introduces a composition with an unnecessary identity. So we build these redundant axioms to give a native action that isn't over some D .⋆IdR/D .⋆IdL path.

I'm eliding a fair bit of detail here, but this definitional behavior is crucial for the comprehension construction.

Like we discussed, this PR will be split out into a few separate ones by topic and one of them will just be these bifunctor/binproduct definitions and some motivating examples.

I'm eliding a fair bit of detail here, but this definitional behavior is crucial for the comprehension construction.

Specifically, it's crucial for making certain compositional constructions spit out the "right" definitions. The main example where it came up for us was when we defined the exponential a -> - as a right adjoint to a x -, the universal property for exponentials involved an annoying id because we were fixing the product functor on one side. We'll be sure to include more info about this in comments when we make the non-draft PR

jpoiret · 2024-02-28T10:54:38Z

Cubical/Categories/Bifunctor/Redundant.agda

+-- 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.


Is there any reason you'd rather use this than Functor (C ×C D) E in this case?

jpoiret · 2024-02-28T11:00:42Z

Cubical/Categories/Constructions/BinProduct.agda

This move probably shouldn't be in this commit.

jpoiret · 2024-02-28T13:17:40Z

Cubical/Categories/Constructions/Elements.agda

+  (isUnivC : isUnivalent C) (F : Functor C (SET ℓS)) where
+  open Covariant {C = C}
+  open isUnivalent
+  isUnivalent∫ : isUnivalent (∫ F)


Should be in a separate commit/PR. Nice to see this proof, I remember wanting it but never got around to writing it down.

jpoiret · 2024-02-28T14:42:59Z

Cubical/Categories/Displayed/Preorder.agda

+  variable
+    ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' : Level
+
+record Preorderᴰ (C : Category ℓC ℓC') ℓCᴰ ℓCᴰ' :


I'm a bit torn on this, I think it would be more maintainable to simply use the hasPropHoms predicate instead of having another structure on which the same operations are defined (eg. reindex lower in this file).

I agree, sort of. You shouldn't be passing around Preorderᴰ structures, you should use Categoryᴰ with hasPropHoms, but if you want to define a Categoryᴰ that hasPropHoms, you define a Preorderᴰ and then use Preorderᴰ→Catᴰ. So think of this as analogous to FullSubcategory

with that in mind, I think Monotoneᴰ and reindex should be removed

jpoiret · 2024-02-28T14:45:37Z

Cubical/Categories/Displayed/Preorder.agda

+        → Cᴰ.Hom[ f ][ xᴰ , yᴰ ]
+        → Qᴰ.Hom[ F .F-hom f ][ F-obᴰ xᴰ , F-obᴰ yᴰ ]) where
+
+    mkP→CᴰFunctorᴰ : Functorᴰ F Cᴰ (Preorderᴰ→Catᴰ Qᴰ)


This is the same principle as detailed in HLevel, one of them has to go.

jpoiret · 2024-02-28T15:14:40Z

Cubical/Categories/Instances/Functors/More.agda

+
+    -- Preimage for the ESO proof
+    -- i.e. an object in (FUNCTOR Γ (FUNCTOR C D)) that maps to λF
+    curryF-ESO-object-preimage : (FUNCTOR Γ (FUNCTOR C D)) .ob →


Maybe naming it uncurryF-ob would be clearer?

jpoiret · 2024-02-28T15:17:12Z

Cubical/Categories/Instances/Functors/More.agda

+      D .id
+      ∎ )
+    -- Half of the isomorphism between (curryF-ESO-object-preimage λF) and λF
+    curryF-ESO-morphism-preimage : (λF : (FUNCTOR Γ (FUNCTOR C D)) .ob) →


uncurryF-curryF→id-ob or something like this?

jpoiret · 2024-02-28T15:34:55Z

Cubical/Categories/Profunctor/Relator.agda

+-- | whereas the category of presheaves as defined currently in the
+-- | library only gives the "separate" functorial action. In practice,
+-- | relators tend to only come with a separate action anyway (e.g.,
+-- | Hom) but in principle


Commentary is cut short.

stschaef marked this pull request as draft February 25, 2024 16:08

stschaef force-pushed the master branch 3 times, most recently from b1c1dbe to bdd1a05 Compare February 25, 2024 17:29

stschaef commented Feb 26, 2024

View reviewed changes

maxsnew reviewed Feb 26, 2024

View reviewed changes

jpoiret reviewed Feb 28, 2024

View reviewed changes

stschaef mentioned this pull request Mar 1, 2024

Displayed Category Constructions #1108

Merged

stschaef closed this May 21, 2024

stschaef force-pushed the master branch from f998210 to 2ae8464 Compare May 21, 2024 15:24


		open Functorᴰ

		mk∫ᴰsrFunctorᴰ : Functorᴰ F Eᴰ ∫Cᴰsr

Functor Comprehension #1106

Functor Comprehension #1106

Conversation

stschaef commented Feb 25, 2024

stschaef commented Feb 25, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

felixwellen commented Feb 26, 2024

stschaef commented Feb 26, 2024

felixwellen commented Feb 26, 2024

Choose a reason for hiding this comment

jpoiret left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment