Definition disp_morph : disp_cat_data (base_precategory_data C D). Proof. use tpair. - exists (λ F₀, ∏ (a b : C), C ⟦a, b⟧ → D ⟦F₀ a, F₀ b⟧). cbn. intros F₀ G₀ F₁ G₁ γ. exact (∏ (a b : C) (f : C ⟦a, b⟧), F₁ _ _ f · γ b = γ a · G₁ _ _ f). - repeat use tpair; cbn. + cbn; intros. etrans. apply id_right. apply pathsinv0. apply id_left. + cbn. intros ???????? S1 S2 a b f. etrans. apply assoc. etrans. apply cancel_postcomposition, S1. etrans. apply assoc'. etrans. apply cancel_precomposition, S2. apply assoc. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.