Structured types
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Victor Blanchi.
Created on 2022-05-07.
Last modified on 2023-09-28.
Files in the structured types folder
module structured-types where open import structured-types.cartesian-products-types-equipped-with-endomorphisms public open import structured-types.central-h-spaces public open import structured-types.commuting-squares-of-pointed-maps public open import structured-types.conjugation-pointed-types public open import structured-types.constant-maps-pointed-types public open import structured-types.contractible-pointed-types public open import structured-types.cyclic-types public open import structured-types.dependent-products-h-spaces public open import structured-types.dependent-products-pointed-types public open import structured-types.dependent-products-wild-monoids public open import structured-types.equivalences-types-equipped-with-endomorphisms public open import structured-types.faithful-pointed-maps public open import structured-types.fibers-of-pointed-maps public open import structured-types.finite-multiplication-magmas public open import structured-types.function-h-spaces public open import structured-types.function-magmas public open import structured-types.function-wild-monoids public open import structured-types.h-spaces public open import structured-types.initial-pointed-type-equipped-with-automorphism public open import structured-types.involutive-type-of-h-space-structures public open import structured-types.involutive-types public open import structured-types.iterated-cartesian-products-types-equipped-with-endomorphisms public open import structured-types.iterated-pointed-cartesian-product-types public open import structured-types.magmas public open import structured-types.mere-equivalences-types-equipped-with-endomorphisms public open import structured-types.morphisms-h-spaces public open import structured-types.morphisms-magmas public open import structured-types.morphisms-types-equipped-with-endomorphisms public open import structured-types.morphisms-wild-monoids public open import structured-types.noncoherent-h-spaces public open import structured-types.pointed-cartesian-product-types public open import structured-types.pointed-dependent-functions public open import structured-types.pointed-dependent-pair-types public open import structured-types.pointed-equivalences public open import structured-types.pointed-families-of-types public open import structured-types.pointed-homotopies public open import structured-types.pointed-maps public open import structured-types.pointed-sections public open import structured-types.pointed-types public open import structured-types.pointed-types-equipped-with-automorphisms public open import structured-types.pointed-unit-type public open import structured-types.symmetric-elements-involutive-types public open import structured-types.symmetric-h-spaces public open import structured-types.types-equipped-with-automorphisms public open import structured-types.types-equipped-with-endomorphisms public open import structured-types.unpointed-maps public open import structured-types.wild-groups public open import structured-types.wild-loops public open import structured-types.wild-monoids public open import structured-types.wild-quasigroups public open import structured-types.wild-semigroups public
Recent changes
- 2023-09-28. Egbert Rijke and Fredrik Bakke. Cyclic types (#800).
- 2023-09-13. Fredrik Bakke and Egbert Rijke. Refactor structured monoids (#761).
- 2023-08-21. Egbert Rijke and Fredrik Bakke. Cyclic groups (#697).
- 2023-07-20. Egbert Rijke. cyclic groups (#684).
- 2023-07-19. Egbert Rijke. Conjugation on higher groups (#681).