{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data.Type.Universe.Subset (
Subset,
WitSubset (..),
makeSubset,
intersection,
union,
symDiff,
mergeSubset,
imergeSubset,
mapSubset,
imapSubset,
subsetToList,
subsetToAny,
subsetToAll,
subsetToNone,
emptySubset,
fullSubset,
) where
import Control.Applicative
import Data.Kind
import Data.Monoid (Alt (..))
import Data.Singletons
import Data.Singletons.Decide
import Data.Type.Functor.Product
import Data.Type.Predicate
import Data.Type.Predicate.Logic
import Data.Type.Predicate.Quantification
import Data.Type.Universe
newtype WitSubset f p (as :: f k) = WitSubset
{ forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitSubset f p as
-> forall (a :: k). Elem f as a -> Decision (p @@ a)
runWitSubset :: forall a. Elem f as a -> Decision (p @@ a)
}
data Subset f :: (k ~> Type) -> (f k ~> Type)
type instance Apply (Subset f p) as = WitSubset f p as
instance (Universe f, Decidable p) => Decidable (Subset f p)
instance (Universe f, Decidable p) => Provable (Subset f p) where
prove :: Prove (Subset f p)
prove = forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Subset f p @@ as
makeSubset @f @_ @p (\Elem f a a
_ -> forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k ~> *). Decidable p => Decide p
decide @p)
makeSubset ::
forall f k p (as :: f k).
Universe f =>
(forall a. Elem f as a -> Sing a -> Decision (p @@ a)) ->
Sing as ->
Subset f p @@ as
makeSubset :: forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Subset f p @@ as
makeSubset forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a)
f Sing as
xs = (forall (a :: k). Elem f as a -> Decision (p @@ a))
-> WitSubset f p as
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> Decision (p @@ a))
-> WitSubset f p as
WitSubset ((forall (a :: k). Elem f as a -> Decision (p @@ a))
-> WitSubset f p as)
-> (forall (a :: k). Elem f as a -> Decision (p @@ a))
-> WitSubset f p as
forall a b. (a -> b) -> a -> b
$ \Elem f as a
i -> Elem f as a -> Sing a -> Decision (p @@ a)
forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a)
f Elem f as a
i (Elem f as a -> Sing as -> Sing a
forall {k} (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f as a
i Sing as
xs)
subsetToList ::
forall f p t.
(Universe f, Alternative t) =>
(Subset f p --># Any f p) t
subsetToList :: forall {k} (f :: * -> *) (p :: k ~> *) (t :: * -> *).
(Universe f, Alternative t) =>
(-->#) (Subset f p) (Any f p) t
subsetToList Sing a
xs Subset f p @@ a
s = Alt t (Any f p @@ a) -> t (Any f p @@ a)
forall {k} (f :: k -> *) (a :: k). Alt f a -> f a
getAlt (Alt t (Any f p @@ a) -> t (Any f p @@ a))
-> Alt t (Any f p @@ a) -> t (Any f p @@ a)
forall a b. (a -> b) -> a -> b
$ ((forall (a :: k). Elem f a a -> Sing a -> Alt t (Any f p @@ a))
-> Sing a -> Alt t (Any f p @@ a)
forall (f :: * -> *) k (as :: f k) m.
(FProd f, Monoid m) =>
(forall (a :: k). Elem f as a -> Sing a -> m) -> Sing as -> m
`ifoldMapSing` Sing a
xs) ((forall (a :: k). Elem f a a -> Sing a -> Alt t (Any f p @@ a))
-> Alt t (Any f p @@ a))
-> (forall (a :: k). Elem f a a -> Sing a -> Alt t (Any f p @@ a))
-> Alt t (Any f p @@ a)
forall a b. (a -> b) -> a -> b
$ \Elem f a a
i Sing a
_ -> t (Any f p @@ a) -> Alt t (Any f p @@ a)
forall {k} (f :: k -> *) (a :: k). f a -> Alt f a
Alt (t (Any f p @@ a) -> Alt t (Any f p @@ a))
-> t (Any f p @@ a) -> Alt t (Any f p @@ a)
forall a b. (a -> b) -> a -> b
$ case WitSubset f p a -> forall (a :: k). Elem f a a -> Decision (p @@ a)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitSubset f p as
-> forall (a :: k). Elem f as a -> Decision (p @@ a)
runWitSubset Subset f p @@ a
WitSubset f p a
s Elem f a a
i of
Proved p @@ a
p -> (Any f p @@ a) -> t (Any f p @@ a)
forall a. a -> t a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Any f p @@ a) -> t (Any f p @@ a))
-> (Any f p @@ a) -> t (Any f p @@ a)
forall a b. (a -> b) -> a -> b
$ Elem f a a -> (p @@ a) -> WitAny f p a
forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny Elem f a a
i p @@ a
p
Disproved Refuted (p @@ a)
_ -> t (Any f p @@ a)
t (WitAny f p a)
forall a. t a
forall (f :: * -> *) a. Alternative f => f a
empty
subsetToAny ::
forall f p.
Universe f =>
Subset f p -?> Any f p
subsetToAny :: forall {k} (f :: * -> *) (p :: k ~> *).
Universe f =>
Subset f p -?> Any f p
subsetToAny Sing a
xs Subset f p @@ a
s = (forall (a :: k). Elem f a a -> Sing a -> Decision (p @@ a))
-> Sing a -> Decision (Apply (Any f p) a)
forall k (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any f p @@ as)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any f p @@ as)
idecideAny (\Elem f a a
i Sing a
_ -> WitSubset f p a -> forall (a :: k). Elem f a a -> Decision (p @@ a)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitSubset f p as
-> forall (a :: k). Elem f as a -> Decision (p @@ a)
runWitSubset Subset f p @@ a
WitSubset f p a
s Elem f a a
i) Sing a
xs
emptySubset :: forall f as. (Universe f, SingI as) => Subset f Impossible @@ as
emptySubset :: forall {k} (f :: * -> *) (as :: f k).
(Universe f, SingI as) =>
Subset f Impossible @@ as
emptySubset = forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: f k ~> *). Provable p => Prove p
prove @(Subset f Impossible) Sing as
forall {k} (a :: k). SingI a => Sing a
sing
fullSubset :: forall f as. (Universe f, SingI as) => Subset f Evident @@ as
fullSubset :: forall {k} (f :: * -> *) (as :: f k).
(Universe f, SingI as) =>
Subset f Evident @@ as
fullSubset = forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: f k ~> *). Provable p => Prove p
prove @(Subset f Evident) Sing as
forall {k} (a :: k). SingI a => Sing a
sing
subsetToNone :: forall f p. Universe f => Subset f p -?> None f p
subsetToNone :: forall {k} (f :: * -> *) (p :: k ~> *).
Universe f =>
Subset f p -?> None f p
subsetToNone Sing a
xs Subset f p @@ a
s = (forall (a :: k). Elem f a a -> Sing a -> Decision (p @@ a))
-> Sing a -> Decision (Apply (Not (Any f p)) a)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (None f p @@ as)
idecideNone (\Elem f a a
i Sing a
_ -> WitSubset f p a -> forall (a :: k). Elem f a a -> Decision (p @@ a)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitSubset f p as
-> forall (a :: k). Elem f as a -> Decision (p @@ a)
runWitSubset Subset f p @@ a
WitSubset f p a
s Elem f a a
i) Sing a
xs
imergeSubset ::
forall f k p q r (as :: f k).
() =>
(forall a. Elem f as a -> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)) ->
Subset f p @@ as ->
Subset f q @@ as ->
Subset f r @@ as
imergeSubset :: forall (f :: * -> *) k (p :: k ~> *) (q :: k ~> *) (r :: k ~> *)
(as :: f k).
(forall (a :: k).
Elem f as a
-> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
-> (Subset f p @@ as) -> (Subset f q @@ as) -> Subset f r @@ as
imergeSubset forall (a :: k).
Elem f as a
-> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)
f Subset f p @@ as
ps Subset f q @@ as
qs = (forall (a :: k). Elem f as a -> Decision (r @@ a))
-> WitSubset f r as
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> Decision (p @@ a))
-> WitSubset f p as
WitSubset ((forall (a :: k). Elem f as a -> Decision (r @@ a))
-> WitSubset f r as)
-> (forall (a :: k). Elem f as a -> Decision (r @@ a))
-> WitSubset f r as
forall a b. (a -> b) -> a -> b
$ \Elem f as a
i ->
Elem f as a
-> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)
forall (a :: k).
Elem f as a
-> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)
f Elem f as a
i (WitSubset f p as
-> forall (a :: k). Elem f as a -> Decision (p @@ a)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitSubset f p as
-> forall (a :: k). Elem f as a -> Decision (p @@ a)
runWitSubset Subset f p @@ as
WitSubset f p as
ps Elem f as a
i) (WitSubset f q as
-> forall (a :: k). Elem f as a -> Decision (q @@ a)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitSubset f p as
-> forall (a :: k). Elem f as a -> Decision (p @@ a)
runWitSubset Subset f q @@ as
WitSubset f q as
qs Elem f as a
i)
mergeSubset ::
forall f k p q r (as :: f k).
() =>
(forall a. Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)) ->
Subset f p @@ as ->
Subset f q @@ as ->
Subset f r @@ as
mergeSubset :: forall (f :: * -> *) k (p :: k ~> *) (q :: k ~> *) (r :: k ~> *)
(as :: f k).
(forall (a :: k).
Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
-> (Subset f p @@ as) -> (Subset f q @@ as) -> Subset f r @@ as
mergeSubset forall (a :: k).
Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)
f = (forall (a :: k).
Elem f as a
-> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
-> Apply (Subset f p) as
-> Apply (Subset f q) as
-> Apply (Subset f r) as
forall (f :: * -> *) k (p :: k ~> *) (q :: k ~> *) (r :: k ~> *)
(as :: f k).
(forall (a :: k).
Elem f as a
-> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
-> (Subset f p @@ as) -> (Subset f q @@ as) -> Subset f r @@ as
imergeSubset (\(Elem f as a
_ :: Elem f as a) Decision (p @@ a)
p -> forall (a :: k).
Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)
f @a Decision (p @@ a)
p)
intersection ::
forall f p q.
() =>
((Subset f p &&& Subset f q) --> Subset f (p &&& q))
intersection :: forall {k} (f :: * -> *) (p :: k ~> *) (q :: k ~> *) (a :: f k).
Sing a
-> ((Subset f p &&& Subset f q) @@ a) -> Subset f (p &&& q) @@ a
intersection Sing a
_ = (WitSubset f p a
-> WitSubset f q a -> Apply (Subset f (p &&& q)) a)
-> (WitSubset f p a, WitSubset f q a)
-> Apply (Subset f (p &&& q)) a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((WitSubset f p a
-> WitSubset f q a -> Apply (Subset f (p &&& q)) a)
-> (WitSubset f p a, WitSubset f q a)
-> Apply (Subset f (p &&& q)) a)
-> (WitSubset f p a
-> WitSubset f q a -> Apply (Subset f (p &&& q)) a)
-> (WitSubset f p a, WitSubset f q a)
-> Apply (Subset f (p &&& q)) a
forall a b. (a -> b) -> a -> b
$ (forall (a :: k).
Elem f a a
-> Decision (p @@ a)
-> Decision (q @@ a)
-> Decision ((p &&& q) @@ a))
-> (Subset f p @@ a)
-> (Subset f q @@ a)
-> Apply (Subset f (p &&& q)) a
forall (f :: * -> *) k (p :: k ~> *) (q :: k ~> *) (r :: k ~> *)
(as :: f k).
(forall (a :: k).
Elem f as a
-> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
-> (Subset f p @@ as) -> (Subset f q @@ as) -> Subset f r @@ as
imergeSubset ((forall (a :: k).
Elem f a a
-> Decision (p @@ a)
-> Decision (q @@ a)
-> Decision ((p &&& q) @@ a))
-> (Subset f p @@ a)
-> (Subset f q @@ a)
-> Apply (Subset f (p &&& q)) a)
-> (forall (a :: k).
Elem f a a
-> Decision (p @@ a)
-> Decision (q @@ a)
-> Decision ((p &&& q) @@ a))
-> (Subset f p @@ a)
-> (Subset f q @@ a)
-> Apply (Subset f (p &&& q)) a
forall a b. (a -> b) -> a -> b
$ \(Elem f a a
_ :: Elem f as a) -> forall {k1} (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p &&& q) @@ a)
forall (p :: k ~> *) (q :: k ~> *) (a :: k).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p &&& q) @@ a)
decideAnd @p @q @a
union ::
forall f p q.
() =>
((Subset f p &&& Subset f q) --> Subset f (p ||| q))
union :: forall {k} (f :: * -> *) (p :: k ~> *) (q :: k ~> *) (a :: f k).
Sing a
-> ((Subset f p &&& Subset f q) @@ a) -> Subset f (p ||| q) @@ a
union Sing a
_ = (WitSubset f p a
-> WitSubset f q a -> Apply (Subset f (p ||| q)) a)
-> (WitSubset f p a, WitSubset f q a)
-> Apply (Subset f (p ||| q)) a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((WitSubset f p a
-> WitSubset f q a -> Apply (Subset f (p ||| q)) a)
-> (WitSubset f p a, WitSubset f q a)
-> Apply (Subset f (p ||| q)) a)
-> (WitSubset f p a
-> WitSubset f q a -> Apply (Subset f (p ||| q)) a)
-> (WitSubset f p a, WitSubset f q a)
-> Apply (Subset f (p ||| q)) a
forall a b. (a -> b) -> a -> b
$ (forall (a :: k).
Elem f a a
-> Decision (p @@ a)
-> Decision (q @@ a)
-> Decision ((p ||| q) @@ a))
-> (Subset f p @@ a)
-> (Subset f q @@ a)
-> Apply (Subset f (p ||| q)) a
forall (f :: * -> *) k (p :: k ~> *) (q :: k ~> *) (r :: k ~> *)
(as :: f k).
(forall (a :: k).
Elem f as a
-> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
-> (Subset f p @@ as) -> (Subset f q @@ as) -> Subset f r @@ as
imergeSubset ((forall (a :: k).
Elem f a a
-> Decision (p @@ a)
-> Decision (q @@ a)
-> Decision ((p ||| q) @@ a))
-> (Subset f p @@ a)
-> (Subset f q @@ a)
-> Apply (Subset f (p ||| q)) a)
-> (forall (a :: k).
Elem f a a
-> Decision (p @@ a)
-> Decision (q @@ a)
-> Decision ((p ||| q) @@ a))
-> (Subset f p @@ a)
-> (Subset f q @@ a)
-> Apply (Subset f (p ||| q)) a
forall a b. (a -> b) -> a -> b
$ \(Elem f a a
_ :: Elem f as a) -> forall {k1} (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ||| q) @@ a)
forall (p :: k ~> *) (q :: k ~> *) (a :: k).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ||| q) @@ a)
decideOr @p @q @a
symDiff ::
forall f p q.
() =>
((Subset f p &&& Subset f q) --> Subset f (p ^^^ q))
symDiff :: forall {k} (f :: * -> *) (p :: k ~> *) (q :: k ~> *) (a :: f k).
Sing a
-> ((Subset f p &&& Subset f q) @@ a) -> Subset f (p ^^^ q) @@ a
symDiff Sing a
_ = (WitSubset f p a
-> WitSubset f q a -> Apply (Subset f (p ^^^ q)) a)
-> (WitSubset f p a, WitSubset f q a)
-> Apply (Subset f (p ^^^ q)) a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((WitSubset f p a
-> WitSubset f q a -> Apply (Subset f (p ^^^ q)) a)
-> (WitSubset f p a, WitSubset f q a)
-> Apply (Subset f (p ^^^ q)) a)
-> (WitSubset f p a
-> WitSubset f q a -> Apply (Subset f (p ^^^ q)) a)
-> (WitSubset f p a, WitSubset f q a)
-> Apply (Subset f (p ^^^ q)) a
forall a b. (a -> b) -> a -> b
$ (forall (a :: k).
Elem f a a
-> Decision (p @@ a)
-> Decision (q @@ a)
-> Decision ((p ^^^ q) @@ a))
-> (Subset f p @@ a)
-> (Subset f q @@ a)
-> Apply (Subset f (p ^^^ q)) a
forall (f :: * -> *) k (p :: k ~> *) (q :: k ~> *) (r :: k ~> *)
(as :: f k).
(forall (a :: k).
Elem f as a
-> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
-> (Subset f p @@ as) -> (Subset f q @@ as) -> Subset f r @@ as
imergeSubset ((forall (a :: k).
Elem f a a
-> Decision (p @@ a)
-> Decision (q @@ a)
-> Decision ((p ^^^ q) @@ a))
-> (Subset f p @@ a)
-> (Subset f q @@ a)
-> Apply (Subset f (p ^^^ q)) a)
-> (forall (a :: k).
Elem f a a
-> Decision (p @@ a)
-> Decision (q @@ a)
-> Decision ((p ^^^ q) @@ a))
-> (Subset f p @@ a)
-> (Subset f q @@ a)
-> Apply (Subset f (p ^^^ q)) a
forall a b. (a -> b) -> a -> b
$ \(Elem f a a
_ :: Elem f as a) -> forall {k1} (p :: k1 ~> *) (q :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ^^^ q) @@ a)
forall (p :: k ~> *) (q :: k ~> *) (a :: k).
Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ^^^ q) @@ a)
decideXor @p @q @a
subsetToAll ::
forall f p.
Universe f =>
Subset f p -?> All f p
subsetToAll :: forall {k} (f :: * -> *) (p :: k ~> *).
Universe f =>
Subset f p -?> All f p
subsetToAll Sing a
xs Subset f p @@ a
s = (forall (a :: k). Elem f a a -> Sing a -> Decision (p @@ a))
-> Sing a -> Decision (Apply (All f p) a)
forall k (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All f p @@ as)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All f p @@ as)
idecideAll (\Elem f a a
i Sing a
_ -> WitSubset f p a -> forall (a :: k). Elem f a a -> Decision (p @@ a)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitSubset f p as
-> forall (a :: k). Elem f as a -> Decision (p @@ a)
runWitSubset Subset f p @@ a
WitSubset f p a
s Elem f a a
i) Sing a
xs
imapSubset ::
(forall a. Elem f as a -> p @@ a -> q @@ a) ->
(forall a. Elem f as a -> q @@ a -> p @@ a) ->
Subset f p @@ as ->
Subset f q @@ as
imapSubset :: forall {k} (f :: * -> *) (as :: f k) (p :: k ~> *) (q :: k ~> *).
(forall (a :: k). Elem f as a -> (p @@ a) -> q @@ a)
-> (forall (a :: k). Elem f as a -> (q @@ a) -> p @@ a)
-> (Subset f p @@ as)
-> Subset f q @@ as
imapSubset forall (a :: k). Elem f as a -> (p @@ a) -> q @@ a
f forall (a :: k). Elem f as a -> (q @@ a) -> p @@ a
g Subset f p @@ as
s = (forall (a :: k). Elem f as a -> Decision (q @@ a))
-> WitSubset f q as
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> Decision (p @@ a))
-> WitSubset f p as
WitSubset ((forall (a :: k). Elem f as a -> Decision (q @@ a))
-> WitSubset f q as)
-> (forall (a :: k). Elem f as a -> Decision (q @@ a))
-> WitSubset f q as
forall a b. (a -> b) -> a -> b
$ \Elem f as a
i ->
(Apply p a -> q @@ a)
-> ((q @@ a) -> Apply p a)
-> Decision (Apply p a)
-> Decision (q @@ a)
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (Elem f as a -> Apply p a -> q @@ a
forall (a :: k). Elem f as a -> (p @@ a) -> q @@ a
f Elem f as a
i) (Elem f as a -> (q @@ a) -> Apply p a
forall (a :: k). Elem f as a -> (q @@ a) -> p @@ a
g Elem f as a
i) (WitSubset f p as
-> forall (a :: k). Elem f as a -> Decision (p @@ a)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitSubset f p as
-> forall (a :: k). Elem f as a -> Decision (p @@ a)
runWitSubset Subset f p @@ as
WitSubset f p as
s Elem f as a
i)
mapSubset ::
Universe f =>
(p --> q) ->
(q --> p) ->
(Subset f p --> Subset f q)
mapSubset :: forall {k} (f :: * -> *) (p :: k ~> *) (q :: k ~> *).
Universe f =>
(p --> q) -> (q --> p) -> Subset f p --> Subset f q
mapSubset p --> q
f q --> p
g Sing a
xs =
Sing a
-> (SingI a => (Subset f p @@ a) -> Subset f q @@ a)
-> (Subset f p @@ a)
-> Subset f q @@ a
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a
xs ((SingI a => (Subset f p @@ a) -> Subset f q @@ a)
-> (Subset f p @@ a) -> Subset f q @@ a)
-> (SingI a => (Subset f p @@ a) -> Subset f q @@ a)
-> (Subset f p @@ a)
-> Subset f q @@ a
forall a b. (a -> b) -> a -> b
$
(forall (a :: k). Elem f a a -> (p @@ a) -> q @@ a)
-> (forall (a :: k). Elem f a a -> (q @@ a) -> p @@ a)
-> (Subset f p @@ a)
-> Subset f q @@ a
forall {k} (f :: * -> *) (as :: f k) (p :: k ~> *) (q :: k ~> *).
(forall (a :: k). Elem f as a -> (p @@ a) -> q @@ a)
-> (forall (a :: k). Elem f as a -> (q @@ a) -> p @@ a)
-> (Subset f p @@ as)
-> Subset f q @@ as
imapSubset
(\Elem f a a
i -> Sing a -> (p @@ a) -> q @@ a
p --> q
f (Elem f a a -> Sing a -> Sing a
forall {k} (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f a a
i Sing a
xs))
(\Elem f a a
i -> Sing a -> (q @@ a) -> p @@ a
q --> p
g (Elem f a a -> Sing a -> Sing a
forall {k} (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f a a
i Sing a
xs))