{-# OPTIONS --rewriting #-}

module TypeIsos where

import DS
import DSK
import CPS
open import DS-DSK
open import DSK-DS
open import DSK-CPS
open import CPS-DSK
open import DS-CPS
open import CPS-DS

open import Data.Unit
open import Data.Empty
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality


-- DS <-> DSK type translations (knT ∘ embT)

-- DS <-> DSK type translations (embT ∘ knT)

-- DSK <-> CPS type translations (cpskT ∘ dskT)

cpskΔ∘dskΔ≡id : (Δ : CPS.Delta) → cpskΔ (dskΔ Δ) ≡ Δ
cpskΔ∘dskΔ≡id (CPS.K) = refl
cpskΔ∘dskΔ≡id (CPS.•) = refl

{-# REWRITE cpskΔ∘dskΔ≡id #-}

cpskΘ∘dskΘ≡id : (Θ : CPS.Theta) → cpskΘ (dskΘ Θ) ≡ Θ
cpskΘ∘dskΘ≡id CPS.G = refl
cpskΘ∘dskΘ≡id (CPS.D Δ) = refl

{-# REWRITE cpskΘ∘dskΘ≡id #-}

-- DSK <-> CPS type translations (dskT ∘ cpskT)

dskΔ∘cpskΔ≡id : (Δ : DSK.Delta) → dskΔ (cpskΔ Δ) ≡ Δ
dskΔ∘cpskΔ≡id (DSK.K) = refl
dskΔ∘cpskΔ≡id (DSK.•) = refl

{-# REWRITE dskΔ∘cpskΔ≡id #-}

dskΘ∘cpskΘ≡id : (Θ : DSK.Theta) → dskΘ (cpskΘ Θ) ≡ Θ
dskΘ∘cpskΘ≡id DSK.G = refl
dskΘ∘cpskΘ≡id (DSK.D Δ) = refl

{-# REWRITE dskΘ∘cpskΘ≡id #-}

-- DS <-> CPS type translations (cpsT ∘ dsT)

-- DS <-> CPS type translations (dsT ∘ cpsT)