Index. Homotopy Type Theory in Cubical Agda [hca]

This index collects the notes I wrote while playing the Hott Game. I compiled them into a small demo I gave here.

propositions as types
lambda abstaction
natural numbers
playing with natural numbers
Identity type
groupoid laws

TheHoTTGame/0Trinitarianism/Quest0.lagda.md TheHoTTGame/0Trinitarianism/Quest1.lagda.md TheHoTTGame/0Trinitarianism/Quest2.lagda.md TheHoTTGame/0Trinitarianism/Quest3.lagda.md TheHoTTGame/0Trinitarianism/Quest4.lagda.md TheHoTTGame/0Trinitarianism/Quest5.lagda.md

Backlinks

Index. Homotopy Type Theory [004R]

Homotopy Type Theory in Cubical Agda

The Empty Type [005P.lagda]

We need to disable the K-Axiom, which is incompatible with Homotopy type theory

{-# OPTIONS --without-K #-}

In agda Set denotes the universe of small types. somelink

The emtpy type is the type with no elements. It can be interpreted as a proposition that has no proofs.

data 𝟘 : Set where

The elimination rule for elements of the empty type yields an element of any depended type indexed by x : 𝟘. This is analogous to the idea, that you can prove anything from falsehood.

𝟘-elim : {A : 𝟘 → Set} (x : 𝟘) → A x
𝟘-elim ()

Note that () refers to the impossible match. Since there is no x : A, there is nothing to define for that branch.

We can define negation as a map that sends any type A : Set to A -> 𝟘 : Set.

neg : Set -> Set
neg A = A -> 𝟘