# Displayed Category from a category with display maps

Definition of the displayed category of display maps over a category C
Given a category with display maps C, we define a displayed category over C. Objects over c:C are display maps into c.

# Definition of a cartesian displayed functor

Definition is_cartesian_disp_functor
{C C' : category} {F : functor C C'}
{D : disp_cat C} {D' : disp_cat C'} (FF : disp_functor F D D') : UU
:= (c c' : C) (f : c' --> c)
(d : D c) (d' : D c') (ff : d' -->[f] d),
is_cartesian ff is_cartesian (#FF ff).

Lemma isaprop_is_cartesian
{C : category} {D : disp_cat C}
{c c' : C} {f : c' --> c}
{d : D c} {d' : D c'} (ff : d' -->[f] d)
: isaprop (is_cartesian ff).
Proof.
repeat (apply impred_isaprop; intro).
apply isapropiscontr.
Qed.

Lemma is_cartesian_from_iso_to_cartesian
{C : category} {D : disp_cat C}
{c} {d : D c} {c' : C} {f : c' --> c}
{d0'} {ff : d0' -->[f] d} (ff_cart : is_cartesian ff)
{d1'} {ff' : d1' -->[f] d}
(i : iso_disp (identity_iso _) d0' d1')
(e : (i ;; ff')%mor_disp
= transportb _ (id_left _) ff)
: is_cartesian ff'.
Proof.
intros c'' g d'' h.
refine (iscontrweqf _ (ff_cart c'' g d'' h)).
use weq_subtypes'.
- eapply weqcomp.
+ (fun gg ⇒ (gg ;; i))%mor_disp.
apply iso_disp_postcomp.
+ (transportf _ (id_right _)).
apply isweqtransportf.
- intros ?; apply homsets_disp.
- intros ?; apply homsets_disp.
- simpl. intros gg.
assert ( X (x y z : X),
x = y (x = z y = z)) as H.
{ intros X x y z p; split.
+ intros q; exact (!p @ q).
+ intros q; exact (p @ q).
}
apply H.
apply pathsinv0.
etrans. apply mor_disp_transportf_postwhisker.
etrans. eapply transportf_bind.
apply assoc_disp_var.
etrans. eapply transportf_bind.
etrans. apply maponpaths, e.
apply mor_disp_transportf_prewhisker.
refine (_ @ idpath_transportf _ _).
apply maponpaths_2, homset_property.
Defined.

For a functor to be cartesian, it’s enough to show that it preserves some cartesian lift of each lifting problem.
Of course, this can only happen when the domain is a fibration; and in practice, it is useful exactly in the case where one has shown it is a fibration by exhibiting some particular construction of (mere existence of) cartesian lifts.
Lemma cartesian_functor_from_fibration
{C C' : category} {F : functor C C'}
{D : disp_cat C} {D' : disp_cat C'} {FF : disp_functor F D D'}
(H : (c c' : C) (f : c' --> c) (d : D c),
total2 (fun ff : cartesian_lift d fis_cartesian (#FF ff)) )
: is_cartesian_disp_functor FF.
Proof.
intros c c' f d d' ff ff_cart.
use (squash_to_prop (H _ _ f d)).
- apply isaprop_is_cartesian.
- intros [ff' ff'_cart].
use (is_cartesian_from_iso_to_cartesian ff'_cart).
+ refine (transportf (fun iiso_disp i _ _)
_
(@disp_functor_on_iso_disp
_ _ _ _ _ FF
_ _ _ _ (identity_iso _) _)).
apply (eq_iso _ _), functor_id.
refine (cartesian_lifts_iso ff' (_,,_)).
exact (_,,ff_cart).
+ etrans. {
apply maponpaths_2.
refine (@pr1_transportf _ _ (fun i ffis_iso_disp i ff) _ _ _ _). }
etrans. {
apply maponpaths_2.
apply functtransportf. }
etrans. {
apply mor_disp_transportf_postwhisker. }
etrans. {
eapply maponpaths. simpl.
etrans. {
eapply pathsinv0, disp_functor_comp_var. }
eapply transportf_bind.
etrans. {
apply maponpaths, cartesian_factorisation_commutes'. }
apply disp_functor_transportf. }
etrans. apply transport_f_f.
unfold transportb. apply maponpaths_2, homset_property.
Qed.

Lemma cartesian_functor_from_cleaving
{C C' : category} {F : functor C C'}
{D : disp_cat C} {D' : disp_cat C'} {FF : disp_functor F D D'}
(clD : cleaving D)
(H : c c' f d, is_cartesian (# FF (clD c c' f d)))
: is_cartesian_disp_functor FF.
Proof.
apply cartesian_functor_from_fibration.
intros c c' f d. apply hinhpr.
(clD c c' f d).
apply H.
Qed.

Definition comprehension_cat_structure (C : category) : UU
:= (D : disp_cat C) (H : cleaving D)
(F : disp_functor (functor_identity _ ) D (disp_codomain C)),
is_cartesian_disp_functor F.

Arguments comprehension_cat_structure _ : clear implicits.