fact: Definition property := (forall a b u, inc u (homs a b) -> source u = a) & (forall a b u, inc u (homs a b) -> target u = b) & (forall a b u, inc u (homs a b) -> Arrow.like u) & (forall a b c u v, inc a obs -> inc b obs -> inc c obs -> inc u (homs b c) -> inc v (homs a b) -> inc (comps u v) (homs a c)) & (forall a, inc a obs -> inc (ids a) (homs a a)) & (forall a b u, inc a obs -> inc b obs -> inc u (homs a b) -> comps u (ids a) = u) & (forall a b u, inc a obs -> inc b obs -> inc u (homs a b) -> comps (ids b) u = u) & (forall a b c d u v w, inc a obs -> inc b obs -> inc c obs -> inc d obs -> inc u (homs c d) -> inc v (homs b c) -> inc w (homs a b) -> comps u (comps v w) = comps (comps u v) w).
imports: Arith ordinal nat_trans