Part II: Homotopy Type Theory
This part is a practical introduction to homotopy type theory in the context of Arend. Themes discussed here include data types with conditions (higher inductive types) and homotopy levels of universes.
This part is a practical introduction to homotopy type theory in the context of Arend. Themes discussed here include data types with conditions (higher inductive types) and homotopy levels of universes.