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)

9 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
22 votes
0 answers
563 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 ...
Mike Shulman's user avatar
  • 3,060
12 votes
0 answers
167 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 ...
Mike Shulman's user avatar
  • 3,060
2 votes
0 answers
61 views

Elimination rules of inductive types

Why does the elimination rule of inductive types sometimes allow the target type to depend on the inductive type and sometimes not? I am confused by that. Is it correct that it makes no difference in ...
Nico's user avatar
  • 722
1 vote
0 answers
64 views

Heterogeneous lists, large indices

Recently I had cause to define a type of heterogeneous lists in Lean, and wrote ...
Brendan Murphy's user avatar
1 vote
0 answers
44 views

how to inductively define paths from paths using unimath

I'd like to define a type of graph where given a set of edges, we can define another graph that has everything from graph 1 but extends the set of edges by adding higher level edges to parallel edges(...
noCrayCray's user avatar
1 vote
0 answers
60 views

Why does Coq not allow constructor argument types to be strictly positive mutual inductive types?

Note: Apologies for the wicked mouthful of a title. I'm still getting acquainted with Coq terminology, so I might not have chosen the best words. If you have a better title suggestion, edits are more ...
Kyle Lin's user avatar
  • 143
1 vote
0 answers
48 views

Can you always replace mutually recursive references with parameters?

This is a follow up to a question someone else previously posted: Expressivity of mutual/nested inductives vs. regular inductives. pigworker answered that Adopting Agda-ish notation, the basic ...
Kyle Lin's user avatar
  • 143
1 vote
0 answers
179 views

Descriptions of heterogenous datatypes

When attempting to describe the datatype as appearing in my previous question, using indexed descriptions in style of The Gentle Art of Levitation to describe this datatype (using Agda for examples): <...
Ilk's user avatar
  • 547
-2 votes
2 answers
114 views

Help with strong induction

I have the following definition of divisibility by 3. ...
deleted_user0972's user avatar