Foundation

Files in the foundation folder

module foundation where

open import foundation.0-connected-types public
open import foundation.0-images-of-maps public
open import foundation.0-maps public
open import foundation.1-types public
open import foundation.2-types public
open import foundation.apartness-relations public
open import foundation.arithmetic-law-coproduct-and-sigma-decompositions public
open import foundation.automorphisms public
open import foundation.axiom-l public
open import foundation.axiom-of-choice public
open import foundation.bands public
open import foundation.binary-embeddings public
open import foundation.binary-equivalences public
open import foundation.binary-equivalences-unordered-pairs-of-types public
open import foundation.binary-functoriality-set-quotients public
open import foundation.binary-homotopies public
open import foundation.binary-operations-unordered-pairs-of-types public
open import foundation.binary-reflecting-maps-equivalence-relations public
open import foundation.binary-relations public
open import foundation.binary-transport public
open import foundation.booleans public
open import foundation.cantor-schroder-bernstein-escardo public
open import foundation.cantors-diagonal-argument public
open import foundation.cartesian-product-types public
open import foundation.cartesian-products-set-quotients public
open import foundation.category-of-sets public
open import foundation.choice-of-representatives-equivalence-relation public
open import foundation.coherently-invertible-maps public
open import foundation.commuting-3-simplices-of-homotopies public
open import foundation.commuting-3-simplices-of-maps public
open import foundation.commuting-cubes-of-maps public
open import foundation.commuting-squares-of-identifications public
open import foundation.commuting-squares-of-maps public
open import foundation.commuting-triangles-of-homotopies public
open import foundation.commuting-triangles-of-maps public
open import foundation.complements public
open import foundation.complements-subtypes public
open import foundation.cones-over-cospans public
open import foundation.conjunction public
open import foundation.connected-components public
open import foundation.connected-components-universes public
open import foundation.connected-maps public
open import foundation.connected-types public
open import foundation.constant-maps public
open import foundation.contractible-maps public
open import foundation.contractible-types public
open import foundation.coproduct-decompositions public
open import foundation.coproduct-decompositions-subuniverse public
open import foundation.coproduct-types public
open import foundation.coslice public
open import foundation.cospans public
open import foundation.decidable-dependent-function-types public
open import foundation.decidable-dependent-pair-types public
open import foundation.decidable-embeddings public
open import foundation.decidable-equality public
open import foundation.decidable-equivalence-relations public
open import foundation.decidable-maps public
open import foundation.decidable-propositions public
open import foundation.decidable-relations public
open import foundation.decidable-subtypes public
open import foundation.decidable-types public
open import foundation.dependent-binomial-theorem public
open import foundation.dependent-pair-types public
open import foundation.dependent-paths public
open import foundation.descent-coproduct-types public
open import foundation.descent-dependent-pair-types public
open import foundation.descent-empty-types public
open import foundation.descent-equivalences public
open import foundation.diagonal-maps-of-types public
open import foundation.diagonals-of-maps public
open import foundation.discrete-reflexive-relations public
open import foundation.discrete-relaxed-sigma-decompositions public
open import foundation.discrete-sigma-decompositions public
open import foundation.discrete-types public
open import foundation.disjunction public
open import foundation.double-negation public
open import foundation.double-powersets public
open import foundation.dubuc-penon-compact-types public
open import foundation.effective-maps-equivalence-relations public
open import foundation.embeddings public
open import foundation.empty-types public
open import foundation.endomorphisms public
open import foundation.epimorphisms public
open import foundation.epimorphisms-with-respect-to-sets public
open import foundation.epimorphisms-with-respect-to-truncated-types public
open import foundation.equality-cartesian-product-types public
open import foundation.equality-coproduct-types public
open import foundation.equality-dependent-function-types public
open import foundation.equality-dependent-pair-types public
open import foundation.equality-fibers-of-maps public
open import foundation.equivalence-classes public
open import foundation.equivalence-extensionality public
open import foundation.equivalence-induction public
open import foundation.equivalence-relations public
open import foundation.equivalences public
open import foundation.equivalences-maybe public
open import foundation.exclusive-disjunction public
open import foundation.existential-quantification public
open import foundation.exponents-set-quotients public
open import foundation.faithful-maps public
open import foundation.fiber-inclusions public
open import foundation.fibered-equivalences public
open import foundation.fibered-involutions public
open import foundation.fibered-maps public
open import foundation.fibers-of-maps public
open import foundation.full-subtypes public
open import foundation.function-extensionality public
open import foundation.functional-correspondences public
open import foundation.functions public
open import foundation.functoriality-cartesian-product-types public
open import foundation.functoriality-coproduct-types public
open import foundation.functoriality-dependent-function-types public
open import foundation.functoriality-dependent-pair-types public
open import foundation.functoriality-fibers-of-maps public
open import foundation.functoriality-function-types public
open import foundation.functoriality-propositional-truncation public
open import foundation.functoriality-set-quotients public
open import foundation.functoriality-set-truncation public
open import foundation.functoriality-truncation public
open import foundation.fundamental-theorem-of-identity-types public
open import foundation.global-choice public
open import foundation.hexagons-of-identifications public
open import foundation.hilberts-epsilon-operators public
open import foundation.homotopies public
open import foundation.identity-systems public
open import foundation.identity-truncated-types public
open import foundation.identity-types public
open import foundation.images public
open import foundation.images-subtypes public
open import foundation.impredicative-encodings public
open import foundation.impredicative-universes public
open import foundation.induction-principle-propositional-truncation public
open import foundation.inhabited-subtypes public
open import foundation.inhabited-types public
open import foundation.injective-maps public
open import foundation.interchange-law public
open import foundation.intersections-subtypes public
open import foundation.involutions public
open import foundation.isolated-points public
open import foundation.isomorphisms-of-sets public
open import foundation.iterated-cartesian-product-types public
open import foundation.iterating-automorphisms public
open import foundation.iterating-functions public
open import foundation.iterating-involutions public
open import foundation.large-dependent-pair-types public
open import foundation.large-homotopies public
open import foundation.large-identity-types public
open import foundation.large-locale-of-propositions public
open import foundation.large-locale-of-subtypes public
open import foundation.law-of-excluded-middle public
open import foundation.lawveres-fixed-point-theorem public
open import foundation.lesser-limited-principle-of-omniscience public
open import foundation.limited-principle-of-omniscience public
open import foundation.locally-small-types public
open import foundation.logical-equivalences public
open import foundation.maybe public
open import foundation.mere-embeddings public
open import foundation.mere-equality public
open import foundation.mere-equivalences public
open import foundation.monomorphisms public
open import foundation.morphisms-cospans public
open import foundation.multisubsets public
open import foundation.multivariable-correspondences public
open import foundation.multivariable-decidable-relations public
open import foundation.multivariable-functoriality-set-quotients public
open import foundation.multivariable-operations public
open import foundation.multivariable-relations public
open import foundation.negation public
open import foundation.noncontractible-types public
open import foundation.pairs-of-distinct-elements public
open import foundation.partial-elements public
open import foundation.partitions public
open import foundation.path-algebra public
open import foundation.path-split-maps public
open import foundation.perfect-images public
open import foundation.powersets public
open import foundation.preidempotent-maps public
open import foundation.preimages-of-subtypes public
open import foundation.principle-of-omniscience public
open import foundation.product-decompositions public
open import foundation.products-binary-relations public
open import foundation.products-equivalence-relations public
open import foundation.products-of-tuples-of-types public
open import foundation.products-unordered-pairs-of-types public
open import foundation.products-unordered-tuples-of-types public
open import foundation.projective-types public
open import foundation.proper-subtypes public
open import foundation.propositional-extensionality public
open import foundation.propositional-maps public
open import foundation.propositional-resizing public
open import foundation.propositional-truncations public
open import foundation.propositions public
open import foundation.pullback-squares public
open import foundation.pullbacks public
open import foundation.raising-universe-levels public
open import foundation.reflecting-maps-equivalence-relations public
open import foundation.reflexive-relations public
open import foundation.relaxed-sigma-decompositions public
open import foundation.repetitions-of-values public
open import foundation.repetitions-sequences public
open import foundation.replacement public
open import foundation.retractions public
open import foundation.russells-paradox public
open import foundation.sections public
open import foundation.sequences public
open import foundation.set-presented-types public
open import foundation.set-quotients public
open import foundation.set-truncations public
open import foundation.sets public
open import foundation.shifting-sequences public
open import foundation.sigma-decomposition-subuniverse public
open import foundation.sigma-decompositions public
open import foundation.singleton-induction public
open import foundation.singleton-subtypes public
open import foundation.slice public
open import foundation.small-maps public
open import foundation.small-types public
open import foundation.small-universes public
open import foundation.split-surjective-maps public
open import foundation.standard-apartness-relations public
open import foundation.strongly-extensional-maps public
open import foundation.structure public
open import foundation.structure-identity-principle public
open import foundation.structured-type-duality public
open import foundation.subterminal-types public
open import foundation.subtype-duality public
open import foundation.subtype-identity-principle public
open import foundation.subtypes public
open import foundation.subuniverses public
open import foundation.surjective-maps public
open import foundation.symmetric-difference public
open import foundation.symmetric-identity-types public
open import foundation.symmetric-operations public
open import foundation.tight-apartness-relations public
open import foundation.transport public
open import foundation.trivial-relaxed-sigma-decompositions public
open import foundation.trivial-sigma-decompositions public
open import foundation.truncated-equality public
open import foundation.truncated-maps public
open import foundation.truncated-types public
open import foundation.truncation-equivalences public
open import foundation.truncation-images-of-maps public
open import foundation.truncation-levels public
open import foundation.truncations public
open import foundation.tuples-of-types public
open import foundation.type-arithmetic-booleans public
open import foundation.type-arithmetic-cartesian-product-types public
open import foundation.type-arithmetic-coproduct-types public
open import foundation.type-arithmetic-dependent-function-types public
open import foundation.type-arithmetic-dependent-pair-types public
open import foundation.type-arithmetic-empty-type public
open import foundation.type-arithmetic-unit-type public
open import foundation.type-duality public
open import foundation.type-theoretic-principle-of-choice public
open import foundation.unions-subtypes public
open import foundation.unique-existence public
open import foundation.uniqueness-image public
open import foundation.uniqueness-set-quotients public
open import foundation.uniqueness-set-truncations public
open import foundation.uniqueness-truncation public
open import foundation.unit-type public
open import foundation.unital-binary-operations public
open import foundation.univalence public
open import foundation.univalence-action-on-equivalences public
open import foundation.univalence-implies-function-extensionality public
open import foundation.univalent-type-families public
open import foundation.universal-property-booleans public
open import foundation.universal-property-cartesian-product-types public
open import foundation.universal-property-coproduct-types public
open import foundation.universal-property-dependent-pair-types public
open import foundation.universal-property-empty-type public
open import foundation.universal-property-fiber-products public
open import foundation.universal-property-identity-types public
open import foundation.universal-property-image public
open import foundation.universal-property-maybe public
open import foundation.universal-property-propositional-truncation public
open import foundation.universal-property-propositional-truncation-into-sets public
open import foundation.universal-property-pullbacks public
open import foundation.universal-property-set-quotients public
open import foundation.universal-property-set-truncation public
open import foundation.universal-property-truncation public
open import foundation.universal-property-unit-type public
open import foundation.universe-levels public
open import foundation.unordered-pairs public
open import foundation.unordered-pairs-of-types public
open import foundation.unordered-tuples public
open import foundation.unordered-tuples-of-types public
open import foundation.vectors-set-quotients public
open import foundation.weak-function-extensionality public
open import foundation.weak-limited-principle-of-omniscience public
open import foundation.weakly-constant-maps public