Questions tagged [inductive-type]
The inductive-type tag has no usage guidance.
9
questions
3
votes
1
answer
123
views
Can the initial algebra of a 2-variable polynomial functor be computed on the diagonal?
Given a polynomial functor $F$, its initial algebra is denoted by $\mu X.F(X)$.
Now, if $F$ is a 2-variable polynomial functor, $Y \mapsto \mu X.F(X,Y)$ turns out to be functorial and we can, again, (...
- 199
6
votes
1
answer
505
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
321
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
112
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
228
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
3
votes
0
answers
108
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 ...
- 701
6
votes
0
answers
125
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 ...
- 900
2
votes
1
answer
339
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:
...
- 701
6
votes
2
answers
251
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