Navigate the formal text
検索語を入力してください。
↑↓ で移動、Enter で開く、Esc で閉じます。
Publication source tree
本文、Leanコード、序文、付録を、GitHubの公開状態に依存せず閲覧できます。 表示対象はビルドに使う全ファイルではなく、読者へ公開する教材ソースに限定しています。
FormalLab.lean
TermsAndTypes.lean
Functions.lean
InductiveTypes.lean
UntypedLambdaCalculus.lean
Universes.lean
Propositions.lean
Connectives.lean
Quantifiers.lean
Equality.lean
ProofSystems.lean
SimplyTypedLambdaCalculus.lean
StructuralRules.lean
OperationalSemantics.lean
RecursiveTypes.lean
TypeSafety.lean
Normalization.lean
SystemF.lean
LogicalRelations.lean
Parametricity.lean
DependentTypes.lean
IdentityTypes.lean
PureTypeSystems.lean
SubtypesAndRefinements.lean
IndexedFamilies.lean
GeneralInductiveFamilies.lean
WTypes.lean
HomotopyTypeTheory.lean
Quotients.lean
TypeClasses.lean
TypeInference.lean
Sets.lean
FunctionProperties.lean
Relations.lean
NaturalNumberInduction.lean
Orders.lean
Cardinality.lean
WellFounded.lean
Lattices.lean
FixedPoints.lean
CoinductivePredicates.lean
DomainTheory.lean
InitialAndTerminal.lean
Products.lean
Coproducts.lean
Categories.lean
Functors.lean
NaturalTransformations.lean
Equivalences.lean
Limits.lean
RepresentableFunctors.lean
YonedaLemma.lean
Adjunctions.lean
Monads.lean
EndofunctorAlgebras.lean
InitialAlgebras.lean
EndofunctorCoalgebras.lean
FinalCoalgebras.lean
Presheaves.lean
Sites.lean
Sheaves.lean
Monadicity.lean
EndsAndCoends.lean
KanExtensions.lean
MonoidalCategories.lean
EnrichedCategories.lean
InductionAndInitialAlgebras.lean
PolynomialFunctorsAndWTypes.lean
CoinductionAndFinalCoalgebras.lean
ThreeNotionsOfInfinity.lean
CartesianClosedCategories.lean
STLCCategoricalSemantics.lean
SlicesIndexedCategoriesAndFibrations.lean
LocallyCartesianClosedCategories.lean
DependentTypeCategoricalSemantics.lean
MonoidalClosedCategories.lean
LinearLogicAndResourceSemantics.lean
MonadsAndComputationalEffects.lean
ToposesAndCategoricalLogic.lean
RecursiveTypeSemantics.lean
Notation.lean
Terminology.lean
HistoricalSources.lean
ExerciseSolutions.lean
FoundationsAndLogic.lean
TypeSystems.lean
Mathematics.lean
Recursion.lean
DependentTypeTheory.lean
CategoryTheoryFoundations.lean
CategoryTheoryConstructions.lean
CategoryTheoryExtensions.lean
InductionCoinductionAndInfinity.lean
CategoricalTypeTheory.lean
LogicAndComputation.lean