mor(A,F,C),mor(C,G,D) -> mor(A,comp(F,G),D). % diagrammatic notation
mor(A,F,B),mor(A,G,C) -> mor(A,pair(F,G),prod(B,C)).
mor(prod(A,B),F,C) -> mor(A,cur(F),func(B,C)).

%mor(A,id(A),A).
%mor(A,drop(A),one).
mor(prod(A,B),fst(A,B),A).
mor(prod(A,B),snd(A,B),B).
mor(pair(func(A,B),A),app(A,B),B).


%mor(A,F,C) -> 
%  comp(id(A),F) = F.
%mor(A,F,C) -> 
%  comp(F,id(C)) = F.


mor(A,F,B),mor(B,G,C),mor(C,H,D) -> 
  comp(comp(F,G),H)=comp(F,comp(G,H)).

% drop <>

%mor(A,F,one) -> 
%  drop(A)=F.

% <F,G> o fst = F

mor(A,F,B),mor(A,G,D) -> 
  comp(pair(F,G),fst(B,D)) = F.


% <F,G> o snd = G

mor(A,F,B),mor(A,G,D) -> 
  comp(pair(F,G),snd(B,D)) = G.

% <F o fst,F o snd> = F

mor(C,F,prod(A,B)) -> 
  pair(comp(F,fst(A,B)),comp(F,snd(A,B))) = F.


% <fst o cur(f),snd> o app = f

mor(prod(A,B),F,C) -> 
   comp(pair(comp(fst(A,B),cur(F)),snd(A,B)),app(B,C)) = F.


% cur(<fst o f,snd> o app ) = f  (*)

mor(A,F,func(B,C)) -> 
   cur(comp(pair(comp(fst(A,B),F),snd(A,B)),app(B,C))) = F.

% Lemma 1: pair F G @ H == pair (F @ H) (G @ H)

%mor(A,F,B),mor(A,G,C),mor(D,H,A) ->
%  comp(H,pair(F,G)) = pair(comp(H,F),comp(H,G)).
   

% Lemma 2: <G o cur(F),H> o app = <G,H> o F

mor(D,G,A),mor(prod(A,B),F,C),mor(D,H,B) ->
   comp(pair(comp(G,cur(F)),H),app(B,C)) = comp(pair(G,H),F).


% conjecture
% Lemma 3: G o (cur F)== cur (<fst o G, snd> o F).
 

mor(c,g,a).
mor(prod(a,b),f,d).
comp(g,cur(f)) = cur(comp(pair(comp(fst(c,b),g),snd(c,b)),f)) -> [].

% expansion by (*)
% cur(comp(pair(comp(fst(c,b),comp(g,cur(f))),snd(c,b)),app(b,d))) = cur(comp(pair(comp(fst(c,b),g),snd(c,b)),f)) -> [].



%precedence([app,fst,snd,func,pair,comp,cur,id,drop,one,mor,a,b,c,f,g]).
precedence([app,fst,snd,func,pair,comp,cur,mor,a,b,c,f,g]).

option([search_depth(3)]).
%:-sama([2]).
:-sarp(+[15]).