Alex Mobius (Feb 27 2026 at 18:29): Alex Mobius (Feb 27 2026 at 18:29):I confess, I'm still not very comfortable with how exactly transfer works. The thing I'm trying to do is to lift a relation from map onto fmap. That itself it easy enough. Then i also want to lift a bunch of theorems concerning left/right uniqueness, converse of converse, relcompp, ... Trouble is, whenever I try to transfer, I am staring at a term like
Transfer.Rel
((pcr_fmap (=) (=) ===>
pcr_fmap (=) (=) ===> (=)) ===>
(=))
?ac10 right_unique
(the schematic var stands in for right_unique in practice too). Now it seems like there should be a general transfer rule here, but I'm unable to figure it out, is it for right-total bi-unique R S, `((R ===> S ===> (=)) ===> (=)) right_unique right_unique"? In any case, this seems like a conspicuous omission... how do people normally lift relations? Clearly the automatic process is able to do it just fine without transfer rules...
Last updated: Mar 04 2026 at 20:34 UTC