Monoid_Mempty  (M:*) = M
Monoid_Mappend (M:*) = M -> M -> M

Monoid_Class
 (M:*) (Data:*)
 =  (mempty:Monoid_Mempty M)
 -> (mappend:Monoid_Mappend M)
 -> Data
Monoid_Polytype
 (M:*) : *p
 = (Data:*) -> Monoid_Class M Data -> Data
Monoid
 (M:*) : *m
 = Monotype (Monoid_Polytype M)

monoid
 (M:*)
 (mempty:Monoid_Mempty M)
 (mappend:Monoid_Mappend M)
 : Monoid M
 = monotype (Monoid_Polytype M)
    (λ(Data:*) (monoid_class:Monoid_Class M Data) ->
      monoid_class mempty mappend)
unMonoid
 (M:*) (Data:*)
 (monoid_class:Monoid_Class M Data)
 (monoid:Monoid M)
 : Data
 = polytype (Monoid_Polytype M) monoid Data monoid_class

Monoid_mempty
 (M:*) (monoid:Monoid M)
 : Monoid_Mempty M
 = unMonoid M (Monoid_Mempty M)
    (λ(mempty:Monoid_Mempty M) (mappend:Monoid_Mappend M) -> mempty)
    monoid
Monoid_mappend
 (M:*) (monoid:Monoid M)
 : Monoid_Mappend M
 = unMonoid M (Monoid_Mappend M)
    (λ(mempty:Monoid_Mempty M) (mappend:Monoid_Mappend M) -> mappend)
    monoid