Skip to main content

Questions tagged [cubical-agda]

The Cubical mode extends Agda with a variety of features from the CHM version of Cubical Type Theory. In particular, computational univalence and higher inductive types which hence gives computational meaning to Homotopy Type Theory and Univalent Foundations.

2 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
2 votes
0 answers
91 views

Lower bounds in type theory proof assistant with ordinals and universes without axioms

I saw a PowerPoint that claimed to achieve $\psi_0(\Gamma_{\Omega+1})$ in Agda without any axioms. I was wondering if a better lower bound exists in 2024? My ...
Ember Edison's user avatar
1 vote
0 answers
144 views

Designing a proof assistant around Cubical

As far as I know, Agda is currently the only "widely popular" theorem prover to have somewhat good HoTT support via it's CubicalTT mode. Now, I understand what has slowed down the addition ...
blueberry's user avatar
  • 111