Brian Zeligson

Last bit is not true. Only works with Reader because of exponentiation (currying) and uniqueness of limits (commutativity of product in Set)

where summary of a diagram is an object for which anything in the diagram is a property, and property of a diagram is an observation that can be made from any object within the diagram, by any pathway through the diagram

Pullback is limit of a coproduct, pushout is colimit of a product

also are free constructions iff initial objects?

Concretely, for some function under test f :: a -> b, a set of properties can be defined by p :: (a -> c, b -> c) when fst p == (snd p) . f.

Interestingly, given an additional g :: a -> x, h :: b -> y, i :: c -> x -> a, and j :: c -> y -> b such that (\a -> i ((fst p) a) (g a)) == id and (\b -> j ((snd p) b) (h b)) == id then i and j effectively capture the data loss from a -> c and b -> c. You know exactly what is and is not covered by your defined properties, and can surgically tune what is included and left out at balance with how close you are to re-implementing the code under test in order to preserve as much resolution as possible.

Basically your function is input -> output, your properties are input <- output. Properties are in essence dual to what they describe.