fact: Definition ob_facts c x := ob c x & mor c (id c x) & composable c (id c x) (id c x) & source (id c x) = x & target (id c x) = x & comp c (id c x) (id c x) = (id c x)& (forall u, mor c u -> source u = x -> comp c u (id c x) = u)& (forall u, mor c u -> target u = x -> comp c (id c x) u = u).
imports: Arith universe