% A few test examples

%% Translation from lambda-terms to categorical combinators

% [[ |- \x.x]]
%query 1 *
abse empty (llam [x] x) M.

% [[ x |- \y.(y,x) ]]
%query 1 *
{x}abse (addv empty x) (llam [y] lpair y x) M.

% [[ |- \x.\y.x y ]]
%query 1 *
abse empty (llam [x] llam [y] lapp x y) M.

%% Translation from categorical combinators to lambda-terms 

% <| id @ snd |>
%query 1 *
conc (id @ snd) E.

% <| app @ <snd, fst> |>
%query 1 *
conc (app @ pair snd fst) E.

% <| cur (app) @ snd |>
%query 1 *
conc (cur app @ snd) E.

%% Preservation of beta-eta equality by [[ ]] - translation
%{
% (\y.(\x.x) y) = \z.z  (using beta, xi)
sigma [ap1:abse empty (llam [y] lapp (llam [x] x) y) M1]
  sigma [ap2:abse empty (llam [z] z) M2]
    ctoe (c_lam [y] c_beta) ap1 ap2 EP.

% (\y.(\x.x) y) = \z.z  (using eta)
sigma [ap1:abse empty (llam [y] lapp (llam [x] x) y) M1]
  sigma [ap2:abse empty (llam [z] z) M2]
    ctoe (c_eta) ap1 ap2 EP.
}%
%% Preservation of CCC equality by <| |> - translation

% app @ (pair ((cur fst) @ fst) snd) = fst
%{
sigma [cp1:conc (app @ (pair ((cur fst) @ fst) snd)) E1]
  sigma [cp2: conc fst E2]
    etoc exp_e cp1 cp2 EP.
}%
%query 1 *
etoc exp_e (ccomp capp (cpair (ccomp (ccur cfst) cfst) csnd)) (cfst) EP.

%% Translation lambda -> ccc -> lambda preserves equality

% translate \x.\y.(x,y) to ccc and back
%{
sigma [ap:abse empty (llam [x] llam [y] lpair x y) M]
  sigma [cp:conc M E]
    sigma [zp:exp empty Z] % a term-representaiton of the environment
      invca ap cp zp EP.
}%

%query 1 *
invca
(alam ([x:term _A1] alam ([x1:term _A2] apair (avar (av_y av_x)) (avar av_x))))
(ccur (ccur (cpair (ccomp csnd cfst) csnd)))
(exp_empty)
EP.

%% Translation ccc -> lamda -> ccc preserves equality

% translate cur(app) @ fst to lambda-term and back
%{
sigma [cp:conc ((cur app) @ fst) E]
  sigma [ap: zabs E F]
    invac cp ap EP.
}%