Library UniMath.Bicategories.ComprehensionCat.FinLimToCompCatLemmas

Some lemmas about the comprehension category arising from a category with finite limits
Every category with finite limits gives rise to a comprehension category. Specifically, let `C` be a category with finite limits. Then we have a comprehension category whose displayed category of types is given by the arrow category together with the codomain functor and whose comprehension is given by the identity functor.
There are various operations that we have within a comprehension category. These are:
  • Coercion. if we have a morphism `A <: B` over the identity, then every term of type `A` gives rise to a term of type `B`.
  • Substitution of terms. If we have a term `t : tm Δ A` and a substitution `s : Γ --> Δ`, then we also have a term `t [ s ]tm : tm Γ (A [ s ])`.
We also have various coherence isomorphisms. For instance, we have an isomorphism expressing that `A [ identity _ ]` is isomorphic to `A`, that `A [ s₂ ] [ s₁ ]` and `A [ s₁ · s₂ ]` are isomorphic, and that `A [ s₁ ]` and `A [ s₂ ]` are isomorphic whenever `s₁ = s₂`. We also have a functoriality operation saying that `A [ s ] <: B [ s ]` whenever `A <: B`.
In this file, we calculate each of these operations in case our comprehension category arises from a category with finite limits.
Contents 1. Operations on comprehension categories arising from categories with finite limits 2. Operations on functors between categories with finite limits 3. Operations on natural transformations
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.
Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Require Import UniMath.CategoryTheory.Limits.Equalizers.
Require Import UniMath.CategoryTheory.Limits.Pullbacks.
Require Import UniMath.CategoryTheory.Monics.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.DisplayedBicats.DispBicat.
Import DispBicat.Notations.
Require Import UniMath.Bicategories.Core.Examples.StructuredCategories.
Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat.
Require Import UniMath.Bicategories.ComprehensionCat.DFLCompCat.
Require Import UniMath.Bicategories.ComprehensionCat.CompCatNotations.
Require Import UniMath.Bicategories.ComprehensionCat.DFLCompCatNotations.
Require Import UniMath.Bicategories.ComprehensionCat.HPropMono.
Require Import UniMath.Bicategories.ComprehensionCat.Biequivalence.FinLimToDFLCompCat.

Local Open Scope cat.
Local Open Scope comp_cat.

1. Operations on comprehension categories arising from categories with finite limits

Section FinLimCompCatCalculation.
  Context {C : univ_cat_with_finlim}.

  Proposition finlim_to_comp_cat_coerce_eq
              {Γ : finlim_to_comp_cat C}
              {A B : ty Γ}
              (f : A <: B)
              (t : tm Γ A)
    : (t ↑ f : _ --> _)
      =
      t · dom_mor f.
  Show proof.
    apply idpath.

  Proposition finlim_to_comp_cat_eq_subst_ty_pullback_pr1
              {Γ Δ : finlim_to_comp_cat C}
              (A : ty Δ)
              {s₁ s₂ : Γ --> Δ}
              (p : s₁ = s₂)
    : dom_mor (eq_subst_ty A p) · PullbackPr1 _
      =
      PullbackPr1 _.
  Show proof.
    induction p.
    rewrite eq_subst_ty_idpath.
    simpl.
    apply id_left.

  Proposition finlim_to_comp_cat_eq_subst_ty_pullback_pr2
              {Γ Δ : finlim_to_comp_cat C}
              (A : ty Δ)
              {s₁ s₂ : Γ --> Δ}
              (p : s₁ = s₂)
    : dom_mor (eq_subst_ty A p) · PullbackPr2 _
      =
      PullbackPr2 _.
  Show proof.
    induction p.
    rewrite eq_subst_ty_idpath.
    simpl.
    apply id_left.

  Proposition finlim_to_comp_cat_comp_subst_ty_pullback_pr1
              {Γ₁ Γ₂ Γ₃ : finlim_to_comp_cat C}
              (A : ty Γ₃)
              {s₁ : Γ₁ --> Γ₂}
              (s₂ : Γ₂ --> Γ₃)
    : dom_mor (comp_subst_ty s₁ s₂ A) · PullbackPr1 _
      =
      PullbackPr1 _ · PullbackPr1 _.
  Show proof.
    etrans.
    {
      apply (PullbackArrow_PullbackPr1 (pullbacks_univ_cat_with_finlim _ _ _ _ _ _)).
    }
    apply transportb_cod_disp.

  Proposition finlim_to_comp_cat_comp_subst_ty_pullback_pr2
              {Γ₁ Γ₂ Γ₃ : finlim_to_comp_cat C}
              (A : ty Γ₃)
              {s₁ : Γ₁ --> Γ₂}
              (s₂ : Γ₂ --> Γ₃)
    : dom_mor (comp_subst_ty s₁ s₂ A) · PullbackPr2 _
      =
      PullbackPr2 _.
  Show proof.
    etrans.
    {
      apply (PullbackArrow_PullbackPr2 (pullbacks_univ_cat_with_finlim _ _ _ _ _ _)).
    }
    apply id_right.

  Proposition finlim_to_comp_cat_id_subst_ty_pullback_pr1
              {Γ : finlim_to_comp_cat C}
              (A : ty Γ)
    : dom_mor (id_subst_ty A) · PullbackPr1 _
      =
      identity _.
  Show proof.
    etrans.
    {
      apply (PullbackArrow_PullbackPr1 (pullbacks_univ_cat_with_finlim _ _ _ _ _ _)).
    }
    apply transportb_cod_disp.

  Proposition finlim_to_comp_cat_id_subst_ty_pullback_pr2
              {Γ : finlim_to_comp_cat C}
              (A : ty Γ)
    : dom_mor (id_subst_ty A) · PullbackPr2 _
      =
      cod_mor A.
  Show proof.
    etrans.
    {
      apply (PullbackArrow_PullbackPr2 (pullbacks_univ_cat_with_finlim _ _ _ _ _ _)).
    }
    apply id_right.

  Proposition finlim_to_comp_cat_coerce_subst_ty_pullback_pr1
              {Γ₁ Γ₂ : finlim_to_comp_cat C}
              {A B : ty Γ₂}
              (s : Γ₁ --> Γ₂)
              (f : A <: B)
    : dom_mor (coerce_subst_ty s f) · PullbackPr1 _
      =
      PullbackPr1 _ · dom_mor f.
  Show proof.
    etrans.
    {
      apply (PullbackArrow_PullbackPr1 (pullbacks_univ_cat_with_finlim _ _ _ _ _ _)).
    }
    apply transportf_cod_disp.

  Proposition finlim_to_comp_cat_coerce_subst_ty_pullback_pr2
              {Γ₁ Γ₂ : finlim_to_comp_cat C}
              {A B : ty Γ₂}
              (s : Γ₁ --> Γ₂)
              (f : A <: B)
    : dom_mor (coerce_subst_ty s f) · PullbackPr2 _
      =
      PullbackPr2 _.
  Show proof.
    etrans.
    {
      apply (PullbackArrow_PullbackPr2 (pullbacks_univ_cat_with_finlim _ _ _ _ _ _)).
    }
    apply id_right.

  Proposition finlim_to_comp_cat_subst_tm_pullback_pr1
              {Γ Δ : finlim_to_comp_cat C}
              (s : Γ --> Δ)
              {A : ty Δ}
              (t : tm Δ A)
    : t [[ s ]]tm · PullbackPr1 _
      =
      s · t.
  Show proof.
    apply (PullbackArrow_PullbackPr1 (comp_cat_pullback A s)).

  Proposition finlim_to_comp_cat_subst_ty_coe_pr1
              {Γ Δ Δ' : finlim_to_comp_cat C}
              (s : Γ --> Δ)
              {A : ty Δ}
              {B : ty Δ'}
              (f : z_iso Δ Δ')
              (ff : z_iso_disp f A B)
    : dom_mor (subst_ty_coe s f ff) · PullbackPr1 _
      =
      PullbackPr1 _ · pr11 ff.
  Show proof.
    etrans.
    {
      apply (PullbackArrow_PullbackPr1 (pullbacks_univ_cat_with_finlim _ _ _ _ _ _)).
    }
    apply transportf_cod_disp.

  Proposition finlim_to_comp_cat_subst_ty_coe_pr2
              {Γ Δ Δ' : finlim_to_comp_cat C}
              (s : Γ --> Δ)
              {A : ty Δ}
              {B : ty Δ'}
              (f : z_iso Δ Δ')
              (ff : z_iso_disp f A B)
    : dom_mor (subst_ty_coe s f ff) · PullbackPr2 _
      =
      PullbackPr2 _.
  Show proof.
    etrans.
    {
      apply (PullbackArrow_PullbackPr2 (pullbacks_univ_cat_with_finlim _ _ _ _ _ _)).
    }
    apply id_right.

  Proposition finlim_to_comp_cat_comp_mor
              {Γ : finlim_to_comp_cat C}
              {A B : ty Γ}
              (s : A -->[ identity _ ] B)
    : comp_cat_comp_mor s = dom_mor s.
  Show proof.
    apply idpath.

  Definition univ_cat_with_finlim_comprehension_functor
             {Γ Δ : C}
             {s : Γ --> Δ}
             {A : disp_codomain C Γ}
             {B : disp_codomain C Δ}
             (f : A -->[ s ] B)
    : comprehension_functor_mor (finlim_comprehension C) f
      =
      pr1 f.
  Show proof.
    apply idpath.

  Proposition finlim_comp_cat_comp_mor_over
              {Γ Δ : finlim_to_comp_cat C}
              (s : Γ --> Δ)
              {A : ty Γ}
              {B : ty Δ}
              (f : A <: B [[ s ]])
    : comp_cat_comp_mor_over s f
      =
      dom_mor f · PullbackPr1 _.
  Show proof.
    apply idpath.

  Proposition finlim_comp_cat_comp_mor_over_sub
              {Γ : finlim_to_comp_cat C}
              {A₁ A₂ : ty Γ}
              (f : A₁ <: A₂)
              {B₁ : ty (Γ & A₁)}
              {B₂ : ty (Γ & A₂)}
              (g : B₁ <: B₂ [[ comp_cat_comp_mor (C := finlim_to_comp_cat C) f ]])
    : comp_cat_comp_mor_over_sub f g
      =
      dom_mor g · PullbackPr1 _.
  Show proof.
    apply idpath.

  Proposition finlim_comp_cat_extend_over
              {Γ Δ : finlim_to_comp_cat C}
              (s : Γ --> Δ)
              (A : ty Δ)
    : comp_cat_extend_over A s = PullbackPr1 _.
  Show proof.
    apply idpath.

  Definition finlim_comp_cat_monic_to_hprop_ty
             {Γ A : finlim_to_dfl_comp_cat C}
             (m : Monic _ A Γ)
    : ty Γ
    := A ,, pr1 m.

  Definition finlim_comp_cat_monic_to_is_hprop_ty
             {Γ A : finlim_to_dfl_comp_cat C}
             (m : Monic _ A Γ)
    : is_hprop_ty (finlim_comp_cat_monic_to_hprop_ty m).
  Show proof.
    use mono_ty_to_hprop_ty.
    apply MonicisMonic.

  Proposition dfl_ext_identity_eq_arrow
              {Γ : finlim_to_dfl_comp_cat C}
              {A : ty Γ}
              (t₁ t₂ : tm Γ A)
    : π (dfl_ext_identity_type t₁ t₂)
      =
      dom_mor (EqualizerArrow (dfl_ext_identity t₁ t₂)).
  Show proof.
    cbn.
    apply id_right.
End FinLimCompCatCalculation.

2. Operations on functors between categories with finite limits

Section FinLimCompCatFunctorCalculation.
  Context {C₁ C₂ : univ_cat_with_finlim}
          (F : functor_finlim C₁ C₂).

  Proposition finlim_to_comp_cat_functor_subst_ty_coe_pr1
              {Γ₁ Γ₂ : finlim_to_comp_cat C₁}
              (s : Γ₁ --> Γ₂)
              (A : ty Γ₂)
    : dom_mor (comp_cat_functor_subst_ty_coe (finlim_to_comp_cat_functor F) s A)
      · PullbackPr1 _
      =
      #F (PullbackPr1 _).
  Show proof.
    etrans.
    {
      apply (PullbackArrow_PullbackPr1 (pullbacks_univ_cat_with_finlim _ _ _ _ _ _)).
    }
    apply transportf_cod_disp.

  Proposition finlim_to_comp_cat_functor_subst_ty_coe_pr2
              {Γ₁ Γ₂ : finlim_to_comp_cat C₁}
              (s : Γ₁ --> Γ₂)
              (A : ty Γ₂)
    : dom_mor (comp_cat_functor_subst_ty_coe (finlim_to_comp_cat_functor F) s A)
      · PullbackPr2 _
      =
      #F (PullbackPr2 _).
  Show proof.
    etrans.
    {
      apply (PullbackArrow_PullbackPr2 (pullbacks_univ_cat_with_finlim _ _ _ _ _ _)).
    }
    apply id_right.

  Proposition finlim_to_comp_cat_functor_coerce
              {Γ : finlim_to_comp_cat C₁}
              {A B : ty Γ}
              (f : A <: B)
    : dom_mor (comp_cat_functor_coerce (finlim_to_comp_cat_functor F) f)
      =
      #F (dom_mor f).
  Show proof.
    apply transportf_cod_disp.

  Proposition finlim_to_comprehension_nat_trans_mor
              {Γ : finlim_to_comp_cat C₁}
              (A : ty Γ)
    : comprehension_nat_trans_mor
        (comp_cat_functor_comprehension
           (finlim_to_comp_cat_functor F))
        A
      =
      identity _.
  Show proof.
    apply idpath.
End FinLimCompCatFunctorCalculation.

3. Operations on natural transformations

Section FinLimCompCatNatTransCalculation.
  Context {C₁ C₂ : univ_cat_with_finlim}
          {F G : functor_finlim C₁ C₂}
          (τ : nat_trans_finlim F G)
          {Γ : finlim_to_dfl_comp_cat C₁}
          (A : ty Γ).

  Proposition finlim_to_comp_cat_fib_nat_trans_pr1
    : dom_mor (comp_cat_type_fib_nat_trans (finlim_to_dfl_comp_cat_nat_trans τ) A)
      · PullbackPr1 _
      =
      τ (cod_dom A).
  Show proof.
    etrans.
    {
      apply (PullbackArrow_PullbackPr1 (pullbacks_univ_cat_with_finlim _ _ _ _ _ _)).
    }
    apply transportf_cod_disp.

  Proposition finlim_to_comp_cat_fib_nat_trans_pr2
    : dom_mor (comp_cat_type_fib_nat_trans (finlim_to_dfl_comp_cat_nat_trans τ) A)
      · PullbackPr2 _
      =
      #F (cod_mor A).
  Show proof.
    etrans.
    {
      apply (PullbackArrow_PullbackPr2 (pullbacks_univ_cat_with_finlim _ _ _ _ _ _)).
    }
    apply id_right.
End FinLimCompCatNatTransCalculation.