The following pages link to Proofs for free (Q2844694):
Displaying 15 items.
- Canonicity of weak \(\omega\)-groupoid laws using parametricity theory (Q283766) (← links)
- Formalizing semantic bidirectionalization and extensions with dependent types (Q347391) (← links)
- The \textsc{MetaCoq} project (Q2209542) (← links)
- Comprehensive Parametric Polymorphism: Categorical Models and Type Theory (Q2811329) (← links)
- Friends with Benefits (Q2988636) (← links)
- Proof-Relevant Parametricity (Q3188282) (← links)
- I Got Plenty o’ Nuttin’ (Q3188289) (← links)
- A Syntax for Higher Inductive-Inductive Types (Q4993350) (← links)
- Pointers in Recursion: Exploring the Tropics (Q5089027) (← links)
- Leibniz equality is isomorphic to Martin-Löf identity, parametrically (Q5120232) (← links)
- (Q5216301) (← links)
- Lax Theory Morphisms (Q5277906) (← links)
- Ornaments for Proof Reuse in Coq (Q5875438) (← links)
- A presheaf model of parametric type theory (Q5971392) (← links)
- Is Impredicativity Implicitly Implicit (Q6079240) (← links)
