From be04f2121b06088e26b81542c26dc437ead5bdaf Mon Sep 17 00:00:00 2001 From: Benedikt Ahrens Date: Fri, 22 Jul 2022 10:00:09 +0200 Subject: [PATCH] add exercise for Synthetic Homotopy Theory --- .../Synthetic_Homotopy_Theory.v | 496 ++++++++++++++++++ README.md | 9 +- 2 files changed, 502 insertions(+), 3 deletions(-) create mode 100644 2022-07-Cortona/7_Synthetic-Homotopy-Theory/Synthetic_Homotopy_Theory.v diff --git a/2022-07-Cortona/7_Synthetic-Homotopy-Theory/Synthetic_Homotopy_Theory.v b/2022-07-Cortona/7_Synthetic-Homotopy-Theory/Synthetic_Homotopy_Theory.v new file mode 100644 index 0000000..06589a9 --- /dev/null +++ b/2022-07-Cortona/7_Synthetic-Homotopy-Theory/Synthetic_Homotopy_Theory.v @@ -0,0 +1,496 @@ +(* -*- coq-prog-args: ("-type-in-type"); -*- *) + +(** * Exercises on Synthetic Homotopy Theory + +Peter LeFanu Lumsdaine +School on Univalent Mathematics, Cortona, July 2022 +https://unimath.github.io/cortona2022/ + +The goal is to remove as many “Admitted” as possible in the code below. The exercises should range from straightforward to very challenging. + +The exercises are divided into 8 groups, each forming a roughly self-contained story. In earlier groups, all statements and most definitions are given, only proofs are missing; in later groups, less is given, and more is left for the student. Apart from the core definitions in group 0, most later groups don’t depend essentially on earlier groups. + +The biggest and most interesting part is group 4 — showing the fundamental group of the circle is the integers. Groups 1–3 can largely be seen as warm-up exercises for this. Depending on taste, I recommend either tackling the file roughly in order, or jumping straight to group 4 and looking back to earlier exercises as necessary. + +A few exercises are marked “off-topic”, when their difficulty is not really related to synthetic homotopy theory. They’re included either because their statements are good to see, or because they’re needed in later exercises; they can all safely be left as “admitted”. They may be good exercises on other topics — mostly on working with UniMath’s integers — but insofar as you want exercises on synthetic homotopy theory, I recommend skipping them to avoid getting bogged down. + +- Group 0: Circle structure +- Group 1: Basics +- Group 2: The circle is unique +- Group 3: The circle is non-trivial +- Group 4: Fundamental group of the circle +- Group 5: Being a circle is a proposition +- Group 6: The recursor is equivalent to the universal mapping property. +- Group 7: Is the circle’s computation rule necessary? +- Group 8: Implementing the circle using Z-torsors + +*) + +Require Import UniMath.Foundations.All. +Require Import UniMath.MoreFoundations.All. +Require Import UniMath.NumberSystems.All. + + +(** * Auxiliary functions + +Almost every development ends up needing a few “auxiliary” definitions that don’t really belong in the development itself, but don’t exist upstream. There are various ways to deal with this; I like to put them in an “auxiliary” file or section, and then upstream them later when there’s a suitable moment. *) +Section Auxiliary. + + (** Generalisation of [maponpaths] to dependent functions. *) + Definition maponpaths_dep {X:UU} {Y : X -> UU} + (f : ∏ x:X, Y x) {x1 x2} (e : x1 = x2) + : transportf _ e (f x1) = f x2. + Proof. + destruct e. apply idpath. + Defined. + +End Auxiliary. + +(** * Group 0: Circle structure + +Definition of circles, as their universal property. *) + +Section Circle_Structure. + + (** This axiomatises the recursor on a type that shows it is “the” circle. *) + Definition circle_rec_structure {S : UU} {b : S} (l : b = b) : UU + := ∏ (Y : S -> UU) (y_b : Y b) (y_l : transportf _ l y_b = y_b), + ∑ (f : ∏ x:S, Y x) + (e_b : f b = y_b), + maponpaths_dep f l + = maponpaths _ e_b @ y_l @ !e_b. + (** The third component (the “computation rule” on the loop) is a bit complicated: the idea is just [maponpaths_dep f l = y_l], but that is only well-typed modulo via the “computation rule” for the basepoint, [e_b : f b = y_b]. *) + + (* With any multiple-component definition, it’s good practice to provide named access functions. (Compared to accessing via lots of [pr1], [pr2], this is both more readable, and more robust for refactoring.) *) + Definition circle_rec + {S : UU} {b : S} {l : b = b} (H : circle_rec_structure l) + {Y : S -> UU} {y_b : Y b} (y_l : transportf _ l y_b = y_b) + : ∏ x:S, Y x. + Proof. + Admitted. + + Definition circle_rec_comp_base + {S : UU} {b : S} {l : b = b} (H : circle_rec_structure l) + {Y : S -> UU} {y_b : Y b} (y_l : transportf _ l y_b = y_b) + : circle_rec H y_l b = y_b. + Proof. + Admitted. + + Definition circle_rec_comp_loop + {S : UU} {b : S} {l : b = b} (H : circle_rec_structure l) + {Y : S -> UU} {y_b : Y b} (y_l : transportf _ l y_b = y_b) + : maponpaths_dep (circle_rec H y_l) l + = maponpaths _ (circle_rec_comp_base _ _) + @ y_l @ ! (circle_rec_comp_base _ _). + Proof. + Admitted. + + (** An alternative formulation of the universal property of the circle: + maps out of it correspond to loops. + + “UMP” stands for the “universal mapping property” (a term category theorists love) *) + Definition circle_ump_structure {S : UU} {b : S} (l : b = b) : UU + := ∏ (Y : UU), + isweq ((fun f => (f b,, maponpaths f l)) : (S -> Y) -> (∑ y:Y, y = y)). + + (* Later, when you need to use [circle_ump_structure], come back here and write access functions for it. *) + +End Circle_Structure. + +(** * Group 1: Basics + +Various fairly straightforward exercises: some that we will need later, others that are warmups for harder things later. *) +Section Basics. + + (* Section contexts are the Coq equivalent of writing “Fix some choice of circle (S,b,l)…” Within the section, these variables are fixed parameters that are available for all results/constructions. After the section, all results/constructions get generalised over whichever of the variables they used: see the “Check” commands below to demonstrate this. *) + Context {S : UU} {b : S} (l : b = b). + + Proposition isaprop_circle_ump_structure : isaprop (circle_ump_structure l). + (* TODO: suggest some useful lemmas, or the search command to search for them *) + Admitted. + + Definition loop_pos_power : nat -> (b = b). + Admitted. + + (* off-topic *) + Definition loop_power : hz -> (b = b). + (* Use [Search hz] to find general results about hz. *) + Admitted. + (* Eventually, we want to show [(b = b) ≃ hz]. *) + + (* Within the section, the variables [S] etc are a fixed context, not shown explicitly in the individual types: *) + Check loop_power. +End Basics. +(* After closing the section, the section variables are generalised: *) +Check loop_power. +(* In actual developments, it’s usually considered bad practice to leave “noisy” commands like “Check”, “Search” etc. in finished proof scripts — better to just issue them as queries in your IDE. *) + +(** * Group 2: the circle is unique + +Goal of this group: any two circles are canonically equivalent. *) +Section Circle_Unique. + + Context {S : UU} {b : S} {l : b = b} (is_circ : circle_rec_structure l). + Context {S' : UU} {b' : S'} {l' : b' = b'} (is_circ' : circle_rec_structure l'). + + (* It’s often helpful to make auxiliary definitions _local_ to their section or file. This means that in later files, this can only be accessed as [Circle_Unique.S_to_S']. If this definition was not marked “local”, then we should give it a more carefully considered name. *) + Local Definition S_to_S' : S -> S'. + Admitted. + + (* This definition could be copy-pasted from [S_to_S'] above; or to avoid code-duplication, you could generalise the variables in that (either by closing the section and opening a new one, or by moving the section variables explicitly to its hypotheses) and then taking this just as an instance of that. *) + Local Definition S'_to_S : S' -> S. + Admitted. + + Local Definition S_to_S'_to_S : S'_to_S ∘ S_to_S' = idfun S. + Admitted. + + Local Definition S'_to_S_to_S' : S_to_S' ∘ S'_to_S = idfun S'. + Admitted. + + Proposition weq_circle_unique : S ≃ S'. + Proof. + (* the lemma [gradth] is often useful for constructing equivalences *) + Admitted. + + (** Optional extra: State and prove the fact that this equivalence is “canonical” — it’s the unique equivalence between [S] and [S'] mapping [l] to [l']. *) + +End Circle_Unique. + +(** * Group 3: The circle is non-trivial + +Using univalence, we can show that the circle is non-trivial. *) +Section Circle_non_trivial. + + (** Outline: + - if the circle was trivial, then every type would be a set + - the universe is not a set, since [bool] has a non-trivial automorphism + *) + + Context {S : UU} {b : S} {l : b = b} (S_circ : circle_rec_structure l). + + Proposition circle_trivial_implies_loops_trivial + : iscontr S -> ∏ (X:UU) (x:X) (l : x=x), l = idpath x. + Admitted. + + Proposition loops_trivial_implies_isaset {X:UU} + : (∏ (x:X) (l : x=x), l = idpath x) -> isaset X. + Admitted. + + Proposition circle_trivial_implies_isaset + : iscontr S -> ∏ (X:UU), isaset X. + Admitted. + + Definition flip : bool ≃ bool. + (* You can either write this yourself, or look for it in [UniMath] iwth [Search (bool ≃ bool)], or [Search (weq bool bool)] if your command prompt makes unicode entry difficult. *) + Admitted. + + Proposition flip_neq_idweq : flip != idweq bool. + (* this uses the fact that [false != true]; + you can either prove this yourself or search for it in [UniMath] *) + Admitted. + + Definition flip_path : bool = bool. + (* this is of univalence; specifically, [weqtopaths] *) + Admitted. + + Proposition flip_path_neq_idpath : flip_path != idpath bool. + (* hints: [Search weqtopaths], [Search eqweqmap], [maponpaths] *) + Admitted. + + Proposition not_isaset_uu : ¬ isaset UU. + Admitted. + + Proposition not_iscontr_circle : ¬ iscontr S. + Admitted. + + (** Optional extra: can you strengthen the conclusion of this section? *) +End Circle_non_trivial. + +(** * Group 4: Fundamental group of the circle + +In this sequence, we show that the fundamental group of the circle is the integers. + +Indeed, we show the slightly stronger statement that the _loop space_ of the circle is equivalent to the integers. (The fundamental group is the set-truncation of the loop space.) *) +Section Fundamental_Group. + + (** Fix a circle type throughout this sequence. *) + Context {Circle : UU} {base : Circle} (loop : base = base). + + (** Outline: + - (1) the identity-types Id_A(a,x) form the free A-indexed family generated by a single element at a; in particular, Id_S(b,x) are the free S-indexed family generated by an element at b + - (2) by univalence, a family over a circle (S,b,l) corresponds to a single type equipped with an auto-equivalence + - (3) so Id_S(b,b) is the free type-with-auto-equivalence generated by a single element + - (4) (Z,succ) is the free type-with-auto-equivalence generated by a single element + - (5) so they have the same universal peroperty, so are equivalent. + + We do not attempt to make all these results fully precise (especially (1), (2)); but they motivate the steps we use, which are just as much of the above results as are needed to make this argument go through. *) + + (** Step (1) is nothing specifically to do with the circle, + just a particular formulation of the universal property of path-types *) + + Section Family_Maps_From_Path_Types. + + Context {X:UU} (x0:X). + + Proposition unique_family_map_from_paths {Y : X -> UU} (y0 : Y x0) + : iscontr (∑ (f : ∏ x:X, x0 = x -> Y x), f x0 (idpath _) = y0). + Admitted. + + End Family_Maps_From_Path_Types. + + Section Auto_Types. + (** In the rest of the proof, we work with types equipped with with an auto-equivalence, and sometimes also with a distinguished element. For conciseness, call these *auto-types* and *pointed auto-types*. + + We set these up explicitly as bundled structures, with access functions and a constructor function. *) + + Definition auto_type : UU := ∑ (X:UU), X ≃ X. + + Definition auto_type_pr1 : auto_type -> UU := pr1. + Coercion auto_type_pr1 : auto_type >-> UU. + + Definition auto_type_auto { X : auto_type } : X ≃ X + := pr2 X. + + (* a constructor function is good practice in general, + but especially necessary in this case since Coq doesn’t generally accept [(X,,e)] for an auto-type: it de-sugars this to [tpair _ X e] and fails to infer the implicit argument correctly *) + Definition make_auto_type {X:UU} (e : X ≃ X) : auto_type + := tpair (fun Y => Y ≃ Y) X e. + + Definition ptd_auto_type : UU := ∑ (X:auto_type), X. + + Definition ptd_auto_type_pr1 : ptd_auto_type -> auto_type := pr1. + Coercion ptd_auto_type_pr1 : ptd_auto_type >-> auto_type. + + Definition ptd_auto_type_pt ( X : ptd_auto_type ) : X + := pr2 X. + + Definition make_ptd_auto_type {X:UU} (e : X ≃ X) (x0 : X) : ptd_auto_type + := (make_auto_type e ,, x0). + End Auto_Types. + + (* we give more concise names, but keep them local *) + Local Definition s {X : auto_type} := @auto_type_auto X. + Local Definition pt {X : ptd_auto_type} := @ptd_auto_type_pt X. + + (** We define “freeness” in a category-theoretic style, using a universal mapping property: *) + Definition free_ptd_auto_type_ump_structure (X : ptd_auto_type) : UU + := ∏ (Y : ptd_auto_type), + iscontr (∑ (f : ∑ (f : X -> Y), f ∘ s = s ∘ f), (pr1 f pt = pt)). + (** a more natural and readable phrasing would be + [ ∑ (f : X -> Y), (f ∘ s = s ∘ f) × (f pt = pt) ] + but associating the first two components together fits much better with the ways we’ll use it below *) + + (* When you use this below, you’ll probably want to come back and write access functions! *) + + (* It might be helpful to bundle “ptd-auto-preserving maps” as a structure following how we bundled ptd-auto-types. *) + + (** Step (2): families over circle correspond to types-with-automorphisms. + + We don’t give a very complete form of this “correspondence” — just as is needed in later steps of the proof. *) + + Section Families_Over_Circle. + + Definition circle_family_of_auto_type + : auto_type -> (Circle -> UU). + Admitted. + + Definition auto_type_of_circle_family + : (Circle -> UU) -> auto_type. + Admitted. + + (** The above two functions should form an equivalence; but we need only one direction of their inverse-ness. *) + Definition auto_type_of_circle_family_of_auto_type + (X : auto_type) + : auto_type_of_circle_family (circle_family_of_auto_type X) + = X. + (* In this kind of situation, it’s often helpful to give a general lemma for building paths of auto-types, named e.g. [auto_type_path], + saying that to show two auto-types equal, it suffices to give an equality [e] between their types, and show their automorphisms commute with the equivalence [eqweqmap e] *) + Admitted. + + Definition weq_family_maps_auto_type_maps {X Y : Circle -> UU} + : (∏ p:Circle, X p -> Y p) + ≃ (∑ (f : auto_type_of_circle_family X + -> auto_type_of_circle_family Y), + (f ∘ s = s ∘ f)). + Proof. + (* look for library lemmas for building equivalences between dependent sum types, + e.g. [Search ((∑ (x:_), _) ≃ (∑ (x:_), _))] *) + Admitted. + + End Families_Over_Circle. + + (** Step (3): [ loop = loop ] is a _free_ pointed-type-with-auto-equivalence. *) + Section Circle_Loops_Free. + + Definition circle_ptd_auto : ptd_auto_type. + Proof. + refine (@make_ptd_auto_type (base = base) _ _). + - admit. + - admit. + Admitted. + + Definition circle_is_free_ptd_auto_type + : free_ptd_auto_type_ump_structure circle_ptd_auto. + (* Need to show: for any other ptd-auto-type, there’s a unique structure-preserving map to it. + By results above, we know: + - every ptd-auto-type arises from a family over S; + - in that case, auto-preserving maps to it correspond to family-maps to it; + - and then tre’s a unique point-preserving family-map to it. + + This proof is where it should be helpful that in the definition of [free_ptd_auto_type_ump_structure], we grouped “auto-preserving-map” together inside “point-preserving, auto-preserving map. *) + Admitted. + + End Circle_Loops_Free. + + (** Step (4): the integers (with successor and zero) are also a free pointed-auto-type. + + This section involves no homotopy theory — it’s almost entirely old-fashioned set-level mathematics. The “almost” is because the universal property we want involves mapping into arbitrary _types_, not just sets. *) + + Section Integers_Free. + + (* off-topic *) + (* [hz] is UniMath’s integers *) + Definition hz_ptd_auto : ptd_auto_type. + Proof. + refine (@make_ptd_auto_type hz _ _). + - admit. + - admit. + Admitted. + + (* off-topic *) + Definition hz_is_free_ptd_auto_type + : free_ptd_auto_type_ump_structure hz_ptd_auto. + (* One possible approach: show that the integers are equivalent to the coproduct of two copies of the naturals (viewed as e.g. the positive and strictly-negative integers); then give the required map (and its uniqueness) by induction over each copy of the naturals separately. *) + Admitted. + + End Integers_Free. + + (** Step (5): we’ve shown that the integers and the loop space of the circle are each a “free pointed auto-type”. Now we use that to show they’re equivalent. *) + Section Free_Ptd_Auto_Type_Unique. + + Definition weq_free_ptd_auto_type_unique + {X : ptd_auto_type} (X_free : free_ptd_auto_type_ump_structure X) + {X' : ptd_auto_type} (X'_free : free_ptd_auto_type_ump_structure X') + : X ≃ X'. + Admitted. + + End Free_Ptd_Auto_Type_Unique. + + Theorem weq_circle_loops_hz : (base = base) ≃ hz. + Proof. + (* now this should be just putting together earlier results, as sketched at the start! *) + Admitted. + + (** Optional extra: we could instead define “freeness” in a more type-theoretic style, as a dependent recursion principle. Using that approach in the proof would be an interesting extra challenge; if you do that, I’d be very interested to see it! *) + Definition free_pointed_auto_type_rec_structure {X:UU} (s:X ≃ X) (x0:X) : UU + := ∏ (Y : X -> UU) (s_y : ∏ x:X, Y x ≃ Y (s x)) (y0 : Y x0), + ∑ (f : ∏ x:X, Y x) (_ : ∏ x, s_y x (f x) = f (s x)), (f x0 = y0). + +End Fundamental_Group. + +(** * Group 5: being a circle is a proposition + +Precisely: for a given type, basepoint, and loop [l], [circle_rec_structure l] is a proposition. *) +Section Circle_Rec_Structure_Unique. + + Context {S : UU} {b : S} (l : b = b). + + Definition isaprop_circle_rec_conclusion + : circle_rec_structure l + -> ∏ (Y : S -> UU) (y_b : Y b) (y_l : transportf _ l y_b = y_b), + isaprop + ( ∑ (f : ∏ x:S, Y x) + (e_b : f b = y_b), + maponpaths_dep f l + = maponpaths _ e_b @ y_l @ !e_b). + (* hint: if you attack this directly by hand, it’s quite nasty; + you will probably want lemmas about how to construct paths in sigma-types, which are available in the library, + and also about lemmas about how [maponpaths_dep] interacts with path-composition, etc, which you will have to prove yourself *) + Admitted. + + Definition isaprop_circle_rec_structure + : isaprop (circle_rec_structure l). + (* hint: look for a general result in the library to deduce this from the preceding result *) + Admitted. + +End Circle_Rec_Structure_Unique. + +(** * Group 6: the recursor is equivalent to the universal mapping property. *) + +Section Circle_Rec_Equiv_UMP. + + Context {S : UU} {b : S} (l : b = b). + + Definition circle_ump_from_rec + : circle_rec_structure l -> circle_ump_structure l. + Admitted. + + Definition circle_rec_from_ump + : circle_ump_structure l -> circle_rec_structure l. + Admitted. + + Definition weq_circle_rec_circle_ump + : circle_ump_structure l ≃ circle_rec_structure l. + (* we’ve shown both sides are propositions, and they imply each other; + now look for a general result in the library to put these together *) + Admitted. + +End Circle_Rec_Equiv_UMP. + +(** * Group 7: is the circle’s computation rule necessary? + +Are the “computation rules” in the universal property of the circle really required, or are then unnecessary? Prove or disprove! *) +Section Comp_Rule_Redundant. + + (** A weakened form of [circle_rec_structure], omitting the “computation rules” *) + Definition weak_circle_rec_structure {S : UU} {b : S} (l : b = b) : UU + := ∏ (Y : S -> UU) (y_b : Y b) (y_l : transportf _ l y_b = y_b), + ∏ x:S, Y x. + + Definition comp_rule_redundant : UU + := ∏ (X:UU) (b:X) (l:b=b), + weak_circle_rec_structure l -> circle_rec_structure l. + + Theorem comp_rule_redundant_or_necessary + : comp_rule_redundant ∨ ¬ comp_rule_redundant. + Proof. + (** Are the computation rules redundant? Either prove they are, or disprove by giving a counterexample! *) + Admitted. + +End Comp_Rule_Redundant. + +(** * Group 8: Implementing the circle using Z-torsors + +The goal of the type is to give an implementation of the circle: we define “Z-torsors”, and show that the type of Z-torsors is a circle. + +The proof is only very roughly outlined — fleshing out the structure of the section is entirely left for the student. *) +Section Z_torsors. + + Definition hz_auto : auto_type. + (* probably better to define this not here, but upstream as a component of the definition of [hz_ptd_auto] *) + Admitted. + + (** There is a general definition of “G-torsor” for an arbitrary group G. + + We don’t give the general definition, but a simplified definition for the special case where G is the integers. *) + Definition Z_torsor : UU + := ∑ (X : auto_type), ∥ X = hz_auto ∥. + + Local Definition base : Z_torsor. + Admitted. + + Local Definition loop : base = base. + Admitted. + + Theorem Z_torsors_circle : circle_rec_structure loop. + Proof. + (* quite long, and quite mathematically substantial! *) + Admitted. + +End Z_torsors. + +(* +*** Local Variables: *** +*** coq-prog-args: ("-type-in-type") *** +*** End: *** +*) diff --git a/README.md b/README.md index 6e83db2..dd4242a 100644 --- a/README.md +++ b/README.md @@ -2,11 +2,11 @@ ## School on Univalent Mathematics, Cortona, 2022 -### Lecture 1: Type Theory (by Gianluca Amato) +### Lecture 1: Type Theory (by [Gianluca Amato](https://www.sci.unich.it/~amato/)) - [Lecture](2022-07-Cortona/1_Type-Theory/Lecture_Type-Theory.pdf) -### Lecture 2: Fundamentals of Coq (by Marco Maggesi) +### Lecture 2: Fundamentals of Coq (by [Marco Maggesi](https://sites.google.com/unifi.it/maggesi/)) - [Lecture](https://github.com/UniMath/Schools/tree/master/2022-07-Cortona/2_Fundamentals-Coq) ### Lecture 3: Univalent foundations (by Paige Randall North) @@ -22,7 +22,7 @@ - [Solutions](2022-07-Cortona/4_Tactics-UniMath/exercises_tactics_with_solutions.v) - [Advanced solutions](2022-07-Cortona/4_Tactics-UniMath/weq_exercises_with_solutions.v) -### Lecture 5: *Set-Level Mathematics* (by [Benedikt Ahrens](https://benediktahrens.gitlab.io)) +### Lecture 5: Set-Level Mathematics (by [Benedikt Ahrens](https://benediktahrens.gitlab.io)) - [Lecture](2022-07-Cortona/5_Set-level-mathematics/5_set_level_mathematics_lecture.pdf) - [Exercises](2022-07-Cortona/5_Set-level-mathematics/set_level_mathematics_exercises.v) - [Solutions](2022-07-Cortona/5_Set-level-mathematics/set_level_mathematics_solutions.v) @@ -34,6 +34,9 @@ - [Exercises](2022-07-Cortona/6_Category_Theory/category_theory_exercises.v) - [Exercises with solutions](2022-07-Cortona/6_Category_Theory/category_theory_solutions.v) +### Lecture 7: Synthetic Homotopy Theory (by [Peter LeFanu Lumsdaine](http://peterlefanulumsdaine.com/)) +- [Exercises](2022-07-Cortona/7_Synthetic-Homotopy-Theory/Synthetic_Homotopy_Theory.v) +