module Korean where

open import Data.String

data Language : Set
data Country : Set
data Citizen : Set
data Noun : Set

data Language where
  _어 : Country → Language

data Country where
  한국 : Country

data Citizen where
  _인 : Country → Citizen

한국어 : Language
한국어 = 한국 어

data Noun where
  [_]₀ : Language → Noun
  [_]₁ : Country → Noun
  [_]₂ : Citizen → Noun
  학교 : Noun
  도시 : Noun
  이름 : Noun

data Thing : Set where
  이 : Noun → Thing
  [_] : Noun → Thing
  저 : Thing
  나 : Thing

data Place : Set where
  _에 : Thing → Place
  _에서 : Thing → Place

한국에 = [ [ 한국 ]₁ ] 에
한국어에 = [ [ 한국 어 ]₀ ] 에

학교에서 : Place
학교에서 = [ 학교 ] 에서

한국인 : Citizen
한국인 = 한국 인







module English where

open import Data.String

data Language : Set
data Country : Set
data Citizen : Set
data Noun : Set

data Language where
  _n/ish : Country → Language

data Country where
  Korea : Country

data Citizen where
  _n : Country → Citizen

data Noun where
  [_]₀ : Language → Noun
  [_]₁ : Country → Noun
  [_]₂ : Citizen → Noun
  school : Noun
  city : Noun
  name : Noun

data Thing : Set where
  this : Noun → Thing
  a : Noun → Thing
  the : Noun → Thing
  a/the/pl : Noun → Thing
  I : Thing

data Place : Set where
  in/at : Thing → Place






module Translate where

open import Data.String

open import Korean as Ko
open import English as En

country : Ko.Country → En.Country
country 한국 = Korea

noun : Ko.Noun -> En.Noun
noun [ x 어 ]₀ = [ (country x) n/ish ]₀
noun [ x ]₁ = [ country x ]₁
noun [ x 인 ]₂ = [ (country x) n ]₂
noun 학교 = school
noun 도시 = city
noun 이름 = name
--noun (이 x) = this (noun x)

thing : Ko.Thing → En.Thing
thing (이 x) = this (noun x)
thing [ x ] = a/the/pl (noun x)
thing 저 = I
thing 나 = I

place : Ko.Place → En.Place
place (x 에) = in/at thing x
place (x 에서) = in/at thing x