proposition: Proposition dfl_full_comp_cat_tm_to_mor_to_tm (t : comp_cat_tm Γ A) : dfl_full_comp_cat_mor_to_tm (dfl_full_comp_cat_tm_to_mor t) = t.
proof: Proof. use eq_comp_cat_tm ; cbn. etrans. { apply maponpaths. exact (maponpaths pr1 (FF_disp_functor_ff_inv (full_comp_cat_comprehension_fully_faithful C) _)). } cbn. rewrite !assoc. etrans. { apply maponpaths_2. apply z_iso_after_z_iso_inv. } apply id_left. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.FiberwiseTerminal UniMath.CategoryTheory.DisplayedCats.FiberwiseProducts UniMath.CategoryTheory.DisplayedCats.FiberwiseEqualizers UniMath.CategoryTheory.DisplayedCats.DependentSums UniMath.CategoryTheory.DisplayedCats.Codomain UniMath.CategoryTheory.DisplayedCats.FullyFaithfulDispFunctor UniMath.CategoryTheory.Monics UniMath.Bicategories.Core.Bicat UniMath.Bicategories.ComprehensionCat.BicatOfCompCat UniMath.Bicategories.ComprehensionCat.CompCatNotations UniMath.Bicategories.ComprehensionCat.DFLCompCat