21. Univalent Foundations

Univalent Foundations

Univalent Foundations is a framework for the formalization of mathematics based on homotopy type theory.

In Univalent Foundations, the univalence axiom is a key principle that states that isomorphic structures are equal.

This principle allows for a more flexible and intuitive treatment of mathematical objects, where equivalences between structures are considered on equal footing with equality.

Key concepts in Univalent Foundations include:

• Univalence axiom: A principle that identifies isomorphic structures as equal.
• Higher inductive types: Types that are generated not only by constructors but also by higher-dimensional paths, capturing more intricate topological structure.
• Identity types: Types that represent equality or paths between elements of a given type.
• Homotopy equivalence: A relation between types that captures the idea of them being "the same" up to continuous deformation.

Univalent Foundations provides a new perspective on the foundations of mathematics, with connections to topology, category theory, and computer science.

Lab Activity: Implementing Higher Inductive Types in Coq

Let's implement a higher inductive type in a proof assistant like Coq to demonstrate Univalent Foundations.

Inductive Circle : Type :=
  | base : Circle
  | loop : base = base.

Definition circle_map (p : loop = loop) : base = base := p.

Definition torus := circle_map loop.
  

In this lab activity, we define a higher inductive type called `Circle` representing a circle.

We then define a function `circle_map` that maps the loop of the circle to itself.

Finally, we define a torus using the circle map, which represents a higher-dimensional torus.