Revert "biequiv for universe types"

This reverts commit c3ba9a6.

Author: nmvdw

UniMath/Bicategories/.package/files

@@ -184,7 +184,6 @@ DisplayedBicats/DispTransformation.v
 DisplayedBicats/DispModification.v
 DisplayedBicats/DispBiequivalence.v
 DisplayedBicats/ProductDispBiequiv.v
-DisplayedBicats/DispPseudoNaturalAdjequiv.v
 
 DoubleCategories/Basics/DoubleCategoryBasics.v
 DoubleCategories/Basics/StrictDoubleCatBasics.v
@@ -457,7 +456,6 @@ ComprehensionCat/DFLCompCatNotations.v
 ComprehensionCat/ComprehensionEso.v
 ComprehensionCat/Biequivalence/DFLCompCatToFinLim.v
 ComprehensionCat/Biequivalence/FinLimToDFLCompCat.v
-ComprehensionCat/FinLimToCompCatLemmas.v
 ComprehensionCat/Biequivalence/Unit.v
 ComprehensionCat/Biequivalence/Counit.v
 ComprehensionCat/Biequivalence/Biequiv.v
@@ -479,20 +477,6 @@ ComprehensionCat/Universes/CompCatUniv/CompCatOb.v
 ComprehensionCat/Universes/CompCatUniv/UniverseType.v
 ComprehensionCat/Universes/CompCatUniv/CompCatWithUniv.v
 
-ComprehensionCat/Universes/CompCatUnivProps.v
-
-ComprehensionCat/Universes/Biequiv/ToCompCatUniv.v
-ComprehensionCat/Universes/Biequiv/ToCatFinLimUnivActions.v
-ComprehensionCat/Universes/Biequiv/ToCatFinLimUnivCell.v
-ComprehensionCat/Universes/Biequiv/ToCatFinLimUnivIdent.v
-ComprehensionCat/Universes/Biequiv/ToCatFinLimUnivComp.v
-ComprehensionCat/Universes/Biequiv/ToCatFinLimUniv.v
-ComprehensionCat/Universes/Biequiv/UnitForUniv.v
-ComprehensionCat/Universes/Biequiv/CounitForUnivMor.v
-ComprehensionCat/Universes/Biequiv/CounitForUnivNat.v
-ComprehensionCat/Universes/Biequiv/CounitForUniv.v
-ComprehensionCat/Universes/UniverseBiequiv.v
-
 ComprehensionCat/Biequivalence/InternalLanguageTopos.v
 
 ComprehensionCat/SetGroupoidModel.v

UniMath/Bicategories/ComprehensionCat/CompCatNotations.v

@@ -40,7 +40,6 @@ Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
 Require Import UniMath.CategoryTheory.DisplayedCats.Total.
 Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.
-Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod.
 Require Import UniMath.CategoryTheory.Limits.Terminal.
 Require Import UniMath.CategoryTheory.Limits.Preservation.
 Require Import UniMath.CategoryTheory.Limits.Pullbacks.
@@ -153,33 +152,6 @@ Definition comp_cat_comp_fiber_z_iso
   : z_iso (Γ & A) (Γ & B)
   := comp_cat_comp_z_iso (z_iso_disp_from_z_iso_fiber _ _ _ _ s).
 
-Definition comp_cat_comp_fiber_z_iso_fib
-           {C : comp_cat}
-           {Γ : C}
-           {A B : ty Γ}
-           (s : z_iso (C := fiber_category _ _) A B)
-  : z_iso
-      (C := fiber_category _ _)
-      (comp_cat_comprehension C Γ A)
-      (comp_cat_comprehension C Γ B).
-Proof.
-  exact (functor_on_z_iso
-           (fiber_functor (comp_cat_comprehension C) Γ)
-           s).
-Defined.
-
-Proposition dom_mor_comp_cat_comp_fiber_z_iso_fib
-            {C : comp_cat}
-            {Γ : C}
-            {A B : ty Γ}
-            (s : z_iso (C := fiber_category _ _) A B)
-  : dom_mor (comp_cat_comp_fiber_z_iso_fib s)
-    =
-    comp_cat_comp_mor (pr1 s).
-Proof.
-  apply idpath.
-Qed.
-
 Definition subst_ty
            {C : comp_cat}
            {Γ Δ : C}