Create implementations for the Free Group and for the Bouquet types a… #721
Conversation
Cubical/HITs/FreeGroup/Base.agda
Outdated
| data FreeGroup (A : Type ℓ) : Type ℓ where | ||
| η : A → FreeGroup A | ||
| m : FreeGroup A → FreeGroup A → FreeGroup A | ||
| e : FreeGroup A |
| data FreeGroupoid (A : Type ℓ) : Type ℓ where | ||
| η : A → FreeGroupoid A | ||
| m : FreeGroupoid A → FreeGroupoid A → FreeGroupoid A | ||
| e : FreeGroupoid A |
|
Maybe, it is better to define FreeGroup as a truncated version of the FreeGroupoid or prove this property of them. |
|
This property is proved in the file Cubical/HITs/Bouquet/FreeGroupoid/Properties.agda. I think that this way of defining the Free Group is more general and more clear to use for someone not interested in its relation to the Bouquet. |
|
I saw in this file that you proved that FreeGrupoid is isomorphic to the truncated version of it. |
|
In the file Cubical/HITs/Bouquet/FreeGroupoid/Properties.agda the construction freeGroupTruncIdempotent≃ is the proof that the Free Group is equivalent to the set truncation of the Free Groupoid (FreeGroup A ≃ ∥ FreeGroupoid A ∥₂). |
|
|
||
| idNaturality : action e ≡ idfun (FreeGroupoid A) | ||
| idNaturality = funExt pointwise where | ||
| pointwise : (g : FreeGroupoid A) → action e g ≡ idfun (FreeGroupoid A) g |
There was a problem hiding this comment.
Why not just prove this in one step?
Cubical/HITs/FreeGroup/Base.agda
Outdated
| data FreeGroup (A : Type ℓ) : Type ℓ where | ||
| η : A → FreeGroup A | ||
| m : FreeGroup A → FreeGroup A → FreeGroup A | ||
| e : FreeGroup A |
|
PS: thanks for the contribution! It's a lot of nice stuff and I'm sorry for taking so long to find the time to review it |
Changes made: - move FreeGroupoid to its own folder inside HITs - change names to better suited ones - shorten proofs with many steps
|
Excellent! Will merge once the CI is finished |
…s HITs.
This PR contains an implementation of the Free Group and the proofs of some basic properties, an implementation of the Bouquet of circles of a type and the proof that the Fundamental Group of the (Bouquet A) is the (FreeGroup A). The proof follows the encode-decode method. As an intermediate construction there is an implementation of the Free Groupoid of A (a free group that has no limitiations over the high dimensional path structure).