12

It turns out that $W$ types plus identity types (eq/= in Coq) allow you to construct pretty much all the general inductive types you want, with the expected computation rules, and even canonicity. This is a very recent result of mine, you can read a preprint at Why not W?, which has been accepted for publication in the TYPES 2020 post-proceedings. The idea ...


6

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 this discussion. The starting point of Church's encodings is the observation that $W_F$ ought to be $$\forall T : \mathsf{Type} \,.\, (F T \to T) \to T.$$ Thus, ...


4

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 not directly provide access to that, so we need to rebuild the tail from the right end. It is the easiest to write the solution in a lambda calculus with ...


1

Here is an example exploiting positivity of an index to prove false: module Whatever where open import Level using (Level) open import Relation.Binary.PropositionalEquality open import Data.Empty variable ℓ : Level A B : Set ℓ data _≅_ (A : Set ℓ) : Set ℓ → Set ℓ where trefl : A ≅ A Subst : (P : Set ℓ → Set ℓ) → A ≅ B → P A → P B Subst P trefl PA = ...


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