AndrasKovacs

{-# OPTIONS --without-K #-}

{-
Claim: finitary inductive types are constructible from Π,Σ,Uᵢ,_≡_ and ℕ, without
quotients. Sketch in two parts.

1. First, construction of finitary inductive types from Π, Σ, Uᵢ, _≡_ and binary trees.
   Here I only show this for really simple, single-sorted closed inductive types,
   but it should work for indexed inductive types as well.