ExternalProduct.hs.txt (2292B)
1 {-# LANGUAGE UndecidableInstances #-} 2 3 module Todo.ExternalProduct where 4 5 import Lude 6 7 -------------------------------------------------------------------------------- 8 9 type Categorical4 :: forall {i} {j} {k} {l}. Cat i -> Cat j -> Cat k -> Cat l -> Constraint 10 type Categorical4 p q r s = All (Categorical p, Categorical q, Categorical r, Categorical s) 11 12 type External 13 :: forall {i} {j} {k} {l} 14 . Cat i 15 -> Cat j 16 -> Cat k 17 -> Cat l 18 -> (k -> l -> Type) 19 -> (i -> k) 20 -> (j -> l) 21 -> (i -> j -> Type) 22 data External p q r s h f g a b = (Obj p a, Obj q b) => MkFoo {unFoo :: h (f a) (g b)} 23 24 instance (BifunctorialOn r s Function h, FunctorialOn p r f, FunctorialOn q s g) => Functorial (External p q r s h f g a) where 25 type Dom (External p q r s h f g a) = q 26 type Cod (External p q r s h f g a) = Function 27 map m = \(MkFoo x) -> MkFoo (rmap (map m) x \\ f `preservesObj` a) \\ witnessMor m 28 29 instance (Categorical4 p q r s, BifunctorialOn r s Function h, FunctorialOn p r f, FunctorialOn q s g) => Functorial (External p q r s h f g) where 30 type Dom (External p q r s h f g) = p 31 type Cod (External p q r s h f g) = q ==> Function 32 map m = Naturally \ @b (MkFoo x) -> MkFoo (lmap (map m) x \\ g `preservesObj` b) \\ witnessMor m 33 34 instance (Categorical4 p q r s, BifunctorialOn r s Function h, FunctorialOn p r f) => Functorial (External p q r s h f) where 35 type Dom (External p q r s h f) = q ==> s 36 type Cod (External p q r s h f) = p ==> q ==> Function 37 map (Naturally m) = Binaturally \ @a @_b (MkFoo x) -> MkFoo (rmap m x \\ f `preservesObj` a) 38 39 instance (Categorical4 p q r s, BifunctorialOn r s Function h) => Functorial (External p q r s h) where 40 type Dom (External p q r s h) = p ==> r 41 type Cod (External p q r s h) = (q ==> s) ==> (p ==> q ==> Function) 42 map (Naturally m) = Naturally \ @g -> Binaturally \ @_a @b (MkFoo x) -> MkFoo (lmap m x \\ g `preservesObj` b) 43 44 instance (Categorical4 p q r s) => Functorial (External p q r s) where 45 type Dom (External p q r s) = r ==> s ==> Function 46 type Cod (External p q r s) = (p ==> r) ==> (q ==> s) ==> (p ==> q ==> Function) 47 map (Binaturally m) = Binaturally \ @f @g -> Binaturally \ @a @b (MkFoo x) -> MkFoo (m x \\ f `preservesObj` a \\ g `preservesObj` b)