Questions tagged [inductive-type]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
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 ...
user avatar
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 ...
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