Eilenberg-Maclane spaces in HoTT

[Ali Caglayan]

I am trying to formalise Eilenberg-Maclane spaces in HoTT just like in Licata and Finster's paper.

Hopefully I can show that pi_1(K(G,1)) = G soon.

I have added to code of what I have done so far at the bottom. There are a couple of things I would like to know though:

 1. What is a good group type to use? I kind of cheated and defined my own here but I know there is a oogroup type hanging around and I am assuming that if I truncate it properly I can get usual group theorems. Would these come automatically with group isomorphisms?

 2. Is there a notion of fundamental group defined so far in the project? I know this is a small thing but I suppose it would help organise.

 3. I have chosen to cheat HIT with the axiom method and I know I am so far missing the recursor and eliminator terms. I have no idea how to write these as this is my first HIT so I would be glad if someone can throw some tips my way.

 4. Tell me anything about the code I would love to hear your opinions so I can approve.

Require Import Basics.
Require Import HIT.Suspension.
Require Import HIT.Truncations.
Require Import Spectra.Spectrum.

Structure AbGroup :=
{
  gset :> Set;
 
  id : gset;
  op : gset -> gset -> gset;
  inv : gset -> gset;
 
  op_assoc : forall (x y z : gset),  op x (op y z) = op (op x y) z;
  op_inv   : forall (x : gset),      (id = op (inv x) x) * (id = op x (inv x));
  op_comm  : forall (x y : gset),    op x y = op y x
}.


(* * First we define the higher inductive type  K(G,1)
    We would wish for it to be defined as *
   
    Inductive EM (G : AbGroup) :=
      | base        : EM G
      | loop        : G -> (base = base)
      | loop-ident  : loop e = refl
      | loop-comp   : forall (x y : G), loop (G.op x y) = (loop y) o (loop x)

*)

Axiom EM : AbGroup -> Type.

Context {abG : AbGroup}.

Axiom base : EM abG.
Axiom loop : abG -> (base = base).
Context {e : abG}.
Axiom loop_ident : loop e = idpath.
Axiom loop_comp  : forall (x y : abG), loop(op abG x y) = (loop y) @ (loop x).


(** Iterated suspension Σ^(n-1) **)
Fixpoint itSusp (n : nat) (a : Type) : Type :=
 match n with
  | O%nat   => a
  | S n'    => Susp (itSusp n' a)
end.

(** Definition of K(G,n)
      K(G,n) := || Σ^(n-1) K(G,1) ||_n **)
Definition EM_Space (G : AbGroup) (n : nat)
  := match n return Type with
      | 0%nat => gset G
      | S n'  => Trunc (S n') (itSusp n' (EM G))
     end.

(**TODO:
  - Use correct Group type
  - Use fundamental group type if given
**)

(** Now we prove that π_1(K(G,1)) isIsoTo G.
π_1(A) := || ΩA ||_0

Proof from Licata and Finster and is long.

**)

Theorem pi_1_EM_Space_G_1_isoTo_G := ??.

[Floris van Doorn]

I don't know the Coq-HoTT library well, so I cannot answer the questions specific to that library.

For the HIT, I would look at one of the other HIT constructions in the Coq-HoTT library, and mimic that. If you use an axiomatic method, the elimination principle will not compute on point constructors, which will make your life harder.

To give you some hints about the elimination principle:

* First try to write down the non-dependent elimination principle. To define a map (EM abG -> X) we need "copies" of all the constructors of (EM abG) in X. So we need a point, we need a family of loops, and some 2-paths.

* Now for the dependent elimination principle, you need to replace the paths by dependent paths or pathovers (I don't know whether these are defined in Coq, but they are very helpful). The argument corresponding to the 2-path will involve a concatenation of pathovers.

Something else: In the definition of group you seem to forgot the identity laws.

If you want, you could look at the existing formalizations in Agda and Lean. Below are the links to the corresponding files in either library (in both cases the first file has the basic definitions and the other files have more results). Even if you don't know the exact syntax of those languages, it should help you along (the syntax of Lean is close to the syntax of Coq). 

Agda: (EM is postulated as a HIT)

https://github.com/HoTT/HoTT-Agda/blob/master/core/lib/types/EilenbergMacLane1.agda

https://github.com/HoTT/HoTT-Agda/blob/master/theorems/homotopy/EilenbergMacLane1.agda

https://github.com/HoTT/HoTT-Agda/blob/master/theorems/homotopy/EilenbergMacLane.agda

Lean: (EM is constructed from homotopy pushouts)

https://github.com/leanprover/lean2/blob/master/hott/homotopy/EM.hlean

https://github.com/cmu-phil/Spectral/blob/master/homotopy/EM.hlean

Hope this helps!

Best,

Floris

--
You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.
To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Floris van Doorn]

PS: as an exercise, try to prove `loop_ident` from `loop_comp`.

[Michael Shulman]

I don't think using ooGroup is a good idea for this; ooGroups are
essentially defined by having a classifying space, whereas here you're
trying to construct classifying spaces. For HITs, as Floris says,
look at the other HITs in the HIT/ directory (and the "Higher
Inductive Types" section in STYLE.md) for guidance. Fundamental
groups are not, I think defined; they would be "Tr 0 (loops A)". The
only other comments I have are that your "EM G" isn't really K(G,1)
yet since you haven't 1-truncated it, and that ideally K(G,1) would
not assume abelianness. Unfortunately pathovers/squareovers/etc. are
not primitive in the HoTT/Coq library yet; you just use equality
between transports.