From 2598dbb42fa82989157bd87fbf1d2fccdd1d474c Mon Sep 17 00:00:00 2001 From: VojtechStep Date: Sun, 19 May 2024 00:41:50 +0200 Subject: [PATCH] Induction principle of identity types of coequalizers --- references.bib | 13 + src/synthetic-homotopy-theory.lagda.md | 1 + ...ciple-identity-types-coequalizers.lagda.md | 392 ++++++++++++++++++ 3 files changed, 406 insertions(+) create mode 100644 src/synthetic-homotopy-theory/induction-principle-identity-types-coequalizers.lagda.md diff --git a/references.bib b/references.bib index 7f75bb02cd..3037943650 100644 --- a/references.bib +++ b/references.bib @@ -251,6 +251,19 @@ @online{GGMS24 keywords = {Computer Science - Logic in Computer Science,Mathematics - Logic} } +@inproceedings{KvR21, + title = {Path spaces of higher inductive types in homotopy type theory}, + author = {Kraus, Nicolai and von Raumer, Jakob}, + year = {2021}, + publisher = {IEEE Press}, + abstract = {The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove a theorem about equality types of coequalizers and pushouts, reminiscent of an induction principle and without any restrictions on the truncation levels. This result makes it possible to reason directly about certain equality types and to streamline existing proofs by eliminating the necessity of auxiliary constructions. To demonstrate this, we give a very short argument for the calculation of the fundamental group of the circle (Licata and Shulman [1]), and for the fact that pushouts preserve embeddings. Further, our development suggests a higher version of the Seifert-van Kampen theorem, and the set-truncation operator maps it to the standard Seifert-van Kampen theorem (due to Favonia and Shulman [2]). We provide a formalization of the main technical results in the proof assistant Lean.}, + booktitle = {Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science}, + articleno = {7}, + numpages = {13}, + location = {Vancouver, Canada}, + series = {LICS '19} +} + @article{KECA17, title = {{Notions of Anonymous Existence in {{Martin-L\"of}} Type Theory}}, author = {Nicolai Kraus and Martín Escardó and Thierry Coquand and Thorsten Altenkirch}, diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md index beb0fd0ca1..bb09b6713e 100644 --- a/src/synthetic-homotopy-theory.lagda.md +++ b/src/synthetic-homotopy-theory.lagda.md @@ -73,6 +73,7 @@ open import synthetic-homotopy-theory.functoriality-sequential-colimits public open import synthetic-homotopy-theory.functoriality-suspensions public open import synthetic-homotopy-theory.groups-of-loops-in-1-types public open import synthetic-homotopy-theory.hatchers-acyclic-type public +open import synthetic-homotopy-theory.induction-principle-identity-types-coequalizers public open import synthetic-homotopy-theory.induction-principle-pushouts public open import synthetic-homotopy-theory.infinite-complex-projective-space public open import synthetic-homotopy-theory.infinite-cyclic-types public diff --git a/src/synthetic-homotopy-theory/induction-principle-identity-types-coequalizers.lagda.md b/src/synthetic-homotopy-theory/induction-principle-identity-types-coequalizers.lagda.md new file mode 100644 index 0000000000..7189f2e795 --- /dev/null +++ b/src/synthetic-homotopy-theory/induction-principle-identity-types-coequalizers.lagda.md @@ -0,0 +1,392 @@ +# The induction principle of identity types of coequalizers + +```agda +{-# OPTIONS --lossy-unification #-} +module synthetic-homotopy-theory.induction-principle-identity-types-coequalizers where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.double-arrows +open import foundation.equivalences +open import foundation.function-types +open import foundation.fundamental-theorem-of-identity-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.singleton-induction +open import foundation.torsorial-type-families +open import foundation.transport-along-identifications +open import foundation.universal-property-identity-types +open import foundation.universe-levels + +open import synthetic-homotopy-theory.coforks +open import synthetic-homotopy-theory.descent-data-coequalizers +open import synthetic-homotopy-theory.descent-data-coequalizers-equivalence-families +open import synthetic-homotopy-theory.descent-data-coequalizers-function-families +open import synthetic-homotopy-theory.descent-property-coequalizers +open import synthetic-homotopy-theory.equivalences-descent-data-coequalizers +open import synthetic-homotopy-theory.families-descent-data-coequalizers +open import synthetic-homotopy-theory.flattening-lemma-coequalizers +open import synthetic-homotopy-theory.morphisms-descent-data-coequalizers +open import synthetic-homotopy-theory.sections-descent-data-coequalizers +open import synthetic-homotopy-theory.universal-property-coequalizers +``` + +
+ +## Idea + +The formalization is inspired by {{#cite KvR21}}, but uses the dependent +induction principle instead of recursion and uniqueness (i.e. initiality), and +doesn't use wild categories for the arguments. + +## Definitions + +### The induction principle of descent data for identity types of coequalizers + +```agda +module _ + {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2} + (P : descent-data-coequalizer F l3) + (Q : descent-data-coequalizer F l4) + where + + ev-point-hom-descent-data-coequalizer : + {b : codomain-double-arrow F} (p : family-descent-data-coequalizer P b) → + hom-descent-data-coequalizer P Q → + family-descent-data-coequalizer Q b + ev-point-hom-descent-data-coequalizer p h = + map-hom-descent-data-coequalizer P Q h _ p + +module _ + {l1 l2 l3 : Level} {F : double-arrow l1 l2} + (P : descent-data-coequalizer F l3) + {b₀ : codomain-double-arrow F} + (p₀ : family-descent-data-coequalizer P b₀) + where + + induction-principle-descent-data-identity-type-coequalizer : UUω + induction-principle-descent-data-identity-type-coequalizer = + {l : Level} + (Q : + descent-data-coequalizer + ( double-arrow-flattening-lemma-descent-data-coequalizer P) + ( l)) → + (q₀ : family-descent-data-coequalizer Q (b₀ , p₀)) → + Σ ( section-descent-data-coequalizer Q) + ( λ s → pr1 s (b₀ , p₀) ＝ q₀) +``` + +### Canonical descent data for identity types of coequalizers + +```agda +module _ + {l1 l2 l3 : Level} {F : double-arrow l1 l2} + {X : UU l3} (c : cofork F X) + (x₀ : X) + where + + descent-data-coequalizer-identity-type : + descent-data-coequalizer F l3 + pr1 descent-data-coequalizer-identity-type b = + x₀ ＝ map-cofork c b + pr2 descent-data-coequalizer-identity-type a = + equiv-concat' x₀ (coh-cofork c a) + + equiv-descent-data-coequalizer-identity-type : + equiv-descent-data-coequalizer + ( descent-data-family-cofork c + ( λ x → x₀ ＝ x)) + ( descent-data-coequalizer-identity-type) + pr1 equiv-descent-data-coequalizer-identity-type _ = + id-equiv + pr2 equiv-descent-data-coequalizer-identity-type a = + tr-Id-right (coh-cofork c a) + + family-with-descent-data-coequalizer-identity-type : + family-with-descent-data-coequalizer c l3 + pr1 family-with-descent-data-coequalizer-identity-type x = + x₀ ＝ x + pr1 (pr2 family-with-descent-data-coequalizer-identity-type) = + descent-data-coequalizer-identity-type + pr2 (pr2 family-with-descent-data-coequalizer-identity-type) = + equiv-descent-data-coequalizer-identity-type +``` + +## Properties + +### The canonical descent data for identity types of coequalizers satisfies the induction principle + +```agda +module _ + {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2} + {X : UU l3} {c : cofork F X} + (b₀ : codomain-double-arrow F) + (Q : family-with-descent-data-coequalizer c l4) + where + + pentagon-ev-point-hom-descent-data-coequalizer : + ( ( map-family-with-descent-data-coequalizer Q b₀) ∘ + ( ev-refl + ( map-cofork c b₀) + { B = + λ x _ → family-cofork-family-with-descent-data-coequalizer Q x})) ~ + ( ( ev-point-hom-descent-data-coequalizer + ( descent-data-coequalizer-identity-type c (map-cofork c b₀)) + ( descent-data-family-with-descent-data-coequalizer Q) + ( refl)) ∘ + ( map-equiv + ( compute-section-family-cofork-function-family + ( family-with-descent-data-coequalizer-identity-type c + ( map-cofork c b₀)) + ( Q))) ∘ + ( section-descent-data-section-family-cofork + ( family-with-descent-data-coequalizer-function-family + ( family-with-descent-data-coequalizer-identity-type c + ( map-cofork c b₀)) + ( Q)))) + pentagon-ev-point-hom-descent-data-coequalizer = refl-htpy + +module _ + {l1 l2 l3 : Level} {F : double-arrow l1 l2} + {X : UU l3} {c : cofork F X} + (up-c : universal-property-coequalizer c) + (b₀ : codomain-double-arrow F) + where + + is-equiv-ev-point-hom-descent-data-coequalizer-identity-type : + {l4 : Level} (Q : family-with-descent-data-coequalizer c l4) → + is-equiv + ( ev-point-hom-descent-data-coequalizer + ( descent-data-coequalizer-identity-type c (map-cofork c b₀)) + ( descent-data-family-with-descent-data-coequalizer Q) + ( refl)) + is-equiv-ev-point-hom-descent-data-coequalizer-identity-type Q = + is-equiv-right-map-triangle + ( ( map-family-with-descent-data-coequalizer Q b₀) ∘ + ( ev-refl + ( map-cofork c b₀) + { B = + λ x _ → family-cofork-family-with-descent-data-coequalizer Q x})) + ( ev-point-hom-descent-data-coequalizer + ( descent-data-coequalizer-identity-type c (map-cofork c b₀)) + ( descent-data-family-with-descent-data-coequalizer Q) + ( refl)) + ( ( map-equiv + ( compute-section-family-cofork-function-family + ( family-with-descent-data-coequalizer-identity-type c + ( map-cofork c b₀)) + ( Q))) ∘ + ( section-descent-data-section-family-cofork + ( family-with-descent-data-coequalizer-function-family + ( family-with-descent-data-coequalizer-identity-type c + ( map-cofork c b₀)) + ( Q)))) + ( pentagon-ev-point-hom-descent-data-coequalizer b₀ Q) + ( is-equiv-comp _ _ + ( is-equiv-ev-refl (map-cofork c b₀)) + ( is-equiv-map-family-with-descent-data-coequalizer Q b₀)) + ( is-equiv-comp _ _ + ( is-equiv-section-descent-data-section-family-cofork _ up-c) + ( is-equiv-map-equiv + ( compute-section-family-cofork-function-family _ _))) + +module _ + {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2} + {X : UU l3} {c : cofork F X} + (up-c : universal-property-coequalizer c) + (b₀ : codomain-double-arrow F) + where + + induction-principle-identity-type-descent-data-coequalizer-identity-type : + induction-principle-descent-data-identity-type-coequalizer + ( descent-data-coequalizer-identity-type c (map-cofork c b₀)) + ( refl) + induction-principle-identity-type-descent-data-coequalizer-identity-type + Q q₀ = + ( ( λ b → + map-hom-descent-data-coequalizer _ _ + ( map-inv-is-equiv is-equiv-ev-point-Q q₀) + ( b) + ( eq-is-contr (is-torsorial-Id (map-cofork c b₀)))) , + ( λ (a , p) → + inv + ( ( ap + ( map-hom-descent-data-coequalizer _ _ + ( map-inv-is-equiv is-equiv-ev-point-Q q₀) + ( right-map-double-arrow F a , p ∙ coh-cofork c a)) + ( eq-is-contr + ( is-prop-is-contr (is-torsorial-Id (map-cofork c b₀)) _ _))) ∙ + ( coherence-hom-descent-data-coequalizer _ _ + ( map-inv-is-equiv is-equiv-ev-point-Q q₀) + ( a , p) + ( eq-is-contr (is-torsorial-Id (map-cofork c b₀))))))) , + ( ( ap + ( map-hom-descent-data-coequalizer _ _ + ( map-inv-is-equiv is-equiv-ev-point-Q q₀) + ( b₀ , refl)) + ( left-inv _)) ∙ + ( is-section-map-inv-is-equiv is-equiv-ev-point-Q q₀)) + where + cofork-flattening : + cofork + ( double-arrow-flattening-lemma-descent-data-coequalizer + ( descent-data-coequalizer-identity-type c (map-cofork c b₀))) + ( Σ X (λ x → map-cofork c b₀ ＝ x)) + cofork-flattening = + cofork-flattening-lemma-descent-coequalizer c + ( descent-data-coequalizer-identity-type c (map-cofork c b₀)) + ( λ x → map-cofork c b₀ ＝ x) + ( inv-equiv-descent-data-coequalizer + ( equiv-descent-data-coequalizer-identity-type c + ( map-cofork c b₀))) + up-flattening : universal-property-coequalizer cofork-flattening + up-flattening = + flattening-lemma-descent-data-coequalizer + ( descent-data-coequalizer-identity-type c (map-cofork c b₀)) + ( λ x → map-cofork c b₀ ＝ x) + ( inv-equiv-descent-data-coequalizer + ( equiv-descent-data-coequalizer-identity-type c + ( map-cofork c b₀))) + ( up-c) + is-equiv-ev-point-Q : + is-equiv + ( ev-point-hom-descent-data-coequalizer + ( descent-data-coequalizer-identity-type + ( cofork-flattening) + ( map-cofork cofork-flattening (b₀ , refl))) + ( descent-data-family-with-descent-data-coequalizer + ( family-with-descent-data-coequalizer-descent-data-coequalizer + ( up-flattening) + ( Q))) + ( refl)) + is-equiv-ev-point-Q = + is-equiv-ev-point-hom-descent-data-coequalizer-identity-type + ( up-flattening) + ( b₀ , refl) + ( family-with-descent-data-coequalizer-descent-data-coequalizer + ( flattening-lemma-descent-data-coequalizer + ( descent-data-coequalizer-identity-type c (map-cofork c b₀)) + ( λ x → map-cofork c b₀ ＝ x) + ( inv-equiv-descent-data-coequalizer + ( equiv-descent-data-coequalizer-identity-type c + ( map-cofork c b₀))) + ( up-c)) + ( Q)) +``` + +## Theorem + +This should eventually be unique uniqueness, i.e. the type of equivalences out +of the descent data for the identity type such that the equivalence sends `refl` +to `p₀` should be contractible, not just inhabited. + +```agda +module _ + {l1 l2 l3 l4 : Level} {F : double-arrow l1 l2} + {X : UU l3} {c : cofork F X} + (up-c : universal-property-coequalizer c) + (P : family-with-descent-data-coequalizer c l4) + {b₀ : codomain-double-arrow F} + (p₀ : family-family-with-descent-data-coequalizer P b₀) + where + + map-compute-identity-type-coequalizer : + (x : X) → (map-cofork c b₀ ＝ x) → + family-cofork-family-with-descent-data-coequalizer P x + map-compute-identity-type-coequalizer .(map-cofork c b₀) refl = + map-inv-equiv (equiv-family-with-descent-data-coequalizer P b₀) p₀ + + module _ + (ip-P : + induction-principle-descent-data-identity-type-coequalizer + ( descent-data-family-with-descent-data-coequalizer P) + ( p₀)) + where + + ind-singleton-induction-principle-descent-data-identity-type-coequalizer : + {l : Level} → + (Q : Σ X (family-cofork-family-with-descent-data-coequalizer P) → UU l) → + (q₀ : + Q ( ( map-cofork c b₀) , + ( map-inv-equiv + ( equiv-family-with-descent-data-coequalizer P b₀) + ( p₀)))) → + (x : Σ X (family-cofork-family-with-descent-data-coequalizer P)) → Q x + ind-singleton-induction-principle-descent-data-identity-type-coequalizer + {l} Q q₀ = + map-inv-is-equiv + ( is-equiv-section-descent-data-section-family-cofork + ( Q , Q-descent-data , id-equiv-descent-data-coequalizer _) + ( flattening-lemma-descent-data-coequalizer + ( descent-data-family-with-descent-data-coequalizer P) + ( family-cofork-family-with-descent-data-coequalizer P) + ( inv-equiv-descent-data-coequalizer + ( equiv-descent-data-family-with-descent-data-coequalizer P)) + ( up-c))) + ( pr1 (ip-P Q-descent-data q₀)) + where + Q-descent-data : + descent-data-coequalizer + ( double-arrow-flattening-lemma-descent-data-coequalizer + ( descent-data-family-with-descent-data-coequalizer P)) + ( l) + Q-descent-data = + descent-data-family-cofork + ( cofork-flattening-lemma-descent-coequalizer c + ( descent-data-family-with-descent-data-coequalizer P) + ( family-cofork-family-with-descent-data-coequalizer P) + ( inv-equiv-descent-data-coequalizer + ( equiv-descent-data-family-with-descent-data-coequalizer P))) + ( Q) + + is-equiv-map-compute-identity-type-coequalizer : + (x : X) → is-equiv (map-compute-identity-type-coequalizer x) + is-equiv-map-compute-identity-type-coequalizer = + fundamental-theorem-id + ( is-contr-ind-singleton _ _ + ( ind-singleton-induction-principle-descent-data-identity-type-coequalizer)) + ( map-compute-identity-type-coequalizer) + + compute-identity-type-coequalizer : + (x : X) → + (map-cofork c b₀ ＝ x) ≃ + family-cofork-family-with-descent-data-coequalizer P x + pr1 (compute-identity-type-coequalizer x) = + map-compute-identity-type-coequalizer x + pr2 (compute-identity-type-coequalizer x) = + is-equiv-map-compute-identity-type-coequalizer x + + abstract + uniqueness-induction-principle-identity-type-coequalizer : + equiv-descent-data-coequalizer + ( descent-data-coequalizer-identity-type c (map-cofork c b₀)) + ( descent-data-family-with-descent-data-coequalizer P) + uniqueness-induction-principle-identity-type-coequalizer = + map-equiv + ( compute-section-family-cofork-equivalence-family + ( family-with-descent-data-coequalizer-identity-type c + ( map-cofork c b₀)) + ( P)) + ( section-descent-data-section-family-cofork + ( family-with-descent-data-coequalizer-equivalence-family + ( family-with-descent-data-coequalizer-identity-type c + ( map-cofork c b₀)) + ( P)) + ( compute-identity-type-coequalizer)) + + compute-uniqueness-induction-principle-identity-type-coequalizer : + map-equiv-descent-data-coequalizer _ _ + ( uniqueness-induction-principle-identity-type-coequalizer) + ( b₀) + ( refl) ＝ + p₀ + compute-uniqueness-induction-principle-identity-type-coequalizer = + is-section-map-inv-equiv + ( equiv-family-with-descent-data-coequalizer P b₀) + ( p₀) +```