namespace latin:/❚

fixmeta ?TypedEquality❚

theory Collection =
  include ?EndoMagma❙
  include ?EndoNeutral❙

  singleton : {a} tm a ⟶ tm &a❘# S 2 prec 60❙
  cons : {a} tm a ⟶ tm &a ⟶ tm &a❘= [a,x,xs] S x ∘ xs❙
❚

theory ListSpec =
  include ?Collection❙
  include ?EndoMonoid❙
❚

theory MultisetSpec =
  include ?ListSpec❙
  include ?EndoCommutative❙
❚

theory FiniteSetSpec =
  include ?MultisetSpec❙
  include ?EndoIdempotent❙
❚

theory OptionSpec =
  include ?ListSpec❙
  include ?EndoFirstNonNeutral❙
❚

theory Lists =
  structure list : ?ListSpec =
    applyType # List 1❙
    op # 2 concat 3❙
    e # nil %I1❙ 
    singleton # list 2❙
 ❚
❚

theory Multisets =
  structure multiset : ?MultisetSpec =
    applyType # Multiset 1❙
    op # 2 munion 3❙
    e # mempty %I1❙ 
    singleton # multiset 2❙
 ❚
❚

theory FiniteSets =
  structure finset : ?FiniteSetSpec =
    applyType # FinSet 1❙
    op # 2 union 3❙
    e # empty %I1❙ 
    singleton # finset 2❙
 ❚
❚

theory Options =
  structure option : ?OptionSpec =
    applyType # Option 1❙
    op # 2 orelse 3❙
    e # none %I1❙ 
    singleton # option 2❙
 ❚
❚