Pseudofunctors for comprehension categories (#1853)

This PR contains the pseudofunctors that (will) constitute a
biequivalence between categories with finite limits and comprehension
categories that are democratic and have unit/product/equalizer/sigma
types. In addition, it contains the results from category theory that
are necessary to construct these pseudofunctors.

UniMath/Bicategories/.package/files

@@ -425,6 +425,8 @@ ComprehensionCat/TypeFormers/EqualizerTypes.v
 ComprehensionCat/TypeFormers/Democracy.v
 ComprehensionCat/TypeFormers/SigmaTypes.v
 ComprehensionCat/DFLCompCat.v
+ComprehensionCat/Biequivalence/DFLCompCatToFinLim.v
+ComprehensionCat/Biequivalence/FinLimToDFLCompCat.v
 
 Logic/ComprehensionBicat.v
 

UniMath/Bicategories/ComprehensionCat/BicatOfCompCat/CompCat.v

@@ -75,6 +75,7 @@ Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
 Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
 Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
 Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.
+Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodFunctor.
 Require Import UniMath.CategoryTheory.DisplayedCats.DisplayedFunctorEq.
 Require Import UniMath.CategoryTheory.DisplayedCats.ComprehensionC.
 Require Import UniMath.CategoryTheory.Limits.Terminal.
@@ -188,6 +189,40 @@ Proof.
   apply idpath.
 Qed.
 
+Proposition comprehension_functor_mor_transportf
+            {C : cat_with_terminal_cleaving}
+            (χ : comprehension_functor C)
+            {x y : C}
+            {f g : x --> y}
+            (p : f = g)
+            {xx : disp_cat_of_types C x}
+            {yy : disp_cat_of_types C y}
+            (ff : xx -->[ f ] yy)
+  : comprehension_functor_mor χ (transportf _ p ff)
+    =
+    comprehension_functor_mor χ ff.
+Proof.
+  induction p ; cbn.
+  apply idpath.
+Qed.
+
+Proposition comprehension_functor_mor_transportb
+            {C : cat_with_terminal_cleaving}
+            (χ : comprehension_functor C)
+            {x y : C}
+            {f g : x --> y}
+            (p : f = g)
+            {xx : disp_cat_of_types C x}
+            {yy : disp_cat_of_types C y}
+            (gg : xx -->[ g ] yy)
+  : comprehension_functor_mor χ (transportb _ p gg)
+    =
+    comprehension_functor_mor χ gg.
+Proof.
+  induction p ; cbn.
+  apply idpath.
+Qed.
+
 (** * 2. Comprehension natural transformations *)
 Definition comprehension_nat_trans
            {C₁ C₂ : cat_with_terminal_cleaving}

UniMath/Bicategories/ComprehensionCat/BicatOfCompCat/FullCompCat.v

@@ -43,10 +43,13 @@ Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
 Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations.
+Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
 Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
 Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
 Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.
+Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodFunctor.
+Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod.
 Require Import UniMath.CategoryTheory.DisplayedCats.DisplayedFunctorEq.
 Require Import UniMath.CategoryTheory.Limits.Terminal.
 Require Import UniMath.CategoryTheory.Limits.Preservation.
@@ -176,6 +179,15 @@ Definition full_comp_cat_comprehension_fully_faithful
   : disp_functor_ff (comp_cat_comprehension C)
   := pr12 C.
 
+Definition full_comp_cat_comprehension_fiber_fully_faithful
+           {C : full_comp_cat}
+           (x : C)
+  : fully_faithful (fiber_functor (comp_cat_comprehension C) x).
+Proof.
+  use fiber_functor_ff.
+  exact (full_comp_cat_comprehension_fully_faithful C).
+Qed.
+
 Definition full_comp_cat_functor
            (C₁ C₂ : full_comp_cat)
   : UU
@@ -206,6 +218,85 @@ Definition full_comp_cat_functor_is_z_iso
       (comprehension_nat_trans_mor (comp_cat_functor_comprehension F) xx)
   := pr22 F x xx.
 
+Proposition full_comp_cat_fiber_nat_trans_ax
+            {C₁ C₂ : full_comp_cat}
+            (F : full_comp_cat_functor C₁ C₂)
+            (x : C₁)
+  : is_nat_trans
+      (fiber_functor (comp_cat_comprehension C₁) x
+       ∙ fiber_functor (disp_codomain_functor F) x)
+      (fiber_functor (comp_cat_type_functor F) x
+       ∙ fiber_functor (comp_cat_comprehension C₂) (F x))
+      (comp_cat_functor_comprehension F x).
+Proof.
+  intros xx xx' f.
+  use eq_mor_cod_fib.
+  refine (comp_in_cod_fib _ _ @ _ @ !(comp_in_cod_fib _ _)).
+  cbn -[fiber_functor].
+  etrans.
+  {
+    apply maponpaths_2.
+    apply disp_codomain_fiber_functor_mor.
+  }
+  pose (disp_nat_trans_ax
+          (comp_cat_functor_comprehension F)
+          (f := identity x)
+          (xx := xx')
+          (xx' := xx)
+          f)
+    as p.
+  refine (maponpaths (λ z, pr1 z) p @ _).
+  refine (transportb_cod_disp _ _ _ @ _).
+  cbn.
+  apply maponpaths.
+  refine (!_).
+  apply comprehension_functor_mor_transportf.
+Qed.
+
+Definition full_comp_cat_fiber_nat_trans
+           {C₁ C₂ : full_comp_cat}
+           (F : full_comp_cat_functor C₁ C₂)
+           (x : C₁)
+  : fiber_functor (comp_cat_comprehension C₁) x
+    ∙ fiber_functor (disp_codomain_functor F) x
+    ⟹
+    fiber_functor (comp_cat_type_functor F) x
+    ∙ fiber_functor (comp_cat_comprehension C₂) (F x).
+Proof.
+  use make_nat_trans.
+  - exact (comp_cat_functor_comprehension F x).
+  - exact (full_comp_cat_fiber_nat_trans_ax F x).
+Defined.
+
+Definition full_comp_cat_fiber_nat_z_iso
+           {C₁ C₂ : full_comp_cat}
+           (F : full_comp_cat_functor C₁ C₂)
+           (x : C₁)
+  : nat_z_iso
+      (fiber_functor (comp_cat_comprehension C₁) x
+       ∙ fiber_functor (disp_codomain_functor F) x)
+      (fiber_functor (comp_cat_type_functor F) x
+       ∙ fiber_functor (comp_cat_comprehension C₂) (F x)).
+Proof.
+  use make_nat_z_iso.
+  - exact (full_comp_cat_fiber_nat_trans F x).
+  - intro xx.
+    use is_z_iso_fiber_from_is_z_iso_disp.
+    use is_z_iso_disp_codomain.
+    apply full_comp_cat_functor_is_z_iso.
+Defined.
+
+Definition full_comp_cat_fiber_nat_z_iso_inv
+           {C₁ C₂ : full_comp_cat}
+           (F : full_comp_cat_functor C₁ C₂)
+           (x : C₁)
+  : nat_z_iso
+      (fiber_functor (comp_cat_type_functor F) x
+       ∙ fiber_functor (comp_cat_comprehension C₂) (F x))
+      (fiber_functor (comp_cat_comprehension C₁) x
+       ∙ fiber_functor (disp_codomain_functor F) x)
+  := nat_z_iso_inv (full_comp_cat_fiber_nat_z_iso F x).
+
 Definition full_comp_cat_nat_trans
            {C₁ C₂ : full_comp_cat}
            (F G : full_comp_cat_functor C₁ C₂)