lude

Haskell prelude alternative
git clone git://git.rr3.xyz/lude | git clone gits://git.rr3.xyz/lude
Log | Files | Refs | README | LICENSE

Bifunctors.hs.txt (2019B)

      1 {-# LANGUAGE UndecidableInstances #-}
      2 
      3 module Todo.Bifunctors where
      4 
      5 import Lude
      6 
      7 --------------------------------------------------------------------------------
      8 
      9 bipreservesObj
     10     :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k)
     11      . forall (f :: i -> j -> k)
     12     ->(BifunctorialOn p q r f)
     13     => forall (a :: i) (b :: j)
     14     ->Obj p a & Obj q b :- Obj r (f a b)
     15 bipreservesObj f a b = Entail (MkEvidence \\ f a `preservesObj` b \\ f `preservesObj` a)
     16 
     17 lpreservesObj
     18     :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k)
     19      . forall (f :: i -> j -> k)
     20     ->(BifunctorialOn p q r f)
     21     => forall (a :: i)
     22     ->forall (b :: j). (Obj q b) => Obj p a :- Obj r (f a b)
     23 lpreservesObj f a @b = Entail (MkEvidence \\ f a `preservesObj` b \\ f `preservesObj` a)
     24 
     25 rpreservesObj
     26     :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k)
     27      . forall (f :: i -> j -> k)
     28     ->(BifunctorialOn p q r f)
     29     => forall (b :: j)
     30     ->forall (a :: i). (Obj p a) => Obj q b :- Obj r (f a b)
     31 rpreservesObj f b @a = Entail (MkEvidence \\ f a `preservesObj` b \\ f `preservesObj` a)
     32 
     33 --------------------------------------------------------------------------------
     34 
     35 type Under :: forall {i} {j}. (i -> j) -> i -> j -> Type
     36 newtype Under (f :: i -> j) (a :: i) (b :: j) = MkUnder {unUnder :: Cod f (f a) b}
     37 
     38 type Over :: forall {i} {j}. (i -> j) -> j -> i -> Type
     39 newtype Over (f :: i -> j) (a :: j) (b :: i) = MkOver {unOver :: Cod f a (f b)}
     40 
     41 --------------------------------------------------------------------------------
     42 
     43 type ProfunctorialOn :: forall {i} {j} {k}. Cat i -> Cat j -> Cat k -> (i -> j -> k) -> Constraint
     44 class (BifunctorialOn (Dual p) q r f) => ProfunctorialOn p q r f | f -> p q r
     45 instance (BifunctorialOn (Dual p) q r f) => ProfunctorialOn p q r f
     46 
     47 type EndoprofunctorialOn :: forall {i} {k}. Cat i -> Cat k -> (i -> i -> k) -> Constraint
     48 class (ProfunctorialOn p p r f) => EndoprofunctorialOn p r f | f -> p r
     49 instance (ProfunctorialOn p p r f) => EndoprofunctorialOn p r f