úÎ! ºè2      !"#$%&'()*+,-./01(C) 2011-2014 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisional5rank2 types, type operators, (optional) type familiesNone &'-HISUVX eqmLeibnizian equality states that two things are equal if you can substitute one for the other in all contextseqEquality is reflexiveeq8If two things are equal you can convert one to the othereqEquality is transitiveeqEquality is symmetriceq/You can lift equality into any type constructoreq... in any position eq\Type constructors are injective, so you can lower equality through any type constructor ... eq... in any position ...eq8... these definitions are poly-kinded on GHC 7.6 and up.eqEquality forms a category  4+(C) 2011-2014 Edward Kmett, 2018 Ryan Scott BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisionalGHCNone &'-.HISUVX! eq"Heterogeneous Leibnizian equality.nLeibnizian equality states that two things are equal if you can substitute one for the other in all contexts.eqEquality is reflexive.eq:If two things are equal, you can convert one to the other.2eqEquality is compositional.eqEquality is transitive.eqEquality is symmetric.eq2You can lift equality into any type constructor...eq... in any position.#eqXType constructors are injective, so you can lower equality through any type constructor.&eqtConvert an appropriately kinded heterogeneous Leibnizian equality into a homogeneous Leibnizian equality '(ET.:=)'.'eqqConvert a homogeneous Leibnizian equality '(ET.:=)' to an appropriately kinded heterogeneous Leibizian equality.1eqEquality forms a category. !"#$%&'()*+, !"#$%&'()*+,43           !"#$%&'eq-4.2.1-9Tv08kPt2Jx7eRyZfkeIMX Data.Eq.TypeData.Eq.Type.Hetero:=Reflsubstreflcoercetranssymmliftlift2lift2'lift3lift3'lowerlower2lower3 fromLeibniz toLeibniz reprLeibniz$fTestCoercionk:=$fTestEqualityk:= $fGroupoidk:=$fSemigroupoidk:= $fCategoryk:=:==HReflhsubst toHomogeneousfromHomogeneousheteroFromLeibnizheteroToLeibniz$fTestCoercionk:==$fTestEqualityk:==$fGroupoidk:==$fSemigroupoidk:==$fCategoryk:==comp