Library UniMath.CategoryTheory.ComprehensionCats.CompCats

Comprehension Categories

This file builds on Displayedcats.Comprehensionc and follows a similar line as Bicategories.ComprehensionCat.CompCatNotations by considering the internal language of comprehension categories. The comprehension categories in Bicategories.ComprehensionCat.CompCatNotations are assumed to be full but we do not assume fullness here. We also do not assume splitness. Following the rules given in "From Semantics to Syntax: A Type Theory for Comprehension Categories" by Najmaei, Van der Weide, Ahrens, and North, we take morphisms between types in a fiber to be witnesses for coercions between types.

References

"From Semantics to Syntax: A Type Theory for Comprehension Categories" by Najmaei, Van der Weide, Ahrens, and North

Contents 1. Notations and Accesories for Comprehension Categories 2. Comprehension Structure and Substitution of Terms 3. Morphisms in Fibers as Coercions 4. Comprehension of Cartesian Lifts 5. Isomorphisms in Fibers 6. Lemmas for Coercing Terms 7. Comprehension Structure ctd. 8. Variable Rule 9. Extension of Substitution with Term

Notations and Accesories for Comprehension Categories

Definition comp_cat
  : UU
  := total2 comprehension_cat_structure.

Coercion comp_cat_to_ctx (C : comp_cat)
  : category
  := pr1 C.

Definition comp_cat_morphisms (C: comp_cat)
  : C -> C -> UU
  := pr211 (pr11 C ).

Definition disp_cat_of_types
  (C : comp_cat)
  : disp_cat C
  := pr12 C.

Definition comp_cat_ty {C : comp_cat}
  (Γ : pr1 C)
  : UU
  := (pr12 C ) Γ.

Definition comp_cat_coercion
  {C : comp_cat}
  {Γ : C}
  (A B : comp_cat_ty Γ)
  : UU
  := fiber_category _ _ ⟦ A , B ⟧.

Notation "A <: B" := (comp_cat_coercion A B) (at level 55).

Definition comp_cat_ext
  {C : comp_cat}
  (Γ : C)
  (A : comp_cat_ty Γ)
  : C
  := pr1 ((pr11 (comprehension (pr2 C))) Γ A).

Notation "Γ '&' A" := (comp_cat_ext Γ A) (at level 20) : comp_cat.

Definition comp_cat_proj
  {C : comp_cat}
  (Γ : C)
  (A : comp_cat_ty Γ)
  : Γ & A --> Γ
  := pr2 ((pr11 (comprehension (pr2 C))) Γ A).

Notation "'π'" := (comp_cat_proj _) : comp_cat.

Definition comp_cat_tm {C : comp_cat}
  {Γ : C} (A : comp_cat_ty Γ)
  : UU
  := ∑ (t : Γ --> Γ & A ), t · π A = identity Γ.

Coercion comp_cat_tm_to_section {C : comp_cat}
  {Γ : C} {A : comp_cat_ty Γ}
  (t : comp_cat_tm A)
  : Γ --> Γ & A
  := pr1 t.

Definition make_comp_cat_tm {C : comp_cat} {Γ : C}
  {A : comp_cat_ty Γ} (t : Γ --> Γ & A) (p : t · π A = identity Γ)
  : comp_cat_tm A
  := t ,, p.

Lemma comp_cat_tm_eq {C : comp_cat} {Γ : C} {A : comp_cat_ty Γ}
  (t1 t2 : comp_cat_tm A) (p : (pr1 t1 : _ ) = pr1 t2)
  : t1 = t2.
Proof.
  use subtypePath.
  intro. apply homset_property.
  exact p.
Qed.

Definition comp_cat_tm_isaset {C : comp_cat} {Γ : C} {A : comp_cat_ty Γ}
  : isaset (comp_cat_tm A).
Proof.
  apply isaset_total2.
  - apply homset_property.
  - intro t. apply isasetaprop. apply homset_property.
Qed.

Definition cleaving_of_types (C : comp_cat)
  : cleaving (disp_cat_of_types C)
  := pr122 C.

Definition comp_cat_subst_ty {C : comp_cat} {Γ Δ : C}
  (s : Γ --> Δ) (A : comp_cat_ty Δ)
  : comp_cat_ty Γ
  := cleaving_ob (cleaving_of_types C) s A.

Notation "A '[[' s ']]'" := (comp_cat_subst_ty s A) (at level 20) : comp_cat.

Comprehension Structure and Substitution of Terms

Morphisms in Fibers as Coercions

Definition coerce_comp_cat_tm {C : comp_cat} {Γ : C} {A B : comp_cat_ty Γ}
  (f : A <: B) (t : comp_cat_tm A) : comp_cat_tm B.
Proof.
  use make_comp_cat_tm.
  - exact (t · comp_cat_comp_mor f).
  - abstract (
        rewrite assoc';
        set (h := comprehension_functor_mor_comm (identity Γ) f);
        eapply pathscomp0;[apply cancel_precomposition, h|];
        rewrite assoc;
        eapply pathscomp0;[apply cancel_postcomposition, (pr2 t)|];
        apply id_right).
Defined.

Notation "t ↑ f" := (coerce_comp_cat_tm f t) (at level 29, left associativity).

Definition comp_cat_reindex_coercion {C : comp_cat} {Γ Δ : C} (s : Δ --> Γ) {A B : comp_cat_ty Γ} (f : A <: B)
  : A [[ s ]] <: B [[ s ]].
Proof.
  set (cl := cleaving_of_types C).
  set (liftA := cl _ _ s A).
  set (liftB := cl _ _ s B).
  set (ffA := mor_disp_of_cartesian_lift _ _ liftA).
  set (ffB := mor_disp_of_cartesian_lift _ _ liftB).
  set (HffB := cartesian_lift_is_cartesian _ _ liftB).
  set (hh := transportf (mor_disp (A [[ s ]]) B) (id_right s) (ffA ;; f)).
  set (hh_id := transportf (mor_disp (A [[ s ]]) B) (pathsinv0 (id_left s)) hh).
  exact (cartesian_factorisation HffB (identity Δ) hh_id).
Defined.

Definition comp_cat_reindex_iso
  {C : comp_cat}
  {Γ Δ : C} (s : Δ --> Γ)
  {A B : comp_cat_ty Γ}
  (i : @z_iso (fiber_category (disp_cat_of_types C) Γ) A B)
  : @z_iso (fiber_category (disp_cat_of_types C) Δ) (A [[ s ]]) (B [[ s ]])
  := (functor_on_z_iso
        (fiber_functor_from_cleaving _ _ s) i).

Comprehension of Cartesian Lifts

Definition comp_cat_ext_subst {C : comp_cat} :
  ∏ {Γ Δ : C} (s : Δ --> Γ) (A : comp_cat_ty Γ ), (Δ & (A [[ s ]])) --> (Γ & A ).
Proof.
  intros Γ Δ s A.
  exact (comprehension_functor_mor s
           (mor_disp_of_cartesian_lift _ _ (cleaving_of_types C _ _ s A))).
Defined.

Lemma comp_cat_ext_subst_commute {C : comp_cat}
  : ∏ {Γ Δ : C} (s : Δ --> Γ) (A : comp_cat_ty Γ ),
    comp_cat_ext_subst s A · (π _) = (π _) · s.
Proof.
  intros Γ Δ s A.
  exact (comprehension_functor_mor_comm s
           (mor_disp_of_cartesian_lift _ _ (cleaving_of_types C _ _ s A))).
Qed.

Lemma comp_cat_ext_subst_term_commute {C : comp_cat} {Γ Δ : C}
  (s : Γ --> Δ) (A : comp_cat_ty Δ) (t : comp_cat_tm A)
  : (t [[ s ]]tm ) · comp_cat_ext_subst s A = s · t.
Proof.
  exact (PullbackArrow_PullbackPr1 (comp_cat_pullback A s) Γ (s · t) (identity Γ) _).
Qed.

Isomorphisms in Fibers

Lemmas for coercing terms

Lemma coerce_tm_after_inv
  {C : comp_cat} {Γ : C} {A B : comp_cat_ty Γ}
  (i : z_iso (C := fiber_category _ _) A B)
  (t : comp_cat_tm B)
  : (t ↑ ⌈ i ⌉⁻¹ ) ↑ ⌈ i ⌉ = t.
Proof.
  apply comp_cat_tm_eq.
  cbn.
  rewrite <- assoc.
  rewrite comp_cat_comp_mor_z_iso_after_z_iso_inv.
  rewrite id_right.
  apply idpath.
Qed.

Lemma coerce_tm_inv_after
  {C : comp_cat} {Γ : C} {A B : comp_cat_ty Γ}
  (i : z_iso (C := fiber_category _ _) A B)
  (t : comp_cat_tm A)
  : (t ↑ ⌈ i ⌉) ↑ ⌈ i ⌉⁻¹ = t.
Proof.
  apply comp_cat_tm_eq.
  cbn.
  rewrite <- assoc.
  rewrite comp_cat_comp_mor_z_iso_inv_after_z_iso.
  rewrite id_right.
  apply idpath.
Qed.

Definition comp_cat_subst_tm_id {C : comp_cat} {Γ : C} {A : comp_cat_ty Γ} (t : comp_cat_tm A) :
  t [[ identity _ ]]tm = t ↑ ⌈comp_cat_subst_ty_id_iso _⌉.
Proof.
  use comp_cat_tm_eq ; cbn.
  refine (!_).
  use (PullbackArrowUnique _ (isPullback_Pullback (comp_cat_pullback _ _))).
  - cbn.
    rewrite !assoc'.
    rewrite id_left.
    refine (_ @ id_right _).
    apply maponpaths.
    unfold comp_cat_comp_mor.
    etrans.
    {
      refine (!_).
      apply (comprehension_functor_mor_comp).
    }
    rewrite cartesian_factorisation_commutes.
    refine (_ @ comprehension_functor_mor_id ).
    unfold comprehension_functor_mor, transportb.
    rewrite disp_functor_transportf, transportf_cod_disp.
    apply idpath.
  - cbn.
    rewrite !assoc'.
    etrans.
    {
      apply cancel_precomposition.
      set (f := cartesian_factorisation (cleaving_of_types C Γ Γ (identity Γ) A) (identity Γ)
                  (transportb (λ z : C ⟦ Γ, Γ ⟧, A -->[ z ] A)
                     (fiber_functor_from_cleaving_identity_data_subproof Γ)
                     (id_disp A))).
      exact (comp_cat_comp_mor_law f).
    }
    exact (pr2 t).
Qed.

Definition comp_cat_subst_tm_comp {C : comp_cat} {Γ Δ Θ : C} {A : comp_cat_ty Γ}
  (f : Δ --> Γ) (g : Θ --> Δ) (t : comp_cat_tm A)
  : t [[ g · f ]]tm = ((t [[ f ]]tm ) [[ g ]]tm ) ↑ ⌈ comp_cat_subst_ty_comp_iso A f g ⌉.
Proof.
  use comp_cat_tm_eq ; cbn.
  refine (!_).
  use (PullbackArrowUnique _ (isPullback_Pullback (comp_cat_pullback A _))).
  - cbn.
    unfold comp_cat_comp_mor.
    rewrite <- assoc.
    etrans.
    {
      apply maponpaths.
      refine (!_).
      apply comprehension_functor_mor_comp.
    }
    rewrite cartesian_factorisation_commutes.
    unfold comprehension_functor_mor, transportb.
    rewrite disp_functor_transportf, transportf_cod_disp.
    etrans.
    {
      apply maponpaths.
      apply comprehension_functor_mor_comp.
    }
    rewrite !assoc.
    etrans.
    {
      apply maponpaths_2.
      apply (PullbackArrow_PullbackPr1 (comp_cat_pullback _ _)).
    }
    do 2 rewrite <- assoc.
    apply cancel_precomposition.
    apply (PullbackArrow_PullbackPr1 (comp_cat_pullback _ _ )).
  - cbn.
    rewrite <- assoc.
    etrans.
    {
      apply maponpaths.
      apply comp_cat_comp_mor_law.
    }
    apply (PullbackArrow_PullbackPr2 (comp_cat_pullback _ _)).
Qed.

Definition comp_cat_subst_tm_comp' {C : comp_cat} {Γ Δ Θ : C} {A : comp_cat_ty Γ}
  (f : Δ --> Γ) (g : Θ --> Δ) (t : comp_cat_tm A)
  : t [[ g · f ]]tm ↑ ⌈ comp_cat_subst_ty_comp_iso A f g ⌉⁻¹ = ((t [[ f ]]tm ) [[ g ]]tm ) .
Proof.
  rewrite comp_cat_subst_tm_comp.
  apply coerce_tm_inv_after.
Qed.

Proposition comp_cat_comp_coerce_tm {C : comp_cat} {Γ : C} {A₁ A₂ A₃ : comp_cat_ty Γ}
  (f : A₁ <: A₂) (g : A₂ <: A₃) (t : comp_cat_tm A₁)
  : t ↑ f ↑ g = t ↑ (f · g ).
Proof.
  use comp_cat_tm_eq ; cbn.
  rewrite assoc'.
  apply maponpaths.
  refine (!_).
  apply comp_cat_comp_mor_comp.
Qed.

Proposition comp_cat_id_coerce_tm {C : comp_cat} {Γ : C} {A : comp_cat_ty Γ} (t : comp_cat_tm A)
  : t ↑ id_disp _ = t.
Proof.
  use comp_cat_tm_eq ; cbn.
  change (t · comp_cat_comp_mor (@identity (fiber_category (disp_cat_of_types C) Γ) A) = pr1 t).
  rewrite comp_cat_comp_mor_id.
  apply id_right.
Qed.

Proposition comp_cat_coerce_eq {C : comp_cat} {Γ : C} {A B : comp_cat_ty Γ}
  {t : comp_cat_tm A} { f f' : A <: B}
  (p : f = f')
  : t ↑ f = t ↑ f'.
Proof.
  use comp_cat_tm_eq.
  apply cancel_precomposition.
  apply maponpaths.
  exact p.
Qed.

Proposition comp_cat_subst_coerce_tm
  {C : comp_cat}
  {Γ₁ Γ₂ : C}
  {A₁ A₂ : comp_cat_ty Γ₂}
  (s : Γ₁ --> Γ₂)
  (f : A₁ <: A₂)
  (t : comp_cat_tm A₁)
  : (t ↑ f ) [[ s ]]tm
    =
      t [[ s ]]tm ↑ comp_cat_reindex_coercion s f.
Proof.
  use comp_cat_tm_eq.
  refine (!_).
  use (PullbackArrowUnique _ (isPullback_Pullback (comp_cat_pullback A₂ s))).
  - unfold comp_cat_comp_mor.
    cbn.
    rewrite <- assoc.
    etrans.
    {
      apply maponpaths.
      refine (!_).
      apply comprehension_functor_mor_comp.
    }
    etrans.
    {
      do 2 apply maponpaths.
      apply cartesian_factorisation_commutes.
    }
    rewrite comprehension_functor_mor_transportf.
    etrans.
    {
      apply maponpaths.
      rewrite comprehension_functor_mor_transportf.
      apply comprehension_functor_mor_comp.
    }
    rewrite !assoc.
    apply maponpaths_2.
    apply (PullbackArrow_PullbackPr1 (comp_cat_pullback A₁ s)).
  - cbn.
    rewrite <- assoc.
    etrans.
    {
      apply maponpaths.
      apply comp_cat_comp_mor_law.
    }
    apply (PullbackArrow_PullbackPr2 (comp_cat_pullback A₁ s)).
Qed.

Proposition comp_cat_id_right_subst_ty
  {C : comp_cat}
  {Γ₁ Γ₂ : C}
  (s : Γ₁ --> Γ₂)
  (A : comp_cat_ty Γ₂)
  : comp_cat_reindex_coercion (s) (⌈ comp_cat_subst_ty_id_iso A ⌉)
      · ⌈ comp_cat_subst_ty_comp_iso A (identity _) s ⌉
      · ⌈ comp_cat_subst_ty_iso A (id_right s) ⌉
    =
      identity _.
Proof.
  refine (_ @ !(disp_cat_cleaving_id_left (cleaving_of_types C) s A)).
  do 2 apply maponpaths_2.
  unfold comp_cat_reindex_coercion.
  simpl.
  rewrite transport_f_f.
  apply idpath.
Qed.

Proposition comp_cat_id_left_subst_ty
  {C : comp_cat}
  {Γ₁ Γ₂ : C}
  (s : Γ₁ --> Γ₂)
  (A : comp_cat_ty Γ₂)
  : ⌈ comp_cat_subst_ty_id_iso (A [[ s ]]) ⌉
      · ⌈ comp_cat_subst_ty_comp_iso A s (identity _) ⌉
      · ⌈ comp_cat_subst_ty_iso A (id_left s) ⌉
    =
      identity _.
Proof.
  apply (!(disp_cat_cleaving_id_right (cleaving_of_types C) s A)).
Qed.

Proposition comp_cat_assoc'_subst_ty
  {C : comp_cat}
  {Γ₁ Γ₂ Γ₃ Γ₄ : C}
  (s₁ : Γ₁ --> Γ₂)
  (s₂ : Γ₂ --> Γ₃)
  (s₃ : Γ₃ --> Γ₄)
  (A : comp_cat_ty Γ₄)
  : comp_cat_subst_ty_comp_iso (A [[ s₃ ]]) s₂ s₁
      · comp_cat_subst_ty_comp_iso A s₃ (s₁ · s₂)
      · (⌈ comp_cat_subst_ty_iso (A) ( assoc' s₁ s₂ s₃) ⌉)
    = comp_cat_reindex_coercion s₁
        (⌈ comp_cat_subst_ty_comp_iso A s₃ s₂ ⌉)
        · ⌈ comp_cat_subst_ty_comp_iso A (s₂ · s₃) s₁ ⌉.
Proof.
  refine (!_).
  unfold comp_cat_reindex_coercion.
  refine (_ @ !disp_cat_cleaving_assoc (cleaving_of_types C) _ _ _ _).
  - rewrite transport_f_f.
    apply idpath.
Qed.

Proposition comp_cat_assoc_subst_ty
  {C : comp_cat}
  {Γ₁ Γ₂ Γ₃ Γ₄ : C}
  (s₁ : Γ₁ --> Γ₂)
  (s₂ : Γ₂ --> Γ₃)
  (s₃ : Γ₃ --> Γ₄)
  (A : comp_cat_ty Γ₄)
  :
  ⌈ comp_cat_subst_ty_comp_iso (C:=C) (A [[ s₃ ]]) s₂ s₁ ⌉
    · ⌈ comp_cat_subst_ty_comp_iso (C:=C) A s₃ (s₁ · s₂) ⌉
  =
    comp_cat_reindex_coercion s₁
      (⌈ comp_cat_subst_ty_comp_iso A s₃ s₂ ⌉)
      · ⌈ comp_cat_subst_ty_comp_iso A (s₂ · s₃) s₁ ⌉
      · ⌈ comp_cat_subst_ty_iso A (assoc s₁ s₂ s₃) ⌉.
Proof.
  rewrite <- comp_cat_assoc'_subst_ty.
  refine (!(id_right _) @ _ @ assoc _ _ _).
  apply maponpaths.
  assert (assoc' s₁ s₂ s₃ @ assoc s₁ s₂ s₃ = idpath _) as p.
  { apply homset_property. }
  set (F := fiber_category (disp_cat_of_types C) Γ₁).
  change (identity _ = ⌈ idtoiso (C:=F)
                          (comp_cat_subst_ty_eq A (assoc' s₁ s₂ s₃)) ⌉
                          · ⌈ idtoiso (C:=F) (comp_cat_subst_ty_eq A (assoc s₁ s₂ s₃)) ⌉).
  etrans.
  2: { apply pr1_idtoiso_concat. }
  Check comp_cat_subst_ty_eq.
  etrans.
  2: {
    do 2 apply maponpaths.
    unfold comp_cat_subst_ty_eq.
    rewrite <- (maponpathscomp0 (λ t : C ⟦ Γ₁, Γ₄ ⟧, A [[t ]])).
    rewrite p.
    apply idpath.
  }
  apply idpath.
Qed.

Definition comp_cat_subst_tm_eq {C : comp_cat} {Γ Δ : C} {A : comp_cat_ty Δ}
  (t : comp_cat_tm A) { s s' : Γ --> Δ } (p : s = s')
  : t [[ s ]]tm ↑ (⌈ (comp_cat_subst_ty_iso _ p ) ⌉) = t [[ s' ]]tm.
Proof.
  induction p.
  apply comp_cat_id_coerce_tm.
Qed.

Definition comp_cat_ext_subst_eq
  {C : comp_cat}
  {Γ Δ : C}
  { s s' : Γ --> Δ}
  (A : comp_cat_ty Δ)
  (p : s = s')
  : comp_cat_ext_subst s A = comp_cat_comp_mor ( ⌈ comp_cat_subst_ty_iso _ p ⌉) · comp_cat_ext_subst s' A.
Proof.
  induction p.
  change (comp_cat_subst_ty_iso A (idpath s)) with
    (idtoiso (C := fiber_category _ _) (idpath (A [[s]]))).
  cbn.
  etrans.
  2 :{
    refine (!_).
    apply maponpaths_2.
    apply comp_cat_comp_mor_id.
  }
  exact (!id_left _).
Qed.

Comprehension Structure ctd.

Pullbacks composed with isos

Definition comp_cat_pullback_compose_iso
  {C : comp_cat} {Γ₁ Γ₂ : C}
  {A : comp_cat_ty Γ₁} (s : Γ₂ --> Γ₁)
  {P' : C}
  (i : z_iso P' (PullbackObject (comp_cat_pullback A s)))
  : Pullback (π A) s.
Proof.
  set (PB := comp_cat_pullback A s).
  use make_Pullback.
  -
    exact P'.
  -
    exact (i · PullbackPr1 PB).
  -
    exact (i · PullbackPr2 PB).
  -
    abstract (
        repeat rewrite <- assoc;
        apply (cancel_precomposition);
        exact (PullbackSqrCommutes PB)
      ).
  -
    refine (isPullback_z_iso (PullbackSqrCommutes PB) (_) (isPullback_Pullback PB) (z_iso_inv i) _ _).
    + abstract (
          cbn;
          rewrite !assoc;
          rewrite z_iso_after_z_iso_inv;
          rewrite id_left;
          apply idpath
        ).
    + abstract (
          cbn ;
          rewrite !assoc ;
          rewrite z_iso_after_z_iso_inv ;
          rewrite id_left ;
          apply idpath
        ).
Defined.

Definition comp_cat_univ_pullback_compose_iso
  {C : comp_cat} {Γ Δ Ω : C}
  {A : comp_cat_ty Δ}
  {s : Γ --> Δ}
  {A' : comp_cat_ty Γ}
  (i : @z_iso (fiber_category _ _) A' (A [[ s ]]))
  {s' : Γ --> Ω} {s'' : Ω --> Δ & A}
  (p : s' · s'' · (π A ) = s)
  : comp_cat_tm A'.
Proof.
  set (PB' := comp_cat_pullback_compose_iso s (comp_cat_comp_iso i)).
  set (PB := comp_cat_pullback A s).

  use make_comp_cat_tm.
  -
    refine (PullbackArrow PB' _ (s' · s'') (identity Γ) _).
    rewrite id_left.
    exact p.
  - abstract (
        cbn;
        set (pr2 := PullbackPr2 PB');
        assert (p' : π A' = PullbackPr2 PB')
          by (unfold PB; cbn;
              change (π A' = comp_cat_comp_mor (⌈ i ⌉) · π (A [[ s ]] ));
              rewrite comp_cat_comp_mor_law;
              apply idpath);
        rewrite p';
        apply (PullbackArrow_PullbackPr2 PB')).
Defined.

Variable Rule

Definition comp_cat_var
  {C : comp_cat}
  {Γ : C}
  (A : comp_cat_ty Γ)
  : comp_cat_tm (A [[ π A ]]).
Proof.
  use make_comp_cat_tm.
  - use (PullbackArrow (comp_cat_pullback _ _)).
    + apply identity.
    + apply identity.
    + abstract
        (rewrite !id_left ;
         apply idpath).
  - abstract
      (apply (PullbackArrow_PullbackPr2 (comp_cat_pullback _ _))).
Defined.

Definition comp_cat_var_subst_coerce
  {C : comp_cat}
  {Γ Δ : C}
  {A : comp_cat_ty Γ}
  (s : Δ --> Γ)
  (t : comp_cat_tm (A [[ s ]]))
  : A [[s ]] <: (A [[ π A ]]) [[ t · comp_cat_ext_subst s _ ]].
Proof.
  refine (⌈comp_cat_subst_ty_iso _ _⌉· ⌈comp_cat_subst_ty_comp_iso _ _ _⌉⁻¹).
  rewrite assoc'.
  rewrite comp_cat_ext_subst_commute.
  rewrite assoc.
  etrans.
  2: {
    refine (!_).
    apply maponpaths_2.
    apply (pr2 t).
  }
  refine (!_).
  apply id_left.
Defined.

Lemma cleaving_of_types_eq
  {C : comp_cat} {Γ Δ : C} {s s' : Δ --> Γ} (p : s = s') (A : comp_cat_ty Γ)
  : (pr1 (idtoiso (C := fiber_category _ _)
            (maponpaths (λ z , pr1 (cleaving_of_types _ _ _ z _)) p))
     ;; cleaving_of_types C Γ Δ s' A
     = transportf (λ z , _ -->[ z ] _) (p @ !(id_left _))
         (cleaving_of_types C Γ Δ s A))%mor_disp.
Proof.
  induction p ; cbn.
  rewrite id_left_disp.
  apply idpath.
Qed.

Proposition comp_cat_var_subst
  {C : comp_cat}
  {Γ Δ : C}
  {A : comp_cat_ty Γ}
  (s : Δ --> Γ)
  (t : comp_cat_tm (A [[ s ]]))
  : comp_cat_var A [[ t · comp_cat_ext_subst s _ ]]tm
    =
      t ↑ comp_cat_var_subst_coerce s t.
Proof.
  use comp_cat_tm_eq.
  refine (!_).
  use (PullbackArrowUnique _ (isPullback_Pullback (comp_cat_pullback _ _))).
  - use (MorphismsIntoPullbackEqual (isPullback_Pullback (comp_cat_pullback A (π A)))).
    + rewrite !assoc'.
      refine (!_).
      etrans.
      { do 2 apply maponpaths.
        apply (PullbackArrow_PullbackPr1 (comp_cat_pullback A (π A))). }
      rewrite id_right.
      refine (!_).
      etrans.
      { apply maponpaths. refine (!_). apply comprehension_functor_mor_comp. }
      rewrite comprehension_functor_mor_comp.
      unfold "↑".
      cbn -[comp_cat_var_subst_coerce].
      rewrite assoc'.
      apply maponpaths.
      etrans.
      {apply maponpaths.
       refine (!_).
       apply comprehension_functor_mor_comp.
      }
      unfold comp_cat_comp_mor.
      etrans.
      { refine (!_).
        apply comprehension_functor_mor_comp.
      }
      etrans.
      { apply maponpaths.
        rewrite assoc_disp.
        apply maponpaths.
        cbn.
        unfold fiber_functor_from_cleaving_comp_inv.
        rewrite !mor_disp_transportf_postwhisker.
        apply maponpaths.
        etrans.
        { apply maponpaths_2.
          rewrite assoc_disp_var.
          rewrite cartesian_factorisation_commutes.
          apply idpath. }
        rewrite mor_disp_transportf_postwhisker.
        apply maponpaths.
        rewrite assoc_disp_var.
        apply maponpaths.
        rewrite cartesian_factorisation_commutes.
        rewrite mor_disp_transportf_prewhisker.
        apply idpath. }
      unfold transportb.
      rewrite !comprehension_functor_mor_transportf.
      etrans.
      { apply maponpaths.
        apply cleaving_of_types_eq. }
      rewrite (comprehension_functor_mor_transportf (C:=C)).
      apply idpath.
    + rewrite !assoc'.
      etrans.
      { apply maponpaths. apply comprehension_functor_mor_comm. }
      etrans.
      { unfold "↑". cbn -[comp_cat_var_subst_coerce]. rewrite assoc'.
        apply maponpaths. rewrite !assoc. do 2 apply maponpaths_2.
        apply comp_cat_comp_mor_law. }
      rewrite !assoc.
      etrans.
      { do 2 apply maponpaths_2. apply (pr2 t). }
      rewrite id_left.
      refine (!_).
      etrans.
      { rewrite !assoc'. do 2 apply maponpaths.
        apply (PullbackArrow_PullbackPr2 (comp_cat_pullback A (π A))). }
      apply maponpaths.
      apply id_right.
  - unfold "↑". cbn -[comp_cat_var_subst_coerce].
    rewrite !assoc'.
    etrans.
    { apply maponpaths. apply comp_cat_comp_mor_law. }
    apply (pr2 t).
Qed.

Extension of Substitution with Term