I didn't give any introduction and elimination rules for analogical equations in my previous post on analogical inference, but of course they exist. Some candidates for introduction rules:
[1] (a=c)
[2] (b=d)
.: (a:b):(c:d)
[1] (a=c)
.: (a:b):(c:d)
[1] (b=d)
.: (a:b):(a:d)
And, of course, they have analogues where the premises start with analogy, :, rather than identity, represented here as =. Actually, this is pretty common: just about anything you do with identity you can do with analogy, except where it really is crucial to assume that there is no difference whatsoever.
Some candidates for elimination rules:
[1] (a:b):(c:d)
.: (a:c)
[1] (a:b):(c:d)
.: (b:d)
And disassociation, mentioned in the previous post, is another such candidate.
In addition, it can sometimes be handy to have introduction and elimination of self-analogy.
[1] a
.: (a:a)
which can go in the other direction, as well, of course. Self-analogy is a little bit more interesting than it looks, because if we take the empty case as trivial, we can count, although it's not as perspicuous as doing so with sets:
( )
( : )
(( : ):( : ))
((( : ):( : )):(( : ):( : )))
and so forth. I imagine you could do fractions, but you'd have to add rules to disambiguate certain expressions.
