Library UniMath.ModelCategories.Helpers

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Arrow.
Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Three.

Local Open Scope cat.

Lemma pr1_transportf_const {A : UU} {B : UU} {P : ∏ (a : A), B -> UU}
    {a a' : A} (e : a = a') (xs : ∑ b : B, P a b) :
    pr1 (transportf (λ x, ∑ b : B, P _ b) e xs) = pr1 xs.
Show proof.

Lemma section_disp_on_eq_morphisms {C : category}
    (F : section_disp (three_disp C))
    {f f' : arrow C} {γ γ': f --> f'}
    (H00 : arrow_mor00 γ = arrow_mor00 γ')
    (H11 : arrow_mor11 γ = arrow_mor11 γ') :
  pr1 (section_disp_on_morphisms F γ) =
    pr1 (section_disp_on_morphisms F γ').
Show proof.

Lemma section_disp_on_eq_morphisms' {C : category}
    (F : section_disp (three_disp C)) {f f' : arrow C} {γ : f --> f'}
    (H : arrow_mor00 γ · f' = f · arrow_mor11 γ) :
  let alternate := ((arrow_mor00 γ,, arrow_mor11 γ),, H) : f --> f' in
  pr1 (section_disp_on_morphisms F alternate) =
    pr1 (section_disp_on_morphisms F γ).
Show proof.

Lemma pr1_section_disp_on_morphisms_comp {C : category}
    (F : section_disp (three_disp C))
    {f f' f'' : arrow C}
    (γ : f --> f') (γ' : f' --> f'') :
  pr1 (section_disp_on_morphisms F γ) · pr1 (section_disp_on_morphisms F γ') =
      pr1 (section_disp_on_morphisms F (γ · γ')).
Show proof.

Lemma eq_section_disp_on_morphism {C : category}
    {F F' : section_disp (three_disp C)} :
  F = F' -> ∏ f, F f = F' f.
Show proof.

Lemma eq_section_nat_trans_disp_on_morphism {C : category}
    {F F' : section_disp (three_disp C)}
    {γ γ' : section_nat_trans_disp F F'} :
  γ = γ' -> ∏ f, γ f = γ' f.
Show proof.

Definition pathscomp1 {X : UU} {a b x y : X} (e1 : a = b) (e2 : a = x) (e3 : b = y) : x = y.
Show proof.

Lemma compeq {C : category} {x y z : C}
    {f f' : x --> y} {g g' : y --> z} :
  f = f' -> g = g' -> f · g = f' · g'.
Show proof.

Lemma funeq {A B : UU} {f g : A -> B}
    (H : f = g) :
  ∏ (a : A), f a = g a.
Show proof.