index

module index where

このサイトは現在制作中です。

import foundations.universe
import foundations.identity-type
import foundations.groupoid-laws
import foundations.function
import foundations.functions-are-functors
import foundations.identity-type-reasoning
import foundations.transport
import foundations.sigma-type
import foundations.product-type
import foundations.fibration
import foundations.dependent-map
import foundations.homotopy
import foundations.homotopies-are-natural-isomorphisms
import foundations.quasi-inverse
import foundations.contractible-type
import foundations.fiber
import foundations.section
import foundations.retraction
import foundations.bi-invertible-map
import foundations.quasi-inverse-to-bi-invertible-map
import foundations.bi-invertible-map-to-quasi-inverse
import foundations.equivalence-is-equivalence-relation
import foundations.sigma-type-identity
import foundations.happly
import foundations.implicit-function
import foundations.function-extensionality
import foundations.identity-type-respects-equivalence
import foundations.identity-type-respects-retract
import foundations.transport-identity
import foundations.proposition
import foundations.natural-number
import foundations.h-level
import foundations.set
import foundations.greater-h-levels
import foundations.h-level-closed-under-retract
import foundations.h-level-closed-under-retract-of-identity
import foundations.h-level-pi
import foundations.h-level-sigma
import foundations.proposition-h-level
import foundations.sigma-type-snd-contr
import foundations.prop-id-contr
import foundations.sigma-type-identity-snd-prop
import foundations.pi-type-distributes-over-sigma-type
import foundations.propositional-truncation
import foundations.axiom-of-choice

import category-theory.category
import category-theory.category-identity
import category-theory.isomorphism
import category-theory.idempotent-morphism
import category-theory.split-idempotent
import category-theory.functor
import category-theory.functor-identity
import category-theory.composition-of-functors
import category-theory.algebra-for-functor
import category-theory.displayed-category
import category-theory.total-category
import category-theory.category-of-functor-algebras
import category-theory.concrete-category
import category-theory.category-of-sets
import category-theory.presheaf
import category-theory.strict-category
import category-theory.category-of-strict-categories
import category-theory.binary-product
import category-theory.indexed-product