{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Data.Eq.Type.Hetero
(
(:==)(..)
, refl
, trans
, symm
, coerce
, apply
, lift
, lift2, lift2'
, lift3, lift3'
, lower
, lower2
, lower3
, toHomogeneous
, fromHomogeneous
, fromLeibniz
, toLeibniz
, heteroFromLeibniz
, heteroToLeibniz
, reprLeibniz
) where
import Control.Category
import Data.Groupoid
import Data.Semigroupoid
import qualified Data.Type.Coercion as Co
import qualified Data.Type.Equality as Eq
import Data.Kind
import qualified Data.Eq.Type as ET
import Prelude hiding (id, (.))
infixl 4 :==
newtype (a :: j) :== (b :: k)
= HRefl { (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst :: forall (c :: forall i. i -> Type). c a -> c b }
type role (:==) nominal nominal
refl :: a :== a
refl :: a :== a
refl = (forall (c :: forall i. i -> *). c a -> c a) -> a :== a
forall j k (a :: j) (b :: k).
(forall (c :: forall i. i -> *). c a -> c b) -> a :== b
HRefl forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
forall (c :: forall i. i -> *). c a -> c a
id
data family Coerce :: forall k. k -> Type
newtype instance Coerce (a :: Type) = Coerce { Coerce a -> a
uncoerce :: a }
coerce :: a :== b -> a -> b
coerce :: (a :== b) -> a -> b
coerce a :== b
f = Coerce b -> b
forall a. Coerce a -> a
uncoerce (Coerce b -> b) -> (a -> Coerce b) -> a -> b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a :== b
f (Coerce a -> Coerce b) -> (a -> Coerce a) -> a -> Coerce b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> Coerce a
forall a. a -> Coerce a
Coerce
newtype Pair1 :: forall j1 k1 j2.
j1 -> k1 -> j2
-> forall k2. k2 -> Type where
Pair1 :: { Pair1 a1 b1 a2 b2 -> '(a1, a2) :== '(b1, b2)
unpair1 :: '(a1, a2) :== '(b1, b2) } -> Pair1 a1 b1 a2 b2
newtype Pair2 :: forall j2 k2 j1.
j2 -> k2 -> j1
-> forall k1. k1 -> Type where
Pair2 :: { Pair2 a2 b2 a1 b1 -> '(a1, a2) :== '(b1, b2)
unpair2 :: '(a1, a2) :== '(b1, b2) } -> Pair2 a2 b2 a1 b1
pair :: a1 :== b1 -> a2 :== b2 -> '(a1, a2) :== '(b1, b2)
pair :: (a1 :== b1) -> (a2 :== b2) -> '(a1, a2) :== '(b1, b2)
pair a1 :== b1
ab1 a2 :== b2
ab2 = Pair2 a2 b2 a1 b1 -> '(a1, a2) :== '(b1, b2)
forall j2 (a2 :: j2) k2 (b2 :: k2) j1 (a1 :: j1) k1 (b1 :: k1).
Pair2 a2 b2 a1 b1 -> '(a1, a2) :== '(b1, b2)
unpair2 (Pair2 a2 b2 a1 b1 -> '(a1, a2) :== '(b1, b2))
-> Pair2 a2 b2 a1 b1 -> '(a1, a2) :== '(b1, b2)
forall a b. (a -> b) -> a -> b
$ (a1 :== b1) -> forall (c :: forall i. i -> *). c a1 -> c b1
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a1 :== b1
ab1 (Pair2 a2 b2 a1 a1 -> Pair2 a2 b2 a1 b1)
-> Pair2 a2 b2 a1 a1 -> Pair2 a2 b2 a1 b1
forall a b. (a -> b) -> a -> b
$ ('(a1, a2) :== '(a1, b2)) -> Pair2 a2 b2 a1 a1
forall j1 j2 k1 k2 (a1 :: j1) (a2 :: j2) (b1 :: k1) (b2 :: k2).
('(a1, a2) :== '(b1, b2)) -> Pair2 a2 b2 a1 b1
Pair2 (('(a1, a2) :== '(a1, b2)) -> Pair2 a2 b2 a1 a1)
-> ('(a1, a2) :== '(a1, b2)) -> Pair2 a2 b2 a1 a1
forall a b. (a -> b) -> a -> b
$ Pair1 a1 a1 a2 b2 -> '(a1, a2) :== '(a1, b2)
forall j1 (a1 :: j1) k1 (b1 :: k1) j2 (a2 :: j2) k2 (b2 :: k2).
Pair1 a1 b1 a2 b2 -> '(a1, a2) :== '(b1, b2)
unpair1 (Pair1 a1 a1 a2 b2 -> '(a1, a2) :== '(a1, b2))
-> Pair1 a1 a1 a2 b2 -> '(a1, a2) :== '(a1, b2)
forall a b. (a -> b) -> a -> b
$ (a2 :== b2) -> forall (c :: forall i. i -> *). c a2 -> c b2
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a2 :== b2
ab2 (Pair1 a1 a1 a2 a2 -> Pair1 a1 a1 a2 b2)
-> Pair1 a1 a1 a2 a2 -> Pair1 a1 a1 a2 b2
forall a b. (a -> b) -> a -> b
$ ('(a1, a2) :== '(a1, a2)) -> Pair1 a1 a1 a2 a2
forall j1 j2 k1 k2 (a1 :: j1) (a2 :: j2) (b1 :: k1) (b2 :: k2).
('(a1, a2) :== '(b1, b2)) -> Pair1 a1 b1 a2 b2
Pair1 '(a1, a2) :== '(a1, a2)
forall k (a :: k). a :== a
refl
data family Apply :: forall j1 j2.
(j1 -> j2) -> j1
-> forall k. k -> Type
newtype instance Apply (f :: j1 -> j2) (a :: j1) '((g :: k1 -> k2), (b :: k1))
= Apply { Apply f a '(g, b) -> f a :== g b
unapply :: f a :== g b }
apply :: f :== g -> a :== b -> f a :== g b
apply :: (f :== g) -> (a :== b) -> f a :== g b
apply f :== g
fg a :== b
ab = Apply f a '(g, b) -> f a :== g b
forall j2 j1 (f :: j1 -> j2) (a :: j1) k2 k1 (g :: k1 -> k2)
(b :: k1).
Apply f a '(g, b) -> f a :== g b
unapply (Apply f a '(g, b) -> f a :== g b)
-> Apply f a '(g, b) -> f a :== g b
forall a b. (a -> b) -> a -> b
$ ('(f, a) :== '(g, b))
-> forall (c :: forall i. i -> *). c '(f, a) -> c '(g, b)
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst ((f :== g) -> (a :== b) -> '(f, a) :== '(g, b)
forall k k k k (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k).
(a1 :== b1) -> (a2 :== b2) -> '(a1, a2) :== '(b1, b2)
pair f :== g
fg a :== b
ab) (Apply f a '(f, a) -> Apply f a '(g, b))
-> Apply f a '(f, a) -> Apply f a '(g, b)
forall a b. (a -> b) -> a -> b
$ (f a :== f a) -> Apply f a '(f, a)
forall j1 j2 k1 k2 (f :: j1 -> j2) (a :: j1) (g :: k1 -> k2)
(b :: k1).
(f a :== g b) -> Apply f a '(g, b)
Apply f a :== f a
forall k (a :: k). a :== a
refl
newtype Push :: (forall j k. j -> k -> Type)
-> forall j. j -> forall k. k -> Type where
Push :: forall (p :: forall j k. j -> k -> Type)
j k (a :: j) (b :: k).
{ Push p a b -> p a b
unpush :: p a b } -> Push p a b
comp :: b :== c -> a :== b -> a :== c
comp :: (b :== c) -> (a :== b) -> a :== c
comp b :== c
f = Push (:==) a c -> a :== c
forall (p :: forall j k. j -> k -> *) j (a :: j) k (b :: k).
Push p a b -> p a b
unpush (Push (:==) a c -> a :== c)
-> ((a :== b) -> Push (:==) a c) -> (a :== b) -> a :== c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (b :== c) -> forall (c :: forall i. i -> *). c b -> c c
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst b :== c
f (Push (:==) a b -> Push (:==) a c)
-> ((a :== b) -> Push (:==) a b) -> (a :== b) -> Push (:==) a c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a :== b) -> Push (:==) a b
forall (p :: forall j k. j -> k -> *) j k (a :: j) (b :: k).
p a b -> Push p a b
Push
instance Category (:==) where
id :: a :== a
id = a :== a
forall k (a :: k). a :== a
refl
. :: (b :== c) -> (a :== b) -> a :== c
(.) = (b :== c) -> (a :== b) -> a :== c
forall k k j (b :: k) (c :: k) (a :: j).
(b :== c) -> (a :== b) -> a :== c
comp
instance Semigroupoid (:==) where
o :: (j :== k1) -> (i :== j) -> i :== k1
o = (j :== k1) -> (i :== j) -> i :== k1
forall k k j (b :: k) (c :: k) (a :: j).
(b :== c) -> (a :== b) -> a :== c
comp
instance Groupoid (:==) where
inv :: (a :== b) -> b :== a
inv = (a :== b) -> b :== a
forall k j (a :: k) (b :: j). (a :== b) -> b :== a
symm
trans :: a :== b -> b :== c -> a :== c
trans :: (a :== b) -> (b :== c) -> a :== c
trans = ((b :== c) -> (a :== b) -> a :== c)
-> (a :== b) -> (b :== c) -> a :== c
forall a b c. (a -> b -> c) -> b -> a -> c
flip (b :== c) -> (a :== b) -> a :== c
forall k k j (b :: k) (c :: k) (a :: j).
(b :== c) -> (a :== b) -> a :== c
comp
newtype Symm :: (forall j. j -> forall k. k -> Type)
-> forall j. j -> forall k. k -> Type where
Symm :: forall (p :: forall j. j -> forall k. k -> Type)
j k (a :: j) (b :: k).
{ Symm p a b -> p b a
unsymm :: p b a } -> Symm p a b
symm :: a :== b -> b :== a
symm :: (a :== b) -> b :== a
symm a :== b
ab = Push (:==) b a -> b :== a
forall (p :: forall j k. j -> k -> *) j (a :: j) k (b :: k).
Push p a b -> p a b
unpush (Push (:==) b a -> b :== a) -> Push (:==) b a -> b :== a
forall a b. (a -> b) -> a -> b
$ Symm (Push (:==)) a b -> Push (:==) b a
forall (p :: forall j. j -> forall i. i -> *) j (a :: j) k
(b :: k).
Symm p a b -> p b a
unsymm (Symm (Push (:==)) a b -> Push (:==) b a)
-> Symm (Push (:==)) a b -> Push (:==) b a
forall a b. (a -> b) -> a -> b
$ (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a :== b
ab (Symm (Push (:==)) a a -> Symm (Push (:==)) a b)
-> Symm (Push (:==)) a a -> Symm (Push (:==)) a b
forall a b. (a -> b) -> a -> b
$ Push (:==) a a -> Symm (Push (:==)) a a
forall (p :: forall j. j -> forall i. i -> *) j k (a :: j)
(b :: k).
p b a -> Symm p a b
Symm (Push (:==) a a -> Symm (Push (:==)) a a)
-> Push (:==) a a -> Symm (Push (:==)) a a
forall a b. (a -> b) -> a -> b
$ (a :== a) -> Push (:==) a a
forall (p :: forall j k. j -> k -> *) j k (a :: j) (b :: k).
p a b -> Push p a b
Push a :== a
forall k (a :: k). a :== a
refl
data family Lift :: forall j r. (j -> r) -> j
-> forall k. k
-> Type
newtype instance Lift f (a :: j) (b :: j) =
Lift { Lift f a b -> f a :== f b
unlift :: f a :== f b }
lift :: a :== b -> f a :== f b
lift :: (a :== b) -> f a :== f b
lift a :== b
f = Lift f a b -> f a :== f b
forall k j (f :: j -> k) (a :: j) (b :: j).
Lift f a b -> f a :== f b
unlift (Lift f a b -> f a :== f b) -> Lift f a b -> f a :== f b
forall a b. (a -> b) -> a -> b
$ (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a :== b
f (Lift f a a -> Lift f a b) -> Lift f a a -> Lift f a b
forall a b. (a -> b) -> a -> b
$ (f a :== f a) -> Lift f a a
forall j k (f :: j -> k) (a :: j) (b :: j).
(f a :== f b) -> Lift f a b
Lift f a :== f a
forall k (a :: k). a :== a
refl
data family Lift2 :: forall j1 j2 r.
(j1 -> j2 -> r) -> j1 -> j2
-> forall k. k
-> Type
newtype instance Lift2 f (a :: j1) (c :: j2) (b :: j1) =
Lift2 { Lift2 f a c b -> f a c :== f b c
unlift2 :: f a c :== f b c }
lift2 :: a :== b -> f a c :== f b c
lift2 :: (a :== b) -> f a c :== f b c
lift2 a :== b
f = Lift2 f a c b -> f a c :== f b c
forall k j2 j1 (f :: j1 -> j2 -> k) (a :: j1) (c :: j2) (b :: j1).
Lift2 f a c b -> f a c :== f b c
unlift2 (Lift2 f a c b -> f a c :== f b c)
-> Lift2 f a c b -> f a c :== f b c
forall a b. (a -> b) -> a -> b
$ (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a :== b
f (Lift2 f a c a -> Lift2 f a c b) -> Lift2 f a c a -> Lift2 f a c b
forall a b. (a -> b) -> a -> b
$ (f a c :== f a c) -> Lift2 f a c a
forall j1 j2 k (f :: j1 -> j2 -> k) (a :: j1) (c :: j2) (b :: j1).
(f a c :== f b c) -> Lift2 f a c b
Lift2 f a c :== f a c
forall k (a :: k). a :== a
refl
lift2' :: a :== b -> c :== d -> f a c :== f b d
lift2' :: (a :== b) -> (c :== d) -> f a c :== f b d
lift2' a :== b
ab c :== d
cd = Push (:==) (f a c) (f b d) -> f a c :== f b d
forall (p :: forall j k. j -> k -> *) j (a :: j) k (b :: k).
Push p a b -> p a b
unpush (Push (:==) (f a c) (f b d) -> f a c :== f b d)
-> Push (:==) (f a c) (f b d) -> f a c :== f b d
forall a b. (a -> b) -> a -> b
$ (a :== b) -> f a d :== f b d
forall k k k (a :: k) (b :: k) (f :: k -> k -> k) (c :: k).
(a :== b) -> f a c :== f b c
lift2 a :== b
ab (f a d :== f b d)
-> Push (:==) (f a c) (f a d) -> Push (:==) (f a c) (f b d)
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
`hsubst` (f a c :== f a d) -> Push (:==) (f a c) (f a d)
forall (p :: forall j k. j -> k -> *) j k (a :: j) (b :: k).
p a b -> Push p a b
Push ((c :== d) -> f a c :== f a d
forall k k (a :: k) (b :: k) (f :: k -> k).
(a :== b) -> f a :== f b
lift c :== d
cd)
data family Lift3 :: forall j1 j2 j3 r.
(j1 -> j2 -> j3 -> r) -> j1 -> j2 -> j3
-> forall k. k
-> Type
newtype instance Lift3 f (a :: j1) (c :: j2) (d :: j3) (b :: j1) =
Lift3 { Lift3 f a c d b -> f a c d :== f b c d
unlift3 :: f a c d :== f b c d }
lift3 :: a :== b -> f a c d :== f b c d
lift3 :: (a :== b) -> f a c d :== f b c d
lift3 a :== b
f = Lift3 f a c d b -> f a c d :== f b c d
forall k j2 j3 j1 (f :: j1 -> j2 -> j3 -> k) (a :: j1) (c :: j2)
(d :: j3) (b :: j1).
Lift3 f a c d b -> f a c d :== f b c d
unlift3 (Lift3 f a c d b -> f a c d :== f b c d)
-> Lift3 f a c d b -> f a c d :== f b c d
forall a b. (a -> b) -> a -> b
$ (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a :== b
f (Lift3 f a c d a -> Lift3 f a c d b)
-> Lift3 f a c d a -> Lift3 f a c d b
forall a b. (a -> b) -> a -> b
$ (f a c d :== f a c d) -> Lift3 f a c d a
forall j1 j2 j3 k (f :: j1 -> j2 -> j3 -> k) (a :: j1) (c :: j2)
(d :: j3) (b :: j1).
(f a c d :== f b c d) -> Lift3 f a c d b
Lift3 f a c d :== f a c d
forall k (a :: k). a :== a
refl
lift3' :: a :== b -> c :== d -> e :== f -> g a c e :== g b d f
lift3' :: (a :== b) -> (c :== d) -> (e :== f) -> g a c e :== g b d f
lift3' a :== b
ab c :== d
cd e :== f
ef = Push (:==) (g a c e) (g b d f) -> g a c e :== g b d f
forall (p :: forall j k. j -> k -> *) j (a :: j) k (b :: k).
Push p a b -> p a b
unpush (Push (:==) (g a c e) (g b d f) -> g a c e :== g b d f)
-> Push (:==) (g a c e) (g b d f) -> g a c e :== g b d f
forall a b. (a -> b) -> a -> b
$ Push (:==) (g a c f) (g b d f) -> g a c f :== g b d f
forall (p :: forall j k. j -> k -> *) j (a :: j) k (b :: k).
Push p a b -> p a b
unpush ((a :== b) -> g a d f :== g b d f
forall k k k k (a :: k) (b :: k) (f :: k -> k -> k -> k) (c :: k)
(d :: k).
(a :== b) -> f a c d :== f b c d
lift3 a :== b
ab (g a d f :== g b d f)
-> Push (:==) (g a c f) (g a d f) -> Push (:==) (g a c f) (g b d f)
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
`hsubst` (g a c f :== g a d f) -> Push (:==) (g a c f) (g a d f)
forall (p :: forall j k. j -> k -> *) j k (a :: j) (b :: k).
p a b -> Push p a b
Push ((c :== d) -> g a c f :== g a d f
forall k k k (a :: k) (b :: k) (f :: k -> k -> k) (c :: k).
(a :== b) -> f a c :== f b c
lift2 c :== d
cd)) (g a c f :== g b d f)
-> Push (:==) (g a c e) (g a c f) -> Push (:==) (g a c e) (g b d f)
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
`hsubst` (g a c e :== g a c f) -> Push (:==) (g a c e) (g a c f)
forall (p :: forall j k. j -> k -> *) j k (a :: j) (b :: k).
p a b -> Push p a b
Push ((e :== f) -> g a c e :== g a c f
forall k k (a :: k) (b :: k) (f :: k -> k).
(a :== b) -> f a :== f b
lift e :== f
ef)
data family Lower :: forall j. j
-> forall k. k
-> Type
newtype instance Lower a (f x) = Lower { Lower a (f x) -> a :== x
unlower :: a :== x }
lower :: forall a b f g. f a :== g b -> a :== b
lower :: (f a :== g b) -> a :== b
lower f a :== g b
f = Lower a (g b) -> a :== b
forall j (a :: j) k k (f :: k -> k) (x :: k).
Lower a (f x) -> a :== x
unlower (Lower a (g b) -> a :== b) -> Lower a (g b) -> a :== b
forall a b. (a -> b) -> a -> b
$ (f a :== g b) -> Lower a (f a) -> Lower a (g b)
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst f a :== g b
f ((a :== a) -> Lower a (f a)
forall j k k (a :: j) (f :: k -> k) (x :: k).
(a :== x) -> Lower a (f x)
Lower a :== a
forall k (a :: k). a :== a
refl :: Lower a (f a))
data family Lower2 :: forall j. j
-> forall k. k
-> Type
newtype instance Lower2 a (f x c) = Lower2 { Lower2 a (f x c) -> a :== x
unlower2 :: a :== x }
lower2 :: forall a b f g c c'. f a c :== g b c' -> a :== b
lower2 :: (f a c :== g b c') -> a :== b
lower2 f a c :== g b c'
f = Lower2 a (g b c') -> a :== b
forall j (a :: j) k k k (f :: k -> k -> k) (x :: k) (c :: k).
Lower2 a (f x c) -> a :== x
unlower2 (Lower2 a (g b c') -> a :== b) -> Lower2 a (g b c') -> a :== b
forall a b. (a -> b) -> a -> b
$ (f a c :== g b c') -> Lower2 a (f a c) -> Lower2 a (g b c')
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst f a c :== g b c'
f ((a :== a) -> Lower2 a (f a c)
forall j k k k (a :: j) (f :: k -> k -> k) (x :: k) (c :: k).
(a :== x) -> Lower2 a (f x c)
Lower2 a :== a
forall k (a :: k). a :== a
refl :: Lower2 a (f a c))
data family Lower3 :: forall j. j
-> forall k. k
-> Type
newtype instance Lower3 a (f x c d) = Lower3 { Lower3 a (f x c d) -> a :== x
unlower3 :: a :== x }
lower3 :: forall a b f g c c' d d'. f a c d :== g b c' d' -> a :== b
lower3 :: (f a c d :== g b c' d') -> a :== b
lower3 f a c d :== g b c' d'
f = Lower3 a (g b c' d') -> a :== b
forall j (a :: j) k k k k (f :: k -> k -> k -> k) (x :: k) (c :: k)
(d :: k).
Lower3 a (f x c d) -> a :== x
unlower3 (Lower3 a (g b c' d') -> a :== b)
-> Lower3 a (g b c' d') -> a :== b
forall a b. (a -> b) -> a -> b
$ (f a c d :== g b c' d')
-> Lower3 a (f a c d) -> Lower3 a (g b c' d')
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst f a c d :== g b c' d'
f ((a :== a) -> Lower3 a (f a c d)
forall j k k k k (a :: j) (f :: k -> k -> k -> k) (x :: k) (c :: k)
(d :: k).
(a :== x) -> Lower3 a (f x c d)
Lower3 a :== a
forall k (a :: k). a :== a
refl :: Lower3 a (f a c d))
data family Flay :: forall j.
(j -> j -> Type) -> j
-> forall k. k
-> Type
newtype instance Flay p (a :: j) (b :: j) = Flay { Flay p a b -> p a b
unflay :: p a b }
toHomogeneous :: a :== b -> a ET.:= b
toHomogeneous :: (a :== b) -> a := b
toHomogeneous a :== b
f = Flay (:=) a b -> a := b
forall j (p :: j -> j -> *) (a :: j) (b :: j). Flay p a b -> p a b
unflay (Flay (:=) a b -> a := b) -> Flay (:=) a b -> a := b
forall a b. (a -> b) -> a -> b
$ (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a :== b
f (Flay (:=) a a -> Flay (:=) a b) -> Flay (:=) a a -> Flay (:=) a b
forall a b. (a -> b) -> a -> b
$ (a := a) -> Flay (:=) a a
forall j (p :: j -> j -> *) (a :: j) (b :: j). p a b -> Flay p a b
Flay a := a
forall k (a :: k). a := a
ET.refl
fromHomogeneous :: a ET.:= b -> a :== b
fromHomogeneous :: (a := b) -> a :== b
fromHomogeneous a := b
f = (a := b) -> (a :== a) -> a :== b
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
ET.subst a := b
f a :== a
forall k (a :: k). a :== a
refl
fromLeibniz :: forall a b. a :== b -> a Eq.:~: b
fromLeibniz :: (a :== b) -> a :~: b
fromLeibniz a :== b
f = Flay (:~:) a b -> a :~: b
forall j (p :: j -> j -> *) (a :: j) (b :: j). Flay p a b -> p a b
unflay (Flay (:~:) a b -> a :~: b) -> Flay (:~:) a b -> a :~: b
forall a b. (a -> b) -> a -> b
$ (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a :== b
f (Flay (:~:) a a -> Flay (:~:) a b)
-> Flay (:~:) a a -> Flay (:~:) a b
forall a b. (a -> b) -> a -> b
$ (a :~: a) -> Flay (:~:) a a
forall j (p :: j -> j -> *) (a :: j) (b :: j). p a b -> Flay p a b
Flay a :~: a
forall k (a :: k). a :~: a
Eq.Refl
toLeibniz :: a Eq.:~: b -> a :== b
toLeibniz :: (a :~: b) -> a :== b
toLeibniz a :~: b
Eq.Refl = a :== b
forall k (a :: k). a :== a
refl
heteroFromLeibniz :: a :== b -> a Eq.:~~: b
heteroFromLeibniz :: (a :== b) -> a :~~: b
heteroFromLeibniz a :== b
f = Push (:~~:) a b -> a :~~: b
forall (p :: forall j k. j -> k -> *) j (a :: j) k (b :: k).
Push p a b -> p a b
unpush (Push (:~~:) a b -> a :~~: b) -> Push (:~~:) a b -> a :~~: b
forall a b. (a -> b) -> a -> b
$ (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a :== b
f (Push (:~~:) a a -> Push (:~~:) a b)
-> Push (:~~:) a a -> Push (:~~:) a b
forall a b. (a -> b) -> a -> b
$ (a :~~: a) -> Push (:~~:) a a
forall (p :: forall j k. j -> k -> *) j k (a :: j) (b :: k).
p a b -> Push p a b
Push a :~~: a
forall k1 (a :: k1). a :~~: a
Eq.HRefl
heteroToLeibniz :: a Eq.:~~: b -> a :== b
heteroToLeibniz :: (a :~~: b) -> a :== b
heteroToLeibniz a :~~: b
Eq.HRefl = a :== b
forall k (a :: k). a :== a
refl
instance Eq.TestEquality ((:==) a) where
testEquality :: (a :== a) -> (a :== b) -> Maybe (a :~: b)
testEquality a :== a
fa a :== b
fb = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just ((a :== b) -> a :~: b
forall k (a :: k) (b :: k). (a :== b) -> a :~: b
fromLeibniz ((a :== a) -> (a :== b) -> a :== b
forall j j k (a :: j) (b :: j) (c :: k).
(a :== b) -> (b :== c) -> a :== c
trans ((a :== a) -> a :== a
forall k j (a :: k) (b :: j). (a :== b) -> b :== a
symm a :== a
fa) a :== b
fb))
reprLeibniz :: a :== b -> Co.Coercion a b
reprLeibniz :: (a :== b) -> Coercion a b
reprLeibniz a :== b
f = Flay Coercion a b -> Coercion a b
forall j (p :: j -> j -> *) (a :: j) (b :: j). Flay p a b -> p a b
unflay (Flay Coercion a b -> Coercion a b)
-> Flay Coercion a b -> Coercion a b
forall a b. (a -> b) -> a -> b
$ (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a :== b
f (Flay Coercion a a -> Flay Coercion a b)
-> Flay Coercion a a -> Flay Coercion a b
forall a b. (a -> b) -> a -> b
$ Coercion a a -> Flay Coercion a a
forall j (p :: j -> j -> *) (a :: j) (b :: j). p a b -> Flay p a b
Flay Coercion a a
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Co.Coercion
instance Co.TestCoercion ((:==) a) where
testCoercion :: (a :== a) -> (a :== b) -> Maybe (Coercion a b)
testCoercion a :== a
fa a :== b
fb = Coercion a b -> Maybe (Coercion a b)
forall a. a -> Maybe a
Just ((a :== b) -> Coercion a b
forall k (a :: k) (b :: k). (a :== b) -> Coercion a b
reprLeibniz ((a :== a) -> (a :== b) -> a :== b
forall j j k (a :: j) (b :: j) (c :: k).
(a :== b) -> (b :== c) -> a :== c
trans ((a :== a) -> a :== a
forall k j (a :: k) (b :: j). (a :== b) -> b :== a
symm a :== a
fa) a :== b
fb))