fact: Definition is_ob_facts a x := is_ob a x & is_mor a (id a x) & source (id a x) = x & target (id a x) = x & (forall f, is_mor a f-> source f = x -> comp a f (id a x) = f) & (forall f, is_mor a f-> target f = x -> comp a (id a x) f = f).
imports: Arith universe