Foundation core

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Vojtěch Štěpančík, Julian KG, Raymond Baker, fernabnor and louismntnu.

Created on 2023-03-03.
Last modified on 2024-09-23.

Modules in the foundation-core namespace

module foundation-core where

open import foundation-core.1-types public
open import foundation-core.cartesian-product-types public
open import foundation-core.coherently-invertible-maps public
open import foundation-core.commuting-prisms-of-maps public
open import foundation-core.commuting-squares-of-homotopies public
open import foundation-core.commuting-squares-of-identifications public
open import foundation-core.commuting-squares-of-maps public
open import foundation-core.commuting-triangles-of-maps public
open import foundation-core.constant-maps public
open import foundation-core.contractible-maps public
open import foundation-core.contractible-types public
open import foundation-core.coproduct-types public
open import foundation-core.decidable-propositions public
open import foundation-core.dependent-identifications public
open import foundation-core.diagonal-maps-cartesian-products-of-types public
open import foundation-core.discrete-types public
open import foundation-core.embeddings public
open import foundation-core.empty-types public
open import foundation-core.endomorphisms public
open import foundation-core.equality-dependent-pair-types public
open import foundation-core.equivalence-relations public
open import foundation-core.equivalences public
open import foundation-core.families-of-equivalences public
open import foundation-core.fibers-of-maps public
open import foundation-core.function-types public
open import foundation-core.functoriality-dependent-function-types public
open import foundation-core.functoriality-dependent-pair-types public
open import foundation-core.homotopies public
open import foundation-core.identity-types public
open import foundation-core.injective-maps public
open import foundation-core.invertible-maps public
open import foundation-core.negation public
open import foundation-core.operations-span-diagrams public
open import foundation-core.operations-spans public
open import foundation-core.path-split-maps public
open import foundation-core.postcomposition-dependent-functions public
open import foundation-core.postcomposition-functions public
open import foundation-core.precomposition-dependent-functions public
open import foundation-core.precomposition-functions public
open import foundation-core.propositional-maps public
open import foundation-core.propositions public
open import foundation-core.pullbacks public
open import foundation-core.retractions public
open import foundation-core.retracts-of-types public
open import foundation-core.sections public
open import foundation-core.sets public
open import foundation-core.small-types public
open import foundation-core.subtypes public
open import foundation-core.torsorial-type-families public
open import foundation-core.transport-along-identifications public
open import foundation-core.truncated-maps public
open import foundation-core.truncated-types public
open import foundation-core.truncation-levels public
open import foundation-core.type-theoretic-principle-of-choice public
open import foundation-core.univalence public
open import foundation-core.universal-property-pullbacks public
open import foundation-core.universal-property-truncation public
open import foundation-core.whiskering-homotopies-concatenation public
open import foundation-core.whiskering-identifications-concatenation public

Recent changes