Questions tagged [extensional-type-theory]

Use for proof assistants or type theories featuring an equality type that has a reflection rule creating judgemental equalities out of them. See also [reflection].

Filter by
Sorted by
Tagged with
11 votes
1 answer
262 views

Normalization by evaluation for extensional type theories

Is there material on how to implement normalization for (any flavor of) ETT? This describes techniques related to doing untyped normalization. But there are (operational and semantic) problems when ...
Trebor's user avatar
  • 3,718
2 votes
1 answer
101 views

Is existence of Stream as final co-algebra for the suitable functor enough to write functions into equality of streams by co-induction in ExtMLTT?

Suppose we work inside MLTT with equality reflection (extensional MLTT). Assume I postulate existence of Streams as final co-algebra for the suitable functor. Is that enough to prove the bisimulation ...
Russoul's user avatar
  • 345