What are arrows in the category of CMRAs?
In cmra.v
, we define CmraMorphism
, and use it int the notion of rFunctor:
Structure rFunctor := RFunctor {
rFunctor_car : ofeT → ofeT → cmraT;
rFunctor_map {A1 A2 B1 B2} :
((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
rFunctor_ne A1 A2 B1 B2 :
NonExpansive (@rFunctor_map A1 A2 B1 B2);
rFunctor_id {A B} (x : rFunctor_car A B) : rFunctor_map (cid,cid) x ≡ x;
rFunctor_compose {A1 A2 A3 B1 B2 B3}
(f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
rFunctor_map (f◎g, g'◎f') x ≡ rFunctor_map (g,g') (rFunctor_map (f,f') x);
rFunctor_mor {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
CmraMorphism (rFunctor_map fg)
}.
However, in the manual we say:
The category
\CMRAs
consists of cameras as objects, and monotone functions as arrows.
My question is: Which is right?