fact: Definition property (o m:E) (c:E2) (i:E1) := (forall x, inc x o = object_property o m i x) & (forall u, inc u m = morphism_property o m c i u) & (forall u v, inc u m -> inc v m -> source u = target v -> composable_property m c u v) & (forall u v w, inc u m -> inc v m -> inc w m -> source u = target v -> source v = target w -> c (c u v) w = c u (c v w)).
imports: Arith universe