(.module:
  [library
   [lux "*"
    ["_" test {"+" [Test]}]
    [abstract
     [monad {"+" [do]}]]
    [math
     ["[0]" random]
     [number
      ["n" nat]]]]]
  [\\library
   ["[0]" / {"+" [CoMonad]}]]
  [//
   [functor {"+" [Injection Comparison]}]])

(def: (left_identity injection (^open "_//[0]"))
  (All (_ f) (-> (Injection f) (CoMonad f) Test))
  (do [! random.monad]
    [sample random.nat
     morphism (# ! each (function (_ diff)
                          (|>> _//out (n.+ diff)))
                 random.nat)
     .let [start (injection sample)]]
    (_.test "Left identity."
            (n.= (morphism start)
                 (|> start _//disjoint (_//each morphism) _//out)))))

(def: (right_identity injection comparison (^open "_//[0]"))
  (All (_ f) (-> (Injection f) (Comparison f) (CoMonad f) Test))
  (do random.monad
    [sample random.nat
     .let [start (injection sample)
           == (comparison n.=)]]
    (_.test "Right identity."
            (== start
                (|> start _//disjoint (_//each _//out))))))

(def: (associativity injection comparison (^open "_//[0]"))
  (All (_ f) (-> (Injection f) (Comparison f) (CoMonad f) Test))
  (do [! random.monad]
    [sample random.nat
     increase (# ! each (function (_ diff)
                          (|>> _//out (n.+ diff)))
                 random.nat)
     decrease (# ! each (function (_ diff)
                          (|>> _//out(n.- diff)))
                 random.nat)
     .let [start (injection sample)
           == (comparison n.=)]]
    (_.test "Associativity."
            (== (|> start _//disjoint (_//each (|>> _//disjoint (_//each increase) decrease)))
                (|> start _//disjoint (_//each increase) _//disjoint (_//each decrease))))))

(def: .public (spec injection comparison subject)
  (All (_ f) (-> (Injection f) (Comparison f) (CoMonad f) Test))
  (<| (_.for [/.CoMonad])
      ($_ _.and
          (..left_identity injection subject)
          (..right_identity injection comparison subject)
          (..associativity injection comparison subject)
          )))