Joined February 2012
·

Brian Zeligson

Boston, MA
·
·

Posted to Some category theory 10 months ago

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

Posted to Limit and Colimit abstractly 10 months ago

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

Posted to Limit and Colimit abstractly 10 months ago

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.

Achievements
177 Karma
1,333 Total ProTip Views