Theorem dfl_full_comp_cat_mor_ind (C : dfl_full_comp_cat) (P : ∏ (Γ Δ : C), Γ --> Δ → UU) (Pπ : ∏ (Γ : C) (A : ty Γ), P _ _ (π A)) {Γ Δ : C} (s : Γ --> Δ) : P _ _ s. Proof. pose (A := comprehension_eso_ty C s). assert (s = comprehension_eso_inv_mor C s · π (comprehension_eso_ty C s)) as p. { rewrite <- comprehension_eso_mor_eq. rewrite !assoc. rewrite comprehension_eso_inv_mor_mor. rewrite id_left. apply idpath. } rewrite p. simple refine (dfl_full_comp_cat_mor_ind_iso C P Pπ _ _ (Pπ Δ A)). - refine (_ ,, _). apply is_z_iso_comprehension_eso_mor. - cbn. rewrite !assoc. refine (!_). etrans. { apply maponpaths_2. apply comprehension_eso_mor_inv_mor. } apply id_left. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Equivalences. Require Import UniMath.CategoryTheory.DisplayedCats.EquivalenceOverId. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseTerminal. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseEqualizers. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.FullyFaithfulDispFunctor. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat. Require Import UniMath.Bicategories.ComprehensionCat.CompCatNotations. Require Import UniMath.Bicategories.ComprehensionCat.DFLCompCat. Require Import UniMath.Bicategories.ComprehensionCat.DFLCompCatNotations.