Foundation core

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.

Created on 2023-03-03.
Last modified on 2023-09-17.

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-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-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-induction public
open import foundation-core.equivalence-relations public
open import foundation-core.equivalences public
open import foundation-core.fibers-of-maps public
open import foundation-core.function-extensionality 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.functoriality-function-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.path-split-maps 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.sections public
open import foundation-core.sets public
open import foundation-core.singleton-induction public
open import foundation-core.small-types public
open import foundation-core.subtypes 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.univalence public
open import foundation-core.universal-property-pullbacks public
open import foundation-core.universal-property-truncation public
open import foundation-core.whiskering-homotopies public

Recent changes