Constructing finitary inductive types from natural numbers

IITfromNat.agda

{-# 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.

   The method is the following: we inductively define signatures as typing contexts,
   and a type for constructor terms. Then for every signature we can construct an
   initial (term) model. This is a minimal simply-typed version of "Constructing
   Quotient Inductive-Inductive Types".

   Every type which we use here can be straightforwardly constructed from binary trees,
   using recursively defined annotations and well-formedness predicates. E.g. natural
   numbers are linear trees, and constructors terms are given with a typing predicate
   on trees.
   
   Also, it seems that if we construct any particular type from binary trees, we get
   strict computation rules for elimination. This could be useful for a "practical"
   reduction for inductive types.

   In this file I only get terms (for the theory of signatures) from trees, and I import other
   types. I do this because when everything is given with trees, I get confusing
   pattern coverage checking behavior from Agda and lots of coding noise.

2. Binary trees are constructible from Π, Σ, Uᵢ, _≡_, and ℕ, with weak computation rules.

   Related:
     This paper gives a construction of finitary inductive types from natural
     numbers and set quotients, which they derive from function and prop extensionality.

       https://arxiv.org/abs/1612.00693

   But it turns out we don't need quotients! In part 1 I sketched constructing
   finitary inductive types from binary tress, so here we set out to construct
   binary trees from natural numbers.

   The classical approach (also used in the above paper) to get binary trees, is
   to take the fixpoint of the functor F = λ A → ⊤ ⊎ (A × A), defined as the
   quotient (Σ ℕ λ n → Fⁿ ⊥)/R, where R relates representations of the same tree
   at different n-levels of Fⁿ⊥ approximation.

   We can ditch quotients if every tree is uniquely represented.  That's doable
   by defining a "height : (n : ℕ) → Fⁿ ⊥ → ℕ" function, then defining Tree as
   (Σ ℕ λ n → Σ (Fⁿ ⊥) λ t → height t ≡ n), which results in cutting out the
   redundant trees. So it is clear that this trick only works for finitary trees
   for which height is computable. My actual definition for Tree here is a more direct
   one which allows easier formalization in Agda.

   However, parts 1 and 2 can only be linked automatically if we work in extensional TT, 
   because in this part we only show propositional computation rules for trees.
   
   It's still believable though that for many inductive types, a direct construction
   from natural numbers (without going through trees) is doable without UIP and funext. 

If we combine this with previous results:

  Page 63 of:
  https://eutypes.cs.ru.nl/eutypes_pmwiki/uploads/Main/books-of-abstracts-TYPES2019.pdf

and some goodwill, we get that:

  Any finitary inductive type (large, indexed, inductive-inductive, you name it)
  can be reduced in *extensional type theory* to Π,Σ,Uᵢ,ℕ,_≡_.

We need the extensional part because reductions of ind-ind types only work
so far with UIP and funext.

As related work, I shall also mention this abstract, which is a really nice
reduction of inductive types:

  https://www.ps.uni-saarland.de/~rech/containers/A_Small_Basis_for_HoTT.pdf

However, this work assumes univalence and propositional resizing.


-}

-- Library
--------------------------------------------------------------------------------

open import Agda.Primitive hiding (_⊔_)
open import Data.Empty
open import Data.Nat hiding (_<_)
open import Data.Product renaming (proj₁ to ₁; proj₂ to ₂)
open import Data.Sum
open import Data.Unit
open import Function
open import Relation.Binary.PropositionalEquality

_◾_ = trans; infixr 4 _◾_
_⁻¹ = sym; infix 6 _⁻¹
ap  = cong
tr  = subst

J : ∀ {α β}{A : Set α} {x : A}
      (P : {y : A} → x ≡ y → Set β) → P refl → ∀ {y}(p : x ≡ y) → P p
J P pr refl = pr

hedberg :
  ∀ {α}{A : Set α}
  → ((x y : A) → (x ≡ y) ⊎ (x ≢ y))
  → ∀ {x y : A}(p q : x ≡ y) → p ≡ q
hedberg {_}{A} eq? {x}{y} p q =
  f-inv p ⁻¹ ◾ ap (_◾ f refl ⁻¹) (f-const p q) ◾ f-inv q
  where
    f : {x y : A} → x ≡ y → x ≡ y
    f {x}{y} p with eq? x y
    ... | inj₁ eq   = eq
    ... | inj₂ ¬eq  = ⊥-elim (¬eq p)

    f-const : ∀ {x y} p q → f {x}{y} p ≡ f q
    f-const {x}{y} p q  with eq? x y
    ... | inj₁ eq  = refl
    ... | inj₂ ¬eq = ⊥-elim (¬eq q)

    f-inv : ∀ {x y} p → (f {x}{y} p ◾ f refl ⁻¹) ≡ p
    f-inv refl = J (λ p → (p ◾ p ⁻¹) ≡ refl) refl (f refl)

data ABC (A B C : Set) : Set where
  inᵃ : A → ABC A B C
  inᵇ : B → ABC A B C
  inᶜ : C → ABC A B C

infix 3 _<_
data _<_ : ℕ → ℕ → Set where  -- also definable by recursion on ℕ
  here  : ∀ {n} → n < suc n
  there : ∀ {n m} → n < m → n < suc m

<-trs : ∀ {n m k} → n < m → m < k → n < k
<-trs p here      = there p
<-trs p (there q) = there (<-trs p q)

pred< : ∀ {n m} → suc n < m → n < m
pred< here = there here
pred< (there p) = there (pred< p)

0<s : ∀ n → 0 < suc n
0<s zero    = here
0<s (suc n) = there (0<s n)

s<s : ∀ {n m} → n < m → suc n < suc m
s<s here      = here
s<s (there p) = there (s<s p)

pred<pred : ∀ {n m} → suc n < suc m → n < m
pred<pred here = here
pred<pred {m = suc m} (there p) = there (pred<pred p)

<-irrefl : ∀ {n} → n < n → ⊥
<-irrefl {suc n} p = <-irrefl {n} (pred<pred p)

ℕ-set : ∀ {n : ℕ}(p : n ≡ n) → p ≡ refl
ℕ-set p = hedberg dec p refl
  where
    open import Relation.Nullary
    dec : (x y : ℕ) → x ≡ y ⊎ x ≢ y
    dec x y with Data.Nat._≟_ x y
    dec x y | yes p = inj₁ p
    dec x y | no ¬p = inj₂ ¬p

<-prop : ∀ {n m}(p q : n < m) → p ≡ q
<-prop p here = lem refl p where
  lem : ∀ {n m}(e : n ≡ m) → (p : n < suc m) → p ≡ tr (λ x → n < suc x) e here
  lem e here rewrite ℕ-set e = refl
  lem refl (there p) = ⊥-elim (<-irrefl p)
<-prop here (there q) = ⊥-elim (<-irrefl q)
<-prop (there p) (there q) = ap there (<-prop p q)

cmp : ∀ n m → ABC (n < m) (m < n) (n ≡ m)
cmp zero zero = inᶜ refl
cmp zero (suc m) = inᵃ (0<s m)
cmp (suc n) zero = inᵇ (0<s n)
cmp (suc n) (suc m) with cmp n m
... | inᵃ p = inᵃ (s<s p)
... | inᵇ p = inᵇ (s<s p)
... | inᶜ p = inᶜ (ap suc p)

cmp-refl : ∀ n → cmp n n ≡ inᶜ refl
cmp-refl zero = refl
cmp-refl (suc n) rewrite cmp-refl n = refl


-- Part 1
--------------------------------------------------------------------------------

module InductiveTypesFromBinaryTree where

  data Tree : Set where
    leaf : Tree
    node : Tree → Tree → Tree

  -- Ty, Con, Var are also constructible from Tree
  infix 2 ι⇒_
  data Ty : Set where     -- as linear trees
    ι : Ty
    ι⇒_ : Ty → Ty

  infixl 3 _▶_
  data Con : Set where    -- as lists (Ty-annotated linear tree)
    ∙   : Con
    _▶_ : Con → Ty → Con

  data Var : Con → Ty → Set where   -- definable by recursion on Con
    vz : ∀ {Γ A} → Var (Γ ▶ A) A
    vs : ∀ {Γ A B} → Var Γ A → Var (Γ ▶ B) A

  -- Terms. The intrinsic inductive definition would be the following:

  -- data Tm n (Γ : Con n) : Ty → Set
  -- data Sp n (Γ : Con n) : Ty → Ty → Set

  -- data Sp n Γ where
  --   []  : ∀ {A} → Sp n Γ A A
  --   _∷_ : ∀ {A B} → Tm n Γ zero → Sp n Γ A B → Sp n Γ (suc A) B

  -- data Tm n Γ where
  --   ne : ∀ {A} → Var n Γ A → Sp n Γ A zero → Tm n Γ zero

  -- well-formedness predicates
  Tmw : Con → Ty → Tree → Set
  Spw : Con → Ty → Ty → Tree → Set
  Tmw Γ i t = ∃ λ A → Var Γ A × Spw Γ A ι t × i ≡ ι
  Spw Γ A   B leaf        = A ≡ B
  Spw Γ ι⇒A B (node t sp) = ∃ λ A → Tmw Γ ι t × Spw Γ A B sp × ι⇒A ≡ (ι⇒ A)

  Tm : Con → Ty → Set
  Tm Γ A = ∃ (Tmw Γ A)

  Sp : Con → Ty → Ty → Set
  Sp Γ A B = ∃ (Spw Γ A B)

  [] : ∀ {Γ A} → Sp Γ A A
  [] = leaf , refl

  infixr 5 _∷_
  _∷_ : ∀ {Γ A B} → Tm Γ ι → Sp Γ A B → Sp Γ (ι⇒ A) B
  _∷_ (t , p) (sp , q) = node t sp , _ , p , q , refl

  ne : ∀ {Γ A} → Var Γ A → Sp Γ A ι → Tm Γ ι
  ne v (sp , p) = sp , _ , v , p , refl

  -- Example: construction of natural numbers from Tm. This is possible for any
  -- signature.
  NatSig : Con
  NatSig = ∙ ▶ ι ▶ (ι⇒ ι)  -- ∙ ▶ zero : Nat ▶ suc : Nat → Nat

  Nat : Set
  Nat = Tm NatSig ι

  Zero : Nat
  Zero = ne (vs vz) []

  Suc : Nat → Nat
  Suc n = ne vz (n ∷ [])

  NatElim : ∀ {i}(P : Nat → Set i) → P Zero → (∀ n → P n → P (Suc n)) → ∀ n → P n
  NatElim P z s (node t leaf , _ , vz , (_ , t* , refl , refl) , refl) =
    s (t , t*) (NatElim P z s (t , t*))
  NatElim P z s (node t (node _ _) , _ , vz , (_ , t* , (_ , _ , _ , ()) , refl) , refl)
  NatElim P z s (leaf , _ , vs vz , refl , refl) = z
  NatElim P z s (sp   , _ , vs (vs ()) , sp* , refl)


-- Part 2
--------------------------------------------------------------------------------

module BinaryTreeFromNaturals where

  -- I'm also using some types here, but all of them can be easily
  -- constructed from natural numbers. E.g. disjoint union with Σ, ⊤ as zero ≡
  -- zero, ⊥ as zero ≡ suc zero, and _<_ given by recursion.


  -- The inductive definition for height-indexed trees would be the following:
  -- data Tree : ℕ → Set
  -- data Tree↓ : ℕ → Set

  -- data Tree where
  --   leaf   : Tree zero
  --   nodeL  : ∀ {n} → Tree  n → Tree↓ n → Tree (suc n)
  --   nodeR  : ∀ {n} → Tree↓ n → Tree  n → Tree (suc n)
  --   nodeLR : ∀ {n} → Tree  n → Tree  n → Tree (suc n)

  -- data Tree↓ where
  --   here  : ∀ {n} → Tree  n → Tree↓ (suc n)
  --   there : ∀ {n} → Tree↓ n → Tree↓ (suc n)

  -- Tree' n is the set of trees with height n.
  -- Tree'↓ n is the set of trees with height less than n.
  Tree'  : ℕ → Set
  Tree'↓ : ℕ → Set
  Tree' zero    = ⊤  -- "leaf" is the only tree with height 0.
  Tree' (suc n) =
    ABC (Tree'  n × Tree'↓ n) -- The left subtree is taller
        (Tree'↓ n × Tree'  n) -- The right subtree is taller
        (Tree'  n × Tree'  n) -- Subtrees have the same height
  Tree'↓ zero    = ⊥
  Tree'↓ (suc n) = Tree' n ⊎ Tree'↓ n

  Tree : Set
  Tree = ∃ Tree'

  tree↓ : ∀ {n m} → m < n → Tree' m → Tree'↓ n
  tree↓ (here   ) t = inj₁ t
  tree↓ (there p) t = inj₂ (tree↓ p t)

  tree↑ : ∀ {n} → Tree'↓ n → (∃ λ m → m < n × Tree' m)
  tree↑ {suc n} (inj₁ t) = n , here , t
  tree↑ {suc n} (inj₂ t) = tree↑ t .₁ , there (tree↑ t .₂ .₁) , tree↑ t .₂ .₂

  tree↓↑ : ∀ {n} (t : Tree'↓ n) → tree↓ (tree↑ t .₂ .₁) (tree↑ t .₂ .₂) ≡ t
  tree↓↑ {suc n} (inj₁ _) = refl
  tree↓↑ {suc n} (inj₂ t) rewrite tree↓↑ t = refl

  --------------------------------------------------------------------------------

  leaf : Tree
  leaf = 0 , tt

  node : Tree → Tree → Tree
  node (n , l) (m , r) with cmp n m
  ... | inᵃ p    = suc m , inᵇ (tree↓ p l , r)
  ... | inᵇ p    = suc n , inᵃ (l , tree↓ p r)
  ... | inᶜ refl = suc n , inᶜ (l , r)

  -- eliminator
  --------------------------------------------------------------------------------
  TreeElim : ∀ {i}(P : Tree → Set i) → P leaf → (∀ {l r} → P l → P r → P (node l r))
               → ∀ {n} (t : Tree' n)  → P (_ , t)
  Tree↓Elim : ∀ {i}(P : Tree → Set i) → P leaf → (∀ {l r} → P l → P r → P (node l r))
               → ∀ {n}(t : Tree'↓ n) → P (_ , tree↑ t .₂ .₂)
  TreeElim P pl pn {zero} tt = pl
  TreeElim P pl pn {suc n} (inᵃ (l , r))
    with cmp n (₁ (tree↑ r)) | pn (TreeElim P pl pn l) (Tree↓Elim P pl pn r)
  ... | inᵃ p | hyp = ⊥-elim (<-irrefl (<-trs (tree↑ r .₂ .₁) p))
  ... | inᵇ p | hyp = tr (λ x → P (suc n , inᵃ (l , x)))
                         (ap (λ x → tree↓ x _) (<-prop _ _) ◾ tree↓↑ r)
                         hyp
  ... | inᶜ p | hyp = ⊥-elim (<-irrefl (tr ( tree↑ r .₁ <_) p (tree↑ r .₂ .₁)))
  TreeElim P pl pn {suc n} (inᵇ (l , r))
    with cmp (₁ (tree↑ l)) n | pn (Tree↓Elim P pl pn l) (TreeElim P pl pn r)
  ... | inᵃ p | hyp = tr (λ x → P (suc n , inᵇ (x , r)))
                         (ap (λ x → tree↓ x _) (<-prop _ _) ◾ tree↓↑ l)
                         hyp
  ... | inᵇ p | hyp = ⊥-elim (<-irrefl (<-trs p (tree↑ l .₂ .₁)))
  ... | inᶜ p | hyp = ⊥-elim (<-irrefl (subst (_< n) p (tree↑ l .₂ .₁)))
  TreeElim P pl pn {suc n} (inᶜ (l , r)) with
    cmp n n | cmp-refl n | pn (TreeElim P pl pn l) (TreeElim P pl pn r)
  ... | _ | refl | hyp = hyp
  Tree↓Elim P pl pn {suc n} (inj₁ t) = TreeElim P pl pn t
  Tree↓Elim P pl pn {suc n} (inj₂ t) = Tree↓Elim P pl pn t


  -- computation rules
  --------------------------------------------------------------------------------
  leafβ : ∀ {i P pl}{pn : ∀ {l r} → P l → P r → P (node l r)}
          → TreeElim {i} P pl pn (leaf .₂) ≡ pl
  leafβ = refl

  -- Agda doesn't want to let me prove this with with-pattern,
  -- I'd have to switch to ABC-elimination.
  -- Seems alright though.
  nodeβ : ∀ {i P pl}{pn : ∀ {l r} → P l → P r → P (node l r)}{l r}
          → TreeElim {i} P pl pn (node l r .₂)
          ≡ pn (TreeElim P pl pn (l .₂)) (TreeElim P pl pn (r .₂))
  nodeβ {i} {P} {pl} {pn} {n , l} {m , r} = {!!}