Skip to main content

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
12 votes
1 answer
471 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 ...
Ms. Molly Stewart-Gallus's user avatar
4 votes
1 answer
209 views

Making a finite graph type in Lean - introduction rule

I'm making a finite directed graph type in Lean. I know type theory from an abstract point of view, but I'm struggling to find the way Lean would produce a type playing the role of a "finite set&...
Ronald J. Zallman's user avatar
16 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 ...
Meven Lennon-Bertrand's user avatar
10 votes
2 answers
541 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 ...
Trebor's user avatar
  • 3,967
9 votes
2 answers
813 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 ...
Ms. Molly Stewart-Gallus's user avatar