▼B629 Spring 2023 – Proofs as Programs
►5 Worksheets
On this page:
5.1 March 28, 2023; Ho  TT:   equivalences and bi-invertible maps
5.2 March 30, 2023; Agda:   identity, Σ, universes
5.3 April 4, 2023; Agda:   HITs
5.4 April 6, 2023; Agda:   Dependent eliminators for HITs
5.5 April 11, 2023; Ho  TT:   Contractibility
5.6 April 13, 2023; Ho  TT:   Propositional truncation
8.7.0.8
    contents  ← prev  up  next → 

5 Worksheets

Installing the HoTTEST prelude

5.1 March 28, 2023; HoTT: equivalences and bi-invertible maps

5.2 March 30, 2023; Agda: identity, Σ, universes

5.3 April 4, 2023; Agda: HITs

5.4 April 6, 2023; Agda: Dependent eliminators for HITs

5.5 April 11, 2023; HoTT: Contractibility

5.6 April 13, 2023; HoTT: Propositional truncation

    contents  ← prev  up  next →