module MapType where

open import Data.Maybe
open import Data.Pair
open import Data.List
open import Data.Either
open import Logic.Id

open import Equivalence
open import Rewrite
open import Lists

-- Changing the type universe

data _==₁_ (A : Set) : Set -> Set where
  refl : A ==₁ A

record TypeMorphism (U₁ U₂ : TypeUniverse) : Set1 where
  module U₁ = TypeUniverse U₁
  module U₂ = TypeUniverse U₂

  field
    fType : U₁.Type -> U₂.Type
    fElem : {a : U₁.Type} -> U₁.El a -> U₂.El (fType a)

    lem-pres-El  : {a : U₁.Type} -> U₁.El a ==₁ U₂.El (fType a)
    lem-pres-≅   : forall {a}(x y : U₁.El a) -> U₁._≅_ x y -> U₂._≅_ (fElem x) (fElem y)
    lem-fElem-id : {a : U₁.Type}(x : U₁.El a) -> x == fElem x

  lem-pres-Fun : forall {Γ a} -> Fun U₁.El Γ a ==₁ Fun U₂.El (map fType Γ) (fType a)
  lem-pres-Fun {Γ = []} = lem-pres-El
  lem-pres-Fun {Γ = a :: Γ}{b} with U₁.El a | lem-pres-El {a} | Fun U₁.El Γ b | lem-pres-Fun {Γ}{b}
  ... | ._ | refl | ._ | refl = refl
  

MapType : {U₁ U₂ : TypeUniverse} -> TypeMorphism U₁ U₂ -> Language U₁ -> Language U₂
MapType {U₁}{U₂} TM L₁ = record
  { Con      = Con
  ; matchCon = matchCon
  ; c⟦_⟧     = c⟦_⟧
  ; ≅-cong   = ≅-cong
  }
  where
    open TypeUniverse U₁ renaming (Type to Type₁; El to El₁; cmpType to cmpType₁; _≅_ to _≅₁_)
    open TypeUniverse U₂ renaming (Type to Type₂; El to El₂; cmpType to cmpType₂; _≅_ to _≅₂_)
    open TypeMorphism TM
    module L₁ = Language L₁

    data Con : List Type₂ -> Type₂ -> Set where
      liftCon : forall {Γ a} -> L₁.Con Γ a -> Con (map fType Γ) (fType a)

    matchCon : forall {Γ Δ a b}(c₁ : Con Γ a)(c₂ : Con Δ b) -> Maybe ((Γ , a , c₁) == (Δ , b , c₂))
    matchCon (liftCon c₁) (liftCon c₂) with L₁.matchCon c₁ c₂
    matchCon (liftCon c ) (liftCon .c) | just refl = just refl
    matchCon (liftCon c₁) (liftCon c₂) | nothing   = nothing

    c⟦_⟧ : forall {Γ a}(c : Con Γ a) -> Fun El₂ Γ a
    c⟦ liftCon {Γ}{a} c ⟧ with Fun El₁ Γ a | lem-pres-Fun {Γ}{a} | L₁.c⟦_⟧ c
    ... | ._ | refl | f = f

    ≅-cong : forall {Γ a}{us vs : All El₂ Γ}(c : Con Γ a) -> Zip _≅₂_ us vs -> c⟦ c ⟧ <#> us ≅₂ c⟦ c ⟧ <#> vs
    ≅-cong (liftCon {Γ}{a} c) ps with Fun El₁ Γ a | lem-pres-Fun {Γ}{a} | L₁.c⟦_⟧ c
    ... | ._ | refl | ⟦c⟧₁ = {!\{us vs} -> L₁.≅-cong {us = us}{vs} c!}