Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Pointed.Require Import Cubical.DPath.Require Import Algebra.AbGroups.Require Import Homotopy.Suspension.Require Import Homotopy.ClassifyingSpace.Require Import Homotopy.HSpace.Coherent.Require Import Homotopy.HomotopyGroup.Require Import Homotopy.Hopf.Require Import Truncations.Core Truncations.Connectedness.Require Import WildCat.(* Formalisation of Eilenberg-MacLane spaces *)LocalOpen Scope pointed_scope.LocalOpen Scope nat_scope.LocalOpen Scope mc_mult_scope.(** The definition of the Eilenberg-Mac Lane spaces. Note that while we allow [G] to be non-abelian for [n > 1], later results will need to assume that [G] is abelian. *)FixpointEilenbergMacLane (G : Group) (n : nat) : pType
:= match n with
| 0 => G
| 1 => pClassifyingSpace G
| m.+1 => pTr m.+1 (psusp (EilenbergMacLane G m))
end.Notation"'K(' G , n )" := (EilenbergMacLane G n).SectionEilenbergMacLane.Context `{Univalence}.
H: Univalence G: Group n: nat
IsTrunc n K( G, n)
H: Univalence G: Group n: nat
IsTrunc n K( G, n)
destruct n as [|[]]; exact _.Defined.(** This is subsumed by the next result, but Coq doesn't always find the next result when it should. *)
H: Univalence G: Group n: nat
IsConnected (Tr n) K( G, n.+1)
H: Univalence G: Group n: nat
IsConnected (Tr n) K( G, n.+1)
induction n; exact _.Defined.
H: Univalence G: Group n: nat
IsConnected (Tr n.-1) K( G, n)
H: Univalence G: Group n: nat
IsConnected (Tr n.-1) K( G, n)
H: Univalence G: Group
IsConnected (Tr 0%nat.-1) K( G, 0)
H: Univalence G: Group n: nat
IsConnected (Tr (n.+1)%nat.-1) K( G, n.+1)
H: Univalence G: Group n: nat
IsConnected (Tr (n.+1)%nat.-1) K( G, n.+1)
apply isconnected_em.Defined.
H: Univalence G: Group n: nat
IsConnected (Tr 0%nat) K( G, n.+1)
H: Univalence G: Group n: nat
IsConnected (Tr 0%nat) K( G, n.+1)
rapply (is0connected_isconnected n.-2).Defined.LocalOpen Scope trunc_scope.(* This is a variant of [pequiv_ptr_loop_psusp] from pSusp.v. All we are really using is that [n.+2 <= n +2+ n], but because of the use of [isconnmap_pred_add], the proof is a bit more specific to this case. *)