From bc69b93514f95af505d7356fc007570c89843be5 Mon Sep 17 00:00:00 2001 From: Nickolay Kudasov Date: Sat, 14 Mar 2020 01:48:21 +0300 Subject: [PATCH 1/6] Add reluniv_cat_is_univalent proof --- TypeTheory/ALV2/RelUniv_Cat_Simple.v | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/TypeTheory/ALV2/RelUniv_Cat_Simple.v b/TypeTheory/ALV2/RelUniv_Cat_Simple.v index 7b4a5343..c02bcc15 100644 --- a/TypeTheory/ALV2/RelUniv_Cat_Simple.v +++ b/TypeTheory/ALV2/RelUniv_Cat_Simple.v @@ -195,10 +195,10 @@ End RelUniv_Cat_Simple. Definition reluniv_cat : category := gen_reluniv_cat rel_universe_structure. + Definition weak_reluniv_cat : category := gen_reluniv_cat is_universe_relative_to. - Section WeakRelUniv_is_univalent. Definition is_weak_reluniv_ob @@ -426,6 +426,23 @@ Section RelUniv_Functor. - apply (weqproperty (weq_relative_universe_weak_relative_universe _ Ccat J_ff)). Defined. + Definition weak_from_reluniv_functor_catiso + (Ccat : is_univalent C) (J_ff : fully_faithful J) + : catiso (reluniv_cat J) (weak_reluniv_cat J) + := (weak_from_reluniv_functor + ,, weak_from_reluniv_functor_is_catiso Ccat J_ff). + + Definition reluniv_cat_is_univalent + (Ccat : is_univalent C) (J_ff : fully_faithful J) + (Dcat : is_univalent D) + : is_univalent (reluniv_cat J). + Proof. + use (catiso_univalent + _ _ (weak_from_reluniv_functor_catiso Ccat J_ff)). + apply weak_reluniv_cat_is_univalent. + apply Dcat. + Defined. + Definition weak_reluniv_isaset (obD_isaset : isaset (ob D)) : isaset (weak_reluniv_cat J). From 8135b70bebf9341d8719d0b7d682c789983f4e20 Mon Sep 17 00:00:00 2001 From: Nickolay Kudasov Date: Sat, 14 Mar 2020 01:58:59 +0300 Subject: [PATCH 2/6] Complete the proof of issurjective reluniv_J_to_J' functor --- TypeTheory/ALV2/RelUnivTransfer.v | 110 ++++-------------------------- 1 file changed, 15 insertions(+), 95 deletions(-) diff --git a/TypeTheory/ALV2/RelUnivTransfer.v b/TypeTheory/ALV2/RelUnivTransfer.v index b07cf706..85cd5030 100644 --- a/TypeTheory/ALV2/RelUnivTransfer.v +++ b/TypeTheory/ALV2/RelUnivTransfer.v @@ -335,8 +335,7 @@ Section RelUniv_Transfer. Defined. Section SURJECTIVE. - Context (D_univ : is_univalent D) - (R_ses : split_ess_surj R) + Context (R_ses : split_ess_surj R) (D'_univ : is_univalent D') (invS : functor D' D) (eta : iso (C:=[D, D, pr2 D]) (functor_identity D) (S ∙ invS)) @@ -547,10 +546,6 @@ Section RelUniv_Transfer. End Helpers. - Axiom STUCK : ∏ X : UU, X. - - Search paths. - Definition inv_reluniv_with_ess_surj : reluniv_cat J' → reluniv_cat J. Proof. @@ -567,32 +562,7 @@ Section RelUniv_Transfer. * apply pb_commutes_and_is_pullback. Defined. - Definition inv_reluniv_with_ess_surj_preserves_mor_total - (u' : reluniv_cat J') - : pr1 (reluniv_functor_with_ess_surj (inv_reluniv_with_ess_surj u')) - = pr1 u'. - Proof. - set (S_weq_on_mor_total - := isweq_left_adj_equivalence_on_mor_total - S D_univ D'_univ AE - : isweq (functor_on_mor_total S)). - apply (homotweqinvweq - (functor_on_mor_total S,,S_weq_on_mor_total)). - Defined. - - Search (∑ (e : ?a = ?a'), _). - Search total2_paths_f. - - Definition maponpaths_pr2_total2_paths_f - (A : Type) (B : A → Type) - (ab ab' : ∑ a : A, B a) - (e : ab = ab') - : transportf _ (maponpaths pr1 e) (pr2 ab) = pr2 ab'. - Proof. - induction e. apply idpath. - Defined. - - Definition reluniv_functor_with_ess_surj_after_inv + Definition reluniv_functor_with_ess_surj_after_inv_iso (u' : reluniv_cat J') : iso u' (reluniv_functor_with_ess_surj (inv_reluniv_with_ess_surj u')). @@ -627,6 +597,18 @@ Section RelUniv_Transfer. * apply (maponpaths (λ k, pr1 k _) (iso_inv_after_iso ε)). Defined. + Definition reluniv_functor_with_ess_surj_after_inv_id + (u' : reluniv_cat J') + : u' = reluniv_functor_with_ess_surj (inv_reluniv_with_ess_surj u'). + Proof. + use isotoid. + - use reluniv_cat_is_univalent. + + apply C'_univ. + + apply ff_J'. + + apply D'_univ. + - apply reluniv_functor_with_ess_surj_after_inv_iso. + Defined. + Definition reluniv_functor_with_ess_surj_issurjective : issurjective reluniv_functor_with_ess_surj. Proof. @@ -634,44 +616,7 @@ Section RelUniv_Transfer. use hinhpr. use tpair. - apply (inv_reluniv_with_ess_surj u'). - - use isotoid. - use (invmaponpathsweq (weqtotal2asstor _ _)). - use total2_paths_f. - + apply (maponpaths pr1 (inv_reluniv_with_ess_surj_preserves_mor_total u')). - + use total2_paths_f. - * etrans. use (pr1_transportf (D' × D')). - use maponpaths_pr2_total2_paths_f. - * etrans. refine (transportf_forall _ _ _). - apply funextsec. intros X'. - etrans. refine (transportf_forall _ _ _). - apply funextsec. intros f'. - use total2_paths_f. - -- use total2_paths_f. - ++ etrans. apply maponpaths. use pr1_transportf. - etrans. use (pr1_transportf (D' ⟦ _, _ ⟧)). - use isotoid. apply C'_univ. - (* we know that Xf' = R (invR Xf'') - * where Xf'' = R(invR X).(_ ;; # S (# invS f) ;; _) - * and invR is the inverse on objects given - * by R being (split) essentially surjective - * However for some reason (because of transportf?) - * pr2 (R_ses _) does not apply :( - *) - apply STUCK. (* Xf' *) - ++ use dirprod_paths. - ** (* This one will probably the hardest to prove formally - * since it is in C' and is constructed - * by going between categories a lot. - *) - apply STUCK. (* pp' *) - ** (* This one should be fairly easy since - * it is only mapped with S and invS - * with some isos prepended to it in both maps - *) - apply STUCK. (* Q' *) - -- use dirprod_paths. - ++ apply homset_property. - ++ apply isaprop_isPullback. + - apply pathsinv0, reluniv_functor_with_ess_surj_after_inv_id. Defined. End SURJECTIVE. @@ -885,30 +830,6 @@ Section WeakRelUniv_Transfer. apply weak_relu_square_commutes. Defined. - Definition reluniv_functor_with_ess_surj_issurjective - (C'_univ : is_univalent C') - (AC : AxiomOfChoice.AxiomOfChoice) - (obC_isaset : isaset C) - : issurjective (reluniv_functor_with_ess_surj - _ _ _ _ J J' - R S α α_is_iso - S_pb C'_univ ff_J' S_full R_es - ). - Proof. - set (W := (weak_from_reluniv_functor J' - ,, weak_from_reluniv_functor_is_catiso J' C'_univ ff_J') - : catiso _ _). - use (Core.issurjective_postcomp_with_weq _ (catiso_ob_weq W)). - use (transportf (λ F, issurjective (pr11 F)) - (! weak_relu_square_commutes_strictly C'_univ)). - use issurjcomp. - - apply weak_from_reluniv_functor_issurjective. - apply AC. - apply obC_isaset. - - apply issurjectiveweq. - apply (catiso_ob_weq (_,,weak_reluniv_functor_is_catiso)). - Defined. - End WeakRelUniv_Transfer. Section RelUniv_Yo_Rezk. @@ -961,7 +882,6 @@ Section RelUniv_Yo_Rezk. use (reluniv_functor_with_ess_surj_issurjective _ _ _ _ Yo Yo _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - AC obC_isaset ). - apply is_univalent_preShv. - apply is_univalent_preShv. From 3445c39692d3f6577d587a92bd83fce13278e4be Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Mon, 20 Apr 2020 00:15:17 +0300 Subject: [PATCH 3/6] Keep both proofs for surjectivity of relative universe transfer functor --- TypeTheory/ALV2/RelUnivTransfer.v | 34 +++++++++++++++++++++++++++---- 1 file changed, 30 insertions(+), 4 deletions(-) diff --git a/TypeTheory/ALV2/RelUnivTransfer.v b/TypeTheory/ALV2/RelUnivTransfer.v index 85cd5030..685c7ae1 100644 --- a/TypeTheory/ALV2/RelUnivTransfer.v +++ b/TypeTheory/ALV2/RelUnivTransfer.v @@ -334,7 +334,7 @@ Section RelUniv_Transfer. - apply reluniv_functor_with_ess_surj_is_faithful, S_faithful. Defined. - Section SURJECTIVE. + Section Surjective_if_R_split_ess_surj. Context (R_ses : split_ess_surj R) (D'_univ : is_univalent D') (invS : functor D' D) @@ -619,7 +619,7 @@ Section RelUniv_Transfer. - apply pathsinv0, reluniv_functor_with_ess_surj_after_inv_id. Defined. - End SURJECTIVE. + End Surjective_if_R_split_ess_surj. End RelUniv_Transfer_with_ess_surj. @@ -830,6 +830,30 @@ Section WeakRelUniv_Transfer. apply weak_relu_square_commutes. Defined. + Definition reluniv_functor_with_ess_surj_issurjective_AC + (C'_univ : is_univalent C') + (AC : AxiomOfChoice.AxiomOfChoice) + (obC_isaset : isaset C) + : issurjective (reluniv_functor_with_ess_surj + _ _ _ _ J J' + R S α α_is_iso + S_pb C'_univ ff_J' S_full R_es + ). + Proof. + set (W := (weak_from_reluniv_functor J' + ,, weak_from_reluniv_functor_is_catiso J' C'_univ ff_J') + : catiso _ _). + use (Core.issurjective_postcomp_with_weq _ (catiso_ob_weq W)). + use (transportf (λ F, issurjective (pr11 F)) + (! weak_relu_square_commutes_strictly C'_univ)). + use issurjcomp. + - apply weak_from_reluniv_functor_issurjective. + apply AC. + apply obC_isaset. + - apply issurjectiveweq. + apply (catiso_ob_weq (_,,weak_reluniv_functor_is_catiso)). + Defined. + End WeakRelUniv_Transfer. Section RelUniv_Yo_Rezk. @@ -879,7 +903,7 @@ Section RelUniv_Yo_Rezk. (obC_isaset : isaset C) : issurjective transfer_of_RelUnivYoneda_functor. Proof. - use (reluniv_functor_with_ess_surj_issurjective + use (reluniv_functor_with_ess_surj_issurjective_AC _ _ _ _ Yo Yo _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ). @@ -891,6 +915,8 @@ Section RelUniv_Yo_Rezk. - apply fully_faithful_implies_full_and_faithful. apply right_adj_equiv_is_ff. - apply R_full. + - apply AC. + - apply obC_isaset. Defined. Definition transfer_of_WeakRelUnivYoneda_functor @@ -928,4 +954,4 @@ Section RelUniv_Yo_Rezk. apply weak_relu_square_commutes_strictly. Defined. -End RelUniv_Yo_Rezk. \ No newline at end of file +End RelUniv_Yo_Rezk. From 190ea0bf28bfc2124d95d93c1e7401465f2663f3 Mon Sep 17 00:00:00 2001 From: Benedikt Ahrens Date: Tue, 21 Apr 2020 17:06:44 -0400 Subject: [PATCH 4/6] Update TypeTheory/ALV2/RelUnivTransfer.v --- TypeTheory/ALV2/RelUnivTransfer.v | 1 - 1 file changed, 1 deletion(-) diff --git a/TypeTheory/ALV2/RelUnivTransfer.v b/TypeTheory/ALV2/RelUnivTransfer.v index 685c7ae1..537b39ba 100644 --- a/TypeTheory/ALV2/RelUnivTransfer.v +++ b/TypeTheory/ALV2/RelUnivTransfer.v @@ -31,7 +31,6 @@ Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.Equivalences.Core. Set Automatic Introduction. -Set Nested Proofs Allowed. Section RelUniv_Transfer. From 99b42b6fec27d98e87ec63d494b5ecb7d16992f7 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Wed, 22 Apr 2020 09:35:42 +0300 Subject: [PATCH 5/6] Remove Check command --- TypeTheory/ALV2/RelUnivTransfer.v | 1 - 1 file changed, 1 deletion(-) diff --git a/TypeTheory/ALV2/RelUnivTransfer.v b/TypeTheory/ALV2/RelUnivTransfer.v index 537b39ba..27a8414e 100644 --- a/TypeTheory/ALV2/RelUnivTransfer.v +++ b/TypeTheory/ALV2/RelUnivTransfer.v @@ -404,7 +404,6 @@ Section RelUniv_Transfer. Local Definition pb_commutes_and_is_pullback : commutes_and_is_pullback f p (# J pp) Q. Proof. - Check @commutes_and_is_pullback_transfer_iso. use (@commutes_and_is_pullback_transfer_iso _ _ _ _ _ _ _ _ _ From 355f6875336e36fd869d1f68bf32c56f4c40a26f Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Wed, 22 Apr 2020 09:38:59 +0300 Subject: [PATCH 6/6] Rename ..._commutes_strictly to ..._commutes_identity --- TypeTheory/ALV2/RelUnivTransfer.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/TypeTheory/ALV2/RelUnivTransfer.v b/TypeTheory/ALV2/RelUnivTransfer.v index 27a8414e..11782c66 100644 --- a/TypeTheory/ALV2/RelUnivTransfer.v +++ b/TypeTheory/ALV2/RelUnivTransfer.v @@ -816,7 +816,7 @@ Section WeakRelUniv_Transfer. - apply weak_relu_square_nat_trans_is_nat_iso. Defined. - Definition weak_relu_square_commutes_strictly + Definition weak_relu_square_commutes_identity (C'_univ : is_univalent C') : (relu_J_to_relu_J' C'_univ ∙ weak_from_reluniv_functor J') = (weak_from_reluniv_functor J ∙ weak_reluniv_functor). @@ -843,7 +843,7 @@ Section WeakRelUniv_Transfer. : catiso _ _). use (Core.issurjective_postcomp_with_weq _ (catiso_ob_weq W)). use (transportf (λ F, issurjective (pr11 F)) - (! weak_relu_square_commutes_strictly C'_univ)). + (! weak_relu_square_commutes_identity C'_univ)). use issurjcomp. - apply weak_from_reluniv_functor_issurjective. apply AC. @@ -945,11 +945,11 @@ Section RelUniv_Yo_Rezk. apply weak_reluniv_functor_is_catiso. Defined. - Definition WeakRelUnivYoneda_functor_square_commutes_strictly + Definition WeakRelUnivYoneda_functor_square_commutes_identity : (transfer_of_RelUnivYoneda_functor ∙ weak_from_reluniv_functor _) = (weak_from_reluniv_functor _ ∙ transfer_of_WeakRelUnivYoneda_functor). Proof. - apply weak_relu_square_commutes_strictly. + apply weak_relu_square_commutes_identity. Defined. End RelUniv_Yo_Rezk.