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