module Cat.Displayed.TwoSided where
Two-sided fibrationsπ
One useful perspective on cartesian fibrations and cocartesian fibrations is that they are (co)presheaves of categories. This raises a natural question: what is the appropriate generalization of profunctors?
module _
{oa βa ob βb oe βe}
{A : Precategory oa βa} {B : Precategory ob βb}
(E : Displayed (A ΓαΆ B) oe βe)
where
private
module A = Cat.Reasoning A
module B = Cat.Reasoning B
open Cat.Displayed.Reasoning E
open Cat.Displayed.Morphism E
open Displayed E
A displayed category is a two-sided fibration when it satisfies the following 3 conditions:
We are given an operation assigning cartesian lifts to each and
Similarly, to each and we are equipped with a cocartesian lift
For every diagram of the form below with cocartesian and cartesian, is cartesian if and only if is cocartesian.
record Two-sided-fibration : Type (oa β βa β ob β βb β oe β βe) where
no-eta-equality
field
cart-lift: β {aβ aβ : A.Ob} {b : B.Ob}
β (u : A.Hom aβ aβ)
β (y' : Ob[ aβ , b ])
β Cartesian-lift E (u , B.id) y'
cocart-lift: β {a : A.Ob} {bβ bβ : B.Ob}
β (v : B.Hom bβ bβ)
β (x' : Ob[ a , bβ ])
β Cocartesian-lift E (A.id , v) x'
cart-beck-chevalley: β {aβ aβ : A.Ob} {bβ bβ : B.Ob}
β {u : A.Hom aβ aβ} {v : B.Hom bβ bβ}
β right-beck-chevalley E
(A.id , v) (u , B.id) (u , B.id) (A.id , v)
(sym A.id-comm ,β B.id-comm)
cocart-beck-chevalley: β {aβ aβ : A.Ob} {bβ bβ : B.Ob}
β {u : A.Hom aβ aβ} {v : B.Hom bβ bβ}
β left-beck-chevalley E
(A.id , v) (u , B.id) (u , B.id) (A.id , v)
(sym A.id-comm ,β B.id-comm)
This definition is rather opaque, so letβs break it down. The first two conditions ensure that we have 2 functorial actions on each of the fibre categories the first acts contravariantly in the second covariantly in These are analogs to the actions and of a profunctor The final condition serves to ensure that the base change and cobase change functors and preserve cocartesian and cartesian morphisms, resp.