Foundation core

Files in the foundation-core folder

module foundation-core where

open import foundation-core.0-maps public
open import foundation-core.1-types public
open import foundation-core.automorphisms public
open import foundation-core.cartesian-product-types public
open import foundation-core.coherently-invertible-maps public
open import foundation-core.commuting-3-simplices-of-homotopies public
open import foundation-core.commuting-3-simplices-of-maps public
open import foundation-core.commuting-cubes-of-maps public
open import foundation-core.commuting-squares-of-maps public
open import foundation-core.commuting-triangles-of-homotopies public
open import foundation-core.commuting-triangles-of-maps public
open import foundation-core.cones-over-cospans 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.cospans public
open import foundation-core.decidable-propositions public
open import foundation-core.dependent-pair-types 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-cartesian-product-types public
open import foundation-core.equality-dependent-pair-types public
open import foundation-core.equality-fibers-of-maps 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.faithful-maps public
open import foundation-core.fibers-of-maps public
open import foundation-core.function-extensionality public
open import foundation-core.functions public
open import foundation-core.functoriality-dependent-function-types public
open import foundation-core.functoriality-dependent-pair-types public
open import foundation-core.functoriality-fibers-of-maps public
open import foundation-core.functoriality-function-types public
open import foundation-core.fundamental-theorem-of-identity-types public
open import foundation-core.homotopies public
open import foundation-core.identity-systems public
open import foundation-core.identity-types public
open import foundation-core.injective-maps public
open import foundation-core.involutions public
open import foundation-core.logical-equivalences public
open import foundation-core.morphisms-cospans 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.subtype-identity-principle public
open import foundation-core.subtypes 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-arithmetic-cartesian-product-types public
open import foundation-core.type-arithmetic-dependent-pair-types 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.universe-levels public