module Data.Type.Witness.Specific.FiniteAllFor where import Data.Type.Witness.General.Finite import Data.Type.Witness.Specific.All import Data.Type.Witness.Specific.Either import Data.Type.Witness.Specific.Some import Import type FiniteAllFor :: forall k. (k -> Type) -> (k -> Type) -> Type data FiniteAllFor f w = MkFiniteAllFor { forall k (f :: k -> Type) (w :: k -> Type). FiniteAllFor f w -> [Some w] finiteDomain :: [Some w] , forall k (f :: k -> Type) (w :: k -> Type). FiniteAllFor f w -> forall (t :: k). w t -> f t finiteGetAllFor :: forall t. w t -> f t } finiteAllFor :: FiniteAllFor f w -> AllFor f w finiteAllFor :: forall {k} (f :: k -> Type) (w :: k -> Type). FiniteAllFor f w -> AllFor f w finiteAllFor (MkFiniteAllFor [Some w] _ forall (t :: k). w t -> f t f) = forall k (f :: k -> Type) (w :: k -> Type). (forall (t :: k). w t -> f t) -> AllFor f w MkAllFor forall (t :: k). w t -> f t f finiteCodomain :: FiniteAllFor f w -> [Some f] finiteCodomain :: forall {k} (f :: k -> Type) (w :: k -> Type). FiniteAllFor f w -> [Some f] finiteCodomain FiniteAllFor f w sw = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b fmap (\(MkSome w a st) -> forall {k} (w :: k -> Type) (a :: k). w a -> Some w MkSome forall a b. (a -> b) -> a -> b $ forall k (f :: k -> Type) (w :: k -> Type). FiniteAllFor f w -> forall (t :: k). w t -> f t finiteGetAllFor FiniteAllFor f w sw w a st) forall a b. (a -> b) -> a -> b $ forall k (f :: k -> Type) (w :: k -> Type). FiniteAllFor f w -> [Some w] finiteDomain FiniteAllFor f w sw mapFiniteAllFor :: (forall t. f1 t -> f2 t) -> FiniteAllFor f1 w -> FiniteAllFor f2 w mapFiniteAllFor :: forall {k} (f1 :: k -> Type) (f2 :: k -> Type) (w :: k -> Type). (forall (t :: k). f1 t -> f2 t) -> FiniteAllFor f1 w -> FiniteAllFor f2 w mapFiniteAllFor forall (t :: k). f1 t -> f2 t ff (MkFiniteAllFor [Some w] ai forall (t :: k). w t -> f1 t i) = forall k (f :: k -> Type) (w :: k -> Type). [Some w] -> (forall (t :: k). w t -> f t) -> FiniteAllFor f w MkFiniteAllFor [Some w] ai forall a b. (a -> b) -> a -> b $ \w t s -> forall (t :: k). f1 t -> f2 t ff forall a b. (a -> b) -> a -> b $ forall (t :: k). w t -> f1 t i w t s eitherFiniteAllFor :: FiniteAllFor t w1 -> FiniteAllFor t w2 -> FiniteAllFor t (EitherType w1 w2) eitherFiniteAllFor :: forall {k} (t :: k -> Type) (w1 :: k -> Type) (w2 :: k -> Type). FiniteAllFor t w1 -> FiniteAllFor t w2 -> FiniteAllFor t (EitherType w1 w2) eitherFiniteAllFor (MkFiniteAllFor [Some w1] a1 forall (t :: k). w1 t -> t t i1) (MkFiniteAllFor [Some w2] a2 forall (t :: k). w2 t -> t t i2) = forall k (f :: k -> Type) (w :: k -> Type). [Some w] -> (forall (t :: k). w t -> f t) -> FiniteAllFor f w MkFiniteAllFor ((forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b fmap (forall k (g :: k -> Type) (w1 :: k -> Type) (w2 :: k -> Type). (forall (t :: k). w1 t -> w2 t) -> SomeFor g w1 -> SomeFor g w2 mapSome forall k (w1 :: k -> Type) (w2 :: k -> Type) (t :: k). w1 t -> EitherType w1 w2 t LeftType) [Some w1] a1) forall a. [a] -> [a] -> [a] ++ (forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b fmap (forall k (g :: k -> Type) (w1 :: k -> Type) (w2 :: k -> Type). (forall (t :: k). w1 t -> w2 t) -> SomeFor g w1 -> SomeFor g w2 mapSome forall k (w1 :: k -> Type) (w2 :: k -> Type) (t :: k). w2 t -> EitherType w1 w2 t RightType) [Some w2] a2)) (forall k (f :: k -> Type) (w :: k -> Type). AllFor f w -> forall (t :: k). w t -> f t unAllFor forall a b. (a -> b) -> a -> b $ forall {k} (f :: k -> Type) (sel1 :: k -> Type) (sel2 :: k -> Type). AllFor f sel1 -> AllFor f sel2 -> AllFor f (EitherType sel1 sel2) eitherAllFor (forall k (f :: k -> Type) (w :: k -> Type). (forall (t :: k). w t -> f t) -> AllFor f w MkAllFor forall (t :: k). w1 t -> t t i1) (forall k (f :: k -> Type) (w :: k -> Type). (forall (t :: k). w t -> f t) -> AllFor f w MkAllFor forall (t :: k). w2 t -> t t i2)) mkFiniteAllFor :: forall f w. FiniteWitness w => (forall t. w t -> f t) -> FiniteAllFor f w mkFiniteAllFor :: forall {k} (f :: k -> Type) (w :: k -> Type). FiniteWitness w => (forall (t :: k). w t -> f t) -> FiniteAllFor f w mkFiniteAllFor = forall k (f :: k -> Type) (w :: k -> Type). [Some w] -> (forall (t :: k). w t -> f t) -> FiniteAllFor f w MkFiniteAllFor forall {k} (w :: k -> Type). FiniteWitness w => [Some w] allWitnesses