diff --git a/UniMath/Algebra/GaussianElimination/Elimination.v b/UniMath/Algebra/GaussianElimination/Elimination.v index 5729e67513..2e8995f580 100644 --- a/UniMath/Algebra/GaussianElimination/Elimination.v +++ b/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. diff --git a/UniMath/Algebra/GaussianElimination/Tests.v b/UniMath/Algebra/GaussianElimination/Tests.v index 4358b341cc..dfc2ee1672 100644 --- a/UniMath/Algebra/GaussianElimination/Tests.v +++ b/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. *) \ No newline at end of file +End Tests_2. *) diff --git a/UniMath/Algebra/IteratedBinaryOperations.v b/UniMath/Algebra/IteratedBinaryOperations.v index d2f2704d0b..a6858aee8e 100644 --- a/UniMath/Algebra/IteratedBinaryOperations.v +++ b/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. diff --git a/UniMath/Algebra/Matrix.v b/UniMath/Algebra/Matrix.v index 84628bf6e8..31e8f2de48 100644 --- a/UniMath/Algebra/Matrix.v +++ b/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. diff --git a/UniMath/Bicategories/.package/files b/UniMath/Bicategories/.package/files index 17951a4f7a..caa18e18f5 100644 --- a/UniMath/Bicategories/.package/files +++ b/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 diff --git a/UniMath/Bicategories/DisplayedBicats/Examples/CategoriesWithStructure/Exponentials.v b/UniMath/Bicategories/DisplayedBicats/Examples/CategoriesWithStructure/Exponentials.v index 64ccc51389..96ef190365 100644 --- a/UniMath/Bicategories/DisplayedBicats/Examples/CategoriesWithStructure/Exponentials.v +++ b/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. diff --git a/UniMath/Bicategories/DisplayedBicats/Examples/CategoriesWithStructure/FiniteColimits.v b/UniMath/Bicategories/DisplayedBicats/Examples/CategoriesWithStructure/FiniteColimits.v new file mode 100644 index 0000000000..59fe8c773a --- /dev/null +++ b/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. diff --git a/UniMath/Bicategories/DisplayedBicats/Examples/CategoriesWithStructure/RegularAndExact.v b/UniMath/Bicategories/DisplayedBicats/Examples/CategoriesWithStructure/RegularAndExact.v index 5e0535ea42..798bdda751 100644 --- a/UniMath/Bicategories/DisplayedBicats/Examples/CategoriesWithStructure/RegularAndExact.v +++ b/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 diff --git a/UniMath/Bicategories/DisplayedBicats/Examples/CategoriesWithStructure/Topoi.v b/UniMath/Bicategories/DisplayedBicats/Examples/CategoriesWithStructure/Topoi.v new file mode 100644 index 0000000000..b905371674 --- /dev/null +++ b/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. diff --git a/UniMath/Bicategories/DisplayedBicats/Examples/FullSub.v b/UniMath/Bicategories/DisplayedBicats/Examples/FullSub.v index 3a71522c23..126b67e1bb 100644 --- a/UniMath/Bicategories/DisplayedBicats/Examples/FullSub.v +++ b/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. diff --git a/UniMath/Bicategories/PseudoFunctors/UniversalArrow.v b/UniMath/Bicategories/PseudoFunctors/UniversalArrow.v index ae40e7b919..ecb0a4973c 100644 --- a/UniMath/Bicategories/PseudoFunctors/UniversalArrow.v +++ b/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. diff --git a/UniMath/Bicategories/RezkCompletions/StructuredCats/BinProducts.v b/UniMath/Bicategories/RezkCompletions/StructuredCats/BinProducts.v index 3b08d808d4..c6b10b5593 100644 --- a/UniMath/Bicategories/RezkCompletions/StructuredCats/BinProducts.v +++ b/UniMath/Bicategories/RezkCompletions/StructuredCats/BinProducts.v @@ -95,7 +95,7 @@ Section CategoriesWithBinProductsAdmitRezkCompletions. - intros C1 C2 C3 F G H α C1_prod C2_prod C3_prod Gw. intros [t Fprod]. exists tt. - exact (weak_equiv_lifts_preserves_binproducts C2 C3 α Gw Fprod). + exact (weak_equiv_lifts_preserves_binproducts α Gw Fprod). Defined. Corollary disp_bicat_have_binproducts_has_Rezk_completions @@ -156,7 +156,7 @@ Section CategoriesWithChosenBinProductsAndPreservationUpToIsoHasRezkCompletions. - intros C1 C2 C3 F G H α C1_prod C2_prod C3_prod Gw. intros [t Fprod]. exists tt. - exact (weak_equiv_lifts_preserves_binproducts C2 C3 α Gw Fprod). + exact (weak_equiv_lifts_preserves_binproducts α Gw Fprod). Defined. Corollary disp_bicat_binproducts_has_Rezk_completions diff --git a/UniMath/Bicategories/RezkCompletions/StructuredCats/Equalizers.v b/UniMath/Bicategories/RezkCompletions/StructuredCats/Equalizers.v index 04e92f8972..cd1f12a8e1 100644 --- a/UniMath/Bicategories/RezkCompletions/StructuredCats/Equalizers.v +++ b/UniMath/Bicategories/RezkCompletions/StructuredCats/Equalizers.v @@ -59,7 +59,7 @@ Section CategoriesWithEqualizersAndPreservationUpToIsoHasRezkCompletions. - intros C ?. refine (tt ,, weak_equiv_preserves_equalizers (η_weak_equiv C)). - intros C1 C2 C3 F G H α E₁ E₂ E₃ Gw [t Feq]. - exact (tt ,, weak_equiv_lifts_preserves_equalizers C2 C3 α Gw Feq). + exact (tt ,, weak_equiv_lifts_preserves_equalizers α Gw Feq). Defined. Corollary disp_bicat_have_equalizers_has_Rezk_completions @@ -118,7 +118,7 @@ Section CategoriesWithChosenEqualizersAndPreservationUpToIsoHasRezkCompletions. - intros C1 C2 C3 F G H α E1 E2 E3 Gw. intros [t F_pe]. exists tt. - exact (weak_equiv_lifts_preserves_equalizers C2 C3 α Gw F_pe). + exact (weak_equiv_lifts_preserves_equalizers α Gw F_pe). Defined. Corollary disp_bicat_equalizers_has_Rezk_completions diff --git a/UniMath/Bicategories/RezkCompletions/StructuredCats/FiniteColimits.v b/UniMath/Bicategories/RezkCompletions/StructuredCats/FiniteColimits.v new file mode 100644 index 0000000000..aa75eb91a7 --- /dev/null +++ b/UniMath/Bicategories/RezkCompletions/StructuredCats/FiniteColimits.v @@ -0,0 +1,129 @@ +(** +In this file, we conclude that the Rezk completion for categories lifts to finitely cocomplete categories. + +Contents: +1. [CategoriesWithFiniteColimitsAdmitRezkCompletions] proves the existence of a displayed universal arrow for the inclusion of univalent finitely cocomplete categories into all finitely cocomplete categories. +*) + +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.WeakEquivalences.Core. +Require Import UniMath.CategoryTheory.WeakEquivalences.Initial. +Require Import UniMath.CategoryTheory.WeakEquivalences.Coequalizers. +Require Import UniMath.CategoryTheory.WeakEquivalences.Preservation.Bincoproducts. +Require Import UniMath.CategoryTheory.WeakEquivalences.LiftPreservation.BinCoproducts. + +Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. +Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. +Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. + +Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. +Require Import UniMath.Bicategories.PseudoFunctors.UniversalArrow. +Import PseudoFunctor.Notations. +Import DispBicat.Notations. + +Require Import UniMath.Bicategories.PseudoFunctors.Examples.BicatOfCatToUnivCat. +Require Import UniMath.Bicategories.DisplayedBicats.Examples.DispBicatOnCatToUniv. +Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod. +Require Import UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure.FiniteColimits. +Require Import UniMath.Bicategories.RezkCompletions.DisplayedRezkCompletions. + +Local Open Scope cat. + +(** * 1. Rezk completion for finitely cocomplete categories *) +Section CategoriesWithFiniteColimitsAdmitRezkCompletions. + + Context (LUR : left_universal_arrow univ_cats_to_cats) + (η_weak_equiv : ∏ C : category, is_weak_equiv (pr12 LUR C)). + + Lemma disp_bicat_initial_has_RC + : cat_with_struct_has_RC η_weak_equiv disp_bicat_initial. + Proof. + simple refine (_ ,, _ ,, _). + - intros C1 C2 C2_univ F Fw [T1 _]. + exact (make_Initial _ (weak_equiv_preserves_initial _ Fw _ (pr2 T1)) ,, tt). + - intros C [T1 ?]. + refine (tt ,, _). + use weak_equiv_preserves_initial. + apply η_weak_equiv. + - simpl ; intros C1 C2 C3 F G H α [T1 _] [T2 _] [T3 _] Gw. + intros [t Fpinit]. + exists tt. + exact (weak_equiv_lifts_preserves_initial α Gw Fpinit). + Defined. + + Corollary disp_bicat_initial_has_Rezk_completions + : cat_with_structure_has_RezkCompletion disp_bicat_initial. + Proof. + apply (make_RezkCompletion_from_locally_contractible _ _ disp_bicat_initial_has_RC). + exact disp_2cells_iscontr_initial. + Defined. + + Lemma disp_bicat_bincoproducts_has_RC + : cat_with_struct_has_RC η_weak_equiv disp_bicat_bincoproducts. + Proof. + simple refine (_ ,, _ ,, _). + - intros C1 C2 C2_univ F Fw [P1 _]. + exact (weak_equiv_creates_bincoproducts Fw P1 C2_univ ,, tt). + - intros C [P1 ?]. + refine (tt ,, _). + use weak_equiv_preserves_bincoproducts. + apply η_weak_equiv. + - simpl ; intros C1 C2 C3 F G H α [T1 _] [T2 _] [T3 _] Gw. + intros [t Fp]. + exists tt. + exact (weak_equiv_lifts_preserves_bincoproducts C2 C3 α Gw Fp). + Defined. + + Corollary disp_bicat_bincoproducts_has_Rezk_completions + : cat_with_structure_has_RezkCompletion disp_bicat_bincoproducts. + Proof. + apply (make_RezkCompletion_from_locally_contractible _ _ disp_bicat_bincoproducts_has_RC). + exact disp_2cells_iscontr_bincoproducts. + Defined. + + Lemma disp_bicat_coequalizers_has_RC + : cat_with_struct_has_RC η_weak_equiv disp_bicat_coequalizers. + Proof. + simple refine (_ ,, _ ,, _). + - intros C1 C2 C2_univ F Fw [P1 _]. + exact (weak_equiv_creates_coequalizers Fw C2_univ P1 ,, tt). + - intros C [P1 ?]. + refine (tt ,, _). + use weak_equiv_preserves_coequalizers. + apply η_weak_equiv. + - simpl ; intros C1 C2 C3 F G H α [T1 _] [T2 _] [T3 _] Gw. + intros [t Fp]. + exists tt. + exact (weak_equiv_lifts_preserves_coequalizers C2 C3 α Gw Fp). + Defined. + + Corollary disp_bicat_coequalizers_has_Rezk_completions + : cat_with_structure_has_RezkCompletion disp_bicat_coequalizers. + Proof. + apply (make_RezkCompletion_from_locally_contractible _ _ disp_bicat_coequalizers_has_RC). + exact disp_2cells_iscontr_coequalizers. + Defined. + + Lemma disp_bicat_colimits_has_RC + : cat_with_struct_has_RC η_weak_equiv disp_bicat_colimits. + Proof. + repeat use make_cat_with_struct_has_RC_from_dirprod. + - apply disp_bicat_initial_has_RC. + - apply disp_bicat_bincoproducts_has_RC. + - apply disp_bicat_coequalizers_has_RC. + Defined. + + Theorem disp_bicat_colimits_has_RezkCompletion + : cat_with_structure_has_RezkCompletion disp_bicat_colimits. + Proof. + apply (make_RezkCompletion_from_locally_contractible η_weak_equiv). + - exact disp_bicat_colimits_has_RC. + - exact disp_2cells_iscontr_colimits. + Defined. + +End CategoriesWithFiniteColimitsAdmitRezkCompletions. diff --git a/UniMath/Bicategories/RezkCompletions/StructuredCats/Pullbacks.v b/UniMath/Bicategories/RezkCompletions/StructuredCats/Pullbacks.v index 1a3e2263d8..618717762e 100644 --- a/UniMath/Bicategories/RezkCompletions/StructuredCats/Pullbacks.v +++ b/UniMath/Bicategories/RezkCompletions/StructuredCats/Pullbacks.v @@ -61,7 +61,7 @@ Section CategoriesWithPullbacksAndPreservationUpToIsoHasRezkCompletions. - intros C1 C2 C3 F G H α ? ? ? Gw. intros [t Fpb]. exists tt. - use (weak_equiv_lifts_preserves_pullbacks C2 C3 α Gw Fpb). + use (weak_equiv_lifts_preserves_pullbacks α Gw Fpb). Defined. Corollary disp_bicat_have_pullbacks_has_Rezk_completions @@ -122,7 +122,7 @@ Section CategoriesWithChosenPullbacksAndPreservationUpToIsoHasRezkCompletions. - intros C1 C2 C3 F G H α P1 P2 P3 Gw. intros [t F_pp]. exists tt. - exact (weak_equiv_lifts_preserves_pullbacks C2 C3 α Gw F_pp). + exact (weak_equiv_lifts_preserves_pullbacks α Gw F_pp). Defined. Corollary disp_bicat_pullbacks_has_Rezk_completions diff --git a/UniMath/Bicategories/RezkCompletions/StructuredCats/Topoi.v b/UniMath/Bicategories/RezkCompletions/StructuredCats/Topoi.v new file mode 100644 index 0000000000..b5ff5920d3 --- /dev/null +++ b/UniMath/Bicategories/RezkCompletions/StructuredCats/Topoi.v @@ -0,0 +1,139 @@ +(** + Rezk Completions For Topoi + + In this file, we show how the Rezk completion for categories lifts to the following types of topoi: elementary topoi, and arithmetic topoi. + + Contents. + 1. [disp_bicat_elementarytopoi_has_RezkCompletion] proves the lifting to elementary topoi + 2. [disp_bicat_arithmetic_elementarytopoi_has_RezkCompletion] proves the lifting to elementary with a parameterized NNO. +*) + +Require Import UniMath.Foundations.All. +Require Import UniMath.MoreFoundations.All. +Require Import UniMath.CategoryTheory.Core.Prelude. + +Require Import UniMath.CategoryTheory.WeakEquivalences.Core. + +Require Import UniMath.CategoryTheory.Exponentials. +Require Import UniMath.CategoryTheory.Limits.BinProducts. +Require Import UniMath.CategoryTheory.Limits.Preservation. +Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier. +Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifierIso. +Require Import UniMath.CategoryTheory.SubobjectClassifier.PreservesSubobjectClassifier. + +Require Import UniMath.CategoryTheory.WeakEquivalences.Terminal. +Require Import UniMath.CategoryTheory.WeakEquivalences.Preservation.Exponentials. +Require Import UniMath.CategoryTheory.WeakEquivalences.LiftPreservation.Exponentials. +Require Import UniMath.CategoryTheory.WeakEquivalences.Preservation.SubobjectClassifier. +Require Import UniMath.CategoryTheory.WeakEquivalences.LiftPreservation.SubobjectClassifier. +Require Import UniMath.CategoryTheory.WeakEquivalences.PNNO. + +Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. +Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. +Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. + +Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. +Require Import UniMath.Bicategories.DisplayedBicats.DispPseudofunctor. +Require Import UniMath.Bicategories.PseudoFunctors.UniversalArrow. +Import PseudoFunctor.Notations. +Import DispBicat.Notations. + +Require Import UniMath.Bicategories.PseudoFunctors.Examples.BicatOfCatToUnivCat. +Require Import UniMath.Bicategories.DisplayedBicats.Examples.DispBicatOnCatToUniv. +Require Import UniMath.Bicategories.DisplayedBicats.DisplayedUniversalArrow. +Require Import UniMath.Bicategories.DisplayedBicats.DisplayedUniversalArrowOnCat. +Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sigma. + +Require Import UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure.Topoi. +Require Import UniMath.Bicategories.RezkCompletions.DisplayedRezkCompletions. +Require Import UniMath.Bicategories.RezkCompletions.StructuredCats.FiniteLimits. +Require Import UniMath.Bicategories.RezkCompletions.StructuredCats.RegularAndExact. + +Local Open Scope cat. + +(** * 1. Lifting Of Rezk Completions To Elementary Topoi *) +Section ElementaryTopoiAdmitRezkCompletions. + + Context (LUR : left_universal_arrow univ_cats_to_cats) + (η_weak_equiv : ∏ C : category, is_weak_equiv (pr12 LUR C)). + + Lemma disp_bicat_elementarytopoi_has_RC + : cat_with_struct_has_RC η_weak_equiv disp_bicat_elementarytopoi. + Proof. + use make_cat_with_struct_has_RC_from_sigma. + - exact (disp_bicat_limits_has_RC LUR η_weak_equiv). + - simpl. + intros C₁ C₂ C₂_univ F F_weq L₁ [[E₁ ?] [Ω₁ ?]]. + refine ((_ ,, tt) ,, (_ ,, tt)). + + apply (weak_equiv_into_univ_creates_exponentials F_weq C₂_univ E₁). + + apply (weak_equiv_creates_subobject_classifier F_weq _ Ω₁). + - intros C L₁ [[E₁ ?] [Ω₁ ?]]. + refine ((tt ,, _) ,, (tt ,, _)). + + apply weak_equiv_preserves_exponentials. + + apply weak_equiv_preserves_subobject_classifier. + - simpl. + intros C₁ C₂ C₃ F G H n + L₁ [[E₁ ?] [Ω₁ ?]] + L₂ [[E₂ ?] [Ω₂ ?]] + L₃ [[E₃ ?] [Ω₃ ?]] + G_weq F_pL [[? F_pexp] [? F_Ω]]. + refine ((tt ,, _) ,, (tt ,, _)). + + use (weak_equiv_lifts_preserves_exponentials'). + * exact (pr112 L₁). + * exact E₁. + * exact F_pexp. + + use preserves_subobject_classifier_independent_of_chosen_terminal_if_univalent. + * apply (weak_equiv_creates_terminal G_weq (pr11 L₁)). + * apply weak_equiv_lifts_preserves_subobject_classifier. + exact F_Ω. + * apply C₂. + Defined. + + Theorem disp_bicat_elementarytopoi_has_RezkCompletion + : cat_with_structure_has_RezkCompletion disp_bicat_elementarytopoi. + Proof. + apply (make_RezkCompletion_from_locally_contractible η_weak_equiv). + - exact disp_bicat_elementarytopoi_has_RC. + - apply disp_bicat_elementarytopoi_is_locally_contractible. + Defined. + +End ElementaryTopoiAdmitRezkCompletions. + +(** * 2. Lifting Of Rezk Completions To Arithmetic Topoi *) +Section ArithmeticTopoiAdmitRezkCompletions. + + Context (LUR : left_universal_arrow univ_cats_to_cats) + (η_weak_equiv : ∏ C : category, is_weak_equiv (pr12 LUR C)). + + Lemma disp_bicat_arithmetic_elementarytopoi_has_RC + : cat_with_struct_has_RC η_weak_equiv disp_bicat_arithmetic_elementarytopoi. + Proof. + use make_cat_with_struct_has_RC_from_sigma. + - exact (disp_bicat_elementarytopoi_has_RC LUR η_weak_equiv). + - simpl. + intros ? ? ? ? F_weq ? [N₁ ?]. + refine (_ ,, tt). + apply (weak_equiv_creates_parameterized_NNO F_weq N₁). + - intro ; intros. + refine (tt ,, _). + apply weak_equiv_preserves_parameterized_NNO'. + - cbn ; intros C₁ C₂ C₃ F G H α + ? [N₁ ?] + ? [N₂ ?] + ? [N₃ ?] + G_weq + ? + [? FN]. + refine (tt ,, _). + exact (weak_equiv_lifts_preserves_parameterized_NNO α G_weq N₁ N₂ N₃ FN). + Defined. + + Theorem disp_bicat_arithmetic_elementarytopoi_has_RezkCompletion + : cat_with_structure_has_RezkCompletion disp_bicat_arithmetic_elementarytopoi. + Proof. + apply (make_RezkCompletion_from_locally_contractible η_weak_equiv). + - exact disp_bicat_arithmetic_elementarytopoi_has_RC. + - apply disp_bicat_arithmetic_elementarytopoi_is_locally_contractible. + Defined. + +End ArithmeticTopoiAdmitRezkCompletions. diff --git a/UniMath/CategoryTheory/.package/files b/UniMath/CategoryTheory/.package/files index c48a76762d..56646be61e 100644 --- a/UniMath/CategoryTheory/.package/files +++ b/UniMath/CategoryTheory/.package/files @@ -226,6 +226,7 @@ CategoryEquality.v Core/PosetCat.v WeakEquivalences/Core.v +WeakEquivalences/TwoOutOfThree.v WeakEquivalences/Opp.v WeakEquivalences/Terminal.v WeakEquivalences/Initial.v @@ -254,6 +255,7 @@ WeakEquivalences/Regular.v WeakEquivalences/Exact.v WeakEquivalences/Preservation/NNO.v WeakEquivalences/PNNO.v +WeakEquivalences/Slice.v RezkCompletions/RezkCompletions.v RezkCompletions/Construction.v @@ -396,6 +398,7 @@ Chains/CoAdamek.v Chains/OmegaCocontFunctors.v OppositeCategory/LimitsAsColimits.v Chains/OmegaContFunctors.v +Chains/OmegaContPolynomialFunctors.v Chains/All.v Inductives/Lists.v Inductives/Trees.v diff --git a/UniMath/CategoryTheory/Adjunctions/Core.v b/UniMath/CategoryTheory/Adjunctions/Core.v index 43fd012915..a230cb9a93 100644 --- a/UniMath/CategoryTheory/Adjunctions/Core.v +++ b/UniMath/CategoryTheory/Adjunctions/Core.v @@ -38,12 +38,12 @@ Local Open Scope cat. (** * Adjunctions *) Section adjunctions. -Definition adjunction_data (A B : category) : UU +Definition adjunction_data (A B : precategory) : UU := ∑ (F : functor A B) (G : functor B A), nat_trans (functor_identity A) (F ∙ G) × nat_trans (G ∙ F) (functor_identity B). -Definition make_adjunction_data {A B : category} +Definition make_adjunction_data {A B : precategory} (F : functor A B) (G : functor B A) (η : functor_identity _ ⟹ (F ∙ G)) @@ -64,12 +64,12 @@ Definition adjcounit {A B} (X : adjunction_data A B) : nat_trans (_ ∙ _ ) (functor_identity _) := pr2 (pr2 (pr2 X)). -Definition triangle_1_statement {A B : category} (X : adjunction_data A B) +Definition triangle_1_statement {A B : precategory} (X : adjunction_data A B) (F := left_functor X) (η := adjunit X) (ε := adjcounit X) : UU := ∏ a : A, # F (η a) · ε (F a) = identity (F a). -Definition triangle_2_statement {A B : category} (X : adjunction_data A B) +Definition triangle_2_statement {A B : precategory} (X : adjunction_data A B) (G := right_functor X) (η := adjunit X) (ε := adjcounit X) : UU := ∏ b : B, η (G b) · # G (ε b) = identity (G b). @@ -77,7 +77,7 @@ Definition triangle_2_statement {A B : category} (X : adjunction_data A B) Definition form_adjunction' {A B} (X : adjunction_data A B) : UU := triangle_1_statement X × triangle_2_statement X. -Definition form_adjunction {A B : category} (F : functor A B) (G : functor B A) +Definition form_adjunction {A B : precategory} (F : functor A B) (G : functor B A) (eta : nat_trans (functor_identity A) (functor_composite F G)) (eps : nat_trans (functor_composite G F) (functor_identity B)) : UU := form_adjunction' (F,,G,,eta,,eps). @@ -92,19 +92,19 @@ Proof. - apply A. Defined. -Definition make_form_adjunction {A B : category} {F : functor A B} {G : functor B A} +Definition make_form_adjunction {A B : precategory} {F : functor A B} {G : functor B A} {eta : nat_trans (functor_identity A) (functor_composite F G)} {eps : nat_trans (functor_composite G F) (functor_identity B)} (H1 : ∏ a : A, # F (eta a) · eps (F a) = identity (F a)) (H2 : ∏ b : B, eta (G b) · # G (eps b) = identity (G b)) : form_adjunction F G eta eps := (H1,,H2). - Definition are_adjoints {A B : category} (F : functor A B) (G : functor B A) : UU := + Definition are_adjoints {A B : precategory} (F : functor A B) (G : functor B A) : UU := ∑ (etaeps : (nat_trans (functor_identity A) (functor_composite F G)) × (nat_trans (functor_composite G F) (functor_identity B))), form_adjunction F G (pr1 etaeps) (pr2 etaeps). - Definition make_are_adjoints {A B : category} + Definition make_are_adjoints {A B : precategory} (F : functor A B) (G : functor B A) (eta : nat_trans (functor_identity A) (functor_composite F G)) (eps : nat_trans (functor_composite G F) (functor_identity B)) @@ -114,26 +114,26 @@ Definition make_form_adjunction {A B : category} {F : functor A B} {G : functor exact HH. Defined. - Definition adjunction (A B : category) : UU + Definition adjunction (A B : precategory) : UU := ∑ X : adjunction_data A B, form_adjunction' X. Coercion data_from_adjunction {A B} (X : adjunction A B) : adjunction_data _ _ := pr1 X. - Definition make_adjunction {A B : category} + Definition make_adjunction {A B : precategory} (adjData : adjunction_data A B) (adjProp : form_adjunction' adjData) : adjunction A B := (adjData ,, adjProp). - Definition form_adjunction_from_adjunction {A B : category} + Definition form_adjunction_from_adjunction {A B : precategory} (adj : adjunction A B) : form_adjunction' adj := pr2 adj. - Definition triangle_1_statement_from_adjunction {A B : category} + Definition triangle_1_statement_from_adjunction {A B : precategory} (adj : adjunction A B) : triangle_1_statement adj := pr1 (pr2 adj). - Definition triangle_2_statement_from_adjunction {A B : category} + Definition triangle_2_statement_from_adjunction {A B : precategory} (adj : adjunction A B) : triangle_2_statement adj := pr2 (pr2 adj). @@ -146,90 +146,90 @@ Definition make_form_adjunction {A B : category} {F : functor A B} {G : functor - exact(form_adjunction_from_adjunction X). Defined. - Definition unit_from_are_adjoints {A B : category} + Definition unit_from_are_adjoints {A B : precategory} {F : functor A B} {G : functor B A} (H : are_adjoints F G) : nat_trans (functor_identity A) (functor_composite F G) := pr1 (pr1 H). - Definition counit_from_are_adjoints {A B : category} + Definition counit_from_are_adjoints {A B : precategory} {F : functor A B} {G : functor B A} (H : are_adjoints F G) : nat_trans (functor_composite G F) (functor_identity B) := pr2 (pr1 H). - Definition is_left_adjoint {A B : category} (F : functor A B) : UU := + Definition is_left_adjoint {A B : precategory} (F : functor A B) : UU := ∑ (G : functor B A), are_adjoints F G. - Coercion adjunction_data_from_is_left_adjoint {A B : category} + Coercion adjunction_data_from_is_left_adjoint {A B : precategory} {F : functor A B} (HF : is_left_adjoint F) : adjunction_data A B := (F,, _ ,,unit_from_are_adjoints (pr2 HF) ,,counit_from_are_adjoints (pr2 HF) ). - Definition is_right_adjoint {A B : category} (G : functor B A) : UU := + Definition is_right_adjoint {A B : precategory} (G : functor B A) : UU := ∑ (F : functor A B), are_adjoints F G. - Definition adjunction_data_from_is_right_adjoint {A B : category} + Definition adjunction_data_from_is_right_adjoint {A B : precategory} {F : functor A B} (HF : is_right_adjoint F) : adjunction_data B A := make_adjunction_data _ F (unit_from_are_adjoints (pr2 HF)) (counit_from_are_adjoints (pr2 HF)). - Definition are_adjoints_to_is_left_adjoint {A B : category} (F : functor A B) (G : functor B A) + Definition are_adjoints_to_is_left_adjoint {A B : precategory} (F : functor A B) (G : functor B A) (H : are_adjoints F G) : is_left_adjoint F := (G,,H). Coercion are_adjoints_to_is_left_adjoint : are_adjoints >-> is_left_adjoint. - Definition are_adjoints_to_is_right_adjoint {A B : category} (F : functor A B) + Definition are_adjoints_to_is_right_adjoint {A B : precategory} (F : functor A B) (G : functor B A) (H : are_adjoints F G) : is_right_adjoint G := (F,,H). Coercion are_adjoints_to_is_right_adjoint : are_adjoints >-> is_right_adjoint. - Definition right_adjoint {A B : category} + Definition right_adjoint {A B : precategory} {F : functor A B} (H : is_left_adjoint F) : functor B A := pr1 H. - Lemma is_right_adjoint_right_adjoint {A B : category} + Lemma is_right_adjoint_right_adjoint {A B : precategory} {F : functor A B} (H : is_left_adjoint F) : is_right_adjoint (right_adjoint H). Proof. exact (F,,pr2 H). Defined. - Definition left_adjoint {A B : category} + Definition left_adjoint {A B : precategory} {G : functor B A} (H : is_right_adjoint G) : functor A B := pr1 H. - Lemma is_left_adjoint_left_adjoint {A B : category} + Lemma is_left_adjoint_left_adjoint {A B : precategory} {G : functor B A} (H : is_right_adjoint G) : is_left_adjoint (left_adjoint H). Proof. exact (G,,pr2 H). Defined. - Definition unit_from_left_adjoint {A B : category} + Definition unit_from_left_adjoint {A B : precategory} {F : functor A B} (H : is_left_adjoint F) : nat_trans (functor_identity A) (functor_composite F (right_adjoint H)) := adjunit H. (* makes use of the coercion above *) - Definition unit_from_right_adjoint {A B : category} + Definition unit_from_right_adjoint {A B : precategory} {G : functor B A} (H : is_right_adjoint G) : nat_trans (functor_identity A) (functor_composite (left_adjoint H) G) := unit_from_are_adjoints (pr2 H). - Definition counit_from_left_adjoint {A B : category} + Definition counit_from_left_adjoint {A B : precategory} {F : functor A B} (H : is_left_adjoint F) : nat_trans (functor_composite (right_adjoint H) F) (functor_identity B) := counit_from_are_adjoints (pr2 H). - Definition counit_from_right_adjoint {A B : category} + Definition counit_from_right_adjoint {A B : precategory} {G : functor B A} (H : is_right_adjoint G) : nat_trans (functor_composite G (left_adjoint H)) (functor_identity B) := counit_from_are_adjoints (pr2 H). - Definition triangle_id_left_ad {A B : category} {F : functor A B} {G : functor B A} + Definition triangle_id_left_ad {A B : precategory} {F : functor A B} {G : functor B A} (H : are_adjoints F G) : ∏ a, # F (unit_from_are_adjoints H a) · counit_from_are_adjoints H (F a) = identity (F a) := pr1 (pr2 H). - Definition triangle_id_right_ad {A B : category} {F : functor A B} {G : functor B A} + Definition triangle_id_right_ad {A B : precategory} {F : functor A B} {G : functor B A} (H : are_adjoints F G) : ∏ b, unit_from_are_adjoints H (G b) · # G (counit_from_are_adjoints H b) = identity (G b) := pr2 (pr2 H). Lemma are_adjoints_functor_composite - {A B C : category} {F1 : functor A B} {F2 : functor B C} + {A B C : precategory} {F1 : functor A B} {F2 : functor B C} {G1 : functor B A} {G2 : functor C B} (H1 : are_adjoints F1 G1) (H2 : are_adjoints F2 G2) : are_adjoints (functor_composite F1 F2) (functor_composite G2 G1). @@ -271,7 +271,7 @@ Definition make_form_adjunction {A B : category} {F : functor A B} {G : functor Defined. Lemma is_left_adjoint_functor_composite - {A B C : category} {F1 : functor A B} {F2 : functor B C} + {A B C : precategory} {F1 : functor A B} {F2 : functor B C} (H1 : is_left_adjoint F1) (H2 : is_left_adjoint F2) : is_left_adjoint (functor_composite F1 F2). Proof. @@ -346,7 +346,7 @@ Definition make_form_adjunction {A B : category} {F : functor A B} {G : functor (** * Identity functor is a left adjoint *) - Lemma is_left_adjoint_functor_identity {A : category} : + Lemma is_left_adjoint_functor_identity {A : precategory} : is_left_adjoint (functor_identity A). Proof. use tpair. @@ -448,7 +448,7 @@ End adjunctions. Section HomSetIso_from_Adjunction. - Context {C D : category} {F : functor C D} {G : functor D C} (H : are_adjoints F G). + Context {C D : precategory} {F : functor C D} {G : functor D C} (H : are_adjoints F G). Let η := unit_from_are_adjoints H. Let ε := counit_from_are_adjoints H. @@ -633,7 +633,7 @@ Definition hom_natural_postcomp {C D : precategory} {F : functor C D} { G : func Section Adjunction_from_HomSetIso. - Context {C D : category} {F : functor C D} {G : functor D C} + Context {C D : precategory} {F : functor C D} {G : functor D C} (H : natural_hom_weq F G). Local Definition hom_inv : ∏ {A : C} {B : D}, A --> G B → F A --> B diff --git a/UniMath/CategoryTheory/Chains/OmegaContPolynomialFunctors.v b/UniMath/CategoryTheory/Chains/OmegaContPolynomialFunctors.v new file mode 100644 index 0000000000..1501265d0a --- /dev/null +++ b/UniMath/CategoryTheory/Chains/OmegaContPolynomialFunctors.v @@ -0,0 +1,295 @@ +(** ** Set-Based Polynomial Functors are omega-continuous + + Author : Antoine Fisse (@AextraT), 2025 +*) + +Require Import UniMath.Foundations.PartD. +Require Import UniMath.Foundations.Sets. +Require Import UniMath.MoreFoundations.All. + +Require Import UniMath.Induction.FunctorCoalgebras_legacy. +Require Import UniMath.Induction.PolynomialFunctors. +Require Import UniMath.Induction.M.Core. +Require Import UniMath.Induction.M.MWithSets. + +Require Import UniMath.CategoryTheory.Categories.Type.Core. +Require Import UniMath.CategoryTheory.Core.Categories. +Require Import UniMath.CategoryTheory.Core.Functors. +Require Import UniMath.CategoryTheory.DisplayedCats.Core. +Require Import UniMath.CategoryTheory.Categories.HSET.All. +Require Import UniMath.CategoryTheory.Chains.CoAdamek. +Require Import UniMath.CategoryTheory.Chains.Chains. +Require Import UniMath.CategoryTheory.Chains.Cochains. +Require Import UniMath.CategoryTheory.Limits.Graphs.Diagrams. +Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. +Require Import UniMath.CategoryTheory.Limits.Terminal. +Require Import UniMath.CategoryTheory.FunctorCoalgebras. + +Local Open Scope cat. +Local Open Scope functions. + +Section OmegaContinuity. + + Context {A : ob HSET} (B : pr1hSet A → ob HSET). + + Local Definition F' := MWithSets.F' B. + + Lemma comp_right_eq_hset + {X Y Z : UU} + {f g : X -> Y} + (h : Y -> Z) + (p : f = g) + : h ∘ f = h ∘ g. + Proof. + induction p. + apply idpath. + Defined. + + Lemma pullback_cone_edge + {X Y0 Y1 Y2: SET} + (x : pr1hSet X) + {f : SET ⟦ Y1, Y2 ⟧} + {g0 : SET ⟦ X, F' Y0 ⟧} + {g1 : SET ⟦ X, F' Y1 ⟧} + {g2 : SET ⟦ X, F' Y2 ⟧} + (p : (#F' f) ∘ g1 = g2) + (q1 : pr1 ∘ g0 = pr1 ∘ g1) + (q2 : pr1 ∘ g0 = pr1 ∘ g2) + : (λ b, f (pr2 (g1 x) (transportf (λ φ, pr1hSet (B (φ x))) q1 b))) = (λ b, pr2 (g2 x) (transportf (λ φ, pr1hSet (B (φ x))) q2 b)). + Proof. + induction p. + cbn. + assert (r : q1 = q2). + { apply (setproperty (SET ⟦ X, A ⟧,, isaset_forall_hSet (pr1hSet X) (λ _, A)) (pr1 ∘ g0) (pr1 ∘ g1)). + } + induction r. + apply idpath. + Qed. + + Lemma pathtozero_cone + {c0 : SET} + {c : cochain SET} + (cc0 : cone (mapdiagram F' c) c0) + (v : nat) + : pr1 ∘ (pr1 cc0 0) = pr1 ∘ (pr1 cc0 v). + Proof. + induction v. + - apply idpath. + - symmetry. + etrans. + + apply (comp_right_eq_hset (λ x : pr1hSet (F' (dob c v)), pr1 x) (pr2 cc0 (S v) v (idpath (S v)))). + + symmetry. apply IHv. + Qed. + + Lemma pullback_cone + {c0 : SET} + (x : pr1hSet c0) + {c : cochain SET} + (cc0 : cone (mapdiagram F' c) c0) + : cone c (B (pr1 (pr1 cc0 0 x))). + Proof. + unfold cone. + unfold cone in cc0. + unfold forms_cone in cc0. + set (f := λ v : vertex conat_graph, (λ b, pr2 (pr1 cc0 v x) (transportf (λ φ, pr1hSet (B (φ x))) (pathtozero_cone cc0 v) b)) : SET ⟦ B (pr1 (pr1 cc0 0 x)), dob c v ⟧). + assert (p : forms_cone c f). + { + unfold forms_cone. + simpl. + intros u v e. + induction e. + set (p := pullback_cone_edge x (pr2 cc0 (S v) v (idpath (S v))) (pathtozero_cone cc0 (S v)) (pathtozero_cone cc0 v)). + apply p. + } + exact (f,, p). + Defined. + + Lemma exists_fun_mapdiagram + {c : cochain SET} + {L : SET} + {cc : cone c L} + (c_limcone : isLimCone c L cc) + (c0 : SET) + (cc0 : cone (mapdiagram F' c) c0) + : SET ⟦ c0, F' L ⟧. + Proof. + intro x. + cbn. + unfold polynomial_functor_obj. + set (a := pr1 (pr1 cc0 0 x) : pr1hSet A). + set (cx := B a). + set (ccx := pullback_cone x cc0). + set (f2x := pr11 (c_limcone cx ccx)). + exact (a,, f2x). + Defined. + + Lemma is_mor_mapdiagram2_point + {X Y c : UU} + (x : X) + {φ1 φ2 : X -> pr1hSet A} + {f : pr1hSet (B (φ1 x)) -> c} + {g : c -> Y} + {h : pr1hSet (B (φ2 x)) -> Y} + (q : φ1 = φ2) + (p : g ∘ f = λ b, h (transportf (λ ψ, pr1hSet (B (ψ x))) q b)) + : transportf (λ a, pr1hSet (B a) -> Y) (toforallpaths _ _ _ q x) (g ∘ f) = h. + Proof. + induction q. + apply p. + Defined. + + Lemma fun_mapdiagram_is_mor + {c : cochain SET} + {L : SET} + {cc : cone c L} + (c_limcone : isLimCone c L cc) + (c0 : SET) + (cc0 : cone (mapdiagram F' c) c0) + (f := exists_fun_mapdiagram c_limcone c0 cc0) + : is_cone_mor cc0 (mapcone F' c cc) f. + Proof. + unfold is_cone_mor. + intro v. + apply funextfun. + intro x. + use total2_paths_f. + - unfold coneOut. + unfold mapcone. + cbn. + apply (toforallpaths _ _ _ (pathtozero_cone cc0 v) x). + - cbn. + unfold coneOut. + set (a := pr1 (pr1 cc0 0 x) : pr1hSet A). + set (cx := B a). + set (ccx := pullback_cone x cc0). + set (p := pr2 (pr1 (c_limcone cx ccx)) v). + cbn in p. + unfold coneOut in p. + apply (is_mor_mapdiagram2_point x (pathtozero_cone cc0 v) p). + Qed. + + Lemma exists_mor_mapdiagram + {c : cochain SET} + {L : SET} + {cc : cone c L} + (c_limcone : isLimCone c L cc) + (c0 : SET) + (cc0 : cone (mapdiagram F' c) c0) + : ∑ f : SET ⟦ c0, F' L ⟧, is_cone_mor cc0 (mapcone F' c cc) f. + Proof. + set (f := exists_fun_mapdiagram c_limcone c0 cc0). + set (p := fun_mapdiagram_is_mor c_limcone c0 cc0). + exact (f,, p). + Defined. + + Lemma move_proof + {X Y Z : SET} + {x : pr1hSet X} + (h1 h2 : SET⟦ X, A ⟧) + (f : SET ⟦ B (h2 x), Y ⟧) + (g : SET ⟦ Y, Z ⟧ ) + (q : h1 = h2) + : g ∘ (transportf (λ a, SET ⟦ B a, Y ⟧) (pathsinv0 (toforallpaths _ _ _ q x)) f) = λ b, g (f (transportf (λ φ, pr1hSet (B (φ x))) q b)). + Proof. + induction q. + cbn. + apply idpath. + Qed. + + Lemma proj_is_cone_mor_point + {X Y Z0 Z : SET} + (x : pr1hSet X) + {f : SET ⟦ X, F' Y ⟧} + {g : SET⟦ Y, Z ⟧} + (h0 : SET⟦ X, F' Z0 ⟧) + (h1 : SET⟦ X, F' Z ⟧) + (p : #F' g ∘ f = h1) + (q : pr1 (f x) = pr1 (h0 x)) + (q' : pr1 ∘ h0 = pr1 ∘ h1) + : g ∘ (transportf _ q (pr2 (f x))) = λ b, (pr2 (h1 x)) (transportf (λ φ, pr1hSet (B (φ x))) q' b). + Proof. + induction p. + cbn. + set (q'x := toforallpaths _ _ _ q' x). + cbn in q'x. + set (q'x' := pathsinv0 q'x). + assert (r : q'x' = q) by apply (setproperty A). + induction r. + apply (move_proof (pr1 ∘ h0) (pr1 ∘ # F' g ∘ f) (pr2 (f x)) g q'). + Qed. + + Lemma proj_is_cone_mor + {c : cochain SET} + {c0 L : SET} + {x : pr1hSet c0} + {cc : cone c L} + {cc0 : cone (mapdiagram F' c) c0} + (f : SET ⟦ c0, F' L ⟧) + {p : pr1 (f x) = pr1 (pr1 cc0 0 x)} + (pf : is_cone_mor cc0 (mapcone F' c cc) f) + : is_cone_mor (pullback_cone x cc0) cc (transportf _ p (pr2 (f x))). + Proof. + set (ccx := pullback_cone x cc0). + cbn. + unfold is_cone_mor. + intro v. + unfold is_cone_mor in pf. + unfold coneOut in pf. + apply (proj_is_cone_mor_point x (pr1 cc0 0) (pr1 cc0 v) (pf v) p (pathtozero_cone cc0 v)). + Qed. + + Lemma morph_unicity_pushout + {c : cochain SET} + {c0 L : SET} + {cc : cone c L} + (c_limcone : isLimCone c L cc) + (cc0 : cone (mapdiagram F' c) c0) + {f' : SET⟦ c0, F' L ⟧} + (pf' : is_cone_mor cc0 (mapcone F' c cc) f') + : f' = pr1 (exists_mor_mapdiagram c_limcone c0 cc0). + Proof. + set (f_pf := exists_mor_mapdiagram c_limcone c0 cc0). + set (f := pr1 f_pf). + set (pf := pr2 f_pf). + apply funextfun. + intro x. + set (p := maponpaths (λ z, pr1 z) (toforallpaths _ _ _ (pf' 0) x)). + use total2_paths_f. + - unfold is_cone_mor in pf'. + unfold mapcone in pf'. + unfold coneOut in pf'. + cbn in pf'. + apply p. + - cbn. + set (a := pr1 (pr1 cc0 0 x) : pr1hSet A). + set (cx := B a). + set (ccx := pullback_cone x cc0). + set (f'2 := transportf _ p (pr2 (f' x)) : SET ⟦ cx, L ⟧). + set (f'2_cone_mor := proj_is_cone_mor f' pf' : is_cone_mor ccx cc f'2). + apply (maponpaths (λ z, pr1 z) (pr2 (c_limcone cx ccx) (f'2,, f'2_cone_mor))). + Qed. + + Lemma PolyFunctor_omega_cont : is_omega_cont F'. + Proof. + unfold is_omega_cont. + unfold preserves_limit. + unfold isLimCone. + intros c L cc c_limcone c0 cc0. + use tpair. + - exact (exists_mor_mapdiagram c_limcone c0 cc0). + - set (f_pf := exists_mor_mapdiagram c_limcone c0 cc0). + set (f := pr1 f_pf). + set (pf := pr2 f_pf). + intro t. + destruct t as [f' pf']. + use total2_paths_f. + + apply (morph_unicity_pushout c_limcone cc0 pf'). + + set (p1 := morph_unicity_pushout c_limcone cc0 pf'). + set (tpf' := transportf (is_cone_mor cc0 (mapcone F' c cc)) p1 pf'). + unfold is_cone_mor in pf. + use funextsec. + intro v. + apply (isaset_forall_hSet (pr1hSet c0) (λ _, F' (dob c v))). + Defined. + +End OmegaContinuity. diff --git a/UniMath/CategoryTheory/DisplayedCats/Codomain/CodFunctor.v b/UniMath/CategoryTheory/DisplayedCats/Codomain/CodFunctor.v index 7ddc5e543d..4be49212e4 100644 --- a/UniMath/CategoryTheory/DisplayedCats/Codomain/CodFunctor.v +++ b/UniMath/CategoryTheory/DisplayedCats/Codomain/CodFunctor.v @@ -89,6 +89,16 @@ Proof. - exact (disp_codomain_functor_axioms F). Defined. +Definition codomain_functor + {C₁ C₂ : category} + (F : C₁ ⟶ C₂) + (x : C₁) + : (C₁ / x) ⟶ (C₂ / F x). +Proof. + use fiber_functor. + use disp_codomain_functor. +Defined. + Proposition disp_codomain_fiber_functor_mor {C₁ C₂ : category} (F : C₁ ⟶ C₂) diff --git a/UniMath/CategoryTheory/DisplayedCats/Codomain/CodLeftAdjoint.v b/UniMath/CategoryTheory/DisplayedCats/Codomain/CodLeftAdjoint.v index 6464f062fb..ff092c9819 100644 --- a/UniMath/CategoryTheory/DisplayedCats/Codomain/CodLeftAdjoint.v +++ b/UniMath/CategoryTheory/DisplayedCats/Codomain/CodLeftAdjoint.v @@ -23,12 +23,14 @@ 5. The adjunction 6. The Beck-Chevalley condition 7. Dependent sums for the codomain + 8. The left adjoint is an isomorphism ***************************************************************************************) Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. +Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. @@ -531,3 +533,31 @@ Proof. - exact (λ x y f, is_right_adjoint_cod_fiber_functor HC f). - exact (λ w x y z f g h k p H, cod_left_beck_chevalley HC f g h k p H). Defined. + +(** * 8. The left adjoint is an adjoint equivalence *) +Definition functor_on_slices_iso_is_adj_equiv {C : category} {c c' : C} (i : z_iso c c') + : adj_equivalence_of_cats (comp_functor i). +Proof. + use rad_equivalence_of_cats'. + - intros [a f] [b g]. + use isweq_iso. + + intros [h ph]. + simpl in *. + exists h. + use (cancel_z_iso _ _ i). + rewrite assoc', ph. + now do 2 rewrite id_right. + + intro. + use eq_mor_cod_fib. + apply idpath. + + intro. + use eq_mor_cod_fib. + apply idpath. + - intros [a f]. + exists (a ,, f · z_iso_inv i). + use make_z_iso_in_slice. + + apply identity_z_iso. + + refine (id_left _ @ ! id_right _ @ _ @ assoc _ _ _). + apply maponpaths, pathsinv0. + apply z_iso_after_z_iso_inv. +Qed. diff --git a/UniMath/CategoryTheory/DisplayedCats/Codomain/FiberCod.v b/UniMath/CategoryTheory/DisplayedCats/Codomain/FiberCod.v index 1764845c70..82a3718fd4 100644 --- a/UniMath/CategoryTheory/DisplayedCats/Codomain/FiberCod.v +++ b/UniMath/CategoryTheory/DisplayedCats/Codomain/FiberCod.v @@ -11,6 +11,7 @@ 3. Standard objects and morphisms in the codomain 4. Calculations for codomain fiber 5. The fiber of terminal objects + 6. Builders for isomorphisms **************************************************************************************) Require Import UniMath.Foundations.All. @@ -532,3 +533,47 @@ Section CodomainFiber. := adjointification cod_fib_terminal_equivalence. End FibTerminal. End CodomainFiber. + +(** * 6. Isomorphisms builders in the slice category *) +Section IsoInSlice. + + Context {C : category} (z : C) (a b : C / z). + + Lemma make_is_z_iso_in_slice {f : C/z⟦a, b⟧} + (i : is_z_isomorphism (dom_mor f)) + : is_z_isomorphism f. + Proof. + use make_is_z_isomorphism. + - use tpair. + + exact (inv_from_z_iso (_,, i)). + + abstract ( + simpl; + refine (_ @ ! id_right _); + rewrite (! id_right _ @ ! pr2 f); + rewrite assoc; + rewrite z_iso_after_z_iso_inv; + apply id_left). + - abstract ( + split ; use eq_mor_cod_fib; + [ etrans; + [ apply transportf_cod_disp + | exact (z_iso_inv_after_z_iso (_ ,, i)) ] + | etrans ; + [ apply transportf_cod_disp + | exact (z_iso_after_z_iso_inv (_ ,, i)) ] + ]). + Defined. + + Lemma make_z_iso_in_slice + (i : z_iso (cod_dom a) (cod_dom b)) + (pf : i · cod_mor b = cod_mor a) + : z_iso a b. + Proof. + use make_z_iso'. + - exists i. + abstract (exact (pf @ ! id_right _)). + - use make_is_z_iso_in_slice. + apply i. + Defined. + +End IsoInSlice. diff --git a/UniMath/CategoryTheory/Equivalences/Core.v b/UniMath/CategoryTheory/Equivalences/Core.v index fb96b9e482..50893f0f7f 100644 --- a/UniMath/CategoryTheory/Equivalences/Core.v +++ b/UniMath/CategoryTheory/Equivalences/Core.v @@ -38,11 +38,11 @@ Local Open Scope cat. (** * Sloppy equivalence of categories *) -Definition forms_equivalence {A B : category} (X : adjunction_data A B) +Definition forms_equivalence {A B : precategory} (X : adjunction_data A B) (η := adjunit X) (ε := adjcounit X) : UU := (∏ a, is_z_isomorphism (η a)) × (∏ b, is_z_isomorphism (ε b)). -Definition make_forms_equivalence {A B : category} +Definition make_forms_equivalence {A B : precategory} (adjData : adjunction_data A B) (η := adjunit adjData) (ε := adjcounit adjData) @@ -50,25 +50,25 @@ Definition make_forms_equivalence {A B : category} (ε_iso : ∏(b : B), is_z_isomorphism (ε b)) : forms_equivalence adjData := (η_iso ,, ε_iso). -Definition equivalence_of_cats (A B : category) : UU +Definition equivalence_of_cats (A B : precategory) : UU := ∑ (X : adjunction_data A B), forms_equivalence X. Coercion adjunction_data_from_equivalence_of_cats {A B} (X : equivalence_of_cats A B) : adjunction_data A B := pr1 X. -Definition make_equivalence_of_cats {A B : category} +Definition make_equivalence_of_cats {A B : precategory} (adjData : adjunction_data A B) (eqvProp : forms_equivalence adjData) : equivalence_of_cats A B := (adjData ,, eqvProp). -Definition adjunitiso {A B : category} (X : equivalence_of_cats A B) +Definition adjunitiso {A B : precategory} (X : equivalence_of_cats A B) (a : A) : z_iso a (right_functor X (left_functor X a)). Proof. exists (adjunit X a). exact (pr1 (pr2 X) a). Defined. -Definition adjcounitiso {A B : category} (X : equivalence_of_cats A B) +Definition adjcounitiso {A B : precategory} (X : equivalence_of_cats A B) (b : B) : z_iso (left_functor X (right_functor X b)) b. Proof. exists (adjcounit X b). @@ -77,14 +77,14 @@ Defined. (** * Equivalence of (pre)categories *) -Definition adj_equivalence_of_cats {A B : category} (F : functor A B) : UU := +Definition adj_equivalence_of_cats {A B : precategory} (F : functor A B) : UU := ∑ (H : is_left_adjoint F), forms_equivalence H. -Definition adj_from_equiv (D1 D2 : category) (F : functor D1 D2): +Definition adj_from_equiv (D1 D2 : precategory) (F : functor D1 D2): adj_equivalence_of_cats F → is_left_adjoint F := λ x, pr1 x. Coercion adj_from_equiv : adj_equivalence_of_cats >-> is_left_adjoint. -Definition make_adj_equivalence_of_cats {A B : category} (F : functor A B) +Definition make_adj_equivalence_of_cats {A B : precategory} (F : functor A B) (G : functor B A) η ε (H1 : form_adjunction F G η ε) (H2 : forms_equivalence ((F,,G,,η,,ε))) @@ -97,7 +97,7 @@ Defined. Section MakeAdjEquivalenceOfCats'. - Context {A B : category}. + Context {A B : precategory}. Context (F : functor A B). Context (G : functor B A). Context (η : functor_identity B ⟹ G ∙ F). @@ -205,7 +205,7 @@ Section MakeAdjEquivalenceOfCats'. End MakeAdjEquivalenceOfCats'. Definition adj_equivalence_from_right_adjoint - {A B : category} + {A B : precategory} (F : functor A B) (H1 : is_right_adjoint F) (H2 : ∏ a, is_z_isomorphism ((unit_from_right_adjoint H1) a)) @@ -220,7 +220,7 @@ Definition adj_equivalence_from_right_adjoint H2 H3. -Definition adj_equivalence_inv {A B : category} +Definition adj_equivalence_inv {A B : precategory} {F : functor A B} (HF : adj_equivalence_of_cats F) : functor B A := right_adjoint HF. @@ -280,7 +280,7 @@ End Accessors. Section Inverse. - Context {A B : category}. + Context {A B : precategory}. Context (F : functor A B). Context (H : adj_equivalence_of_cats F). diff --git a/UniMath/CategoryTheory/Limits/BinCoproducts.v b/UniMath/CategoryTheory/Limits/BinCoproducts.v index ee9dd1dbd4..18d3d39610 100644 --- a/UniMath/CategoryTheory/Limits/BinCoproducts.v +++ b/UniMath/CategoryTheory/Limits/BinCoproducts.v @@ -233,6 +233,16 @@ Proof. apply (base_paths _ _ X'). Qed. +Lemma BinCoproduct_of_identities {a b : C} (CC : BinCoproduct a b) + : BinCoproductOfArrows CC CC (identity a) (identity b) = identity CC. +Proof. + apply pathsinv0, BinCoproduct_endo_is_identity. + - etrans. { apply BinCoproductOfArrowsIn1. } + apply id_left. + - etrans. { apply BinCoproductOfArrowsIn2. } + apply id_left. +Qed. + Definition from_BinCoproduct_to_BinCoproduct {a b : C} (CC CC' : BinCoproduct a b) : BinCoproductObject CC --> BinCoproductObject CC'. Proof. diff --git a/UniMath/CategoryTheory/WeakEquivalences/Coequalizers.v b/UniMath/CategoryTheory/WeakEquivalences/Coequalizers.v index f4c469151a..a6f1859497 100644 --- a/UniMath/CategoryTheory/WeakEquivalences/Coequalizers.v +++ b/UniMath/CategoryTheory/WeakEquivalences/Coequalizers.v @@ -9,6 +9,7 @@ 1. Preservation [weak_equiv_preserves_coequalizers, weak_equiv_preserves_chosen_coequalizers] 2. Reflection [weak_equiv_reflects_coequalizers] 3. Lift Preservation [weak_equiv_lifts_preserves_coequalizers] + 4. Creation [weak_equiv_creates_coequalizers] Remark: These results are an immediate consequence of the fact that the dual statement hold and that the opposite of a weak equivalence is again a weak equivalence. *) @@ -27,6 +28,7 @@ Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.WeakEquivalences.Core. Require Import UniMath.CategoryTheory.WeakEquivalences.Opp. Require Import UniMath.CategoryTheory.WeakEquivalences.Preservation.Equalizers. +Require Import UniMath.CategoryTheory.WeakEquivalences.Creation.Equalizers. Require Import UniMath.CategoryTheory.WeakEquivalences.Reflection.Equalizers. Require Import UniMath.CategoryTheory.WeakEquivalences.LiftPreservation.Equalizers. @@ -113,9 +115,42 @@ Section WeakEquivLiftPreservationCoequalizers. Proof. use (invweq (preserves_coequalizer_opp H)). set (oF_pe := pr1weq (preserves_coequalizer_opp F) Feq). - use (weak_equiv_lifts_preserves_equalizers oC₂ oC₃ + use (weak_equiv_lifts_preserves_equalizers (F := functor_op F) _ (opp_is_weak_equiv Gw) oF_pe). exact (nat_z_iso_inv (make_nat_z_iso _ _ _ (op_nt_is_z_iso α (pr2 α)))). Qed. End WeakEquivLiftPreservationCoequalizers. + +(** * 4. Creation *) +Proposition weak_equiv_creates_coequalizers + {C D : category} {F : C ⟶ D} (Fw : is_weak_equiv F) + (D_univ : is_univalent D) (coeq : Coequalizers C) + : Coequalizers D. +Proof. + intros d₁ d₂ f' g'. + use (factor_through_squash _ _ (eso_from_weak_equiv _ Fw d₁)). + { apply isaprop_Coequalizer, D_univ. } + intros [c₁ i₁]. + use (factor_through_squash _ _ (eso_from_weak_equiv _ Fw d₂)). + { apply isaprop_Coequalizer, D_univ. } + intros [c₂ i₂]. + + set (f := fully_faithful_inv_hom (pr2 Fw) _ _ (i₁ · f' · z_iso_inv i₂)). + set (g := fully_faithful_inv_hom (pr2 Fw) _ _ (i₁ · g' · z_iso_inv i₂)). + + set (coeq_fg := weak_equiv_preserves_coequalizer Fw f g (coeq _ _ f g)). + use (coequalizer_stable_under_iso _ _ _ _ _ _ coeq_fg). + - exact (z_iso_inv i₁). + - exact (z_iso_inv i₂). + - abstract ( + unfold f ; rewrite functor_on_fully_faithful_inv_hom; + do 2 rewrite assoc; + simpl ; rewrite z_iso_after_z_iso_inv; + now rewrite id_left). + - abstract ( + unfold g ; rewrite functor_on_fully_faithful_inv_hom; + do 2 rewrite assoc; + simpl ; rewrite z_iso_after_z_iso_inv; + now rewrite id_left). +Defined. diff --git a/UniMath/CategoryTheory/WeakEquivalences/Core.v b/UniMath/CategoryTheory/WeakEquivalences/Core.v index b0df3adcf1..368eba9ab5 100644 --- a/UniMath/CategoryTheory/WeakEquivalences/Core.v +++ b/UniMath/CategoryTheory/WeakEquivalences/Core.v @@ -1,14 +1,19 @@ (** -Section ``WeakEquivalences'' contains: - 1. the definition of a weak equivalence (i.e., essentially surjective and fully faithful); - 2. together with accessors; - 3. a proof that ``is a weak equivalence'' is a proposition; - 4. a proof that every identity functor (resp. the composite of weak equivalences) is a weak equivalence + The basics of weak equivalences -Section ``WeakEquivalenceInducesIsoOnUnivalentFunctorCategories'' contains a proof for the statement: -Let H : C → D be a weak equivalence (between not-necesssarily univalent categories) and E a univalent category. -Then, the functor (H · -) : [D, E] → [C, E] is an isomorphism of (univalent) categories; and hence an isomorphism. + Contents. + 1. Section ``WeakEquivalences'' contains: + - the definition of a weak equivalence (i.e., essentially surjective and fully faithful); + - together with accessors; + - a proof that ``is a weak equivalence'' is a proposition; + - a proof that every identity functor (resp. the composite of weak equivalences) is a weak equivalence + + 2. Section ``WeakEquivalenceInducesIsoOnUnivalentFunctorCategories'' contains a proof for the statement: + Let H : C → D be a weak equivalence (between not-necesssarily univalent categories) and E a univalent category. + Then, the functor (H · -) : [D, E] → [C, E] is an isomorphism of (univalent) categories; and hence an isomorphism. + + 3. Section ``WeakAndAdjointEquivalences'' contains relations between weak and adjoint equivalences *) @@ -19,6 +24,9 @@ Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. +Require Import UniMath.CategoryTheory.Equivalences.Core. +Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful. + Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.whiskering. @@ -109,3 +117,29 @@ Section WeakEquivalenceInducesIsoOnUnivalentFunctorCategories. Defined. End WeakEquivalenceInducesIsoOnUnivalentFunctorCategories. + +Section WeakAndAdjointEquivalences. + + Context {A B : category} {F : A ⟶ B}. + + Lemma rad_equivalence_of_cats'' + (A_univ : is_univalent A) + (F_weq : is_weak_equiv F) + : adj_equivalence_of_cats F. + Proof. + apply rad_equivalence_of_cats. + - exact A_univ. + - apply F_weq. + - apply F_weq. + Defined. + + Lemma weak_equiv_from_equiv + (Fe : adj_equivalence_of_cats F) + : is_weak_equiv F. + Proof. + split. + - apply functor_from_equivalence_is_essentially_surjective, Fe. + - apply fully_faithful_from_equivalence, Fe. + Qed. + +End WeakAndAdjointEquivalences. diff --git a/UniMath/CategoryTheory/WeakEquivalences/LiftPreservation/BinProducts.v b/UniMath/CategoryTheory/WeakEquivalences/LiftPreservation/BinProducts.v index 70f0d3464d..56654a4527 100644 --- a/UniMath/CategoryTheory/WeakEquivalences/LiftPreservation/BinProducts.v +++ b/UniMath/CategoryTheory/WeakEquivalences/LiftPreservation/BinProducts.v @@ -25,8 +25,7 @@ Require Import UniMath.CategoryTheory.WeakEquivalences.Preservation.Binproducts. Local Open Scope cat. Lemma weak_equiv_lifts_preserves_binproducts - {C1 : category} - (C2 C3 : univalent_category) + {C1 C2 C3 : category} {F : C1 ⟶ C3} {G : C1 ⟶ C2} {H : C2 ⟶ C3} diff --git a/UniMath/CategoryTheory/WeakEquivalences/LiftPreservation/Equalizers.v b/UniMath/CategoryTheory/WeakEquivalences/LiftPreservation/Equalizers.v index ca1379b980..bacafd4067 100644 --- a/UniMath/CategoryTheory/WeakEquivalences/LiftPreservation/Equalizers.v +++ b/UniMath/CategoryTheory/WeakEquivalences/LiftPreservation/Equalizers.v @@ -26,8 +26,7 @@ Local Open Scope cat. Section LiftAlongWeakEquivalencePreservesEqualizers. - Context {C1 : category} - (C2 C3 : univalent_category) + Context {C1 C2 C3 : category} {F : C1 ⟶ C3} {G : C1 ⟶ C2} {H : C2 ⟶ C3} diff --git a/UniMath/CategoryTheory/WeakEquivalences/LiftPreservation/Exponentials.v b/UniMath/CategoryTheory/WeakEquivalences/LiftPreservation/Exponentials.v index 15d4d1453e..88d4a963c7 100644 --- a/UniMath/CategoryTheory/WeakEquivalences/LiftPreservation/Exponentials.v +++ b/UniMath/CategoryTheory/WeakEquivalences/LiftPreservation/Exponentials.v @@ -77,7 +77,7 @@ Section WeakEquivLiftsExponentialPreservation. (F_pE : preserves_exponential_objects P₁ P₃ F_pP). Let H_pP : preserves_binproduct H - := weak_equiv_lifts_preserves_binproducts C₂ C₃ α G_weq F_pP. + := weak_equiv_lifts_preserves_binproducts α G_weq F_pP. Let G_pP : preserves_binproduct G := weak_equiv_preserves_binproducts G_weq. @@ -398,7 +398,7 @@ Lemma weak_equiv_lifts_preserves_exponentials' (G_weq : is_weak_equiv G) {F_pP : preserves_binproduct F} (F_pE : preserves_exponentials E₁ E₃ F_pP) - : preserves_exponentials E₂ E₃ (weak_equiv_lifts_preserves_binproducts C₂ C₃ α G_weq F_pP). + : preserves_exponentials E₂ E₃ (weak_equiv_lifts_preserves_binproducts α G_weq F_pP). Proof. use weak_equiv_lifts_preserves_exponentials. { exact P₁. } diff --git a/UniMath/CategoryTheory/WeakEquivalences/LiftPreservation/Pullbacks.v b/UniMath/CategoryTheory/WeakEquivalences/LiftPreservation/Pullbacks.v index 59413cd66d..6b04b3ae2d 100644 --- a/UniMath/CategoryTheory/WeakEquivalences/LiftPreservation/Pullbacks.v +++ b/UniMath/CategoryTheory/WeakEquivalences/LiftPreservation/Pullbacks.v @@ -26,8 +26,7 @@ Local Open Scope cat. Section LiftAlongWeakEquivalencePreservesPullbacks. - Context {C1 : category} - (C2 C3 : univalent_category) + Context {C1 C2 C3 : category} {F : C1 ⟶ C3} {G : C1 ⟶ C2} {H : C2 ⟶ C3} diff --git a/UniMath/CategoryTheory/WeakEquivalences/Preservation/Bincoproducts.v b/UniMath/CategoryTheory/WeakEquivalences/Preservation/Bincoproducts.v index 3027f8016b..d74172b34a 100644 --- a/UniMath/CategoryTheory/WeakEquivalences/Preservation/Bincoproducts.v +++ b/UniMath/CategoryTheory/WeakEquivalences/Preservation/Bincoproducts.v @@ -143,3 +143,23 @@ Proof. use (weak_equiv_preserves_bincoproducts Fw). apply isBinCoproduct_BinCoproduct. Qed. + +Proposition weak_equiv_creates_bincoproducts + {C D : category} {F : C ⟶ D} (Fw : is_weak_equiv F) (BP : BinCoproducts C) + (D_univ : is_univalent D) + : BinCoproducts D. +Proof. + intros d₁ d₂. + + use (factor_through_squash _ _ (eso_from_weak_equiv _ Fw d₁)). + { apply isaprop_BinCoproduct, D_univ. } + intros [c₁ i₁]. + use (factor_through_squash _ _ (eso_from_weak_equiv _ Fw d₂)). + { apply isaprop_BinCoproduct, D_univ. } + intros [c₂ i₂]. + + use (bincoproduct_of_isos _ i₁ i₂). + apply preserves_bincoproduct_to_bincoproduct. + - apply weak_equiv_preserves_bincoproducts, Fw. + - apply BP. +Defined. diff --git a/UniMath/CategoryTheory/WeakEquivalences/Slice.v b/UniMath/CategoryTheory/WeakEquivalences/Slice.v new file mode 100644 index 0000000000..ad471a3da6 --- /dev/null +++ b/UniMath/CategoryTheory/WeakEquivalences/Slice.v @@ -0,0 +1,107 @@ +(** + Rezk Completion Of Slice Categories + + In this file, we show that any weak equivalence induces a weak equivalence between the slices. + That is, if F : C₀ → C₁ is a weak equivalence, then for every x : C₀ there is a weak equivalence F^(x) : C₀/x → C₁/F(x). + Consequently, if C₁ is univalent, then C₁/F(x) is the Rezk completion of C₀/x. + + Contents + 1. Proof that F^(x) is a weak equivalence if F is a weak equivalence [functor_to_functor_on_slice_is_weq] + *) + +Require Import UniMath.Foundations.All. +Require Import UniMath.MoreFoundations.All. +Require Import UniMath.CategoryTheory.Core.Prelude. +Require Import UniMath.CategoryTheory.WeakEquivalences.Core. +Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. +Require Import UniMath.CategoryTheory.DisplayedCats.Functors. +Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. +Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. +Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodFunctor. + +Local Open Scope cat. + +(** * 1. Rezk Completion For Slice Categories *) +Section RezkCompletionOfSliceCategories. + + Context {C₀ C₁ : category} {F : functor C₀ C₁} (x : C₀). + + Lemma functor_to_functor_on_slice_is_ff + (Ff : fully_faithful F) + : fully_faithful (codomain_functor F x). + Proof. + intros a b. + use isweq_iso. + - intro f. + exists (fully_faithful_inv_hom Ff _ _ (pr1 f)). + abstract ( + apply (faithful_reflects_morphism_equality _ Ff); + do 2 rewrite functor_comp; + rewrite functor_on_fully_faithful_inv_hom; + rewrite functor_id; + apply (pr2 f)). + - intro f. + use subtypePath. + { intro ; apply homset_property. } + apply (faithful_reflects_morphism_equality _ Ff). + etrans. { apply functor_on_fully_faithful_inv_hom. } + etrans. { apply (@pr1_transportf (C₁⟦_,_⟧) (λ _, C₁⟦_,_⟧)). } + now rewrite transportf_const. + - intro f. + use subtypePath. + { intro ; apply homset_property. } + etrans. { apply (@pr1_transportf (C₁⟦_,_⟧) (λ _, C₁⟦_,_⟧)). } + rewrite transportf_const. + apply functor_on_fully_faithful_inv_hom. + Qed. + + (* observe that fully faithfulness is needed to prove essential surjectivity *) + Lemma functor_to_functor_on_slice_is_eso + (F_weq : is_weak_equiv F) + : essentially_surjective (codomain_functor F x). + Proof. + intros [b₁ f₁]. + use (factor_through_squash _ _ (eso_from_weak_equiv _ F_weq b₁)). + { apply isapropishinh. } + intros [b₀ f₀]. + apply hinhpr. + simple refine (_ ,, (_ ,, _)). + - exact (b₀ ,, fully_faithful_inv_hom (pr2 F_weq) _ _ (f₀ · f₁)). + - exists f₀. + rewrite id_right. + apply pathsinv0, functor_on_fully_faithful_inv_hom. + - use make_is_z_isomorphism. + + exists (z_iso_inv f₀). + cbn ; rewrite id_right. + etrans. + { apply maponpaths, functor_on_fully_faithful_inv_hom. } + rewrite assoc. + etrans. { apply maponpaths_2, z_iso_after_z_iso_inv. } + apply id_left. + + split ; (use subtypePath; + [ intro ; apply homset_property | + etrans ; [ apply (@pr1_transportf (C₁⟦_,_⟧) (λ _, C₁⟦_,_⟧)) | ]; + rewrite transportf_const; + apply z_iso_inv_after_z_iso]). + Qed. + + Lemma functor_to_functor_on_slice_is_weq + (F_weq : is_weak_equiv F) + : is_weak_equiv (codomain_functor F x). + Proof. + split. + - apply functor_to_functor_on_slice_is_eso, F_weq. + - apply functor_to_functor_on_slice_is_ff, F_weq. + Defined. + + Lemma Rezk_of_slice + (F_weq : is_weak_equiv F) + : weak_equiv (C₀ / x) (C₁ / F x). + Proof. + simple refine (_ ,, (_ ,, _)). + - exact (codomain_functor F x). + - apply functor_to_functor_on_slice_is_eso, F_weq. + - apply functor_to_functor_on_slice_is_ff, F_weq. + Defined. + +End RezkCompletionOfSliceCategories. diff --git a/UniMath/CategoryTheory/WeakEquivalences/TwoOutOfThree.v b/UniMath/CategoryTheory/WeakEquivalences/TwoOutOfThree.v new file mode 100644 index 0000000000..c5d4e2c93e --- /dev/null +++ b/UniMath/CategoryTheory/WeakEquivalences/TwoOutOfThree.v @@ -0,0 +1,107 @@ +(* + A (partial) 2-out-of-3 law for weak equivalences + + Let α : F ≅ G · H be a triangle of functors. + If F and G are weak equivalences, then so is H. + + Contents. + 1. [two_out_of_three_weak_equiv] proves that H is a weak equivalence. + + *) + +Require Import UniMath.Foundations.All. +Require Import UniMath.MoreFoundations.All. +Require Import UniMath.CategoryTheory.Core.Prelude. +Require Import UniMath.CategoryTheory.WeakEquivalences.Core. + +Local Open Scope cat. + +Section TwoOutOfThree. + + Context {C D E : category} (F : functor C E) (G : functor C D) (H : functor D E) + (α : nat_z_iso F (functor_composite G H)). + + Lemma two_out_of_three_eso + : essentially_surjective F → essentially_surjective G → essentially_surjective H. + Proof. + intros Fe Ge. + intro e. + use (factor_through_squash _ _ (Fe e)). + { apply isapropishinh. } + intros [c i]. + + apply hinhpr. + exists (G c). + exact (z_iso_inv (z_iso_comp (z_iso_inv i) (nat_z_iso_pointwise_z_iso α c))). + Defined. + + Lemma two_out_of_three_ff + : fully_faithful F → is_weak_equiv G → fully_faithful H. + Proof. + intros Ff Gf. + intros d₁ d₂. + + use (factor_through_squash _ _ (pr1 Gf d₁)). + { apply isapropisweq. } + intros [c₁ i₁]. + use (factor_through_squash _ _ (pr1 Gf d₂)). + { apply isapropisweq. } + intros [c₂ i₂]. + + set (α₁ := (nat_z_iso_pointwise_z_iso α c₁)). + set (α₂ := (nat_z_iso_pointwise_z_iso α c₂)). + + use isweq_iso. + - intro f_E. + set (f_C := fully_faithful_inv_hom Ff _ _ (α₁ · #H i₁ · f_E · #H (z_iso_inv i₂) · z_iso_inv α₂)). + exact (z_iso_inv i₁ · #G f_C · i₂). + - intro f_D. + use z_iso_inv_to_right. + use z_iso_inv_on_right. + etrans. + 2: { apply (functor_on_fully_faithful_inv_hom _ (pr2 Gf)). } + apply maponpaths. + use (faithful_reflects_morphism_equality _ (Ff)). + etrans. { apply functor_on_fully_faithful_inv_hom. } + apply pathsinv0. + use z_iso_inv_on_left. + rewrite ! assoc'. + apply pathsinv0. + use z_iso_inv_to_left. + etrans. { + apply maponpaths, (nat_trans_ax α). + } + rewrite assoc. + rewrite z_iso_after_z_iso_inv. + rewrite id_left. + simpl. + rewrite functor_on_fully_faithful_inv_hom. + now rewrite ! functor_comp. + - intro f_E. + simpl. + rewrite ! functor_comp. + + use (z_iso_inv_to_right _ _ _ _ (functor_on_z_iso H i₂)). + use (z_iso_inv_on_right _ _ _ (functor_on_z_iso H i₁)). + cbn. + + use (cancel_z_iso' α₁). + etrans. { apply pathsinv0, (nat_trans_ax α). } + etrans. { + apply maponpaths_2, functor_on_fully_faithful_inv_hom. + } + rewrite ! assoc'. + rewrite z_iso_after_z_iso_inv. + now rewrite id_right. + Qed. + + Corollary two_out_of_three_weak_equiv + : is_weak_equiv F → is_weak_equiv G → is_weak_equiv H. + Proof. + intros [Fe Ff] GG. + split. + - exact (two_out_of_three_eso Fe (pr1 GG)). + - exact (two_out_of_three_ff Ff GG). + Qed. + +End TwoOutOfThree. diff --git a/UniMath/Combinatorics/.package/files b/UniMath/Combinatorics/.package/files index 3ec023bb6f..8a4654c14a 100644 --- a/UniMath/Combinatorics/.package/files +++ b/UniMath/Combinatorics/.package/files @@ -2,6 +2,9 @@ StandardFiniteSets.v Vectors.v VectorsTests.v Lists.v +FVectors.v +FMatrices.v +FLists.v FiniteSets.v KFiniteTypes.v KFiniteSubtypes.v @@ -11,7 +14,6 @@ GraphPaths.v Equivalence_Relations.v WellFoundedRelations.v ZFstructures.v -FiniteSequences.v BoundedSearch.v MetricTree.v Tests.v diff --git a/UniMath/Combinatorics/FiniteSequences.v b/UniMath/Combinatorics/FLists.v similarity index 77% rename from UniMath/Combinatorics/FiniteSequences.v rename to UniMath/Combinatorics/FLists.v index 5633da59e5..086f51f03a 100644 --- a/UniMath/Combinatorics/FiniteSequences.v +++ b/UniMath/Combinatorics/FLists.v @@ -1,205 +1,23 @@ (** * Finite sequences -Vectors and matrices defined in March 2018 by Langston Barrett (@siddharthist). +Defined in March 2018 by Langston Barrett (@siddharthist). *) (** ** Contents - - Vectors - - Matrices - - Sequences - - Definitions - - Lemmas + Sequences + - Definitions + - Lemmas *) -Require Export UniMath.Combinatorics.FiniteSets. -Require Export UniMath.Combinatorics.Lists. -Require Import UniMath.Combinatorics.Vectors. - -Require Import UniMath.MoreFoundations.PartA. +Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. -Local Open Scope transport. - -(** ** Vectors *) - -(** A [Vector] of length n with values in X is an ordered n-tuple of elements of X, - encoded here as a function ⟦n⟧ → X. *) -Definition Vector (X : UU) (n : nat) : UU := stn n -> X. - -(** hlevel of vectors *) -Lemma vector_hlevel (X : UU) (n : nat) {m : nat} (ism : isofhlevel m X) : - isofhlevel m (Vector X n). -Proof. - apply impred; auto. -Defined. - -(** Constant vector *) -Definition const_vec {X : UU} {n : nat} (x : X) : Vector X n := λ _, x. - -(** The unique empty vector *) -Definition iscontr_vector_0 X : iscontr (Vector X 0). -Proof. - intros. apply (@iscontrweqb _ (empty -> X)). - - apply invweq. apply weqbfun. apply weqstn0toempty. - - apply iscontrfunfromempty. -Defined. - -Definition empty_vec {X : UU} : Vector X 0 := iscontrpr1 (iscontr_vector_0 X). - -(** Every type is equivalent to vectors of length 1 on that type. *) -Lemma weq_vector_1 {X : UU} : X ≃ Vector X 1. - intermediate_weq (unit → X). - - apply invweq, weqfunfromunit. - - apply weqbfun. - exact weqstn1tounit. -Defined. - -Section Append. - - Context {X : UU} {n : nat} (vec : Vector X n) (x : X). - - Definition append_vec : Vector X (S n). - Proof. - intros i. - induction (natlehchoice4 (pr1 i) n (pr2 i)) as [c|d]. - - exact (vec (pr1 i,,c)). - - exact x. - Defined. - - Definition append_vec_compute_1 i : append_vec (dni lastelement i) = vec i. - Proof. - intros. - induction i as [i b]; simpl. - rewrite replace_dni_last. - unfold append_vec; simpl. - induction (natlehchoice4 i n (natlthtolths i n b)) as [p|p]. - - simpl. apply maponpaths. apply isinjstntonat; simpl. reflexivity. - - simpl. destruct p. induction (isirreflnatlth i b). - Defined. - - Definition append_vec_compute_2 : append_vec lastelement = x. - Proof. - intros; unfold append_vec; simpl. - induction (natlehchoice4 n n (natgthsnn n)) as [a|a]; simpl. - - contradicts a (isirreflnatlth n). - - reflexivity. - Defined. - -End Append. - -Lemma drop_and_append_vec {X n} (x : Vector X (S n)) : - append_vec (x ∘ dni_lastelement) (x lastelement) = x. -Proof. - intros. - apply funextfun; intros [i b]. - simpl. - induction (natlehchoice4 i n b) as [p|p]. - - simpl. - unfold append_vec. simpl. - induction (natlehchoice4 i n b) as [q|q]. - + simpl. apply maponpaths. apply isinjstntonat; simpl. reflexivity. - + induction q. contradicts p (isirreflnatlth i). - - induction p. - unfold append_vec; simpl. - induction (natlehchoice4 i i b) as [r|r]. - * simpl. apply maponpaths. - apply isinjstntonat; simpl. reflexivity. - * simpl. apply maponpaths. apply isinjstntonat; simpl. reflexivity. -Defined. - -(** An induction principle for vectors: If a statement is true for the empty - vector, and if it is true for vectors of length n it is also true for those - of length S n, then it is true for all vectors. - *) -Definition Vector_rect {X : UU} {P : ∏ n, Vector X n -> UU} - (p0 : P 0 empty_vec) - (ind : ∏ (n : nat) (vec : Vector X n) (x : X), - P n vec -> P (S n) (append_vec vec x)) - {n : nat} (vec : Vector X n) : P n vec. -Proof. - intros. - induction n as [|n IH]. - - refine (transportf (P 0) _ p0). - apply proofirrelevancecontr, iscontr_vector_0. - - exact (transportf (P _) (drop_and_append_vec vec) - (ind _ (vec ∘ dni_lastelement) - (vec lastelement) - (IH (vec ∘ dni_lastelement)))). -Defined. - -Section Lemmas. - - Context {X : UU} {n : nat}. - - Definition vectorEquality {m : nat} (f : Vector X n) (g : Vector X m) (p : n = m) : - (∏ i, f i = g (transportf stn p i)) - -> transportf (Vector X) p f = g. - Proof. - intro. - induction p. - apply funextfun. - assumption. - Defined. - - Definition tail (vecsn : Vector X (S n)) : Vector X n := - vecsn ∘ dni (0,, natgthsn0 n). - - (** It doesn't matter what the proofs are in the stn inputs. *) - Definition vector_stn_proofirrelevance {vec : Vector X n} - {i j : stn n} : (stntonat _ i = stntonat _ j) -> vec i = vec j. - Proof. - intro. - apply maponpaths, isinjstntonat; assumption. - Defined. -End Lemmas. - -(** ** Matrices *) - -Local Open Scope stn. - -(** An m × n matrix is an m-length vector of n-length vectors (rows). -<< - <--- n ---> - | [ * * * * ] - m [ * * * * ] - | [ * * * * ] ->> - Since [Vector]s are encoded as functions ⟦n⟧ → X, a matrix is a function (of - two arguments). Thus, the (i, j)-entry of a matrix Mat is simply Mat i j. - *) -Definition Matrix (X : UU) (m n : nat) : UU := Vector (Vector X n) m. - -(** The transpose is obtained by flipping the arguments. *) -Definition transpose {X : UU} {n m : nat} (mat : Matrix X m n) : Matrix X n m := - flip mat. - -Definition row {X : UU} {m n : nat} (mat : Matrix X m n) : ⟦ m ⟧ → Vector X n := mat. - -Definition col {X : UU} {m n : nat} (mat : Matrix X m n) : ⟦ n ⟧ → Vector X m := transpose mat. - -Definition row_vec {X : UU} {n : nat} (vec : Vector X n) : Matrix X 1 n := - λ i j, vec j. - -Definition col_vec {X : UU} {n : nat} (vec : Vector X n) : Matrix X n 1 := - λ i j, vec i. - -(** hlevel of matrices *) -Lemma matrix_hlevel (X : UU) (n m : nat) {o : nat} (ism : isofhlevel o X) : - isofhlevel o (Matrix X n m). -Proof. - do 2 apply vector_hlevel; assumption. -Defined. - -(** Constant matrix *) -Definition const_matrix {X : UU} {n m : nat} (x : X) : Matrix X n m := - const_vec (const_vec x). - -(** Every type is equivalent to 1 × 1 matrices on that type. *) -Lemma weq_matrix_1_1 {X : UU} : X ≃ Matrix X 1 1. - intermediate_weq (Vector X 1); apply weq_vector_1. -Defined. +Require Import UniMath.Combinatorics.FiniteSets. +Require Import UniMath.Combinatorics.Lists. +Require Import UniMath.Combinatorics.Vectors. +Require Import UniMath.Combinatorics.FVectors. (** ** Sequences *) diff --git a/UniMath/Combinatorics/FMatrices.v b/UniMath/Combinatorics/FMatrices.v new file mode 100644 index 0000000000..bd2074c632 --- /dev/null +++ b/UniMath/Combinatorics/FMatrices.v @@ -0,0 +1,62 @@ +(** * Finite sequences + +Matrices defined in March 2018 by Langston Barrett (@siddharthist). + *) + +(** ** Contents + + Matrices + + *) + +Require Import UniMath.Foundations.All. +Require Import UniMath.MoreFoundations.PartA. + +Require Import UniMath.Combinatorics.StandardFiniteSets. +Require Import UniMath.Combinatorics.FVectors. + +(** ** Matrices *) + +Local Open Scope stn. + +(** An m × n matrix is an m-length vector of n-length vectors (rows). +<< + <--- n ---> + | [ * * * * ] + m [ * * * * ] + | [ * * * * ] +>> + Since [Vector]s are encoded as functions ⟦n⟧ → X, a matrix is a function (of + two arguments). Thus, the (i, j)-entry of a matrix Mat is simply Mat i j. + *) +Definition Matrix (X : UU) (m n : nat) : UU := Vector (Vector X n) m. + +(** The transpose is obtained by flipping the arguments. *) +Definition transpose {X : UU} {n m : nat} (mat : Matrix X m n) : Matrix X n m := + flip mat. + +Definition row {X : UU} {m n : nat} (mat : Matrix X m n) : ⟦ m ⟧ → Vector X n := mat. + +Definition col {X : UU} {m n : nat} (mat : Matrix X m n) : ⟦ n ⟧ → Vector X m := transpose mat. + +Definition row_vec {X : UU} {n : nat} (vec : Vector X n) : Matrix X 1 n := + λ i j, vec j. + +Definition col_vec {X : UU} {n : nat} (vec : Vector X n) : Matrix X n 1 := + λ i j, vec i. + +(** hlevel of matrices *) +Lemma matrix_hlevel (X : UU) (n m : nat) {o : nat} (ism : isofhlevel o X) : + isofhlevel o (Matrix X n m). +Proof. + do 2 apply vector_hlevel; assumption. +Defined. + +(** Constant matrix *) +Definition const_matrix {X : UU} {n m : nat} (x : X) : Matrix X n m := + const_vec (const_vec x). + +(** Every type is equivalent to 1 × 1 matrices on that type. *) +Lemma weq_matrix_1_1 {X : UU} : X ≃ Matrix X 1 1. + intermediate_weq (Vector X 1); apply weq_vector_1. +Defined. diff --git a/UniMath/Combinatorics/FVectors.v b/UniMath/Combinatorics/FVectors.v new file mode 100644 index 0000000000..feeb2f02a2 --- /dev/null +++ b/UniMath/Combinatorics/FVectors.v @@ -0,0 +1,146 @@ +(** * Finite sequences + +Vectors defined in March 2018 by Langston Barrett (@siddharthist). + *) + +(** ** Contents + + Vectors + + *) + +Require Import UniMath.Foundations.All. +Require Import UniMath.Combinatorics.StandardFiniteSets. + +(** ** Vectors *) + +(** A [Vector] of length n with values in X is an ordered n-tuple of elements of X, + encoded here as a function ⟦n⟧ → X. *) +Definition Vector (X : UU) (n : nat) : UU := stn n -> X. + +(** hlevel of vectors *) +Lemma vector_hlevel (X : UU) (n : nat) {m : nat} (ism : isofhlevel m X) : + isofhlevel m (Vector X n). +Proof. + apply impred; auto. +Defined. + +(** Constant vector *) +Definition const_vec {X : UU} {n : nat} (x : X) : Vector X n := λ _, x. + +(** The unique empty vector *) +Definition iscontr_vector_0 X : iscontr (Vector X 0). +Proof. + intros. apply (@iscontrweqb _ (empty -> X)). + - apply invweq. apply weqbfun. apply weqstn0toempty. + - apply iscontrfunfromempty. +Defined. + +Definition empty_vec {X : UU} : Vector X 0 := iscontrpr1 (iscontr_vector_0 X). + +(** Every type is equivalent to vectors of length 1 on that type. *) +Lemma weq_vector_1 {X : UU} : X ≃ Vector X 1. + intermediate_weq (unit → X). + - apply invweq, weqfunfromunit. + - apply weqbfun. + exact weqstn1tounit. +Defined. + +Section Append. + + Context {X : UU} {n : nat} (vec : Vector X n) (x : X). + + Definition append_vec : Vector X (S n). + Proof. + intros i. + induction (natlehchoice4 (pr1 i) n (pr2 i)) as [c|d]. + - exact (vec (pr1 i,,c)). + - exact x. + Defined. + + Definition append_vec_compute_1 i : append_vec (dni lastelement i) = vec i. + Proof. + intros. + induction i as [i b]; simpl. + rewrite replace_dni_last. + unfold append_vec; simpl. + induction (natlehchoice4 i n (natlthtolths i n b)) as [p|p]. + - simpl. apply maponpaths. apply isinjstntonat; simpl. reflexivity. + - simpl. destruct p. induction (isirreflnatlth i b). + Defined. + + Definition append_vec_compute_2 : append_vec lastelement = x. + Proof. + intros; unfold append_vec; simpl. + induction (natlehchoice4 n n (natgthsnn n)) as [a|a]; simpl. + - contradicts a (isirreflnatlth n). + - reflexivity. + Defined. + +End Append. + +Lemma drop_and_append_vec {X n} (x : Vector X (S n)) : + append_vec (x ∘ dni_lastelement) (x lastelement) = x. +Proof. + intros. + apply funextfun; intros [i b]. + simpl. + induction (natlehchoice4 i n b) as [p|p]. + - simpl. + unfold append_vec. simpl. + induction (natlehchoice4 i n b) as [q|q]. + + simpl. apply maponpaths. apply isinjstntonat; simpl. reflexivity. + + induction q. contradicts p (isirreflnatlth i). + - induction p. + unfold append_vec; simpl. + induction (natlehchoice4 i i b) as [r|r]. + * simpl. apply maponpaths. + apply isinjstntonat; simpl. reflexivity. + * simpl. apply maponpaths. apply isinjstntonat; simpl. reflexivity. +Defined. + +(** An induction principle for vectors: If a statement is true for the empty + vector, and if it is true for vectors of length n it is also true for those + of length S n, then it is true for all vectors. + *) +Definition Vector_rect {X : UU} {P : ∏ n, Vector X n -> UU} + (p0 : P 0 empty_vec) + (ind : ∏ (n : nat) (vec : Vector X n) (x : X), + P n vec -> P (S n) (append_vec vec x)) + {n : nat} (vec : Vector X n) : P n vec. +Proof. + intros. + induction n as [|n IH]. + - refine (transportf (P 0) _ p0). + apply proofirrelevancecontr, iscontr_vector_0. + - exact (transportf (P _) (drop_and_append_vec vec) + (ind _ (vec ∘ dni_lastelement) + (vec lastelement) + (IH (vec ∘ dni_lastelement)))). +Defined. + +Section Lemmas. + + Context {X : UU} {n : nat}. + + Definition vectorEquality {m : nat} (f : Vector X n) (g : Vector X m) (p : n = m) : + (∏ i, f i = g (transportf stn p i)) + -> transportf (Vector X) p f = g. + Proof. + intro. + induction p. + apply funextfun. + assumption. + Defined. + + Definition tail (vecsn : Vector X (S n)) : Vector X n := + vecsn ∘ dni (0,, natgthsn0 n). + + (** It doesn't matter what the proofs are in the stn inputs. *) + Definition vector_stn_proofirrelevance {vec : Vector X n} + {i j : stn n} : (stntonat _ i = stntonat _ j) -> vec i = vec j. + Proof. + intro. + apply maponpaths, isinjstntonat; assumption. + Defined. +End Lemmas. diff --git a/UniMath/Combinatorics/FiniteSets.v b/UniMath/Combinatorics/FiniteSets.v index 7ec7029f2d..b1e45a66e1 100644 --- a/UniMath/Combinatorics/FiniteSets.v +++ b/UniMath/Combinatorics/FiniteSets.v @@ -618,3 +618,12 @@ Delimit Scope finset with finset. Notation "'∑' x .. y , P" := (FiniteSetSum (λ x,.. (FiniteSetSum (λ y, P))..)) (at level 200, x binder, y binder, right associativity) : finset. (* type this in emacs in agda-input method with \sum *) + +(* A surjection from stn 0 is an equivalence *) +Lemma surj_from_stn0_to_neg {X : UU} (f : ⟦ 0 ⟧ → X ) : (issurjective f) → nelstruct 0 X. +Proof. + intros surj. apply tpair with (pr1 := f). intros x. + apply fromempty, (squash_to_prop (surj x) (isapropempty)). + intros [contra eq]; clear surj. + apply negstn0, contra. +Qed. diff --git a/UniMath/Combinatorics/KFiniteTypes.v b/UniMath/Combinatorics/KFiniteTypes.v index adc71ff2ad..61ac7f1384 100644 --- a/UniMath/Combinatorics/KFiniteTypes.v +++ b/UniMath/Combinatorics/KFiniteTypes.v @@ -23,6 +23,7 @@ Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations. +Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.Combinatorics.StandardFiniteSets. @@ -241,3 +242,90 @@ Section kfinite_definition. := hinhfun kfinstruct_finstruct. End kfinite_definition. + +Section iskfinite_isdeceq_isfinite. +(** + This section provides the necessary construction to prove that + every K-Finite type with decidable equality is Bishop-finite. + + Proof outline: + Let X be a K-Finite type. Then there exists n : nat with a surjection + from stn n to X. + + The proof goes by induction on n, with the type X being generalized. + In the base case, we have a surjection from an uninhabited type to X. + Thus, X must also have no elements and therefore, X is equivalent with + stn 0. + + In the inductive step, we assume that for any type X for which there + exists a surjection from stn n to X and has decidable equality is + Bishop finite. We have to show that if there exists a surjection f + from stn (S n) to X and X has decidable equality, then X is Bishop + finite. + Let g : stn n -> X such that g (x) := f x. If X has decidable equality, + then it is decidable whether f (n) is included in the image of g. + + We will thus proceed by case analysis on whether f n is included in the image of g. + If f n is included in the image of g, then g must be a surjection as well. By the inductive + hypothesis X is Bishop finite. If f n is not included in the image of g, we will denote + y := f n. We now consider the type X / y (pair X (\x -> x != y)) which is inhabited by + terms different than y. First, we note that X / y has decidable equality. Secondly, we note + that X / y + unit is equivalent to X. Lastly, we note that by restricting the codomain of g + to X / y, we obtain a surjection g1 : stn n -> X / y. By the inductive hypothesis, the type + X / y is Bishop finite, and thus equivalent to stn m for some m : nat. + To conclude, we have the following chain of equivalences + X ≃ X / y + 1 ≃ stn m + 1 ≃ stn (S m). Thus, X is Bishop finite. + + *) + + Lemma issurjective_stnfun_singleton_complement {X : UU} {n : nat} (f : stn (S n) → X) + (nfib : ¬ hfiber (fun_stnsn_to_stnn f) (f lastelement)) : issurjective f → + issurjective (stnfun_singleton_complement f nfib). + Proof. + intros surjf y. + destruct y as [x neq]. + use squash_to_prop. + - exact (hfiber f x). + - exact (surjf x). + - apply propproperty. + - intros [[m lth] q]; clear surjf. apply hinhpr. + induction (natlehchoice _ _ (natlthsntoleh _ _ lth)). + + apply (tpair _ (m ,, a)). + unfold stnfun_singleton_complement, fun_stnsn_to_stnn, make_stn. + apply subtypePath_prop; cbn. + induction q. apply maponpaths, stn_eq, idpath. + + assert (H : (m ,, lth = lastelement)) by apply stn_eq, b. + apply fromempty. induction neq. induction H. apply pathsinv0, q. + Qed. + + Lemma kfinstruct_dec_finstruct {X : UU} : isdeceq X → kfinstruct X → finstruct X. + Proof. + intros deceqX [n [f surj]]. + generalize dependent X. + induction n; intros. + - apply tpair with (pr1 := 0). + apply surj_from_stn0_to_neg with (f := f). assumption. + - set (g := fun_stnsn_to_stnn f). + set (y := f lastelement). + induction (isdeceq_isdecsurj g y deceqX). + + apply IHn with (f := g); try apply surj_fun_stnsn_to_stnn; assumption. + + set (g' := stnfun_singleton_complement f b). + set (surjg' := (issurjective_stnfun_singleton_complement f b surj)). + specialize IHn with (f := g'). + apply IHn in surjg'; + [ | apply isdeceq_subtype; try assumption; intros x; apply isapropneg ]. + destruct surjg' as [s1 s2]. + apply tpair with (pr1 := (S s1)); unfold nelstruct. + eapply weqcomp. + * apply invweq, weqdnicoprod, lastelement. + * eapply weqcomp. + { eapply weqcoprodf1, s2. } + apply weq_singleton_complement_unit; assumption. + Qed. + + Lemma iskfinite_dec_to_isfinite {X : UU} : isdeceq X → iskfinite X → isfinite X. + Proof. + intros deceqX. apply hinhfun, kfinstruct_dec_finstruct, deceqX. + Qed. + +End iskfinite_isdeceq_isfinite. diff --git a/UniMath/Combinatorics/StandardFiniteSets.v b/UniMath/Combinatorics/StandardFiniteSets.v index e5170c53cf..519d4b1edb 100644 --- a/UniMath/Combinatorics/StandardFiniteSets.v +++ b/UniMath/Combinatorics/StandardFiniteSets.v @@ -2025,3 +2025,55 @@ Lemma stn_ord_bij {n : nat} (f : ⟦ n ⟧ ≃ ⟦ n ⟧) : Proof. apply (stn_ord_inj (weqtoincl f)). Defined. + +(* Functions with domain in Standard finite sets. *) +Definition fun_stnsn_to_stnn {X : UU} {n : nat} (f : stn (S n) → X) : stn n → X := f ∘ dni_lastelement. + +Definition stnfun_singleton_complement {X : UU} {n : nat} (f : stn (S n) → X) : + ¬ hfiber (fun_stnsn_to_stnn f) (f lastelement) → stn n → + (singleton_complement (f lastelement)). +Proof. + intros X0 X1. + exists (fun_stnsn_to_stnn f X1). + intros contra. apply X0. + eexists. apply contra. +Defined. + +Lemma isdeceq_isdecsurj {X : UU} {n : nat} (f : ⟦ n ⟧ → X ) (y : X) : + isdeceq X → decidable (hfiber f y). +Proof. + generalize dependent X. + induction n; intros X f x deceqX. + - right. intros contra. eapply weqstn0toempty, pr1, contra. + - set (g := fun_stnsn_to_stnn f). specialize IHn with (f := g) (y := x). + set (H := IHn deceqX). + induction H. + + left. induction a as [p eq]. induction p as [m lth]. + apply tpair with (pr1 := (m ,, (natlthtolths _ _ lth))), eq. + + induction (deceqX (f (lastelement)) x); [left | right]. + * apply (tpair _ lastelement). assumption. + * intros H. induction H as [p eq]. induction p as [m lth]. + induction (natlehchoice _ _ (natlthsntoleh _ _ lth)). + -- apply b. apply tpair with (pr1 := (m ,, a)). + induction eq. unfold g, fun_stnsn_to_stnn, make_stn. unfold funcomp. + apply maponpaths, stn_eq, idpath. + -- apply b0. unfold lastelement. induction b1, eq. + apply maponpaths, stn_eq, idpath. +Qed. + +Lemma surj_fun_stnsn_to_stnn {X : UU} {n : nat} (f : ⟦ S n ⟧ → X) : isdeceq X → issurjective f → + hfiber (fun_stnsn_to_stnn f) (f lastelement) → issurjective (fun_stnsn_to_stnn f). +Proof. + intros deceqX surj x. induction x as [x eq]. + intros y'. + induction (deceqX (f lastelement) y'). + - induction a. apply hinhpr, tpair with (pr1 := x), eq. + - apply (squash_to_prop (surj y')); try apply propproperty. + intros m. induction m as [m eq']; induction m as [m lth]. apply hinhpr. + induction (natlehchoice _ _ (natlthsntoleh _ _ lth)). + + apply tpair with (pr1 := m ,, a). + unfold fun_stnsn_to_stnn, make_stn, funcomp. + induction eq'. apply maponpaths, stn_eq, idpath. + + induction eq', b0. apply fromempty, b. + apply maponpaths, stn_eq, idpath. +Qed. diff --git a/UniMath/Combinatorics/Tests.v b/UniMath/Combinatorics/Tests.v index e8815aa14a..85fa95e9b3 100644 --- a/UniMath/Combinatorics/Tests.v +++ b/UniMath/Combinatorics/Tests.v @@ -2,7 +2,6 @@ Require Import UniMath.Foundations.Preamble. Require UniMath.Combinatorics.Lists. Require UniMath.Combinatorics.StandardFiniteSets. Require UniMath.Combinatorics.FiniteSets. -Require UniMath.Combinatorics.FiniteSequences. Require UniMath.Combinatorics.FiniteSets. Require UniMath.OrderTheory.OrderedSets.OrderedSets. Require UniMath.Combinatorics.StandardFiniteSets. @@ -345,8 +344,6 @@ End Test_fin. Section Test_seq. - Import UniMath.Combinatorics.FiniteSequences. - Local Open Scope stn. End Test_seq. diff --git a/UniMath/Induction/.package/files b/UniMath/Induction/.package/files index 6b4a40fd7c..f69e092136 100644 --- a/UniMath/Induction/.package/files +++ b/UniMath/Induction/.package/files @@ -1,9 +1,11 @@ FunctorAlgebras_legacy.v FunctorCoalgebras_legacy.v +FunctorCoalgebras_legacy_alt_UU.v PolynomialFunctors.v PolynomialAlgebras2Cells.v ImpredicativeInductiveSets.v +SetBasedPolynomialFunctors.v M/Core.v M/Limits.v M/Uniqueness.v @@ -15,3 +17,7 @@ W/Naturals.v W/Uniqueness.v M/Chains.v M/ComputationalM.v +M/MWithSets.v +M/FinalCoalgebraHSET.v +M/ComputationalMWithSets.v +M/BinaryBooleanMTrees.v diff --git a/UniMath/Induction/FunctorCoalgebras_legacy_alt_UU.v b/UniMath/Induction/FunctorCoalgebras_legacy_alt_UU.v new file mode 100644 index 0000000000..edcb8938b1 --- /dev/null +++ b/UniMath/Induction/FunctorCoalgebras_legacy_alt_UU.v @@ -0,0 +1,140 @@ +(** + An alternative definition of coalgebra in type_precat that + gives a precategory, so that an adjunction can be shown + in MWithSets +*) + +Require Import UniMath.Foundations.Propositions. +Require Import UniMath.CategoryTheory.Core.Categories. +Require Import UniMath.CategoryTheory.Core.Isos. +Require Import UniMath.CategoryTheory.Core.Functors. +Require Import UniMath.CategoryTheory.Limits.Terminal. +Require Import UniMath.CategoryTheory.Categories.Type.Core. + +Local Open Scope cat. + +Section Coalgebra_Definition. + +Context (F : functor type_precat type_precat). + +Definition coalgebra : UU := ∑ X : type_precat, X --> F X. + +Definition coalgebra_ob (X : coalgebra) : type_precat := pr1 X. +Local Coercion coalgebra_ob : coalgebra >-> ob. + +Definition coalgebra_mor (X : coalgebra) : type_precat ⟦X, F X ⟧ := pr2 X. + +(** A homomorphism of F-coalgebras (F A, α : C ⟦A, F A⟧) and (F B, β : C ⟦B, F B⟧) + is a morphism f : C ⟦A, B⟧ s.t. the below diagram commutes in a sense of pointwise propositionally truncated equality. + + << + f + A -----> B + | | + | α | β + | | + V V + F A ---> F B + F f + >> +*) + +Definition is_coalgebra_homo {X Y : coalgebra} (f : type_precat ⟦X, Y⟧) (x : coalgebra_ob X) : UU + := ((coalgebra_mor X) · #F f) x = (f · (coalgebra_mor Y)) x. + +Definition coalgebra_homo (X Y : coalgebra) := ∑ f : type_precat ⟦X, Y⟧, ∏ x : coalgebra_ob X, ∥ is_coalgebra_homo f x ∥. + +Definition mor_from_coalgebra_homo (X Y : coalgebra) (f : coalgebra_homo X Y) + : type_precat ⟦X, Y⟧ := pr1 f. +Coercion mor_from_coalgebra_homo : coalgebra_homo >-> precategory_morphisms. + +Lemma coalgebra_homo_commutes {X Y : coalgebra} (f : coalgebra_homo X Y) (x : coalgebra_ob X) (P : hProp) : + (((coalgebra_mor X) · #F f) x = (f · (coalgebra_mor Y)) x -> P) -> P. +Proof. + intro Hyp. + apply (factor_through_squash (pr2 P) Hyp). + exact (pr2 f x). +Qed. + +Definition coalgebra_homo_id (X : coalgebra) : coalgebra_homo X X. +Proof. + exists (identity _). + intro x. + unfold is_coalgebra_homo. + rewrite id_left. + rewrite functor_id. + rewrite id_right. + exact (hinhpr (idpath (coalgebra_mor X x))). +Defined. + +Lemma coalgebra_homo_comp (X Y Z : coalgebra) (f : coalgebra_homo X Y) + (g : coalgebra_homo Y Z) : coalgebra_homo X Z. +Proof. + exists (f · g). + intro x. + unfold is_coalgebra_homo. + rewrite functor_comp. + rewrite assoc. + apply (coalgebra_homo_commutes f x). + intro Hypf. + assert (p1 : (coalgebra_mor X · # F f · # F g) x = (# F g) ((coalgebra_mor X · # F f) x)) by apply idpath. + rewrite p1. + rewrite Hypf. + assert (p2 : # F g ((f · coalgebra_mor Y) x) = (f · coalgebra_mor Y · # F g) x) by apply idpath. + rewrite p2. + rewrite <- assoc. + apply (coalgebra_homo_commutes g (pr1 f x)). + intro Hypg. + assert (p3 : (f · (coalgebra_mor Y · # F g)) x = (coalgebra_mor Y · # F g) (pr1 f x)) by apply idpath. + rewrite p3. + rewrite Hypg. + assert (p4 : (g · coalgebra_mor Z) (pr1 f x) = (f · (g · coalgebra_mor Z)) x) by apply idpath. + rewrite p4. + rewrite assoc. + exact (hinhpr (idpath _)). +Defined. + +Definition CoAlg_precategory_ob_mor : precategory_ob_mor := + make_precategory_ob_mor coalgebra coalgebra_homo. + +Definition CoAlg_precategory_data: precategory_data := + make_precategory_data CoAlg_precategory_ob_mor + coalgebra_homo_id + coalgebra_homo_comp. + +End Coalgebra_Definition. + +Lemma CoAlg_is_precategory (F : functor type_precat type_precat) + : is_precategory (CoAlg_precategory_data F). +Proof. + split. + - split. + + intros. + use total2_paths_f. + * apply idpath. + * apply funextsec. + intro. + apply isapropishinh. + + intros. + use total2_paths_f. + * apply idpath. + * apply funextsec. + intro. + apply isapropishinh. + - split. + + intros. + use total2_paths_f. + * apply idpath. + * apply funextsec. + intro. + apply isapropishinh. + + intros. + use total2_paths_f. + * apply idpath. + * apply funextsec. + intro. + apply isapropishinh. +Qed. + +Definition CoAlg_precategory (F : functor type_precat type_precat) : precategory + := make_precategory (CoAlg_precategory_data F) (CoAlg_is_precategory F). diff --git a/UniMath/Induction/M/BinaryBooleanMTrees.v b/UniMath/Induction/M/BinaryBooleanMTrees.v new file mode 100644 index 0000000000..1d8631da1a --- /dev/null +++ b/UniMath/Induction/M/BinaryBooleanMTrees.v @@ -0,0 +1,227 @@ +(** ** Example of construction of M Types using ComputationalMWithSets + + Author : Antoine Fisse (@AextraT), 2025 +*) + +Require Import UniMath.Foundations.PartD. +Require Import UniMath.Foundations.Sets. +Require Import UniMath.MoreFoundations.All. + +Require Import UniMath.Combinatorics.Lists. +Require Import UniMath.Combinatorics.StandardFiniteSets. + +Require Import UniMath.Induction.FunctorCoalgebras_legacy. +Require Import UniMath.Induction.PolynomialFunctors. +Require Import UniMath.Induction.M.Core. +Require Import UniMath.Induction.M.ComputationalM. +Require Import UniMath.Induction.M.ComputationalMWithSets. +Require Import UniMath.Induction.M.MWithSets. +Require Import UniMath.Induction.M.FinalCoalgebraHSET. + +Require Import UniMath.CategoryTheory.Categories.Type.Core. +Require Import UniMath.CategoryTheory.Core.Categories. +Require Import UniMath.CategoryTheory.Core.Functors. +Require Import UniMath.CategoryTheory.Categories.HSET.All. +Require Import UniMath.CategoryTheory.Limits.Terminal. +Require Import UniMath.CategoryTheory.Chains.OmegaContPolynomialFunctors. +Require UniMath.CategoryTheory.FunctorCoalgebras. + +Local Open Scope cat. + +Local Definition A := setcoprod unitset boolset. +Local Definition B : pr1hSet A -> SET := + λ a, match a with + | ii1 _ => emptyset + | ii2 _ => setcoprod unitset unitset + end. + +Local Definition F := MWithSets.F B. +Local Definition F' := MWithSets.F' B. + +(* The final coalgebra obtained corresponds to the type of possibly infinite binary trees labeled with booleans. *) +Local Definition C' : FunctorCoalgebras.CoAlg_category F' + := pr1 (GetMType_HSET B). +Local Definition C'_isfinal : isTerminal (FunctorCoalgebras.CoAlg_category F') C' + := pr2 (GetMType_HSET B). + +Local Definition C'1 : FunctorCoalgebras.CoAlg_category F' + := ComputationalMWithSets.C' B C' C'_isfinal. +Local Definition C'1_isfinal : isTerminal (CoAlg_category F') C'1 + := ComputationalMWithSets.finalC' B C' C'_isfinal. +Local Definition corec_C1 := ComputationalMWithSets.corecC B C' C'_isfinal. +Local Definition c1 : UU := pr11 C'1. +Local Definition destr_c1 : c1 -> F c1 := pr2 C'1. + +Definition get_subtrees_list_rec_step (t0 : c1) (acc : list c1) : list c1 + := match destr_c1 t0 with + | (ii1 _,, _) => acc + | (ii2 _,, f) => cons (f (ii1 tt)) (cons (f (ii2 tt)) acc) + end. + +Definition get_subtrees_list_at_depth (t : c1) (depth : nat) : list c1. +Proof. + induction depth. + - exact (cons t nil). + - exact (list_ind + (λ _, list c1) + nil + (λ t0 _ acc, get_subtrees_list_rec_step t0 acc) + IHdepth). +Defined. + +Definition get_labels_list_rec_step (t0 : c1) (acc : list bool) : list bool + := match destr_c1 t0 with + | (ii1 _,, _) => acc + | (ii2 b,, _) => cons b acc + end. + +Definition get_labels_list_at_depth (t : c1) (depth : nat) : list bool. +Proof. + set (l := get_subtrees_list_at_depth t depth). + exact (list_ind + (λ _, list bool) + nil + (λ t0 _ acc, get_labels_list_rec_step t0 acc) + l). +Defined. + +(* Full tree only labeled true *) +Definition t_full_true : c1. +Proof. + set (c := unit). + set (s_c := λ _ : c, (ii2 true,, λ _, tt) : F c). + exact (corec_C1 (c,, s_c) tt). +Defined. + +Lemma only_true : get_labels_list_at_depth t_full_true 4 = functionToList 16 (λ _, true). +Proof. + apply idpath. +Defined. + +(* true + / \ + false true + / / \ + true true false +*) +Definition t_ex_finite : c1. +Proof. + set (c := nat). + set (a0 := ii2 true : A). + set (a1 := ii2 false : A). + set (a2 := ii2 true : A). + set (s_c := λ x : c, match x with + | 0 => (a0,, λ y : pr1hSet (B a0), match y with + | ii1 _ => 1 + | ii2 _ => 2 + end : c) + | 1 => (a1,, λ y : pr1hSet (B a1), match y with + | ii1 _ => 3 + | ii2 _ => 5 + end : c) + | 2 => (a2,, λ y : pr1hSet (B a2), match y with + | ii1 _ => 3 + | ii2 _ => 4 + end : c) + | 3 => (ii2 true,, λ _, 5) + | 4 => (ii2 false,, λ _, 5) + | _ => (ii1 tt,, λ _, 5) + end : F c). + exact (corec_C1 (c,, s_c) 0). +Defined. + +Lemma row2 : get_labels_list_at_depth t_ex_finite 2 = cons true (cons true (cons false nil)). +Proof. + apply idpath. +Defined. + +(* Note though that the refinement of ComputationalM is needed to have + proofs by idpath. *) +Local Definition C : coalgebra F := MWithSets.C0 B C'. +Local Definition C_isfinal : is_final C := MWithSets.C0_is_final B C' C'_isfinal. +Local Definition corec_C := ComputationalM.corecM0 _ _ C C_isfinal. +Local Definition c : UU := pr1 C. +Local Definition destr_c : c -> F c := pr2 C. + +Definition get_subtrees_list_rec_step_no_refinement (t0 : c) (acc : list c) : list c + := match destr_c t0 with + | (ii1 _,, _) => acc + | (ii2 _,, f) => cons (f (ii1 tt)) (cons (f (ii2 tt)) acc) + end. + +Definition get_subtrees_list_at_depth_no_refinement (t : c) (depth : nat) : list c. +Proof. + induction depth. + - exact (cons t nil). + - exact (list_ind + (λ _, list c) + nil + (λ t0 _ acc, get_subtrees_list_rec_step_no_refinement t0 acc) + IHdepth). +Defined. + +Definition get_labels_list_rec_step_no_refinement (t0 : c) (acc : list bool) : list bool + := match destr_c t0 with + | (ii1 _,, _) => acc + | (ii2 b,, _) => cons b acc + end. + +Definition get_labels_list_at_depth_no_refinement (t : c) (depth : nat) : list bool. +Proof. + set (l := get_subtrees_list_at_depth_no_refinement t depth). + exact (list_ind + (λ _, list bool) + nil + (λ t0 _ acc, get_labels_list_rec_step_no_refinement t0 acc) + l). +Defined. + +(* In some simple cases we do have a proof by idpath *) +Definition t_full_true_no_refinement : c. +Proof. + set (c := unit). + set (s_c := λ _ : c, (ii2 true,, λ _, tt) : F c). + exact (corec_C (c,, s_c) tt). +Defined. + +Lemma only_true_no_refinement : get_labels_list_at_depth_no_refinement t_full_true_no_refinement 4 = functionToList 16 (λ _, true). +Proof. + apply idpath. +Defined. + +(* In more complex cases a more complex proof is needed *) +Definition coalg_t_ex_finite_no_refinement : coalgebra F. +Proof. + set (c := nat). + set (a0 := ii2 true : A). + set (a1 := ii2 false : A). + set (a2 := ii2 true : A). + set (s_c := λ x : c, match x with + | 0 => (a0,, λ y : pr1hSet (B a0), match y with + | ii1 _ => 1 + | ii2 _ => 2 + end : c) + | 1 => (a1,, λ y : pr1hSet (B a1), match y with + | ii1 _ => 3 + | ii2 _ => 5 + end : c) + | 2 => (a2,, λ y : pr1hSet (B a2), match y with + | ii1 _ => 3 + | ii2 _ => 4 + end : c) + | 3 => (ii2 true,, λ _, 5) + | 4 => (ii2 false,, λ _, 5) + | _ => (ii1 tt,, λ _, 5) + end : F c). + exact (c,, s_c). +Defined. + +Definition t_ex_finite_no_refinement : c. +Proof. + exact (corec_C coalg_t_ex_finite_no_refinement 0). +Defined. + +Lemma row2_no_refinement : get_labels_list_at_depth_no_refinement t_ex_finite_no_refinement 2 = cons true (cons true (cons false nil)). +Proof. + Fail apply idpath. +Abort. diff --git a/UniMath/Induction/M/ComputationalM.v b/UniMath/Induction/M/ComputationalM.v index 44f005d7d6..83f07b1989 100644 --- a/UniMath/Induction/M/ComputationalM.v +++ b/UniMath/Induction/M/ComputationalM.v @@ -9,6 +9,12 @@ Author: Dominik Kirst (@dominik-kirst) and Ralph Matthes (@rmatthes) + massive overhaul by Ralph Matthes (May to July 2025), the crucial element + being the total rewrite of the proof of Lemma P_isaprop that now tries to + generate the new goals as much as possible, while the previous version + announced the intermediate goals through intermediate_weq with formulas + conceived in the UniMath 2017 school formalization + *) Require Import UniMath.Foundations.All. @@ -30,54 +36,79 @@ Require Import UniMath.Induction.M.Uniqueness. equational rule of coiteration holding definitionally: Lemma [corec_computation] is proved merely by [idpath]. Of course, both coalgebras are equal - provably (Lemma [coalgebras_eq]). -*) + *) +Local Open Scope cat. + Section Refinement. Context (A : UU). Context (B : A → UU). - Local Notation F := (polynomial_functor A B). + + Local Definition F : type_precat ⟶ type_precat + := polynomial_functor A B. Variable M0 : coalgebra F. - Local Notation carrierM0 := (coalgebra_ob _ M0). - Local Notation destrM0 := (coalgebra_mor _ M0). + Local Definition carrierM0 : type_precat := coalgebra_ob F M0. + Local Definition destrM0 : type_precat ⟦ carrierM0, F carrierM0 ⟧ + := coalgebra_mor F M0. Variable finalM0 : is_final M0. - Local Notation corecM0 C := (pr11 (finalM0 C)). + Local Definition corecM0 (C : coalgebra F) : type_precat ⟦ coalgebra_ob F C, carrierM0 ⟧ + := pr1 (iscontrpr1 (finalM0 C)). + + Lemma corec_equational_aux (C : coalgebra F) (c : coalgebra_ob F C) : is_coalgebra_homo F (corecM0 C). + Proof. + exact (pr2 (iscontrpr1 (finalM0 C))). + Defined. (* defined because the target of the morphisms is a precategory only *) + + (** recall the provable equation governing corec *) + Lemma corec_equational (C : coalgebra F) (c : coalgebra_ob F C) : + destrM0 (corecM0 C c) = # F (corecM0 C) (coalgebra_mor F C c). + Proof. + set (aux := toforallpaths _ _ _ (corec_equational_aux C c)). + apply pathsinv0, aux. + Defined. - Local Open Scope cat. Local Open Scope functions. - (* Refinement of the final coalgebra to computable elements *) + (** refinement of the final coalgebra to purely coiterative elements *) + Definition is_purelycoiterativeM0 (m0 : carrierM0) : UU := ∃ (C : coalgebra F) (c : coalgebra_ob F C), corecM0 C c = m0. - Definition carrierM := ∑ m0 : carrierM0, ∃ C c, corecM0 C c = m0. + Definition carrierM : UU := total2 is_purelycoiterativeM0. - (* Definition of the corecursor *) + (* Check (carrierM = ∑ m0 : carrierM0, ∃ (C : coalgebra F) (c : coalgebra_ob F C), corecM0 C c = m0). *) - Definition corecM (C : coalgebra F) (c : coalgebra_ob _ C) : carrierM. + (** definition of the corecursor *) + Definition corecM (C : coalgebra F) (c : coalgebra_ob F C) : carrierM. Proof. exists (corecM0 C c). apply hinhpr. exists C, c. apply idpath. Defined. - (* Definition of a proposition we factor the computation through *) + (** a form of functoriality of [F] w.r.t. convertibility *) + Lemma corecM_corecM0 (C : coalgebra F) (cf: F (coalgebra_ob F C)) : + #F pr1 (#F (corecM C) cf) = #F (corecM0 C) cf. + Proof. + apply idpath. + Defined. - Local Definition P (m0 : carrierM0) := - ∑ af : F carrierM, destrM0 m0 = # F pr1 af. + (** definition of a proposition we factor the computation through *) + Local Definition P (m0 : carrierM0) : UU + := ∑ af : F carrierM, destrM0 m0 = # F pr1 af. (** in order to show [P] to be a proposition, a not obviously equivalent formulation is given for which it is easy to show [isaprop] *) - Local Definition P' (m0 : carrierM0) := - ∑ ap : ∑ a : A, pr1 (destrM0 m0) = a, - ∏ (b : B (pr1 ap)), - ∑ mp : ∑ m0' : carrierM0, - transportf (λ a, B a -> carrierM0) + Local Definition P' (m0 : carrierM0) : UU := + ∑ ap : (∑ a : A, pr1 (destrM0 m0) = a), + ∏ b : B (pr1 ap), + ∑ mp : (∑ m0' : carrierM0, + transportf (λ a : A, B a -> carrierM0) (pr2 ap) (pr2 (destrM0 m0)) b = - m0', - ∃ C c, corecM0 C c = pr1 mp. + m0'), + is_purelycoiterativeM0 (pr1 mp). (** the easy auxiliary lemma *) - Local Lemma P'_isaprop m0 : - isaprop (P' m0). + Local Lemma P'_isaprop (m0 : carrierM0) : isaprop (P' m0). Proof. apply isofhleveltotal2. - apply isofhlevelcontr. @@ -92,127 +123,89 @@ Section Refinement. Defined. (** the crucial lemma *) - Local Lemma P_isaprop (m0 : carrierM0) : - isaprop (P m0). + Local Lemma P_isaprop (m0 : carrierM0) : isaprop (P m0). Proof. use (@isofhlevelweqb _ _ (P' m0) _ (P'_isaprop m0)). - simple refine (weqcomp (weqtotal2asstor _ _) _). - simple refine (weqcomp _ (invweq (weqtotal2asstor _ _))). + eapply weqcomp. + { apply weqtotal2asstor. } + (* working on the right end: *) + eapply weqcomp. + 2: { apply invweq. + apply weqtotal2asstor. } + (* reducing the problem: *) apply weqfibtototal; intro a. - intermediate_weq ( - ∑ f : B a → carrierM, - ∑ p : pr1 (destrM0 m0) = a, - transportf - (λ a, B a -> carrierM0) - p - (pr2 (destrM0 m0)) = - pr1 ∘ f). - { - apply weqfibtototal; intro f. + eapply weqcomp. + { apply weqfibtototal; intro f. apply total2_paths_equiv. } - intermediate_weq (∑ p : pr1 (destrM0 m0) = a, - ∑ f : B a → carrierM, - transportf - (λ a, B a → carrierM0) - p - (pr2 (destrM0 m0)) = - pr1 ∘ f). + unfold PathPair. simpl. + eapply weqcomp. { apply weqtotal2comm. } + (* reducing the problem: *) apply weqfibtototal; intro p. - intermediate_weq (∑ fg : ∑ f : B a -> carrierM0, - ∏ b, ∃ C c, corecM0 C c = f b, - transportf - (λ a, B a -> carrierM0) - p - (pr2 (destrM0 m0)) = - pr1 fg). - { use weqbandf. - - apply weqfuntototaltototal. - - cbn. - intro f. - apply idweq. + (* the next line serves to illustrate the the right-hand side will not be touched during the next five transformations *) + match goal with |[ |- _ ≃ ?rhs] => set (therhs := rhs) end. + eapply weqcomp. + { set (H1 := weqfuntototaltototal (B a) is_purelycoiterativeM0). + apply (weqbandf H1 _ (fun fg => transportf (λ a : A, B a -> carrierM0) p (pr2 (destrM0 m0)) = pr1 fg)). (* the second argument to [weqbandf] is [fun f => transportf (λ x : A, B x → carrierM0) p (pr2 (destrM0 m0)) = pr1 ∘ f] *) + (* solving a trivial subproblem: *) + cbn. + intro f. + apply idweq. } - intermediate_weq (∑ f : B a → carrierM0, - ∑ _ : ∏ b, ∃ C c, corecM0 C c = f b, - transportf - (λ a, B a → carrierM0) - p - (pr2 (destrM0 m0)) = - f). + simpl. + eapply weqcomp. { apply weqtotal2asstor. } - intermediate_weq (∑ f : B a → carrierM0, - ∑ _ : ∏ b, ∃ C c, corecM0 C c = f b, - ∏ b, transportf - (λ a, B a → carrierM0) - p - (pr2 (destrM0 m0)) b = - f b). + simpl. + eapply weqcomp. { apply weqfibtototal; intro f. - apply weqfibtototal; intros _. + apply weqfibtototal; intro Hyp. apply weqtoforallpaths. } - intermediate_weq (∑ f : B a → carrierM0, - ∏ b, ∑ _ : ∃ C c, corecM0 C c = f b, - transportf - (λ a, B a → carrierM0) - p - (pr2 (destrM0 m0)) b = - f b). + simpl. + unfold homot. + eapply weqcomp. { apply weqfibtototal; intro f. apply invweq. - apply weqforalltototal. + apply (weqforalltototal _ (fun x _ => transportf (λ a0 : A, B a0 → carrierM0) p (pr2 (destrM0 m0)) x = f x)). (* the first argument to [weqforalltototal] is [fun x => is_computableM0 (f x)] *) } - intermediate_weq (∏ b, ∑ m0' : carrierM0, - ∑ _ : ∃ C c, corecM0 C c = m0', - transportf - (λ a, B a -> carrierM0) - p - (pr2 (destrM0 m0)) b = - m0'). + simpl. + eapply weqcomp. { apply invweq. - apply weqforalltototal. + apply (weqforalltototal _ (fun b y => ∑ _ : is_purelycoiterativeM0 y, transportf (λ a0 : A, B a0 → carrierM0) p (pr2 (destrM0 m0)) b = y)). (* the first argument to [weqforalltototal] is [fun _ => carrierM0] *) } + (* reducing the problem: *) apply weqonsecfibers; intro b. - intermediate_weq (∑ m0' : carrierM0, - ∑ _ : transportf - (λ a, B a -> carrierM0) - p - (pr2 (destrM0 m0)) b = - m0', - ∃ C c, corecM0 C c = m0'). - { - apply weqfibtototal; intro m0'. + (* no longer need to illustrate the fixed right-hand side: *) + clear therhs. + eapply weqcomp. + { apply weqfibtototal; intro m0'. apply weqdirprodcomm. } - intermediate_weq (∑ mp : ∑ m0', transportf (λ a, B a → carrierM0) p - (pr2 (destrM0 m0)) b = m0', - ∃ C c, corecM0 C c = pr1 mp). - { - apply invweq. - apply weqtotal2asstor. - } - use weqbandf. - - apply weqfibtototal; intro m0'. - apply idweq. - - cbn. intro mp. - apply idweq. + simpl. + (* the final step is on the current right-hand side: *) + apply invweq. + apply weqtotal2asstor. (* the first argument to [weqtotal2asstor] is [fun x => transportf (λ a0 : A, B a0 → carrierM0) p (pr2 (destrM0 m0)) b = x], the second is [fun y => is_computableM0 (pr1 y)] *) Defined. (* Now the destructor of M can be defined *) + Local Lemma destrM'_aux (m0 : carrierM0) (C : coalgebra F) (c : coalgebra_ob F C) (H1 : corecM0 C c = m0) : + destrM0 m0 = # F pr1 ((# F (corecM C) ∘ coalgebra_mor F C) c). + Proof. + etrans. + { rewrite <- H1. apply corec_equational. } + apply pathsinv0, corecM_corecM0. + Defined. + Local Definition destrM' (m : carrierM) : P (pr1 m). Proof. - induction m as [m0 H]. apply (squash_to_prop H); try apply P_isaprop. + induction m as [m0 H]. apply (squash_to_prop H); [apply P_isaprop|]. intros [C [c H1]]. - refine ((# F (corecM C) ∘ (pr2 C)) c,, _). cbn [pr1]. clear H. - assert (H : is_coalgebra_homo F (corecM0 C)). - { destruct finalM0 as [[G H] H']. apply H. } - apply toforallpaths in H. - apply pathsinv0. - intermediate_path (destrM0 (corecM0 C c)). - - apply H. - - apply maponpaths. assumption. + exists ((# F (corecM C) ∘ (coalgebra_mor F C)) c). + cbn [pr1]. + apply destrM'_aux. + assumption. Defined. Definition destrM (m : carrierM) : F carrierM := @@ -221,28 +214,33 @@ Section Refinement. Definition M : coalgebra F := (carrierM,, destrM). - (* The destructor satisfies the corecursion equation definitionally *) - - Lemma corec_computation C c : - destrM (corecM C c) = # F (corecM C) (pr2 C c). + (** the destructor satisfies the corecursion equation definitionally *) + Lemma corec_computation (C : coalgebra F) (c : coalgebra_ob F C) : + destrM (corecM C c) = # F (corecM C) (coalgebra_mor F C c). Proof. apply idpath. Defined. - (* The two carriers are equal *) - - Lemma eq_corecM0 m0 : + (** for the moment only an experiment *) + Goal ∏ (m0 : carrierM0), P m0 -> is_purelycoiterativeM0 m0. + Proof. + intros m0 [[a f] Hyp]. + simpl in Hyp. + unfold polynomial_functor_arr in Hyp. + simpl in Hyp. + Abort. (* there should be a notion of computable element that is wider than purely coiterative *) + + (** the two carriers are equal *) + Lemma eq_corecM0 (m0 : carrierM0) : corecM0 M0 m0 = m0. Proof. - induction finalM0 as [[G H1] H2]. cbn. - specialize (H2 (coalgebra_homo_id F M0)). - change (pr1 (G,, H1) m0 = pr1 (coalgebra_homo_id F M0) m0). - apply (maponpaths (fun X => pr1 X m0)). apply pathsinv0. - assumption. + assert (aux := path_to_ctr _ _ (finalM0 M0) (pr1 (coalgebra_homo_id F M0)) (pr2 (coalgebra_homo_id F M0))). + apply toforallpaths in aux. + apply aux. Defined. - Definition injectM0 m0 : + Definition injectM0 (m0 : carrierM0) : ∃ C c, corecM0 C c = m0. Proof. apply hinhpr. exists M0, m0. apply eq_corecM0. @@ -278,7 +276,7 @@ Section Refinement. unfold carriers_eq. rewrite weqpath_transport. apply idpath. Defined. - Local Lemma eq3 m0 : + Local Lemma eq3 (m0 : carrierM0) : destrM (m0,, injectM0 m0) = pr1 (destrM0 m0),, corecM M0 ∘ pr2 (destrM0 m0). Proof. apply idpath. @@ -287,13 +285,13 @@ Section Refinement. Lemma coalgebras_eq : M = M0. Proof. - use total2_paths_f; try apply carriers_eq. + use total2_paths_f; [apply carriers_eq|]. apply funextfun. intro m0. rewrite eq1. rewrite eq2. rewrite eq3. cbn. unfold polynomial_functor_obj. rewrite transportf_total2_const. - use total2_paths_f; try apply idpath. - cbn. apply funextsec. intros b. rewrite <- helper_A. + use total2_paths_f; [apply idpath|]. + cbn. apply funextsec. intros b. rewrite <- UniMath.MoreFoundations.PartA.helper_A. unfold carriers_eq. rewrite weqpath_transport. cbn. rewrite eq_corecM0. apply idpath. Defined. diff --git a/UniMath/Induction/M/ComputationalMWithSets.v b/UniMath/Induction/M/ComputationalMWithSets.v new file mode 100644 index 0000000000..0d5f8ff407 --- /dev/null +++ b/UniMath/Induction/M/ComputationalMWithSets.v @@ -0,0 +1,68 @@ +(** ** Refinement of M-Types in the case of sets + + The file starts with a final coalgebra in HSET and uses + ComputationalM to get a new final coalgebra, still in HSET + and that satisfies the computational rule. + + Author : Antoine Fisse (@AextraT), 2025 + + *) + +Require Import UniMath.Foundations.PartD. +Require Import UniMath.Foundations.Sets. +Require Import UniMath.MoreFoundations.All. + +Require Import UniMath.Induction.FunctorCoalgebras_legacy. +Require Import UniMath.Induction.PolynomialFunctors. +Require Import UniMath.Induction.M.Core. +Require Import UniMath.Induction.M.ComputationalM. +Require Import UniMath.Induction.M.MWithSets. + +Require Import UniMath.CategoryTheory.Categories.Type.Core. +Require Import UniMath.CategoryTheory.Core.Categories. +Require Import UniMath.CategoryTheory.Core.Functors. +Require Import UniMath.CategoryTheory.Categories.HSET.All. +Require Import UniMath.CategoryTheory.Limits.Terminal. +Require UniMath.CategoryTheory.FunctorCoalgebras. + +Local Open Scope cat. + +Section Refinement. + + Context {A : ob HSET} (B : pr1hSet A → ob HSET). + + Local Definition F := MWithSets.F B. + Local Definition F' := MWithSets.F' B. + + Context (C0' : FunctorCoalgebras.coalgebra_ob F') (C0'_is_final : isTerminal (FunctorCoalgebras.CoAlg_category F') C0'). + + Let c0' : hSet := FunctorCoalgebras.coalg_carrier F' C0'. + + Let C0 : coalgebra F := MWithSets.C0 B C0'. + Let finalC0 : is_final C0 := MWithSets.C0_is_final B C0' C0'_is_final. + + Let C : coalgebra F := ComputationalM.M (pr1 A) (λ a, pr1 (B a)) C0 finalC0. + Let finalC : is_final C := finalM (pr1 A) (λ a, pr1 (B a)) C0 finalC0. + Let c : type_precat := coalgebra_ob F C. + Let s_c := coalgebra_mor F C. + + Lemma c_isaset : isaset c. + Proof. + cbn. + unfold carrierM. + apply (isaset_total2_hSet c0' (λ m0, hProp_to_hSet (∃ (C : coalgebra F) (c : coalgebra_ob F C), (pr11 (finalC0 C)) c = m0))). + Defined. + + Local Definition C' : FunctorCoalgebras.coalgebra_ob F' + := MWithSets.C0' B C c_isaset. + Local Definition finalC' : isTerminal (FunctorCoalgebras.CoAlg_category F') C' + := MWithSets.C0'_is_final B C c_isaset finalC. + + Local Definition corecC := ComputationalM.corecM (pr1 A) (λ a, pr1 (B a)) C0 finalC0. + + Lemma corec_computation_set C1 c1 : s_c (corecC C1 c1) = # F (corecC C1) (pr2 C1 c1). + Proof. + apply idpath. + Defined. + +End Refinement. diff --git a/UniMath/Induction/M/FinalCoalgebraHSET.v b/UniMath/Induction/M/FinalCoalgebraHSET.v new file mode 100644 index 0000000000..2fcfc44a76 --- /dev/null +++ b/UniMath/Induction/M/FinalCoalgebraHSET.v @@ -0,0 +1,54 @@ +(** ** A final coalgebra of a polynomial functor defined by sets is a set. + + Author : Antoine Fisse (@AextraT), 2025 + *) + +Require Import UniMath.Foundations.PartD. +Require Import UniMath.Foundations.Sets. +Require Import UniMath.MoreFoundations.All. + +Require Import UniMath.Induction.FunctorCoalgebras_legacy. +Require Import UniMath.Induction.PolynomialFunctors. +Require Import UniMath.Induction.M.Core. +Require Import UniMath.Induction.M.MWithSets. +Require Import UniMath.Induction.M.Uniqueness. + +Require Import UniMath.CategoryTheory.Categories.Type.Core. +Require Import UniMath.CategoryTheory.Core.Categories. +Require Import UniMath.CategoryTheory.Core.Functors. +Require Import UniMath.CategoryTheory.DisplayedCats.Core. +Require Import UniMath.CategoryTheory.Categories.HSET.All. +Require Import UniMath.CategoryTheory.Chains.CoAdamek. +Require Import UniMath.CategoryTheory.Chains.Chains. +Require Import UniMath.CategoryTheory.Chains.Cochains. +Require Import UniMath.CategoryTheory.Chains.OmegaContPolynomialFunctors. +Require Import UniMath.CategoryTheory.Limits.Terminal. +Require Import UniMath.CategoryTheory.FunctorCoalgebras. + +Local Open Scope cat. +Local Open Scope functions. + +Section MTypesAreSets. + + Context {A : ob HSET} (B : pr1hSet A → ob HSET). + + Local Definition F := MWithSets.F B. + + Lemma GetMType_HSET : Terminal (CoAlg_category (OmegaContPolynomialFunctors.F' B)). + Proof. + exact (limCoAlgTerminal TerminalHSET (PolyFunctor_omega_cont B) (LimConeHSET _ (termCochain TerminalHSET (OmegaContPolynomialFunctors.F' B)))). + Defined. + + Lemma FinalCoalgAreSets (C : coalgebra F) (C_isfinal : is_final C) : isaset (pr1 C). + Proof. + set (C1'_t := GetMType_HSET). + unfold Terminal in C1'_t. + destruct C1'_t as [C1' C1'_isterm]. + set (C1 := MWithSets.C0 B C1'). + set (C1_isfinal := C0_is_final B C1' C1'_isterm : is_final C1). + set (p := M_carriers_eq (pr1hSet A) (λ a, pr1hSet (B a)) (C1,, C1_isfinal) (C,, C_isfinal) : pr1 C1 = pr1 C). + set (C1_isaset := pr21 C1' : isaset (pr1 C1)). + apply (transportf (λ c, isaset c) p C1_isaset). + Qed. + +End MTypesAreSets. diff --git a/UniMath/Induction/M/MWithSets.v b/UniMath/Induction/M/MWithSets.v new file mode 100644 index 0000000000..f7edeb1b60 --- /dev/null +++ b/UniMath/Induction/M/MWithSets.v @@ -0,0 +1,445 @@ +(** ** Equivalence between being a final coalgebra in UU and in HSET + + Authors : Antoine Fisse (@AextraT), Ralph Matthes (@rmatthes), 2025 + + *) + +Require Import UniMath.Foundations.PartD. +Require Import UniMath.Foundations.Sets. +Require Import UniMath.MoreFoundations.All. + +Require Import UniMath.Induction.FunctorCoalgebras_legacy. +Require Import UniMath.Induction.PolynomialFunctors. +Require Import UniMath.Induction.SetBasedPolynomialFunctors. +Require Import UniMath.Induction.M.Core. +Require UniMath.Induction.FunctorCoalgebras_legacy_alt_UU. + +Require Import UniMath.CategoryTheory.Categories.Type.Core. +Require Import UniMath.CategoryTheory.Core.Categories. +Require Import UniMath.CategoryTheory.Core.Functors. +Require Import UniMath.CategoryTheory.DisplayedCats.Core. +Require Import UniMath.CategoryTheory.Categories.HSET.All. +Require Import UniMath.CategoryTheory.Limits.Terminal. +Require UniMath.CategoryTheory.FunctorCoalgebras. +Require Import UniMath.CategoryTheory.Adjunctions.Core. +Require Import UniMath.CategoryTheory.Core.NaturalTransformations. + +Local Open Scope cat. + +Section M. + Context {A : ob HSET} (B : pr1hSet A → ob HSET). + + Local Definition F : type_precat ⟶ type_precat := polynomial_functor (pr1hSet A) (fun a => pr1hSet (B a)). + + Local Definition F' : functor HSET HSET := polynomial_functor_HSET A B. + + Definition FromCoalgInHSET (C' : FunctorCoalgebras.CoAlg_category F') : coalgebra F. + Proof. + use tpair. + - exact (pr1hSet (FunctorCoalgebras.coalg_carrier F' C')). + - exact (FunctorCoalgebras.coalg_map F' C'). + Defined. + + Definition ToCoalgInHSET (C : coalgebra F) : isaset (coalgebra_ob F C) -> FunctorCoalgebras.CoAlg_category F'. + Proof. + intro Hyp. + use tpair. + - exact (coalgebra_ob F C ,, Hyp). + - exact (coalgebra_mor F C). + Defined. + + Section ToFinalInHSET. + + Context (C0 : coalgebra F). + + Let c0 : type_precat := coalgebra_ob F C0. + + Context (c0_isaset : isaset c0). + + Definition C0' : FunctorCoalgebras.coalgebra_ob F'. + Proof. + exact (ToCoalgInHSET C0 c0_isaset). + Defined. + + Context (C0_is_final : is_final C0). + + Lemma C0'_is_final : isTerminal (FunctorCoalgebras.CoAlg_category F') C0'. + Proof. + intro C'. + destruct (C0_is_final (FromCoalgInHSET C')) as [[φ p2] isunique]. + cbn in φ. + use tpair. + - use tpair. + + exact φ. + + change (pr2 C' -->[φ] pr2 C0'). + exact p2. + - intro ψ. + apply isunique. + Defined. + + End ToFinalInHSET. + + Section IngredientsOfAnAdjunction. + + Local Definition out_set_trunc (C : coalgebra F) : coalgebra_ob F C → pr1hSet (F' (settrunc (coalgebra_ob F C))). + Proof. + intro x. + destruct C as [c s_c]. + cbn -[settrunc]. + unfold polynomial_functor_obj. + use tpair. + - exact (pr1(s_c(x))). + - intro b. + exact (settruncin c (pr2(s_c(x))(b))). + Defined. + + Definition coalg_set_trunc (C : coalgebra F) : FunctorCoalgebras.CoAlg_category F'. + Proof. + exists (settrunc (coalgebra_ob F C)). + exact (settrunc_rec _ (out_set_trunc C)). + Defined. + + Lemma is_coalgebra_homo_comp_with_settruncin (C : coalgebra F) (C0' : FunctorCoalgebras.coalgebra_ob F') (f : FunctorCoalgebras.CoAlg_category F' ⟦coalg_set_trunc C, C0'⟧) + : is_coalgebra_homo F (X:=C) (Y:=FromCoalgInHSET C0') (λ x, pr1 f (settruncin ((coalgebra_ob F C)) x)). + Proof. + destruct f as [φ p1]. + set (s0' := FunctorCoalgebras.coalg_map F' C0'). + destruct C as [c s_c]. + cbn in c. + cbn in s_c. + unfold polynomial_functor_obj in s_c. + set (c' := settrunc c). + set (C' := coalg_set_trunc (c,, s_c) : FunctorCoalgebras.coalgebra_ob F'). + set (s_c' := FunctorCoalgebras.coalg_map _ C' : c' → pr1hSet (F' c')). + cbn -[settrunc] in φ. + set (ψ := λ x, φ(settruncin c x) : pr1 (FunctorCoalgebras.coalg_carrier F' C0')). + change (is_coalgebra_homo F (X:=(c,,s_c)) (Y:=FromCoalgInHSET C0') ψ). + unfold is_coalgebra_homo. + apply funextfun. + intro x. + cbn in x. + symmetry. + assert (p21 : (s0'(ψ(x)) = s0'(φ(settruncin c x)))). + { unfold ψ. apply idpath. } + assert (p22 : s0'(ψ(x)) = (#F φ)(s_c'(settruncin c x))). + { + etrans. + - apply p21. + - set (f1 := λ y : c', s0'(φ(y))). + set (f2 := λ y : c', (#F φ)(s_c'(y))). + set (x' := settruncin c x : c'). + assert (p221 : f1 = f2). + { cbn -[settrunc] in p1. unfold f1, f2. cbn -[settrunc]. unfold s0'. symmetry. apply p1. } + assert (p222 : f1 x' = f2 x'). + { apply (toforallpaths _ f1 f2 p221). } + apply p222. + } + assert (p23 : s0'(ψ(x)) = (#F ψ)(s_c(x))). + { + etrans. + - apply p22. + - apply idpath. + } + apply p23. + Qed. + + Lemma is_homo_of_coalgebras_settrunc_rec (C : coalgebra F) (C0' : FunctorCoalgebras.coalgebra_ob F') (f' : coalgebra_homo F _ (FromCoalgInHSET C0')) + : pr2 (coalg_set_trunc C) -->[settrunc_rec _ (pr1 f')] pr2 (FromCoalgInHSET C0'). + Proof. + destruct f' as [ψ' p']. + cbn in ψ'. + set (φ' := settrunc_rec _ ψ'). + destruct C as [c s_c]. + set (s0' := FunctorCoalgebras.coalg_map F' C0'). + set (C' := coalg_set_trunc (c,, s_c) : FunctorCoalgebras.coalgebra_ob F'). + set (s_c' := FunctorCoalgebras.coalg_map _ C'). + assert (p11' : (s0' ∘ φ' ∘ (settruncin c))%functions = ((#F φ') ∘ s_c' ∘ (settruncin c))%functions). + { + unfold is_coalgebra_homo in p'. + cbn in p'. + symmetry. + apply p'. + } + apply settrunc_rec_unique. + intro x. + apply pathsinv0. + apply (toforallpaths _ _ _ p11'). + Qed. + + End IngredientsOfAnAdjunction. + + Section FromFinalInHSET. + + Context (C0' : FunctorCoalgebras.coalgebra_ob F'). + Context (C0'_is_final : isTerminal (FunctorCoalgebras.CoAlg_category F') C0'). + + Definition C0 : coalgebra F := FromCoalgInHSET C0'. + + Lemma C0_is_final_unicity + {c : UU} + {s_c : c -> F c} + (C' := (coalg_set_trunc (c,, s_c) : FunctorCoalgebras.coalgebra_ob F') + : FunctorCoalgebras.coalgebra_ob F') + {f : FunctorCoalgebras.CoAlg_category F' ⟦ C', C0' ⟧} + (isunique : ∏ t : FunctorCoalgebras.CoAlg_category F' ⟦ C', C0' ⟧, t = f) + (f' : coalgebra_homo F (c,, s_c) C0) + : f' = + (λ x : coalgebra_ob F (c,, s_c), (pr1 f (settruncin (coalgebra_ob F (c,, s_c)) x)) : coalgebra_ob F C0),, + is_coalgebra_homo_comp_with_settruncin (c,, s_c) C0' f. + Proof. + set (φ' := settrunc_rec _ (pr1 f')). + set (p1' := is_homo_of_coalgebras_settrunc_rec _ _ f'). + assert (p41 : (φ',, p1') = f). + { + apply (isunique (φ',, p1')). + } + assert (p411 := maponpaths (λ x, pr1 x) p41 : (φ' = pr1 f)). + clear p41. + use total2_paths_f. + + apply funextfun. + intro x. + etrans. + * assert (p421 : pr1 f' x = φ' (settruncin c x)). + { + apply idpath. + } + apply p421. + * apply (toforallpaths _ φ' (pr1 f) p411). + + (* show_id_type. + unfold is_coalgebra_homo in TYPE. *) + set (is_set := isaset_forall_hSet c (λ _, F' (pr1 C0'))). + apply is_set. + Qed. + + Lemma C0_is_final : is_final C0. + Proof. + set (s0' := FunctorCoalgebras.coalg_map F' C0'). + intros [c s_c]. + cbn in c. + cbn in s_c. + unfold polynomial_functor_obj in s_c. + set (c' := settrunc c). + set (C' := coalg_set_trunc (c,, s_c) : FunctorCoalgebras.coalgebra_ob F'). + set (s_c' := FunctorCoalgebras.coalg_map _ C' : c' → pr1hSet (F' c')). + destruct (C0'_is_final C') as [f isunique]. + use tpair. + - use tpair. + 2: { apply (is_coalgebra_homo_comp_with_settruncin _ _ f). } + - intro f'. + apply C0_is_final_unicity. + apply isunique. + Defined. + + End FromFinalInHSET. + + Section FunctorAdjunctions_UU_HSET. + + (** If the definition of a coalgebra is tweaked, we can show an adjunction between the + two functors going from UU coalgebras to HSET coalgebras and vice versa. + This result shall not be used for other purposes but rather gives an intuition for + the results above. + *) + + Local Definition cat1 := UniMath.Induction.FunctorCoalgebras_legacy_alt_UU.CoAlg_precategory F. + Local Definition cat2 := CoAlg_precategory F'. + + (* HSET -> UU coalgebras functor*) + + Definition functor_coalgebra_HSET_to_UU_obj (C : FunctorCoalgebras.coalgebra_ob F') : (coalgebra F). + Proof. + exact (pr1 (pr1 C),, pr2 C). + Defined. + + Definition functor_coalgebra_HSET_to_UU_data : functor_data cat2 cat1. + Proof. + use make_functor_data. + - exact functor_coalgebra_HSET_to_UU_obj. + - intros a b f. + exists (pr1 f). + intro x. + exact (hinhpr (toforallpaths _ _ _ (pr2 f) x)). + Defined. + + Lemma functor_coalgebra_HSET_to_UU_is_functor : is_functor functor_coalgebra_HSET_to_UU_data. + Proof. + split. + - unfold functor_idax. + intro. + use total2_paths_f. + + apply idpath. + + use funextsec. intro. + apply isapropishinh. + - unfold functor_compax. + intros. + use total2_paths_f. + + apply idpath. + + use funextsec. intro. + apply isapropishinh. + Defined. + + Definition functor_coalgebra_HSET_to_UU : functor cat2 cat1 := _,, functor_coalgebra_HSET_to_UU_is_functor. + + (* UU -> HSET coalgebras functor *) + + Definition functor_coalgebra_UU_to_HSET_obj (C : coalgebra F) : FunctorCoalgebras.coalgebra_ob F'. + Proof. + exact (coalg_set_trunc C). + Defined. + + Lemma is_morph_UU_to_HSET {a b : coalgebra F} {f : type_precat ⟦ pr1 a, pr1 b ⟧} (x : pr1 a) (p : ((pr2 a) · #F f) x = (f · (pr2 b)) x ) : + tpair (λ a, pr1hSet (B a) -> settrunc (pr1 b)) (pr1 (((pr2 a) · #F f) x)) (λ y, settruncin _ (pr2 (((pr2 a) · #F f) x) y)) = tpair (λ a, pr1hSet (B a) -> settrunc (pr1 b)) (pr1 ((f · (pr2 b)) x)) (λ y, settruncin _ (pr2 ((f · (pr2 b)) x) y)). + Proof. + induction p. + apply idpath. + Defined. + + Definition functor_coalgebra_UU_to_HSET_data : functor_data cat1 cat2. + Proof. + use make_functor_data. + - exact functor_coalgebra_UU_to_HSET_obj. + - intros a b f. + cbn. + cbn -[settrunc]. + set (f0 := settrunc_rec _ (λ x, settruncin _ (pr1 f x)) : SET ⟦ pr1 (functor_coalgebra_UU_to_HSET_obj a), pr1 (functor_coalgebra_UU_to_HSET_obj b) ⟧). + assert (p1 : ∏ x : pr1 a, ∥ (pr2 (functor_coalgebra_UU_to_HSET_obj a) · # F' f0) (settruncin _ x) = (f0 · pr2 (functor_coalgebra_UU_to_HSET_obj b)) (settruncin _ x) ∥ ). + { + intro x. + cbn -[F']. + set (goal := ∥ # F' f0 (out_set_trunc a x) = out_set_trunc b (pr1 f x) ∥). + set (p11 := UniMath.Induction.FunctorCoalgebras_legacy_alt_UU.coalgebra_homo_commutes F f x goal). + apply p11. + cbn -[F F']. + intro p12. + set (p13 := is_morph_UU_to_HSET x p12). + exact (hinhpr p13). + } + assert (p2 : ∏ x : pr1 (settrunc (coalgebra_ob F a)), ∥ ((pr2 (functor_coalgebra_UU_to_HSET_obj a)) · #F' f0) x = (f0 · (pr2 (functor_coalgebra_UU_to_HSET_obj b))) x ∥). + { + use setquotunivprop'. + - intro. apply propproperty. + - apply p1. + } + assert (p3 : is_coalgebra_homo F' f0). + { + use funextfun. + intro x. + simple refine (factor_through_squash _ _ (p2 x)). + - apply setproperty. + - trivial. + } + exact (f0,, p3). + Defined. + + Lemma functor_coalgebra_UU_to_HSET_is_functor : is_functor functor_coalgebra_UU_to_HSET_data. + Proof. + split. + - intro. + use total2_paths_f. + + cbn -[settrunc]. + assert (p : ∏ x : pr1 a, settrunc_rec (FunctorCoalgebras_legacy_alt_UU.coalgebra_ob F a) (λ x : FunctorCoalgebras_legacy_alt_UU.coalgebra_ob F a, settruncin (FunctorCoalgebras_legacy_alt_UU.coalgebra_ob F a) x) (settruncin _ x) = (λ x : settrunc (coalgebra_ob F a), x) (settruncin _ x)). + { intro x. + apply idpath. + } + apply (settrunc_rec_unique _ _ _ p). + + apply isaset_forall_hSet. + - unfold functor_compax. + intros. + use total2_paths_f. + + assert (p : ∏ x : pr1 a, pr1 (# functor_coalgebra_UU_to_HSET_data (f · g)) (settruncin _ x)= + pr1 (# functor_coalgebra_UU_to_HSET_data f · # functor_coalgebra_UU_to_HSET_data g) (settruncin _ x)). + { intro x. apply idpath. } + apply (settrunc_rec_unique _ _ _ p). + + apply isaset_forall_hSet. + Defined. + + Definition functor_coalgebra_UU_to_HSET : functor cat1 cat2 := _,, functor_coalgebra_UU_to_HSET_is_functor. + + (* Adjunction *) + + Definition adj_unit_coalg_data : nat_trans_data (pr1 (functor_identity cat1)) (pr1 (functor_coalgebra_UU_to_HSET ∙ functor_coalgebra_HSET_to_UU)). + Proof. + unfold nat_trans_data. + intro X. + cbn. + unfold FunctorCoalgebras_legacy_alt_UU.coalgebra_homo. + cbn -[F F' settrunc]. + set (f := (settruncin (pr1 X)) : type_precat ⟦ FunctorCoalgebras_legacy_alt_UU.coalgebra_ob F X, FunctorCoalgebras_legacy_alt_UU.coalgebra_ob F ((functor_coalgebra_UU_to_HSET ∙ functor_coalgebra_HSET_to_UU) X) ⟧). + assert (p : ∏ x : FunctorCoalgebras_legacy_alt_UU.coalgebra_ob F X, ∥ (FunctorCoalgebras_legacy_alt_UU.is_coalgebra_homo F f x) ∥). + { + intro x. + exact (hinhpr (idpath ((#F f ∘ (pr2 X)) x))). + } + exact (f,, p). + Defined. + + Lemma adj_unit_coalg_is_nat_trans : is_nat_trans _ _ adj_unit_coalg_data. + Proof. + unfold is_nat_trans. + intros. + cbn -[F F' functor_coalgebra_UU_to_HSET functor_coalgebra_HSET_to_UU]. + use total2_paths_f. + - apply idpath. + - use funextsec. intro. apply isapropishinh. + Defined. + + Definition adj_unit_coalg : nat_trans _ _ := _,, adj_unit_coalg_is_nat_trans. + + Definition adj_counit_coalg_data : nat_trans_data (pr1 (functor_coalgebra_HSET_to_UU ∙ functor_coalgebra_UU_to_HSET)) (pr1 (functor_identity cat2)). + Proof. + unfold nat_trans_data. + intro X. + cbn. + cbn -[F F' settrunc]. + set (f := settrunc_rec _ (λ x : pr11 X, x) : SET ⟦ pr1 ((functor_coalgebra_HSET_to_UU ∙ functor_coalgebra_UU_to_HSET) X), pr1 X ⟧). + assert (p1 : ∏ x : pr1 (settrunc (pr11 X)), ∥ ((pr2 ((functor_coalgebra_HSET_to_UU ∙ functor_coalgebra_UU_to_HSET) X)) · #F' f) x = (f · pr2 X) x ∥). + { + use setquotunivprop'. + - intro. apply propproperty. + - intro. exact (hinhpr (idpath (((pr2 X) ∘ f) (settruncin _ x)))). + } + assert (p2 : is_coalgebra_homo F' f). + { + use funextfun. + intro x. + simple refine (factor_through_squash _ _ (p1 x)). + - apply setproperty. + - trivial. + } + exact (f,, p2). + Defined. + + Lemma adj_counit_coalg_is_nat_trans : is_nat_trans _ _ adj_counit_coalg_data. + Proof. + unfold is_nat_trans. + intros. + cbn -[F F' functor_coalgebra_UU_to_HSET functor_coalgebra_HSET_to_UU]. + use total2_paths_f. + - cbn -[F F' settrunc]. + use settrunc_rec_unique. + intro. apply idpath. + - apply isaset_forall_hSet. + Defined. + + Definition adj_counit_coalg : nat_trans _ _ := _,, adj_counit_coalg_is_nat_trans. + + Lemma adj_coalg : are_adjoints functor_coalgebra_UU_to_HSET functor_coalgebra_HSET_to_UU. + Proof. + assert (p : form_adjunction _ _ adj_unit_coalg adj_counit_coalg). + { + use make_form_adjunction. + - intro. + use total2_paths_f. + + cbn -[F F' settrunc]. + use settrunc_rec_unique. + intro. apply idpath. + + apply isaset_forall_hSet. + - intro. + use total2_paths_f. + + apply idpath. + + use funextsec. intro. apply isapropishinh. + } + exact ((adj_unit_coalg,, adj_counit_coalg),, p). + Defined. + + End FunctorAdjunctions_UU_HSET. +End M. diff --git a/UniMath/Induction/SetBasedPolynomialFunctors.v b/UniMath/Induction/SetBasedPolynomialFunctors.v new file mode 100644 index 0000000000..07043a7008 --- /dev/null +++ b/UniMath/Induction/SetBasedPolynomialFunctors.v @@ -0,0 +1,56 @@ +(** ** Set Based Polynomial Functors + + Author : Ralph Matthes (@rmatthes), 2025 + +*) + +Require Import UniMath.Induction.PolynomialFunctors. +Require Import UniMath.Induction.M.Core. +Require Import UniMath.CategoryTheory.Categories.Type.Core. +Require Import UniMath.Foundations.Sets. +Require Import UniMath.CategoryTheory.Core.Categories. +Require Import UniMath.CategoryTheory.Core.Functors. +Require Import UniMath.CategoryTheory.DisplayedCats.Core. +Require Import UniMath.CategoryTheory.Categories.HSET.All. + +Local Open Scope cat. + +Section SetBasedPolynomialFunctors. + + Context (A : hSet). + Context (B : A -> hSet). + + Definition polynomial_functor_HSET_obj (X : hSet) : hSet. + Proof. + exists (polynomial_functor_obj (pr1hSet A) (fun a => pr1hSet (B a)) X). + unfold polynomial_functor_obj. + transparent assert (f : (pr1hSet A -> hSet)). + { intro a. + use tpair. + - exact (pr1hSet (B a) -> pr1hSet X). + - apply isaset_forall_hSet. + } + exact (isaset_total2_hSet _ f). + Defined. + + Definition polynomial_functor_HSET_data : functor_data HSET HSET. + Proof. + use make_functor_data. + - exact polynomial_functor_HSET_obj. + - intros X Y. + simpl. + apply (polynomial_functor_arr (pr1hSet A) (fun a => pr1hSet (B a))). + Defined. + + Lemma polynomial_functor_HSET_is_functor : is_functor polynomial_functor_HSET_data. + Proof. + split. + - intro. + apply idpath. + - intros ? ? ? ? ?. + apply idpath. + Qed. + + Definition polynomial_functor_HSET : functor HSET HSET := _ ,, polynomial_functor_HSET_is_functor. + +End SetBasedPolynomialFunctors. diff --git a/UniMath/MoreFoundations/DecidablePropositions.v b/UniMath/MoreFoundations/DecidablePropositions.v index 41f231a4b2..744860fde9 100644 --- a/UniMath/MoreFoundations/DecidablePropositions.v +++ b/UniMath/MoreFoundations/DecidablePropositions.v @@ -456,6 +456,39 @@ Definition natneq_DecidableProposition : DecidableRelation nat := End DecidablePropositions. +Section DecidableEquality. + +Lemma isdeceq_subtype {X : UU} (P : hsubtype X) : + isdeceq X → isdeceq P. +Proof. + intros deceqX predP. apply isdeceq_total2. + + apply deceqX. + + intros x. apply isdeceqifisaprop, propproperty. +Qed. + + Definition singleton_complement {X : UU} (y : X) : hsubtype X := λ x, make_hProp (x != y) (isapropneg (x = y)). + + Lemma weq_singleton_complement_unit {X : UU} (y : X) : isdeceq X → carrier (singleton_complement y) ⨿ unit ≃ X. + Proof. + intros deceqx. + use weq_iso. + - intros [[x neq] | tt]; [apply x | apply y]. + - intros x. induction (deceqx x y); [right; apply tt | left]. + apply tpair with (pr1 := x), b. + - intros [[x neq] | tt]. + + induction (deceqx x y). + * apply fromempty. induction neq. assumption. + * cbn. apply maponpaths, subtypePath_prop, idpath. + + induction (deceqx y y). + * induction tt. apply idpath. + * apply fromempty, b, idpath. + - intros x; cbn beta. + induction (deceqx x y); cbn beta; + try induction a; apply idpath. + Qed. + +End DecidableEquality. + Declare Scope decidable_nat. Notation " x < y " := (natlth_DecidableProposition x y) (at level 70, no associativity) : decidable_nat. diff --git a/UniMath/MoreFoundations/Sets.v b/UniMath/MoreFoundations/Sets.v index 5ad3989281..25e24a1bfe 100644 --- a/UniMath/MoreFoundations/Sets.v +++ b/UniMath/MoreFoundations/Sets.v @@ -12,6 +12,7 @@ Require Export UniMath.Foundations.Sets. - The equivalence relation of being in the same fiber - Subsets - Binary relations + - Set truncation *) Local Open Scope logic. @@ -497,3 +498,105 @@ Proof. rewrite hSet_univalence_map_univalence_hSet. apply idpath. Qed. + +(** ** Set truncation + Based on a post by Niels van der Weide on June 13, 2023 + *) + +Local Close Scope logic. + +Lemma path_eqrel_iseqrel + (X : UU) + : iseqrel (λ x₁ x₂ : X, ∥ x₁ = x₂ ∥ : hProp). +Proof. + repeat split. + + intros x₁ x₂ x₃. + use factor_through_squash. + { + apply impred ; intro. + apply propproperty. + } + intro p. + use factor_through_squash. + { + apply propproperty. + } + intro q. + apply hinhpr. + exact (p @ q). + + intros x. + exact (hinhpr (idpath _)). + + intros x₁ x₂. + use factor_through_squash. + { + apply propproperty. + } + intro p. + apply hinhpr. + exact (!p). +Qed. + +Definition path_eqrel + (X : UU) + : eqrel X. +Proof. + use make_eqrel. + - exact (λ x₁ x₂, ∥ x₁ = x₂ ∥ : hProp). + - apply path_eqrel_iseqrel. +Defined. + +Definition settrunc + (X : UU) + : hSet + := setquotinset (path_eqrel X). + +Definition settruncin + (X : UU) + : X → settrunc X + := setquotpr (path_eqrel X). + + +Definition settrunc_rec + (X : UU) + {Y : hSet} + (i : X → Y) + : settrunc X → Y. +Proof. + use setquotuniv. + - exact i. + - intros x₁ x₂. + use factor_through_squash. + { + apply setproperty. + } + intro p. + exact (maponpaths i p). +Defined. + +Definition settrunc_rec_eq + (X : UU) + {Y : hSet} + (i : X → Y) + (x : X) + : settrunc_rec X i (settruncin X x) = i x. +Proof. + apply idpath. +Qed. + +Definition settrunc_rec_unique + (X : UU) + {Y : hSet} + (f g : settrunc X → Y) + (p : ∏ (x : X), f (settruncin X x) = g (settruncin X x)) + : f = g. +Proof. + use funextsec. + use setquotunivprop'. + { + intro. + apply setproperty. + } + intro x. + cbn. + exact (p x). +Qed. diff --git a/UniMath/Topology/Prelim.v b/UniMath/Topology/Prelim.v index b6eb62a9e6..a8fe3e7188 100644 --- a/UniMath/Topology/Prelim.v +++ b/UniMath/Topology/Prelim.v @@ -3,7 +3,9 @@ Require Export UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Subtypes. -Require Export UniMath.Combinatorics.FiniteSequences. +Require Export UniMath.Combinatorics.StandardFiniteSets. +Require Export UniMath.Combinatorics.FVectors. +Require Export UniMath.Combinatorics.FLists. Require Export UniMath.Foundations.NaturalNumbers. Require Export UniMath.Tactics.EnsureStructuredProofs.