Structured types

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Tom de Jong and Victor Blanchi.

Created on 2022-05-07.
Last modified on 2024-03-23.

{-# OPTIONS --guardedness #-}

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-homotopies public
open import structured-types.commuting-squares-of-pointed-maps public
open import structured-types.commuting-triangles-of-pointed-maps public
open import structured-types.conjugation-pointed-types public
open import structured-types.constant-pointed-maps 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.dependent-types-equipped-with-automorphisms public
open import structured-types.equivalences-h-spaces public
open import structured-types.equivalences-pointed-arrows public
open import structured-types.equivalences-types-equipped-with-automorphisms 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.globular-types 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.large-globular-types public
open import structured-types.large-reflexive-globular-types public
open import structured-types.large-symmetric-globular-types public
open import structured-types.large-transitive-globular-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-pointed-arrows public
open import structured-types.morphisms-twisted-pointed-arrows public
open import structured-types.morphisms-types-equipped-with-automorphisms 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.opposite-pointed-spans public
open import structured-types.pointed-2-homotopies 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-isomorphisms public
open import structured-types.pointed-maps public
open import structured-types.pointed-retractions public
open import structured-types.pointed-sections public
open import structured-types.pointed-span-diagrams public
open import structured-types.pointed-spans 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.pointed-universal-property-contractible-types public
open import structured-types.postcomposition-pointed-maps public
open import structured-types.precomposition-pointed-maps public
open import structured-types.reflexive-globular-types public
open import structured-types.sets-equipped-with-automorphisms public
open import structured-types.small-pointed-types public
open import structured-types.symmetric-elements-involutive-types public
open import structured-types.symmetric-globular-types public
open import structured-types.symmetric-h-spaces public
open import structured-types.transitive-globular-types public
open import structured-types.transposition-pointed-span-diagrams public
open import structured-types.types-equipped-with-automorphisms public
open import structured-types.types-equipped-with-endomorphisms public
open import structured-types.uniform-pointed-homotopies public
open import structured-types.universal-property-pointed-equivalences public
open import structured-types.unpointed-maps public
open import structured-types.whiskering-pointed-2-homotopies-concatenation public
open import structured-types.whiskering-pointed-homotopies-composition 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