Trebor-Huang
/ freeCCC.agda
Last active
August 12, 2025 08:46
Defines STLC as the free CCC over the base type in Agda directly with HITs. Proves canonicity directly by induction.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# OPTIONS --cubical --no-import-sorts --postfix-projections -W ignore #-} | |
| module freeCCC where | |
| open import Cubical.Foundations.Prelude | |
| open import Cubical.Foundations.HLevels | |
| open import Cubical.Foundations.Function | |
| open import Cubical.Foundations.Isomorphism | |
| open import Cubical.Data.Unit using (Unit; isPropUnit; isSetUnit) | |
| open import Cubical.Data.Bool using (Bool; true; false; if_then_else_; isSetBool) | |
| open import Cubical.Data.Sum using (_⊎_; inr; inl) | |
| open import Cubical.Data.Sigma using (Σ; _×_; ΣPathP) |