Questions tagged [inductive-type]

The tag has no usage guidance.

3 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
6
votes
0answers
127 views

Postulating self types in a proof assistant

Self types introduce two typing new rules (simplified): $ \frac{\Gamma \; \vdash \; t : [t/x]T}{\Gamma \; \vdash \; t : \iota x. T}$ I-self and $ \frac{\Gamma \; \vdash \; t : \iota x. T}{\Gamma \; \...
6
votes
0answers
101 views

Programmatic higher inductive/inductive-inductive types with equalities between equalities

I can think of practical HITs in verified software that capture some form of alpha equivalence, context equivalence or the example which defines well-typed syntax of type theory from Signatures and ...
2
votes
0answers
34 views

Parigot encoding for F-Algebras

In this answer it is shown we can encode inductive types in System F-omega using the church encoding: $Fix F = \forall T : \mathsf{Type} \,.\, (F T \to T) \to T$ for some type constructor $F$. It ...