Questions tagged [inductive-type]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
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, (...
sparusaurata's user avatar
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 ...
user avatar
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 ...
ionchy's user avatar
  • 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 ...
მამუკა ჯიბლაძე's user avatar
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 \; \...
Łukasz Lew's user avatar
  • 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 ...
Labbekak's user avatar
  • 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 ...
Ilk's user avatar
  • 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: ...
Labbekak's user avatar
  • 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 ...
Turion's user avatar
  • 584