Skip to main content
14 votes
Accepted

Defining inductive types in intensional type theory purely in terms of type-theoretic data

It turns out that $W$ types plus identity types (eq/= in Coq) allow you to construct pretty much all the general inductive types ...
Jasper Hugunin's user avatar
6 votes
Accepted

From Church-encoding to induction principle

Let $F : \mathsf{Type} \to \mathsf{Type}$ be a type constructor and let $W_F$ be the inductive type defined by $W_F = F W_F$. Not every $F$ has such an inductive types, but this is not important for ...
Andrej Bauer's user avatar
  • 29.2k
4 votes

How to define list zipping categorically/inductively?

This complication is the same as in the definition of the Church predecessor function. We need to take the tail of a list, but we only have a folding operation given by (weak) initiality, which does ...
András Kovács's user avatar
3 votes
Accepted

How to prove that $\exists A. ~ A \times (A\to F~ A)$ encodes the greatest fixpoint of $F$?

The surjective pairing rule is really just as written there by Wadler. Andrej's interpretation is correct. What the equation ...
Li-yao Xia's user avatar
2 votes
Accepted

Can the initial algebra of a 2-variable polynomial functor be computed on the diagonal?

I finally came up with a proof under the hypotheses of (and thoroughly using) Adamek's fix-point theorem, I'll post it here as soon as I write it down properly. Anyway, I found a bit late that this is ...
sparusaurata's user avatar
1 vote

How to prove that $\exists A. ~ A \times (A\to F~ A)$ encodes the greatest fixpoint of $F$?

Is this not just confusion about notation? If the notation (X, y) is used to signify the introduction rule for then it does ...
Andrej Bauer's user avatar
  • 29.2k
1 vote
Accepted

Intuition behind nested positivity and counterexamples

Here is an example exploiting positivity of an index to prove false: ...
Dan Doel's user avatar
  • 1,021

Only top scored, non community-wiki answers of a minimum length are eligible