module RecursiveTypes.Subtyping.Semantic.Equivalence where
open import Data.Nat
open import Codata.Musical.Notation
open import Function.Base
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 = ≤∞⇒≤↓