This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Foundation core

Files in the foundation-core folder

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