------------------------------------------------------------------------
-- The two semantical definitions of subtyping are equivalent
------------------------------------------------------------------------

module RecursiveTypes.Subtyping.Semantic.Equivalence where

open import Data.Nat
open import Coinduction
open import Function

open import RecursiveTypes.Syntax
open import RecursiveTypes.Subtyping.Semantic.Inductive
open import RecursiveTypes.Subtyping.Semantic.Coinductive

mutual

  ≤∞⇒≤↓ :  {n} {σ τ : Tree n}  σ ≤∞ τ  σ ≤↓ τ
  ≤∞⇒≤↓ le              zero    = 
  ≤∞⇒≤↓                (suc k) = 
  ≤∞⇒≤↓                (suc k) = 
  ≤∞⇒≤↓ var             (suc k) = refl
  ≤∞⇒≤↓ (τ₁≤σ₁  σ₂≤τ₂) (suc k) = ≤∞⇒≤↑ ( τ₁≤σ₁) k  ≤∞⇒≤↓ ( σ₂≤τ₂) k

  ≤∞⇒≤↑ :  {n} {σ τ : Tree n}  σ ≤∞ τ  σ ≤↑ τ
  ≤∞⇒≤↑ le              zero    = 
  ≤∞⇒≤↑                (suc k) = 
  ≤∞⇒≤↑                (suc k) = 
  ≤∞⇒≤↑ var             (suc k) = refl
  ≤∞⇒≤↑ (τ₁≤σ₁  σ₂≤τ₂) (suc k) = ≤∞⇒≤↓ ( τ₁≤σ₁) k  ≤∞⇒≤↑ ( σ₂≤τ₂) k

domain :  {n} {σ₁ σ₂ τ₁ τ₂ : FinTree n} 
         σ₁  σ₂ ≤Fin τ₁  τ₂  σ₂ ≤Fin τ₂
domain refl            = refl
domain (τ₁≤σ₁  σ₂≤τ₂) = σ₂≤τ₂

codomain :  {n} {σ₁ σ₂ τ₁ τ₂ : FinTree n} 
           σ₁  σ₂ ≤Fin τ₁  τ₂  τ₁ ≤Fin σ₁
codomain refl            = refl
codomain (τ₁≤σ₁  σ₂≤τ₂) = τ₁≤σ₁

mutual

  ≤↑⇒≤∞ :  {n} (σ τ : Tree n)  σ ≤↑ τ  σ ≤∞ τ
  ≤↑⇒≤∞  _ le = 
  ≤↑⇒≤∞ _  le = 
  ≤↑⇒≤∞   le with le 1
  ... | ()
  ≤↑⇒≤∞  (var x) le with le 1
  ... | ()
  ≤↑⇒≤∞  (σ  τ) le with le 1
  ... | ()
  ≤↑⇒≤∞ (var x)  le with le 1
  ... | ()
  ≤↑⇒≤∞ (var x) (var x′) le with le 1
  ≤↑⇒≤∞ (var x) (var .x) le | refl = var
  ≤↑⇒≤∞ (var x) (σ  τ) le with le 1
  ... | ()
  ≤↑⇒≤∞ (σ₁  τ₁)  le with le 1
  ... | ()
  ≤↑⇒≤∞ (σ₁  τ₁) (var x) le with le 1
  ... | ()
  ≤↑⇒≤∞ (σ₁  τ₁) (σ₂  τ₂) le =
     ≤↓⇒≤∞ ( σ₂) ( σ₁) (codomain  le  suc) 
     ≤↑⇒≤∞ ( τ₁) ( τ₂) (domain    le  suc)

  ≤↓⇒≤∞ :  {n} (σ τ : Tree n)  σ ≤↓ τ  σ ≤∞ τ
  ≤↓⇒≤∞  _ le = 
  ≤↓⇒≤∞ _  le = 
  ≤↓⇒≤∞   le with le 1
  ... | ()
  ≤↓⇒≤∞  (var x) le with le 1
  ... | ()
  ≤↓⇒≤∞  (σ  τ) le with le 1
  ... | ()
  ≤↓⇒≤∞ (var x)  le with le 1
  ... | ()
  ≤↓⇒≤∞ (var x) (var x′) le with le 1
  ≤↓⇒≤∞ (var x) (var .x) le | refl = var
  ≤↓⇒≤∞ (var x) (σ  τ) le with le 1
  ... | ()
  ≤↓⇒≤∞ (σ₁  τ₁)  le with le 1
  ... | ()
  ≤↓⇒≤∞ (σ₁  τ₁) (var x) le with le 1
  ... | ()
  ≤↓⇒≤∞ (σ₁  τ₁) (σ₂  τ₂) le =
     ≤↑⇒≤∞ ( σ₂) ( σ₁) (codomain  le  suc) 
     ≤↓⇒≤∞ ( τ₁) ( τ₂) (domain    le  suc)

Ind⇒Coind :  {n} {σ τ : Ty n}  σ ≤Ind τ  σ ≤Coind τ
Ind⇒Coind = ≤↓⇒≤∞ _ _

Coind⇒Ind :  {n} {σ τ : Ty n}  σ ≤Coind τ  σ ≤Ind τ
Coind⇒Ind = ≤∞⇒≤↓