(.module:
  [library
   [lux "*"
    ["_" test {"+" [Test]}]
    [abstract
     [monad {"+" [do]}]
     [\\specification
      [functor
       ["$[0]" contravariant]]]]
    [data
     ["[0]" bit ("[1]\[0]" equivalence)]]
    [math
     ["[0]" random]
     [number
      ["[0]" nat]]]]]
  [\\library
   ["[0]" / {"+" [Hash]}
    [//
     [equivalence {"+" [Equivalence]}]]]])

(def: .public test
  Test
  (do random.monad
    [leftN random.nat
     rightN random.nat
     .let [hash (: (Equivalence (/.Hash Nat))
                   (implementation
                    (def: (= (^open "left\[0]") (^open "right\[0]"))
                      (and (bit\= (left\= (left\hash leftN) (left\hash leftN))
                                  (right\= (right\hash leftN) (right\hash leftN)))
                           (bit\= (left\= (left\hash rightN) (left\hash rightN))
                                  (right\= (right\hash rightN) (right\hash rightN)))
                           (bit\= (left\= (left\hash leftN) (left\hash rightN))
                                  (right\= (right\hash leftN) (right\hash rightN)))))))]]
    (<| (_.covering /._)
        ($_ _.and
            (_.for [/.functor]
                   ($contravariant.spec hash nat.hash /.functor))
            ))))