------------------------------------------------------------------------ -- An example ------------------------------------------------------------------------ module RecursiveTypes.Subtyping.Example where open import Coinduction open import Data.Fin open import Data.Nat open import RecursiveTypes.Syntax open import RecursiveTypes.Subtyping.Semantic.Coinductive -- σ = μX. X ⟶ X. σ : Ty 0 σ = μ var zero ⟶ var zero -- τ = μX. (X ⟶ ⊥) ⟶ ⊤. τ : Ty 0 τ = μ (var zero ⟶ ⊥) ⟶ ⊤ -- σ is a subtype of τ. σ≤τ : σ ≤Coind τ σ≤τ = ♯ (♯ σ≤τ ⟶ ♯ ⊥) ⟶ ♯ ⊤