Library UniMath.CategoryTheory.DisplayedCats.Codomain

The slice displayed category

Definition of the slice displayed category
Proof that a morphism is cartesian if and only if it is a pullback

Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.PartA.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.limits.pullbacks.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.

Local Open Scope cat.

The displayed codomain

The total category associated to this displayed category is going to be isomorphic to the arrow category, but it won't be the same: the components of the objects and morphisms will be arranged differently

Section Codomain_Disp.

Context (C : category).

Definition cod_disp_ob_mor : disp_cat_ob_mor C.
Show proof.

  exists (λ x : C , ∑ y , y --> x).
  simpl; intros x y xx yy f.
    exact (∑ ff : pr1 xx --> pr1 yy, ff · pr2 yy = pr2 xx · f).

Definition cod_id_comp : disp_cat_id_comp _ cod_disp_ob_mor.
Show proof.

  split.
  - simpl; intros.
    exists (identity _ ).
    abstract (
        etrans; [apply id_left |];
        apply pathsinv0, id_right ).
  - simpl; intros x y z f g xx yy zz ff gg.
    exists (pr1 ff · pr1 gg).
    abstract (
        apply pathsinv0;
        etrans; [apply assoc |];
        etrans; [apply maponpaths_2, (! (pr2 ff)) |];
        etrans; [eapply pathsinv0, assoc |];
        etrans; [apply maponpaths, (! (pr2 gg))|];
        apply assoc).

Definition cod_disp_data : disp_cat_data _
:= (cod_disp_ob_mor ,, cod_id_comp).

Lemma cod_disp_axioms : disp_cat_axioms C cod_disp_data.
Show proof.

  repeat apply tpair; intros; try apply homset_property.
  - apply subtypePath.
    { intro. apply homset_property. }
    etrans. apply id_left.
    destruct ff as [ff H].
    apply pathsinv0.
    etrans. use (pr1_transportf (A := C ⟦x,y⟧)).
    cbn; apply (eqtohomot (transportf_const _ _)).
  - apply subtypePath.
    { intro. apply homset_property. }
    etrans. apply id_right.
    destruct ff as [ff H].
    apply pathsinv0.
    etrans. use (pr1_transportf (A := C ⟦x,y⟧)).
    cbn; apply (eqtohomot (transportf_const _ _)).
  - apply subtypePath.
    { intro. apply homset_property. }
    etrans. apply assoc.
    destruct ff as [ff H].
    apply pathsinv0.
    etrans. unfold mor_disp.
    use (pr1_transportf (A := C ⟦x,w⟧)).
    cbn; apply (eqtohomot (transportf_const _ _)).
  - apply (isofhleveltotal2 2).
    + apply homset_property.
    + intro. apply isasetaprop. apply homset_property.

Definition disp_codomain : disp_cat C
  := (cod_disp_data ,, cod_disp_axioms).

End Codomain_Disp.

Section Pullbacks_Cartesian.

Context {C:category}.

Definition isPullback_cartesian_in_cod_disp
    { Γ Γ' : C } {f : Γ' --> Γ}
    {p : disp_codomain _ Γ} {p' : disp_codomain _ Γ'} (ff : p' -->[f ] p)
  : (isPullback (pr2 ff)) -> is_cartesian ff.
Show proof.

  intros Hpb Δ g q hh.
  eapply iscontrweqf.
  2: {
    use Hpb.
    + exact (pr1 q).
    + exact (pr1 hh).
    + simpl in q. use (pr2 q · g).
    + etrans. apply (pr2 hh). apply assoc.
  }
  eapply weqcomp.
  2: apply weqtotal2asstol.
  apply weq_subtypes_iff.
  - intro. apply isapropdirprod; apply homset_property.
  - intro. apply (isofhleveltotal2 1).
    + apply homset_property.
    + intros. apply homsets_disp.
  - intros gg; split; intros H.
    + exists (pr2 H).
      apply subtypePath.
        intro; apply homset_property.
      exact (pr1 H).
    + split.
      * exact (maponpaths pr1 (pr2 H)).
      * exact (pr1 H).

Definition cartesian_isPullback_in_cod_disp
    { Γ Γ' : C } {f : Γ' --> Γ}
    {p : disp_codomain _ Γ} {p' : disp_codomain _ Γ'} (ff : p' -->[f ] p)
  : (isPullback (pr2 ff)) <- is_cartesian ff.
Show proof.

  intros cf c h k H.
  destruct p as [a x].
  destruct p' as [b y].
  destruct ff as [H1 H2].
  unfold is_cartesian in cf.
  simpl in *.
  eapply iscontrweqf.
  2: {
    use cf.
    + exact Γ'.
    + exact (identity _ ).
    + exists c. exact k.
    + cbn. exists h.
      etrans. apply H. apply maponpaths. apply (! id_left _ ).
  }
  eapply weqcomp.
  apply weqtotal2asstor.
  apply weq_subtypes_iff.

  - intro. apply (isofhleveltotal2 1).
    + apply homset_property.
    + intros.
      match goal with |[|- isofhlevel 1 (?x = _ )] =>
                       set (X := x) end.
      set (XR := @homsets_disp _ (disp_codomain C )).
      specialize (XR _ _ _ _ _ X).
      apply XR.
  - cbn. intro. apply isapropdirprod; apply homset_property.
  - intros gg; split; intros HRR.
    + split.
      * exact (maponpaths pr1 (pr2 HRR)).
      * etrans. apply (pr1 HRR). apply id_right.
    + use tpair.
      * rewrite id_right.
        exact (pr2 HRR).
      * apply subtypePath.
        intro; apply homset_property.
      exact (pr1 HRR).

Definition cartesian_iff_isPullback
    { Γ Γ' : C } {f : Γ' --> Γ}
    {p : disp_codomain _ Γ} {p' : disp_codomain _ Γ'} (ff : p' -->[f ] p)
  : (isPullback (pr2 ff)) <-> is_cartesian ff.
Show proof.

  split.
  - apply isPullback_cartesian_in_cod_disp.
  - apply cartesian_isPullback_in_cod_disp.

End Pullbacks_Cartesian.