Foundations

Learn what a claim covers, explain why it works, and recognise an allowed case that shows it needs changing.

Classical logic combines truth-valued propositions using defined connectives.

A mathematical proof derives a conclusion within stated assumptions and rules.

A set specifies membership without counting duplicate listings.

A function assigns exactly one output to each input in its domain.

A base case and general successor step establish a predicate on all nonnegative integers.

Quantifiers bind variables over a specified domain.

Set existence is governed by explicit axioms and schemas.

Upper-bounded nonempty real sets have least upper bounds.

Countability includes finite sets in this convention.

An equivalence relation partitions a set into classes.

Semantic consequence and arithmetic completeness are distinct.

The nerve of an ordinary category has n-simplices given by chains of n composable arrows; inner horns have unique fillers encoding composition.

A category has objects, composable morphisms, associative composition and an identity for every object.

A natural transformation eta:F⇒G assigns a morphism eta-X:F(X)→G(X) to every object so that G(f) eta-X=eta-Y F(f).

For a locally small category C, a functor F:C→Set and object c, natural transformations from Hom(c,−) to F correspond bijectively to elements of F(c), by evaluating at the identity of c.

An adjunction F left-adjoint to U is a natural bijection Hom-D(FX,Y)≅Hom-C(X,UY).

In intensional dependent type theory, a term x:A inhabits a type, dependent products encode functions/proofs with variable-dependent result types, and identity types encode identifications.

Univalence states that the canonical map from identity of types in a universe to equivalence of types is itself an equivalence.