%%% Cartesian closed category
%%% Prepared for first-order theorem proving experiments

%% Categorical language

% objects
obj : type.  %name obj A.

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

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

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

% equations
refl : F == F.
then : F == F' -> F' == F'' -> F == F''. %infix right 4 then.
sym : F == F' -> F' == F.

=@= : F == F' -> G == G' -> F @ G == F' @ G'.

id_l : id @ F == F.
id_r : F @ id == F.
ass  : H @ (G @ F) == (H @ G) @ F.

%% Products

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

% morphisms
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).

% equations
=pair= : F == F' -> G == G' -> pair F G == pair F' G'.

term_u : H == drop.

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

%% Exponentials

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

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

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

exp_e : app @ (pair ((cur F) @ fst) snd) == F.
exp_u : cur (app @ (pair (G @ fst) snd)) == G.

% lemmas
distp : pair F G @ H == pair (F @ H) (G @ H).

appl : app @ pair (cur F @ G) H == F @ pair G H.

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