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)
40
questions
23
votes
0
answers
570
views
Categorical semantics of Agda
I would like to know the state of the art regarding the categorical semantics of the type theory implemented by Agda — or at least some approximation of that type theory that is amenable to ...
- 3,200
18
votes
1
answer
1k
views
What are the complex induction patterns supported by Agda?
A question was recently asked on the Coq-club mailing list on Coq rejecting a nastily nested inductive type. We encountered a similar difficulty while trying to port code from Agda to Coq: Agda ...
- 5,510
16
votes
3
answers
247
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 ...
- 1,026
12
votes
1
answer
490
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
...
- 2,868
12
votes
0
answers
169
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 ...
- 3,200
11
votes
2
answers
412
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 ...
- 213
10
votes
1
answer
629
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 ...
- 6,306
10
votes
2
answers
547
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 ...
- 4,025
10
votes
2
answers
217
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 ...
- 6,306
9
votes
2
answers
822
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 inductive types within the theory.
I ...
- 2,868
9
votes
1
answer
322
views
Strong eta-rules for functions on sum types
I am wondering whether a rule like the following is consistent with decidable conversion and type-checking for dependent type theory:
$$ \frac{f\, g : (x:\mathsf{bool}) \to C~x\quad f~\mathsf{tt} \...
- 3,200
6
votes
4
answers
841
views
Inductive vs. recursive definitions
In Coq there are two ways to define a new type on an inductive type: Using Inductive and using Fixpoint. What are pros and cons ...
- 224
6
votes
2
answers
273
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.
...
- 722
6
votes
1
answer
253
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 ...
- 921
5
votes
1
answer
149
views
Explain all the arguments to this rec eliminator
I defined this inductive type for representing JSON elements
...
- 273