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
- 2023-09-17. Egbert Rijke. Moving file about hexagons of identifications (#782).
- 2023-09-12. Egbert Rijke. Factoring out whiskering (#756).
- 2023-09-11. Fredrik Bakke. Transport along and action on equivalences (#706).
- 2023-09-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).
- 2023-06-25. Fredrik Bakke, louismntnu, fernabnor, Egbert Rijke and Julian KG. Posets are categories, and refactor binary relations (#665).