fact: Definition is_scale (u : E) := A (mor_axioms u) (A (injective u) (A (is_well_ordered (source u)) (A (is_well_ordered (target u)) (forall x y : E, inc x (U (source u)) -> leq (target u) y (ev u x) -> ex (fun z : E => A (inc z (U (source u))) (ev u z = y)))))).
imports: universe