By OTT, we mean Loïc Pujet and Nicolas Tabareau's Impredicative Observational Equality.
A type a : A b : A
------------------------
a ~_A b : Prop
cast A B : A ~_U B → A → B
KonjacSource
/ qit_syntax.md
Last active
August 15, 2026 15:31
Syntax for pattern matching QIT (and maybe HIT) in OTT (and maybe HOTT)