Free higher groups in homotopy type theory
Given a type A in homotopy type theory (HoTT), we can define the free ∞-group on A as the higher inductive type F (A)with constructors unit: F(A),cons : A → F(A) → F(A), and conditions saying that every cons(a)is an auto-equivalence on F(A). Equivalently, we can take the loop space of the suspension...
| Main Authors: | , |
|---|---|
| Format: | Conference or Workshop Item |
| Language: | English |
| Published: |
2018
|
| Online Access: | https://eprints.nottingham.ac.uk/51212/ |