Homotopies for Free!

Introduction

i : A → (X : U) → (A → X) → X, i ≡ λ a. λ (X, g). ga.

Abstraction Theorem Applied

An Embedding

i ≡ λ (a : A). λ (X : U, g : A → X). g a

Church Encodings of Spaces

(X : U) (x : X) F_A(X, x) → X

The Circle

(S^1 → X) ≃ (x : X) x = x.

Spheres

S^n (X : U) (x : X) Ω^n(X, x) → X

Suspensions

S^n (X : U) (x, y : X) (A → x = y) → X.

Joins

The Hopf Map

Homotopy Type Theory