namespace latin:/algebraic❚

fixmeta latin:/?SFOLEQND❚

theory Set = 
  universe : tp❙
  U = tm universe❙
❚

theory SetHom = 
   structure domain : ?Set❚
   structure codomain : ?Set❚
   U : domain/U ⟶ codomain/U ❙
❚

theory SubSet = 
  structure parent : ?Set =
    U # P❙
  ❚
  universe : P ⟶ prop❘# U 1 prec 40❙
❚