Questions tagged [inductive-type]
The inductive-type tag has no usage guidance.
8
questions
6
votes
1
answer
463
views
Defining inductive types in intensional type theory purely in terms of type-theoretic data
To define a (non-indexed) W-type all we need is a type $A:U$ and a function $B:A\to U$ and we get a type $W_{a:A}B(a)$. To check that this definition is valid we only need to check that the ...
user61651
6
votes
2
answers
307
views
Intuition behind nested positivity and counterexamples
I'm looking at the nested positivity conditions for inductive types stated in the Coq manual. First off, are there any other references (not necessarily for Coq, but in dependent type theories ...
- 325
3
votes
0
answers
103
views
Request for an update on a discussion about coinductive types in HoTT (or anywhere else)
Googling something else I stumbled on a conversation titled "coinductives" initiated by Vladimir Voevodsky on Google groups in 2014. It lasted for three days, invloved a dozen people, and ...
- 131
6
votes
0
answers
207
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 \; \...
- 1,177
2
votes
0
answers
88
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 ...
- 691
6
votes
0
answers
119
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 ...
- 841
2
votes
1
answer
285
views
From Church-encoding to induction principle
I am looking for an algorithm to go from a Church-encoded datatype to their induction principle in the Calculus of Constructions. For example:
...
- 691
6
votes
2
answers
229
views
How to define list zipping categorically/inductively?
Lists and fixpoints
The type of $A$-lists is defined as $\mu F_A$, where $F_A(X) = 1 + A \times X$ is the "cons-or-nil"-functor and $\mu$ is the least fixpoint operator. In Haskell syntax, this would ...
- 584