The results of my internship

UniMath/Algebra/GaussianElimination/Elimination.v

@@ -14,7 +14,6 @@ Require Import UniMath.MoreFoundations.Nat.
 Require Import UniMath.MoreFoundations.Tactics.
 
 Require Import UniMath.Combinatorics.StandardFiniteSets.
-Require Import UniMath.Combinatorics.FiniteSequences.
 Require Import UniMath.Combinatorics.Vectors.
 Require Import UniMath.Combinatorics.Maybe.
 
@@ -1000,7 +999,7 @@ Section Gauss.
     : ∏ r : (⟦ m ⟧%stn), r < iter -> r > k_i
     -> ((gauss_clear_column mat k_i k_j iter) r k_j = 0%ring).
   Proof.
-    destruct iter as [sep p]. 
+    destruct iter as [sep p].
     intros r r_le_sep r_gt_k.
     rewrite (gauss_clear_column_inv2  k_i k_j (sep ,, p) mat r r_le_sep)
       , <- gauss_clear_column_step_eq.

UniMath/Algebra/GaussianElimination/Tests.v

@@ -4,7 +4,6 @@ Require Import UniMath.Algebra.GaussianElimination.RowOps.
 Require Import UniMath.Algebra.Matrix.
 
 Require Import UniMath.Combinatorics.Maybe.
-Require Import UniMath.Combinatorics.FiniteSequences.
 Require Import UniMath.Combinatorics.StandardFiniteSets.
 Require Import UniMath.Combinatorics.Vectors.
 
@@ -155,4 +154,4 @@ Section Tests_2.
     (* Let eval6 := Eval cbn in
         ((@gaussian_elimination hq _ _ (row_vec v3))). *)
 
-End Tests_2. *)
+End Tests_2. *)

UniMath/Algebra/IteratedBinaryOperations.v

@@ -1,5 +1,8 @@
+Require Export UniMath.Combinatorics.StandardFiniteSets.
 Require Export UniMath.Combinatorics.Lists.
-Require Export UniMath.Combinatorics.FiniteSequences.
+Require Export UniMath.Combinatorics.FVectors.
+Require Export UniMath.Combinatorics.FMatrices.
+Require Export UniMath.Combinatorics.FLists.
 Require Export UniMath.Algebra.RigsAndRings.
 Require Export UniMath.Foundations.UnivalenceAxiom.
 
@@ -68,7 +71,7 @@ Section BinaryOperations.
     ∏ n (m:stn n → nat) (x : ∏ i (j:stn (m i)), X), iterop_fun (StandardFiniteSets.flatten' x) = iterop_fun_fun x.
 
   Definition isAssociative_seq :=
-    ∏ (x : Sequence (Sequence X)), iterop_seq (FiniteSequences.flatten x) = iterop_seq_seq x.
+    ∏ (x : Sequence (Sequence X)), iterop_seq (FLists.flatten x) = iterop_seq_seq x.
 
   Local Open Scope stn.
 

UniMath/Algebra/Matrix.v

@@ -7,7 +7,6 @@ Author: Langston Barrett (@siddharthist) (March 2018)
 
 Require Import UniMath.Foundations.PartA.
 Require Import UniMath.MoreFoundations.PartA.
-Require Import UniMath.Combinatorics.FiniteSequences.
 Require Import UniMath.Algebra.BinaryOperations.
 Require Import UniMath.Algebra.IteratedBinaryOperations.
 

UniMath/Bicategories/.package/files

@@ -75,10 +75,12 @@ DisplayedBicats/Examples/CategoriesWithStructure/BinProducts.v
 DisplayedBicats/Examples/CategoriesWithStructure/Pullbacks.v
 DisplayedBicats/Examples/CategoriesWithStructure/Equalizers.v
 DisplayedBicats/Examples/CategoriesWithStructure/FiniteLimits.v
+DisplayedBicats/Examples/CategoriesWithStructure/FiniteColimits.v
 DisplayedBicats/Examples/CategoriesWithStructure/SubobjectClassifier.v
 DisplayedBicats/Examples/CategoriesWithStructure/RegularAndExact.v
 DisplayedBicats/Examples/CategoriesWithStructure/ParameterizedNNO.v
 DisplayedBicats/Examples/CategoriesWithStructure/Exponentials.v
+DisplayedBicats/Examples/CategoriesWithStructure/Topoi.v
 
 MonoidalCategories/MonoidalFromBicategory.v
 MonoidalCategories/EndofunctorsMonoidal.v
@@ -502,9 +504,11 @@ RezkCompletions/StructuredCats/BinProducts.v
 RezkCompletions/StructuredCats/Pullbacks.v
 RezkCompletions/StructuredCats/Equalizers.v
 RezkCompletions/StructuredCats/FiniteLimits.v
+RezkCompletions/StructuredCats/FiniteColimits.v
 RezkCompletions/StructuredCats/SubobjectClassifier.v
 RezkCompletions/StructuredCats/RegularAndExact.v
 RezkCompletions/StructuredCats/ParameterizedNNO.v
 RezkCompletions/StructuredCats/Exponentials.v
+RezkCompletions/StructuredCats/Topoi.v
 
 DaggerCategories/BicatOfDaggerCats.v

UniMath/Bicategories/DisplayedBicats/Examples/CategoriesWithStructure/Exponentials.v

@@ -1,5 +1,12 @@
 (**
+   Bicategory Of Cartesian Closed Categories
+
   In this file, we construct the (displayed) bicategory [disp_bicat_exponentials] whose objects are categories equipped with chosen binary products and exponentials, and whose morphisms are functors that preserve binary products and exponentials.
+  We furthermore define the bicategory of finitely complete cartesian closed categories.
+
+  Contents.
+  1. Definition of the bicategory of cartesian closed categories [disp_bicat_exponentials]
+  2. Definition of the bicategory of finitely complete cartesian closed categories [disp_bicat_exponentials_over_lim]
  *)
 
 Require Import UniMath.Foundations.All.
@@ -13,9 +20,11 @@ Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
 Require Import UniMath.Bicategories.Core.Examples.BicatOfCats.
 Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations.
 Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell.
+Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub.
 Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sigma.
 
 Require Import UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure.BinProducts.
+Require Import UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure.FiniteLimits.
 
 Local Open Scope cat.
 
@@ -26,7 +35,7 @@ Section CategoriesWithExponentials.
   Proof.
     use disp_subbicat.
     - exact (λ C, Exponentials (pr12 C)).
-    - exact (λ C₁ C₂ E1 E2 F, preserves_exponentials E1 E2 (pr22 F)).
+    - exact (λ C₁ C₂ E₁ E₂ F, preserves_exponentials E₁ E₂ (pr22 F)).
     - exact (λ C _, id_preserves_exponentials _).
     - exact (λ _ _ _ _ _ _ _ _ HF HG, comp_preserves_exponentials HF HG).
   Defined.
@@ -50,3 +59,23 @@ Section CategoriesWithExponentials.
   Qed.
 
 End CategoriesWithExponentials.
+
+Section FinitelyCompleteCategoriesWithExponentials.
+
+  Definition disp_bicat_exponentials_over_lim
+    : disp_bicat (total_bicat disp_bicat_limits).
+  Proof.
+    use disp_subbicat.
+    - exact (λ C, Exponentials (pr1 (pr122 C))).
+    - exact (λ _ _ E₁ E₂ F, preserves_exponentials E₁ E₂ (pr21 (pr22 F))).
+    - exact (λ C _, id_preserves_exponentials _).
+    - exact (λ _ _ _ _ _ _ _ _ HF HG, comp_preserves_exponentials HF HG).
+  Defined.
+
+  Lemma disp_2cells_iscontr_exponentials_over_lim
+    : disp_2cells_iscontr disp_bicat_exponentials_over_lim.
+  Proof.
+    apply disp_2cells_iscontr_subbicat.
+  Qed.
+
+End FinitelyCompleteCategoriesWithExponentials.

UniMath/Bicategories/DisplayedBicats/Examples/CategoriesWithStructure/FiniteColimits.v

@@ -0,0 +1,109 @@
+(**
+  Bicategories for finite colimits
+
+  We define the bicategory of finitely cocomplete categories and finite colimit preserving functors.
+  In particular, we define the bicategories whose objects are categories equipped with colimits for a fixed diagram.
+
+  Contents.
+  1. Definition bicategories of categories equipped with
+     - an initial object [disp_bicat_initial];
+     - binary coproducts [disp_bicat_bincoproducts];
+     - and coequalizers respectively [disp_bicat_coequalizers].
+  2. Definition bicategory of finite cocomplete categories [disp_bicat_colimits]
+
+*)
+
+Require Import UniMath.Foundations.All.
+Require Import UniMath.MoreFoundations.All.
+Require Import UniMath.CategoryTheory.Core.Prelude.
+Require Import UniMath.CategoryTheory.Limits.Initial.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
+Require Import UniMath.CategoryTheory.Limits.Coequalizers.
+Require Import UniMath.CategoryTheory.Limits.Preservation.
+Require Import UniMath.CategoryTheory.DisplayedCats.Core.
+Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
+Require Import UniMath.Bicategories.Core.Examples.BicatOfCats.
+Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations.
+Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell.
+Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod.
+
+Local Open Scope cat.
+
+(** * 1. Bicategories of categories equipped with a colimit of a fixed diagram *)
+Section CategoriesWithChosenInitialAndPreservationUpToIso.
+
+  Definition disp_bicat_initial
+    : disp_bicat bicat_of_cats.
+  Proof.
+    use disp_subbicat.
+    - exact (λ C, Initial (C : category)).
+    - exact (λ C₁ C₂ _ _ F, preserves_initial F).
+    - exact (λ C _, identity_preserves_initial _).
+    - exact (λ _ _ _ _ _ _ _ _ HF HG, composition_preserves_initial HF HG).
+  Defined.
+
+  Lemma disp_2cells_iscontr_initial
+    : disp_2cells_iscontr disp_bicat_initial.
+  Proof.
+    apply disp_2cells_iscontr_subbicat.
+  Qed.
+
+End CategoriesWithChosenInitialAndPreservationUpToIso.
+
+Section CategoriesWithChosenBinCoproductsAndPreservationUpToIso.
+
+  Definition disp_bicat_bincoproducts
+    : disp_bicat bicat_of_cats.
+  Proof.
+    use disp_subbicat.
+    - exact (λ C, BinCoproducts C).
+    - exact (λ C₁ C₂ _ _ F, preserves_bincoproduct F).
+    - exact (λ C _, identity_preserves_bincoproduct _).
+    - exact (λ _ _ _ _ _ _ _ _ HF HG, composition_preserves_bincoproduct HF HG).
+  Defined.
+
+  Lemma disp_2cells_iscontr_bincoproducts
+    : disp_2cells_iscontr disp_bicat_bincoproducts.
+  Proof.
+    apply disp_2cells_iscontr_subbicat.
+  Qed.
+
+End CategoriesWithChosenBinCoproductsAndPreservationUpToIso.
+
+Section CategoriesWithChosenCoequalizersAndPreservationUpToIso.
+
+  Definition disp_bicat_coequalizers
+    : disp_bicat bicat_of_cats.
+  Proof.
+    use disp_subbicat.
+    - exact (λ C, Coequalizers (C : category)).
+    - exact (λ C₁ C₂ _ _ F, preserves_coequalizer F).
+    - exact (λ C _, identity_preserves_coequalizer _).
+    - exact (λ _ _ _ _ _ _ _ _ HF HG, composition_preserves_coequalizer HF HG).
+  Defined.
+
+  Lemma disp_2cells_iscontr_coequalizers
+    : disp_2cells_iscontr disp_bicat_coequalizers.
+  Proof.
+    apply disp_2cells_iscontr_subbicat.
+  Qed.
+
+End CategoriesWithChosenCoequalizersAndPreservationUpToIso.
+
+(** * 2. Bicategory of finitely cocomplete categories *)
+Section CategoriesWithChosenFiniteColimitsAndPreservationUpToIso.
+
+  Definition disp_bicat_colimits : disp_bicat bicat_of_cats
+    := disp_dirprod_bicat
+         disp_bicat_initial
+         (disp_dirprod_bicat
+            disp_bicat_bincoproducts
+            disp_bicat_coequalizers).
+
+  Lemma disp_2cells_iscontr_colimits
+    : disp_2cells_iscontr disp_bicat_colimits.
+  Proof.
+    repeat apply disp_2cells_of_dirprod_iscontr ; apply disp_2cells_iscontr_subbicat.
+  Qed.
+
+End CategoriesWithChosenFiniteColimitsAndPreservationUpToIso.

UniMath/Bicategories/DisplayedBicats/Examples/CategoriesWithStructure/RegularAndExact.v

@@ -71,7 +71,7 @@ Section ExactCategories.
   Lemma disp_2cells_iscontr_exact'
     : disp_2cells_iscontr disp_bicat_exact'.
   Proof.
-    intro ; intros ; apply iscontrunit.
+    apply disp_2cells_iscontr_fullsubbicat.
   Qed.
 
   Definition disp_bicat_exact

UniMath/Bicategories/DisplayedBicats/Examples/CategoriesWithStructure/Topoi.v

@@ -0,0 +1,107 @@
+(**
+  Displayed Bicategories Of Topoi
+
+  In this file, we define bicategories of topoi.
+
+  Contents
+  1. Elementary topoi [disp_bicat_elementarytopoi]
+  2. Arithmetic topoi [disp_bicat_elementarytopoi_NNO]
+ *)
+
+Require Import UniMath.Foundations.All.
+Require Import UniMath.MoreFoundations.All.
+Require Import UniMath.CategoryTheory.Core.Prelude.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+Require Import UniMath.CategoryTheory.Limits.Preservation.
+Require Import UniMath.CategoryTheory.Arithmetic.ParameterizedNNO.
+
+Require Import UniMath.CategoryTheory.DisplayedCats.Core.
+Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
+Require Import UniMath.Bicategories.Core.Examples.BicatOfCats.
+Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations.
+Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell.
+Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub.
+Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sigma.
+Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod.
+
+Require Import UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure.FiniteLimits.
+Require Import UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure.RegularAndExact.
+Require Import UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure.SubobjectClassifier.
+Require Import UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure.Exponentials.
+Require Import UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure.ParameterizedNNO.
+
+Local Open Scope cat.
+
+(** * 1. Elementary Topoi = Finite Limits & Cartesian Closed & Subobject Classifier *)
+Section ElementaryTopoi.
+
+  Definition disp_bicat_elementarytopoi'
+    : disp_bicat (total_bicat disp_bicat_limits).
+  Proof.
+    apply disp_dirprod_bicat.
+    - exact disp_bicat_exponentials_over_lim.
+    - exact disp_bicat_subobject_classifier'.
+  Defined.
+
+  Lemma disp_bicat_elementarytopoi'_is_locally_contractible
+    : disp_2cells_iscontr disp_bicat_elementarytopoi'.
+  Proof.
+    apply disp_2cells_of_dirprod_iscontr.
+    - apply disp_2cells_iscontr_exponentials_over_lim.
+    - apply disp_2cells_iscontr_subobject_classifier'.
+  Qed.
+
+  Definition disp_bicat_elementarytopoi
+    : disp_bicat bicat_of_cats.
+  Proof.
+    exact (sigma_bicat _ _ disp_bicat_elementarytopoi').
+  Defined.
+
+  Lemma disp_bicat_elementarytopoi_is_locally_contractible
+    : disp_2cells_iscontr disp_bicat_elementarytopoi.
+  Proof.
+    apply disp_2cells_of_sigma_iscontr.
+    - apply disp_2cells_iscontr_limits.
+    - apply disp_bicat_elementarytopoi'_is_locally_contractible.
+  Qed.
+
+End ElementaryTopoi.
+
+(** * 2. Arithmetic Topoi *)
+Section ArithmeticTopoi.
+
+  Definition disp_bicat_arithmetic_elementarytopoi'
+    : disp_bicat (total_bicat disp_bicat_elementarytopoi).
+  Proof.
+    use disp_subbicat.
+    - intros [C [[[T ?] [[P ?] ?]] ?]].
+      exact (parameterized_NNO T P).
+    - simpl.
+      intros C₁ C₂ N₁ N₂ [F [[[? pt] ?] ?]].
+      exact (preserves_parameterized_NNO N₁ N₂ _ pt).
+    - intro ; intro ; apply id_preserves_parameterized_NNO.
+    - exact (λ _ _ _ _ _ _ _ _ p₁ p₂, comp_preserves_parameterized_NNO p₁ p₂).
+  Defined.
+
+  Definition disp_bicat_arithmetic_elementarytopoi
+    : disp_bicat bicat_of_cats.
+  Proof.
+    exact (sigma_bicat _ _ disp_bicat_arithmetic_elementarytopoi').
+  Defined.
+
+  Lemma disp_bicat_arithmetic_elementarytopoi'_is_locally_contractible
+    : disp_2cells_iscontr disp_bicat_arithmetic_elementarytopoi'.
+  Proof.
+    apply disp_2cells_iscontr_subbicat.
+  Qed.
+
+  Lemma disp_bicat_arithmetic_elementarytopoi_is_locally_contractible
+    : disp_2cells_iscontr disp_bicat_arithmetic_elementarytopoi.
+  Proof.
+    apply disp_2cells_of_sigma_iscontr.
+    - apply disp_bicat_elementarytopoi_is_locally_contractible.
+    - apply disp_bicat_arithmetic_elementarytopoi'_is_locally_contractible.
+  Qed.
+
+End ArithmeticTopoi.

UniMath/Bicategories/DisplayedBicats/Examples/FullSub.v

@@ -322,4 +322,10 @@ Section FullSubBicat.
     - exact disp_2cells_isaprop_fullsubbicat.
   Qed.
 
+  Definition disp_2cells_iscontr_fullsubbicat
+    : disp_2cells_iscontr disp_fullsubbicat.
+  Proof.
+    intro ; intros ; exact iscontrunit.
+  Qed.
+
 End FullSubBicat.

UniMath/Bicategories/PseudoFunctors/UniversalArrow.v

@@ -161,7 +161,7 @@ Section RightUniversalArrow.
     Proof.
       simple refine (R ,, ε ,, _) ; cbn.
       intros x y.
-      use rad_equivalence_of_cats.
+      simple refine (rad_equivalence_of_cats _ _ _ (right_universal_arrow_functor x y ε) _ _).
       - apply is_univ_hom.
         exact HB₁.
       - use full_and_faithful_implies_fully_faithful.
@@ -319,7 +319,7 @@ Section LeftUniversalArrow.
     Proof.
       simple refine (L ,, η ,, _) ; cbn.
       intros x y.
-      use rad_equivalence_of_cats.
+      simple refine (rad_equivalence_of_cats _ _ _ (left_universal_arrow_functor x y η) _ _).
       - apply is_univ_hom.
         exact HB₂.
       - use full_and_faithful_implies_fully_faithful.