Proofs draw morphisms from A -> B so they remov...

# arrow-contributors

[raulraja]

Proofs draw morphisms from A -> B so they remove the need to explicitly extend or subtype other types in the hierarchy in order to provide ad-hoc behaviors over the values of these types.