fact: Definition is_subcategory a b := Category.axioms a & Category.axioms b & structure a = structure b & (forall x, ob a x -> ob b x) & (forall u, mor a u -> mor b u) & (forall u v, mor a u -> mor a v -> source u = target v -> comp a u v = comp b u v) & (forall x, ob a x -> id a x = id b x).
imports: Arith ordinal nat_trans