%%% Cartesian closed category
%%%
%%% Categorical language

%%%%  objects
obj : type.  %name obj O.


%% Products
% objects
1 : obj.
* : obj -> obj -> obj. %infix none 10 *.

%% Exponentials
=> : obj -> obj -> obj. %infix right 7 =>.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%% morphisms
mor : obj -> obj -> type.  %name mor F.

% morphisms
id : mor A A.
@ : mor B C -> mor A B -> mor A C. 
%infix none 10 @.

drop : mor A 1.

fst : mor (A * B) A.
snd : mor (A * B) B.
pair : mor A B -> mor A C -> mor A (B * C).

app : mor ((B => C) * B) C.
cur : mor (A * B) C -> mor A (B => C).

% morphism equality
f:mor A1 A2.
g:mor A1 A3.
h:mor A4 A1.

== : mor A B -> mor A B -> type.  %name == ME.
 %infix none 5 ==.
%tabled ==.

% equations
% reordered equations for tabling purposes
% still needs at least abstraction to prevent
% getting stuck 
% 
ass  : H @ (G @ F) == (H @ G) @ F.

prod_l : fst @ (pair F G) == F.
prod_r : snd @ (pair F G) == G.
prod_u : H == pair (fst @ H) (snd @ H).


% @(H @(G F))
=@= : F @ G == F' @ G'
       <- F == F' 
       <- G == G'.

=pair= : pair F G == pair F' G'
	  <- F == F' 
	  <- G == G'.


refl : F == F.

then : F == F''
	<- F == F'
	<- F' == F''. %infix right 4 then. 


% sym : F == F' -> F' == F. 
% id_l : id @ F == F.
% id_r : F @ id == F.



% term_u : H == drop.


% =cur= : F == F' -> cur F == (cur F').

% exp_e : app @ (pair ((cur F) @ fst) snd) == F.
% term-depth : 4
% (@  app pair(@((cur F) fst) snd))  

% term-depth : 
% exp_u : cur (app @ (pair (G @ fst) snd)) == G.
% term-depth: 4
% cur(@ app (pair (@ G fst) snd))

% distp : pair F G @ H == pair (F @ H) (G @ H).
% distc : (cur F) @ G == cur (F @ (pair (G @ fst) snd)).