data Nat :: Set = zero | suc (n :: Nat)

idata Vec (!X :: Set) :: Nat -> Set where
  vnil :: Vec X zero
  vcons (|n :: Nat)(x :: X)(xs :: Vec X n) :: Vec X (suc n)

{-
vtail (X :: Set)(n :: Nat) :: Vec X (suc n) -> Vec X n
vtail xs = {!xs !}
-}

vecElim (X :: Set)(n :: Nat)
  :: (xs :: Vec X n)->
       (P :: (n :: Nat)-> Vec X n -> Set)->
         (mvnil :: P zero vnil)->
         (mvcons :: (n :: Nat)|-> (x :: X)-> (xs :: Vec X n)->
                    P n xs -> P (suc n) (vcons x xs))->
           P n xs
vecElim xs P mvnil mvcons = case xs of 
  (vnil)-> mvnil 
  (vcons n' x xs')-> mvcons x xs' (vecElim xs' P mvnil mvcons )

JMEq (A,B :: Set) :: A -> B -> Set
JMEq a b = JMeq A a B b

JMSubst (A :: Set)(a,a' :: A) :: (q :: JMEq a a')->(C :: A -> Set)-> C a -> C a'
JMSubst q C c = case q of 
                    (same)->  c

NatNoConfStmt :: (m,n :: Nat)-> Set -> Set
NatNoConfStmt m n P = case m of 
  (zero)-> case n of 
    (zero)-> P -> P 
    (suc n')-> P 
  (suc m')-> case n of 
    (zero)-> P 
    (suc n')-> (JMEq m' n' -> P) -> P 

NatNoConf (P :: Set)(m,n :: Nat) :: JMEq m n -> NatNoConfStmt m n P
NatNoConf q = case q of 
                  (same)-> case m of 
                               (zero)-> \p -> p 
                               (suc n')-> \(h::JMeq Nat n' Nat n' -> P)-> 
                                          h same 



vTail (X :: Set)(n :: Nat) :: Vec X (suc n) -> Vec X n
vTail xs = vecElim xs
           (\m -> \ys -> (n::Nat)-> Vec X (suc n)->
              JMEq m (suc n) -> Vec X n)
           (\(n'::Nat)-> 
            \(h::Vec X (suc n'))-> 
            \(h'::JMeq Nat zero Nat (suc n'))-> 
            NatNoConf h')
           (\(n'::Nat) |-> \(x::X)-> \(xs'::Vec X n')->
            \(h::(n0::Nat)-> Vec X (suc n0)-> JMEq n' (suc n0)-> Vec X n0)->
            \(n0::Nat)-> \(h'::Vec X (suc n0))->
            \(h0::JMeq Nat (suc n') Nat (suc n0))->
            NatNoConf h0 (\(h1::JMeq Nat n' Nat n0)-> 
              JMSubst h1 (\n0 -> Vec X n0) xs' ))
           n xs same


vec (X :: Set)(n :: Nat) :: X -> Vec X n
vec x = case n of 
            (zero)-> vnil
            (suc n')-> vcons x (vec x)

vapp (S,T :: Set)(n :: Nat) :: Vec (S -> T) n -> Vec S n -> Vec T n
vapp gs ss = vecElim gs (\n -> \gs -> Vec S n -> Vec T n)
  (\(h::Vec S zero)-> 
   vecElim h (\n' -> \h -> JMEq n' zero -> Vec T zero) 
     (\(h'::JMeq Nat zero Nat zero)->  vnil)
     (\(n'::Nat) |-> \(x::S)-> \(xs::Vec S n')-> 
      \(h'::JMeq Nat n' Nat zero -> Vec T zero)-> 
      \(h0::JMeq Nat (suc n') Nat zero)->  NatNoConf h0)
     same)
  (\(n'::Nat) |-> \(x::S -> T)-> \(xs::Vec (S -> T) n')-> 
   \(h::Vec S n' -> Vec T n')-> 
   \(h'::Vec S (suc n'))-> 
   vecElim h'
   (\m ->
    \ys ->
    (n'::Nat)->
    (x::S -> T)->
    (xs::Vec (S -> T) n')->
    (h::Vec S n' -> Vec T n')->
    (h'::Vec S (suc n'))->
    JMEq m (suc n')-> Vec T (suc n'))
   (\(n''::Nat)->
    \(x'::S -> T)->
    \(xs'::Vec (S -> T) n'')->
    \(h0::Vec S n'' -> Vec T n'')->
    \(h''::Vec S (suc n''))->
    \(h1::JMeq Nat zero Nat (suc n''))->
    NatNoConf h1)
   (\(n0::Nat) |->
    \(x'::S)->
    \(xs'::Vec S n0)->
    \(h0::(n''::Nat)-> (x0::S -> T)-> (xs0::Vec (S -> T) n'')->
          (h0::Vec S n'' -> Vec T n'')->
          (h''::Vec S (suc n''))-> JMEq n0 (suc n'')-> Vec T (suc n''))->
    \(n''::Nat)->
    \(x0::S -> T)->
    \(xs0::Vec (S -> T) n'')->
    \(h1::Vec S n'' -> Vec T n'')->
    \(h''::Vec S (suc n''))->
    \(h2::JMeq Nat (suc n0) Nat (suc n''))->
    NatNoConf h2 (\(h3::JMeq Nat n0 Nat n'')-> 
      JMSubst h3 (\n'' -> Vec (S -> T) n'' -> 
                         (Vec S n'' -> Vec T n'') -> Vec T (suc n''))
        (\gs' -> \vappgs' -> 
         vcons (x0 x' )
               (vappgs' xs' ))
        xs0 h1))
   n' x xs h h' same)
  ss 

transpose (m,n :: Nat)(X :: Set) :: Vec (Vec X n) m -> Vec (Vec X m) n
transpose xnm = case xnm of 
                    (vnil)-> vec vnil 
                    (vcons n' x xs)-> vec vcons `vapp` x `vapp` transpose xs 

VecNoConfStmt (X :: Set)(n,n'  :: Nat) :: Vec X n -> Vec X n' -> Set -> Set
VecNoConfStmt xs xs' P = case xs of 
  (vnil)-> case xs' of 
    (vnil)-> P -> P 
    (vcons n0 x xs0)-> P 
  (vcons n0 x xs0)-> case xs' of 
    (vnil)-> P 
    (vcons n1 x' xs1)-> (JMEq n0 n1 -> JMEq x x' -> JMEq xs0 xs1 -> P)-> P 

VecNoConf (P :: Set)
          (X :: Set)(n :: Nat)(xs,xs' :: Vec X n)
          :: JMEq xs xs' -> VecNoConfStmt xs xs' P
VecNoConf q = case q of 
  (same)-> case xs of 
    (vnil)-> \p -> p 
    (vcons n' x xs0)-> \(h::JMeq Nat n' Nat n' ->
                            JMeq X x X x ->
                            JMeq (Vec X n') xs0 (Vec X n') xs0 -> P)-> 
                            h same same same 

{----------------------------------------------------------------------------}

data Ty :: Set = N | Arr (s,t :: Ty)

TyNoConfStmt :: (s,t::Ty)-> Set -> Set
TyNoConfStmt s t P = case s of 
  (N)-> case t of 
    (N)-> P -> P 
    (Arr s1 t1)-> P 
  (Arr s0 t0)-> case t of 
    (N)-> P 
    (Arr s1 t1)-> (JMEq s0 s1 -> JMEq t0 t1 -> P) -> P 

TyNoConf (P :: Set)(s,t :: Ty) :: JMEq s t -> TyNoConfStmt s t P
TyNoConf q = case q of 
  (same)-> case s of 
    (N)-> \(h::P)-> 
           h
    (Arr s' t')-> \(h::JMEq s' s' -> JMEq t' t' -> P)-> 
                  h same same

data Ctxt :: Set = EC | CC (G :: Ctxt) (T :: Ty)

CtxtNoConfStmt :: (P :: Set)-> (G,H :: Ctxt)-> Set
CtxtNoConfStmt P G H = case G of 
  (EC)-> case H of 
    (EC)-> P -> P 
    (CC G1 T1)-> P 
  (CC G0 T0)-> case H of 
    (EC)-> P 
    (CC G1 T1)-> (JMEq G0 G1 -> JMEq T0 T1 -> P ) -> P

CtxtNoConf (G,H :: Ctxt)(P :: Set) :: JMEq G H -> CtxtNoConfStmt P G H
CtxtNoConf q = case q of 
  (same)-> case G of 
    (EC)-> \(h::P)-> h 
    (CC G' T)-> \(h::JMEq G' G' -> JMEq T T -> P)-> 
                h same same

idata Var (!T :: Ty) :: Ctxt -> Set where
  { vz (G :: Ctxt) :: Var T (CC G T)
  ; vs (|G :: Ctxt)(x :: Var T G)(|S :: Ty) :: Var T (CC G S)
  }

idata Tm :: Ty -> Ctxt -> Set where
  { var (|T :: Ty)(|G :: Ctxt)(x :: Var T G) :: Tm T G
  ; app (|S,|T :: Ty)(|G :: Ctxt)(f :: Tm (Arr S T) G)(s :: Tm S G) :: Tm T G
  ; lam (|S,|T :: Ty)(|G :: Ctxt)(t :: Tm T (CC G S)) :: Tm (Arr S T) G
  }

Env :: (F :: Ty -> Set)-> (G :: Ctxt)-> Set
Env F G = (S :: Ty)|-> Var S G -> F S 

enil1 :: (F :: Ty -> Set)-> (G :: Ctxt)-> (q :: JMEq G EC) -> Env F G
enil1 F G q = \S |-> \i -> case i of 
  (vz G')-> CtxtNoConf q
  (vs G' x S')-> CtxtNoConf q

enil :: (F :: Ty -> Set) -> Env F EC
enil F = enil1 F EC same

econs1 (F :: Ty -> Set)(G,H :: Ctxt)(S,S' :: Ty) ::
       JMEq H (CC G S) -> Env F G -> F S -> Var S' H -> F S'
econs1 = \(q::JMEq H (CC G S))-> 
         \(h'::Env F G)-> 
         \(h0::F S)-> 
         \(h1::Var S' H)-> 
         case h1 of 
           (vz G')-> CtxtNoConf q
                      (\(h2::JMEq  G'  G)-> 
                       \(h3::JMEq  S'  S)-> 
                       JMSubst h3 (\S -> F S -> F S') (\(h4::F S')-> h4 ) h0  )
           (vs G' x S0)-> CtxtNoConf q
                           (\(h2::JMEq G' G)-> 
                            \(h3::JMEq S0 S)-> 
                              JMSubst h2 (\G -> Env F G -> F S')
                              (\(h4::Env F G')-> h4 x ) h' )

econs (F :: Ty -> Set)(G :: Ctxt) :: (g :: Env F G) -> (S :: Ty)-> (s :: F S) ->
                                     Env F (CC G S)
econs g S s = \(S'::Ty) |-> \(i::Var S' (CC G S))-> econs1 same g s i

image (G,H :: Ctxt)(T :: Ty) ::
         (F :: Ty -> Ctxt -> Set) ->
         (VarF :: (T :: Ty)-> (G :: Ctxt)-> Var T G -> F T G) ->
         (FTm :: (T :: Ty)-> (G :: Ctxt)-> F T G -> Tm T G) ->
         (FWk :: (T,S :: Ty)-> (G :: Ctxt)-> F T G -> F T (CC G S)) ->
         Env (\S -> F S H) G ->
         Tm T G -> Tm T H
image F VarF FTm FWk tau t = case t of 
  (var T' G' x)-> FTm T' H (tau x)
  (app S T' G' f s)->
    app (image F VarF FTm FWk tau f)
        (image F VarF FTm FWk tau s )
  (lam S T' G' t)->
    lam (image F VarF FTm FWk
           (econs (\(S'::Ty) |-> \(h'::Var S' G')->
                     FWk S' S H (tau h'))
                  S
                  (VarF S (CC H S) (vz H)))
         t)


rename (G,H :: Ctxt)(U :: Ty) :: ((S :: Ty)|-> Var S G -> Var S H) ->
                                               Tm U G -> Tm U H
rename rho u = image Var
                     (\(T::Ty)-> 
                      \(G'::Ctxt)-> 
                      \(h::Var T G')-> 
                      h )
                     (\(T::Ty)-> 
                      \(G'::Ctxt)-> 
                      \(h::Var T G')-> 
                      var h )
                     (\(T,S::Ty)-> 
                      \(G'::Ctxt)-> 
                      \(h::Var T G')-> 
                      vs h )
                     rho
                     u

subst (G,H :: Ctxt)(U :: Ty) :: ((S :: Ty)|-> Var S G -> Tm S H) ->
                                               Tm U G -> Tm U H
subst sgm u = image Tm
                    (\(T::Ty)-> 
                     \(G'::Ctxt)-> 
                     \(h::Var T G')-> 
                     var h )
                    (\(T::Ty)-> 
                     \(G'::Ctxt)-> 
                     \(h::Tm T G')-> 
                     h )
                    (\(T,S::Ty)-> 
                     \(G'::Ctxt)-> 
                     \(h::Tm T G')-> 
                     rename (\(S'::Ty) |-> \(h'::Var S' G')-> 
                                          vs h' )
                            h )
                    sgm 
                    u


fred :: Tm (Arr N N) (CC EC (Arr N N))
fred = lam (app (var (vs (vz EC)))
                (var (vz (CC EC (Arr N N)))))

jim :: Tm (Arr N N) (CC (CC EC (Arr N N)) N)
jim = rename (econs (enil (\(h::Ty)-> 
                           Var h
                               (CC (CC EC (Arr N N)) N)))
                    (Arr N N)
                    (vs (vz EC))) fred

sheila :: Tm (Arr N N) EC
sheila = subst (econs (enil (\(h::Ty)-> 
                             Tm h EC))
                      (Arr N N)
                      (lam (var (vz EC)))) fred
{-
Val :: Ty -> Set
Val T = {! !}

eval (G :: Ctxt)(T :: Ty) :: Tm T G -> Env Val G -> Val T
eval t gam = {! !}
-}