Questions tagged [inductive-type]

In terms of categorical semantics, an inductive type is a type whose interpretation is given by an initial algebra of an endofunctor. (from nLab)

Filter by
Sorted by
Tagged with
8 votes
3 answers
513 views

Construction of inductive types "the hard way"

Most theorem provers simply axiomize inductive types (or equivalently W types) in the abstract which is fine. But I'm curious about explicit constructions of recursive types within the theory. I know ...
user avatar
4 votes
2 answers
133 views

Turning off some sProp checks

In Definitional Proof Irrelevance Without K, inductives in sProp need to satisfy three conditions to allow large elimination: (1) Every non-forced argument must be in sProp. (2) The return types of ...
user avatar
  • 856
5 votes
2 answers
155 views

How to prove in Lean that sums are distributive?

Assume we are given three types in Lean. constants A B C : Type There is a canonical map of the following form. ...
user avatar
  • 433
11 votes
2 answers
325 views

Proving uniqueness of an instance of an indexed inductive type

Consider the simple indexed inductive type Inductive Single : nat -> Set := | single_O : Single O | single_S {n} : Single n -> Single (S n). Intuitively, I ...
user avatar
  • 213
11 votes
2 answers
423 views

Replacing (strict) positivity with monotonicity on propositions

When defining an inductive type, there is a famous "positivity" restriction on the constructor types. For example, an inductive type $\mathsf D$ has constructor $\mathsf c : F(\mathsf D) \to ...
user avatar
  • 2,256
6 votes
1 answer
171 views

Parameterized Datatypes in a Universe à la Tarski?

I'm wondering, is there a way to make a Universe à la Tarski that models all of the types in an open type theory, where there can be user defined parameterized inductive types? For context, I'm trying ...
user avatar
11 votes
0 answers
77 views

Rules for mutual inductive/coinductive types

Some proof assistants, like Agda and maybe Coq, allow families of mutually defined types, or nested definitions of types, in which some are inductive and others are coinductive. I have no idea what ...
user avatar
  • 2,079
10 votes
1 answer
212 views

Is induction over mutually inductive coinductive types possible?

You can encode ordinals in Coq as Inductive ord := O | S (n: ord) | Lim (s: nat -> ord). Suppose you use the following encoding instead ...
user avatar
10 votes
1 answer
208 views

What are well-founded inductive types?

W-types are said to be "a well-founded inductive type" that is parameterized over arities and constructors, similar to a "tree of possible constructions". On nlab, it is said that ...
user avatar
  • 4,136
15 votes
3 answers
187 views

Expressivity of mutual/nested inductives vs. regular inductives

This question is from @TaliaRinger: Are mutually inductive types and plain old inductive types equally expressive? (Say, in Coq.) I assume yes, but the motive for induction will be a huge mess. But ...
user avatar
  • 856
2 votes
1 answer
123 views

Defining Lists and Prove Associativity of Append [closed]

When I saw this question asking what is the "Hello, World!" for proof assistants I immediately thought of that exercise. Not a long time after this answer by Couchy was proposed. Therefore, ...
user avatar
  • 898
9 votes
2 answers
134 views

Are eliminators useful in practice, or are they only useful in the metatheory?

We can derive eliminators (as functions) for inductive types and translate (structurally) recursive functions into invocations of eliminators. However, eliminators seem to be essentially recursive ...
user avatar
  • 4,136