Questions tagged [inductive-type]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
6 votes
1 answer
372 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
284 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 ...
user avatar
  • 215
3 votes
0 answers
94 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 ...
user avatar
6 votes
0 answers
177 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 \; \...
user avatar
  • 1,147
2 votes
0 answers
64 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 ...
user avatar
  • 691
6 votes
0 answers
114 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 ...
user avatar
  • 713
2 votes
1 answer
211 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: ...
user avatar
  • 691
6 votes
2 answers
220 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 ...
user avatar
  • 574