module Data.Type.Witness.Apply where import Import applyRefl :: forall k1 k2 (fa :: k1 -> k2) (fb :: k1 -> k2) (a :: k1) (b :: k1). fa :~: fb -> a :~: b -> (fa a) :~: (fb b) applyRefl :: forall k1 k2 (fa :: k1 -> k2) (fb :: k1 -> k2) (a :: k1) (b :: k1). (fa :~: fb) -> (a :~: b) -> fa a :~: fb b applyRefl fa :~: fb Refl a :~: b Refl = forall {k} (a :: k). a :~: a Refl withRefl :: forall k (a :: k) (b :: k) (r :: Type). a :~: b -> (a ~ b => r) -> r withRefl :: forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r withRefl a :~: b Refl (a ~ b) => r r = (a ~ b) => r r reflId :: forall k (cat :: k -> k -> Type) (a :: k) (b :: k). Category cat => a :~: b -> cat a b reflId :: forall k (cat :: k -> k -> Type) (a :: k) (b :: k). Category cat => (a :~: b) -> cat a b reflId a :~: b Refl = forall {k} (cat :: k -> k -> Type) (a :: k). Category cat => cat a a id reflId1 :: forall kq (cat :: kq -> kq -> Type) kp (w :: kp -> kq) (a :: kp) (b :: kp). Category cat => a :~: b -> cat (w a) (w b) reflId1 :: forall kq (cat :: kq -> kq -> Type) kp (w :: kp -> kq) (a :: kp) (b :: kp). Category cat => (a :~: b) -> cat (w a) (w b) reflId1 a :~: b Refl = forall {k} (cat :: k -> k -> Type) (a :: k). Category cat => cat a a id