Tesla Zhang
ice1000@types.pl
<p>Spherical Agda in a vacuum</p>
Posts
-
Post #3183684
If A is subtype of A&#39;, let a : A, and define f : A&#39; := a, should f : A hold judgmentally? How would you implement this? (subtyping can show up if you have subtyping-based cumulative universe)
-
Post #3183683
@jesper In definitional proof-irrelevance without K, how did you setup this beautiful Rocq code syntax highlighting?
-
Post #3183681
Cobisimulation
-
Post #3183680
where&#39;s the new pl minus context