HomIso.hs.txt (21044B)
1 {-# LANGUAGE UndecidableInstances #-} 2 3 module Todo.HomIso where 4 5 import Data.Coerce 6 import Lude 7 8 -- NOTE: https://gist.github.com/Icelandjack/ae22c42b01c9be7e8a82f80bc8ab3f1c 9 10 -------------------------------------------------------------------------------- 11 12 -- mapIso 13 -- :: forall {i} {j} (f :: i -> j) (a :: i) (b :: i) 14 -- . (Functorial f) => Iso (Dom f) a b -> Iso (Cod f) (f a) (f b) 15 -- mapIso = fork MkIso (map . to) (map . fro) 16 17 -------------------------------------------------------------------------------- 18 -- Haskell 19 20 type Pointwise :: forall {i} {j}. Cat j -> Cat (i -> j) 21 newtype Pointwise q f g = MkPointwise (forall a. f a `q` g a) 22 23 instance (Categorical q, Obj q ~ Always) => Categorical (Pointwise q) where 24 identity = MkPointwise identity 25 compose (MkPointwise a) (MkPointwise b) = MkPointwise (compose a b) 26 27 instance (Categorical q, Obj q ~ Always) => Functorial (Pointwise q f) where 28 type Dom (Pointwise q f) = Pointwise q 29 type Cod (Pointwise q f) = Function 30 map = compose 31 32 instance (Categorical q, Obj q ~ Always) => Functorial (Pointwise q) where 33 type Dom (Pointwise q) = Dual (Pointwise q) 34 type Cod (Pointwise q) = Pointwise q ==> Function 35 map (MkDual f) = Naturally (. f) 36 37 type (<->) :: forall (r :: Repr). Cat (Type# r) 38 type (<->) @r = Iso (Function# r) 39 40 type (:-:) :: Cat Constraint 41 type (:-:) = Iso Entailment 42 43 type (<~>) :: forall i (r :: Repr). Cat (i -> Type# r) 44 type (<~>) @i @r = Iso (Pointwise (Function# r)) 45 46 type (:~:) :: forall i. Cat (i -> Constraint) 47 type (:~:) @i = Iso (Pointwise Entailment) 48 49 -------------------------------------------------------------------------------- 50 51 data FunctorB :: forall i j. Cat i -> Cat j -> Brand 52 type FunctorK :: forall i j. Cat i -> Cat j -> Kind 53 type FunctorK p q = OpenKind (FunctorB p q) 54 55 type IsFunctor :: forall {i} {j} (p :: Cat i) (q :: Cat j). FunctorK p q -> Constraint 56 class (Categorical p, Categorical q) => IsFunctor (f :: FunctorK @i @j p q) where 57 type Omap (f :: FunctorK @i @j p q) (_ :: i) :: j 58 mmap :: For f (forall (a :: i) (b :: i). a `p` b -> Omap f a `q` Omap f b) 59 60 data IdF :: forall i. forall (p :: Cat i) -> FunctorK p p 61 instance (Categorical p) => IsFunctor (IdF p) where 62 type Omap (IdF p) a = a 63 mmap _ h = h 64 65 data ComposeF :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k). FunctorK q r -> FunctorK p q -> FunctorK p r 66 instance (IsFunctor f, IsFunctor g) => IsFunctor (ComposeF f g) where 67 type Omap (ComposeF f g) a = (Omap f . Omap g) a 68 mmap _ = mmap f . mmap g 69 70 data NominalF :: forall i j. forall (p :: Cat i) (q :: Cat j) (f :: i -> j) -> FunctorK p q 71 instance (FunctorialOn p q f) => IsFunctor (NominalF p q f) where 72 type Omap (NominalF _ _ f) a = f a 73 mmap _ = map 74 75 data CoerceF :: forall i. forall (p :: Cat i) (q :: Cat i) -> FunctorK p q 76 instance (Categorical p, Categorical q, Coercible p q) => IsFunctor (CoerceF p q) where 77 type Omap (CoerceF _ _) a = a 78 mmap _ = coerce 79 80 type SomeCat :: Kind 81 data SomeCat = forall i. MkSomeCat (Cat i) 82 type Funct :: Cat SomeCat 83 data Funct _ _ where 84 MkFunct :: forall {i} {j} (p :: Cat i) (q :: Cat j). forall (f :: FunctorK p q) -> (IsFunctor f) => Funct (MkSomeCat p) (MkSomeCat q) 85 type IsCat :: Predicate SomeCat 86 class IsCat sp where isCat :: forall r. (forall {i}. forall (p :: Cat i) -> (MkSomeCat p ~ sp, Categorical p) => r) -> r 87 instance (Categorical p) => IsCat (MkSomeCat p) where isCat k = k p 88 instance Categorical Funct where 89 type Obj Funct = IsCat 90 identity @sp = isCat @sp \p -> MkFunct (IdF p) 91 compose (MkFunct f) (MkFunct g) = MkFunct (ComposeF f g) 92 witnessMor (MkFunct _) = MkEvidence 93 94 data Iso_Map :: forall {i} {j} (p :: Cat i) (q :: Cat j) (a :: i) (b :: i) (x :: j) (y :: j). forall (f :: FunctorK p q) -> IsoK p a b -> IsoK q x y 95 instance (IsFunctor f, IsIso iso, Omap f a ~ x, Omap f b ~ y) => IsIso (Iso_Map (f :: FunctorK p q) (iso :: IsoK p a b) :: IsoK q x y) where 96 fwd _ = mmap f (fwd iso) 97 bwd _ = mmap f (bwd iso) 98 99 type Relabel :: forall i. Cat (Cat i) 100 data Relabel p q = (Categorical p, Categorical q) => MkRelabel {relabel :: forall a b. a `p` b -> a `q` b} 101 instance Categorical Relabel where 102 type Obj Relabel = Categorical 103 identity = MkRelabel identity 104 compose (MkRelabel f) (MkRelabel g) = MkRelabel (compose f g) 105 witnessMor (MkRelabel _) = MkEvidence 106 107 data Iso_Transfer :: forall {i} (p :: Cat i) (q :: Cat i) (a :: i) (b :: i). IsoK Relabel p q -> IsoK p a b -> IsoK q a b 108 instance (Categorical p, Categorical q, IsIso rel, IsIso iso) => IsIso (Iso_Transfer (rel :: IsoK Relabel p q) (iso :: IsoK p a b)) where 109 fwd _ = relabel (fwd rel) (fwd iso) 110 bwd _ = relabel (fwd rel) (bwd iso) 111 112 data Iso_RelabelHom :: forall {i}. forall (p :: Cat i) -> IsoK Relabel (Hom p) p 113 instance (Categorical p) => IsIso (Iso_RelabelHom p) where 114 fwd _ = MkRelabel unHom 115 bwd _ = MkRelabel MkHom 116 117 -- data Iso_RelabelNT :: forall {i} {j} (p :: Cat i) (p' :: Cat i) (q :: Cat j) (q' :: Cat j). IsoK Relabel p p' -> IsoK Relabel q q' -> IsoK Relabel (p ==> q) (p' ==> q') 118 -- instance (IsIso relp, IsIso rel) => IsIso (Iso_RelabelNT relp rel) where 119 -- fwd _ = MkRelabel \(Naturally f) -> Naturally (relabel (fwd rel) f) 120 121 -------------------------------------------------------------------------------- 122 123 data MorphB :: forall i. Cat i -> i -> i -> Brand 124 type MorphK :: forall i. Cat i -> i -> i -> Kind 125 type MorphK p a b = OpenKind (MorphB p a b) 126 127 type IsMorph :: forall {i} (p :: Cat i) (a :: i) (b :: i). MorphK p a b -> Constraint 128 class (Categorical p) => IsMorph (this :: MorphK p a b) where 129 morph :: For this (a `p` b) 130 131 type Morph :: forall i. Cat i -> i -> i -> Kind 132 data Morph _ _ _ where 133 MkMorph :: forall {i} (p :: Cat i) (a :: i) (b :: i). forall (rw :: MorphK p a b) -> (IsMorph rw) => Morph p a b 134 135 instance (Categorical p) => Categorical (Morph p) where 136 type Obj (Morph p) = Obj p 137 identity = MkMorph (Morph_Identity p) 138 compose (MkMorph f) (MkMorph g) = MkMorph (Morph_Compose f g) 139 witnessMor (MkMorph f) = MkEvidence \\ witnessMor (morph f) 140 141 data Morph_Identity :: forall {i}. forall (p :: Cat i) -> forall (a :: i). MorphK p a a 142 instance forall i (p :: Cat i) (a :: i). (Categorical p, Obj p a) => IsMorph (Morph_Identity p @a) where 143 morph _ = identity 144 {-# INLINE morph #-} 145 146 data Morph_Compose :: forall {i} (p :: Cat i) (a :: i) (b :: i) (c :: i). MorphK p b c -> MorphK p a b -> MorphK p a c 147 instance forall i (p :: Cat i) (a :: i) (b :: i) (c :: i) (s :: MorphK p a b) (t :: MorphK p b c). (IsMorph s, IsMorph t) => IsMorph (Morph_Compose t s) where 148 morph _ = morph t . morph s 149 {-# INLINE morph #-} 150 151 data Morph_Dual :: forall {i} (p :: Cat i) (a :: i) (b :: i). MorphK p b a -> MorphK (Dual p) a b 152 instance forall i (p :: Cat i) (a :: i) (b :: i) (s :: MorphK p b a). (IsMorph s) => IsMorph (Morph_Dual s) where 153 morph _ = MkDual (morph s) 154 {-# INLINE morph #-} 155 156 data Morph_App :: forall {i} {j} (p :: Cat i) (q :: Cat j) (f :: i -> j) (a :: i) (g :: i -> j) (b :: i). MorphK (p ==> q) f g -> MorphK p a b -> MorphK q (f a) (g b) 157 instance forall i j (p :: Cat i) (q :: Cat j) (f :: i -> j) (a :: i) (g :: i -> j) (b :: i) (s :: MorphK (p ==> q) f g) (t :: MorphK p a b). (Categorical q, IsMorph s, IsMorph t) => IsMorph (Morph_App s t) where 158 morph _ = (comp (morph s) \\ witnessMor (morph t)) . (map (morph t) \\ witnessMor (morph s)) 159 {-# INLINE morph #-} 160 161 data Morph_IsoFwd :: forall {i} (p :: Cat i) (a :: i) (b :: i). IsoK p a b -> MorphK p a b 162 instance forall i (p :: Cat i) (a :: i) (b :: i) (iso :: IsoK p a b). (IsIso iso) => IsMorph (Morph_IsoFwd iso) where 163 morph _ = fwd iso 164 {-# INLINE morph #-} 165 166 data Morph_IsoBwd :: forall {i} (p :: Cat i) (a :: i) (b :: i). IsoK p a b -> MorphK p b a 167 instance forall i (p :: Cat i) (a :: i) (b :: i) (iso :: IsoK p a b). (IsIso iso) => IsMorph (Morph_IsoBwd iso) where 168 morph _ = bwd iso 169 {-# INLINE morph #-} 170 171 -------------------------------------------------------------------------------- 172 173 type Rewrite :: forall {i} (p :: Cat i) (a :: i) (b :: i). IsoK p a b -> forall {k}. forall (q :: Cat k) (x :: k) (y :: k) -> MorphK q x y 174 type family Rewrite _ _ _ _ where 175 Rewrite (iso :: IsoK p a b) p a b = Morph_IsoFwd iso 176 Rewrite iso (Dual q) x y = Morph_Dual (Rewrite (Iso_Inv iso) q y x) 177 Rewrite iso q x y = Rewrite' iso q x y (RewriteTouches iso x y) 178 179 type Rewrite' :: forall {i} (p :: Cat i) (a :: i) (b :: i). IsoK p a b -> forall {k}. forall (q :: Cat k) (x :: k) (y :: k) -> Bool -> MorphK q x y 180 type family Rewrite' _ _ _ _ _ where 181 -- We check these two cases *after* checking for direct applicability of the 182 -- iso, so either (a) we need to recurse to apply the iso at some location 183 -- deep in the input, or (b) the iso doesn't apply at all. These two cases 184 -- are distinguished by the bool computed by `RewriteTouches`. By only 185 -- recursing when the bool is true, we avoid needlessly requiring *all* 186 -- types of function kind to be functors, and we avoid getting stuck on 187 -- type variables in some circumstances. 188 Rewrite' iso q (f x) (g y) True = RewriteApp iso q f (Dom f) (Cod f) x g (Dom g) (Cod g) y 189 Rewrite' _ q x x False = Morph_Identity q 190 Rewrite' iso q x y _ = 191 TypeError 192 ( ErrText "Could not rewrite type " 193 !// ErrType x 194 !// ErrText " to type " 195 !// ErrType y 196 !// ErrText " along isomorphism " 197 !// ErrType iso 198 !// ErrText " in category " 199 !// ErrType q 200 ) 201 202 type RewriteTouches :: forall {i} (p :: Cat i) (a :: i) (b :: i). IsoK p a b -> forall {k}. k -> k -> Bool 203 type family RewriteTouches _ _ _ where 204 RewriteTouches (_ :: IsoK _ a b) a b = True 205 RewriteTouches iso (f x) (g y) = RewriteTouches iso f g || RewriteTouches iso x y 206 RewriteTouches _ _ _ = False 207 208 -- | Helper for `Rewrite'` to ensure functor (co)domains align 209 type RewriteApp :: forall {i} (p :: Cat i) (a :: i) (b :: i). IsoK p a b -> forall {j} {k}. forall (q :: Cat k) (f :: j -> k) -> Cat j -> Cat k -> forall (x :: j) (g :: j -> k) -> Cat j -> Cat k -> forall (y :: j) -> MorphK q (f x) (g y) 210 type family RewriteApp _ _ _ _ _ _ _ _ _ _ where 211 RewriteApp iso q f r q x g r q y = Morph_App (Rewrite iso (r ==> q) f g) (Rewrite iso r x y) 212 RewriteApp _ _ f fdom fcod _ g gdom gcod _ = 213 TypeError 214 ( ErrText "Could not rewrite type application between (functor, dom, cod) triples " 215 !// ErrType (f, fdom, fcod) 216 !// ErrText " and " 217 !// ErrType (g, gdom, gcod) 218 !// ErrText " because the (co)domains do not match" 219 ) 220 221 rewrite :: forall {i} (p :: Cat i) (a :: i) (b :: i). forall (iso :: IsoK p a b) -> forall {j} (x :: j) (y :: j) (q :: Cat j). (IsMorph (Rewrite iso q x y)) => x `q` y 222 rewrite iso = morph (Rewrite iso _ _ _) 223 {-# INLINE rewrite #-} 224 225 rewrittenAlong :: forall (x :: Type). x -> forall {i} (p :: Cat i) (a :: i) (b :: i). forall (iso :: IsoK p a b) -> forall (y :: Type). (IsMorph (Rewrite iso Function x y)) => y 226 x `rewrittenAlong` iso = rewrite iso x 227 {-# INLINE rewrittenAlong #-} 228 229 -------------------------------------------------------------------------------- 230 231 data IsoB :: forall i. Cat i -> i -> i -> Brand 232 type IsoK :: forall i. Cat i -> i -> i -> Kind 233 type IsoK p a b = OpenKind (IsoB p a b) 234 235 type IsIso :: forall {i} (p :: Cat i) (a :: i) (b :: i). IsoK p a b -> Constraint 236 class (Categorical p) => IsIso (this :: IsoK p a b) where 237 fwd :: For this (a `p` b) 238 bwd :: For this (b `p` a) 239 240 fwd1 :: forall {i} {j} (p :: Cat i) (q :: Cat j) (a :: i -> j) (b :: i -> j). forall (iso :: IsoK (p ==> q) a b) -> (IsIso iso) => NT_ p q a b 241 fwd1 iso = comp (fwd iso) 242 243 bwd1 :: forall {i} {j} (p :: Cat i) (q :: Cat j) (a :: i -> j) (b :: i -> j). forall (iso :: IsoK (p ==> q) a b) -> (IsIso iso) => NT_ p q b a 244 bwd1 iso = comp (bwd iso) 245 246 fwd2 :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k) (a :: i -> j -> k) (b :: i -> j -> k). forall (iso :: IsoK (p ==> q ==> r) a b) -> (IsIso iso) => BiNT_ p q r a b 247 fwd2 iso = bicomp (fwd iso) 248 249 bwd2 :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k) (a :: i -> j -> k) (b :: i -> j -> k). forall (iso :: IsoK (p ==> q ==> r) a b) -> (IsIso iso) => BiNT_ p q r b a 250 bwd2 iso = bicomp (bwd iso) 251 252 -- type Fwd :: forall {i} (p :: Cat i) (a :: i) (b :: i). IsoK p a b -> forall {k}. k -> k 253 -- type family Fwd _ _ where 254 -- Fwd (_ :: IsoK _ a b) a = b 255 -- Fwd iso (x y) = (Fwd iso x) (Fwd iso y) 256 -- Fwd _ x = x 257 258 -- type Bwd :: forall {i} (p :: Cat i) (a :: i) (b :: i). IsoK p a b -> forall {k}. k -> k 259 -- type family Bwd _ _ where 260 -- Bwd (_ :: IsoK _ a b) b = a 261 -- Bwd iso (x y) = (Bwd iso x) (Bwd iso y) 262 -- Bwd _ x = x 263 264 -- TODO: Iso type, analogous to Morph 265 266 -------------------------------------------------------------------------------- 267 268 data Iso_Identity :: forall {i}. forall (p :: Cat i) -> forall (a :: i). IsoK p a a 269 instance (Categorical p, Obj p a) => IsIso (Iso_Identity p @a) where 270 fwd _ = identity 271 bwd _ = identity 272 273 data Iso_Compose :: forall {i} (p :: Cat i) (a :: i) (b :: i) (c :: i). IsoK p b c -> IsoK p a b -> IsoK p a c 274 instance (IsIso iso0, IsIso iso1) => IsIso (Iso_Compose iso0 iso1) where 275 fwd _ = fwd iso0 . fwd iso1 276 bwd _ = bwd iso1 . bwd iso0 277 278 data Iso_Inv :: forall {i} (p :: Cat i) (a :: i) (b :: i). IsoK p b a -> IsoK p a b 279 instance (IsIso iso) => IsIso (Iso_Inv iso) where 280 fwd _ = bwd iso 281 bwd _ = fwd iso 282 283 data Iso_Coerce :: forall (a :: Type) (b :: Type) -> IsoK Function a b 284 instance (Coercible a b) => IsIso (Iso_Coerce a b) where 285 fwd _ = coerce 286 bwd _ = coerce 287 288 data Iso_Coerce1 :: forall {i} (p :: Cat i). forall (a :: i -> Type) (b :: i -> Type) -> IsoK (p ==> Function) a b 289 instance (Categorical p, FunctorialOn p Function a, FunctorialOn p Function b, Coercible a b) => IsIso (Iso_Coerce1 @p a b) where 290 fwd _ = Naturally coerce 291 bwd _ = Naturally coerce 292 293 data Iso_Coerce2 :: forall {i} {j} (p :: Cat i) (q :: Cat j). forall (a :: i -> j -> Type) (b :: i -> j -> Type) -> IsoK (p ==> q ==> Function) a b 294 instance (Categorical p, Categorical q, BifunctorialOn p q Function a, BifunctorialOn p q Function b, Coercible a b) => IsIso (Iso_Coerce2 @p @q a b) where 295 fwd _ = Binaturally coerce 296 bwd _ = Binaturally coerce 297 298 data Iso_Swap :: forall (a :: Type) (b :: Type) -> IsoK Function (Tuple2 a b) (Tuple2 b a) 299 instance IsIso (Iso_Swap a b) where 300 fwd _ (x, y) = (y, x) 301 bwd _ (y, x) = (x, y) 302 303 data Iso_Assoc :: forall (a :: Type) (b :: Type) (c :: Type) -> IsoK Function (Tuple2 (Tuple2 a b) c) (Tuple2 a (Tuple2 b c)) 304 instance IsIso (Iso_Assoc a b c) where 305 fwd _ ((x, y), z) = (x, (y, z)) 306 bwd _ (x, (y, z)) = ((x, y), z) 307 308 -------------------------------------------------------------------------------- 309 310 type Transport :: forall (a :: Type) (b :: Type). IsoK Function a b -> Type 311 newtype Transport @a @_ _ = MkTransport {unTransport :: a} 312 313 data Iso_Transport :: forall (a :: Type) (b :: Type). forall (iso :: IsoK Function a b) -> IsoK Function b (Transport iso) 314 instance (IsIso iso) => IsIso (Iso_Transport iso) where 315 fwd _ = MkTransport . bwd iso 316 bwd _ = fwd iso . unTransport 317 318 transport :: forall (a :: Type) (b :: Type). forall (iso :: IsoK Function a b) -> forall (x :: Type) (y :: Type). (IsMorph (Rewrite (Iso_Transport iso) Function x y)) => x -> y 319 transport iso = rewrite (Iso_Transport iso) 320 {-# INLINE transport #-} 321 322 -------------------------------------------------------------------------------- 323 324 class Sg a where (++) :: Biendo a 325 326 instance (Sg a, Sg b, Sg c) => Sg (Tuple2 (Tuple2 a b) c) where 327 ((a1, b1), c1) ++ ((a2, b2), c2) = ((a1 ++ a2, b1 ++ b2), c1 ++ c2) 328 329 -- instance (Sg a, Sg b, Sg c) => Sg (Tuple2 a (Tuple2 b c)) where 330 -- (++) = rewrite (Iso_Assoc a b c) ((++) @(Tuple2 (Tuple2 a b) c)) 331 332 instance (IsIso iso, Sg b) => Sg (Transport (iso :: IsoK Function a b)) where 333 (++) = transport iso ((++) @b) 334 335 deriving via Transport (Iso_Inv (Iso_Assoc a b c)) instance (Sg a, Sg b, Sg c) => Sg (Tuple2 a (Tuple2 b c)) 336 337 -------------------------------------------------------------------------------- 338 339 type Transport1 :: forall {i} (p :: Cat i) (a :: i -> Type) (b :: i -> Type). IsoK (p ==> Function) a b -> i -> Type 340 newtype Transport1 @_ @a @_ _ x = MkTransport1 {unTransport1 :: a x} 341 342 instance forall i (p :: Cat i) (a :: i -> Type) (b :: i -> Type) (iso :: IsoK (p ==> Function) a b). (Categorical p, IsIso iso, FunctorialOn p Function b) => Functorial (Transport1 iso) where 343 type Dom (Transport1 @p _) = p 344 type Cod (Transport1 @_ _) = Function 345 map f = coerce $ bwd1 iso . map f . fwd1 iso \\ witnessMor f 346 347 -------------------------------------------------------------------------------- 348 349 type Transport2 :: forall {i} {j} (p :: Cat i) (q :: Cat j) (a :: i -> j -> Type) (b :: i -> j -> Type). IsoK (p ==> q ==> Function) a b -> i -> j -> Type 350 newtype Transport2 @_ @_ @a @_ _ x y = MkTransport2 {unTransport2 :: a x y} 351 352 instance forall i j (p :: Cat i) (q :: Cat j) (a :: i -> j -> Type) (b :: i -> j -> Type) (iso :: IsoK (p ==> q ==> Function) a b) (x :: i). (Categorical q, IsIso iso, Obj p x, FunctorialOn q Function (b x)) => Functorial (Transport2 iso x) where 353 type Dom (Transport2 @_ @q _ _) = q 354 type Cod (Transport2 @_ @_ _ _) = Function 355 map f = coerce $ bwd2 iso . map f . fwd2 iso \\ witnessMor f 356 357 instance forall i j (p :: Cat i) (q :: Cat j) (a :: i -> j -> Type) (b :: i -> j -> Type) (iso :: IsoK (p ==> q ==> Function) a b). (Categorical p, IsIso iso, BifunctorialOn p q Function b) => Functorial (Transport2 iso) where 358 type Dom (Transport2 @p @_ _) = p 359 type Cod (Transport2 @_ @q _) = q ==> Function 360 map @x @y f = 361 Naturally (coerce $ bwd2 iso . nmap f . fwd2 iso) 362 \\ (b `preservesObj` x) 363 \\ (b `preservesObj` y) 364 \\ witnessMor f 365 366 -- data Iso_Transport2 :: forall {i} {j} (p :: Cat i) (q :: Cat j) (a :: i -> j -> Type) (b :: i -> j -> Type). forall (iso :: IsoK (p ==> q ==> Function) a b) -> IsoK (p ==> q ==> Function) b (Transport2 iso) 367 -- instance forall i j (p :: Cat i) (q :: Cat j) (a :: i -> j -> Type) (b :: i -> j -> Type) (iso :: IsoK (p ==> q ==> Function) a b). (BifunctorialOn p q Function a, IsIso iso) => IsIso (Iso_Transport2 iso) where 368 -- fwd _ = Binaturally MkTransport2 . bwd iso 369 -- bwd _ = fwd iso . Binaturally unTransport2 370 -- 371 -- transport2 :: forall {i} {j} (p :: Cat i) (q :: Cat j) (a :: i -> j -> Type) (b :: i -> j -> Type). forall (iso :: IsoK (p ==> q ==> Function) a b) -> forall (x :: Type) (y :: Type). (IsMorph (Rewrite (Iso_Transport2 iso) Function x y)) => x -> y 372 -- transport2 iso = rewrite (Iso_Transport2 iso) 373 -- {-# INLINE transport2 #-} 374 375 -------------------------------------------------------------------------------- 376 377 -- instance (IsIso iso, Categorical p, BifunctorialOn (Dual p) p Function a, BifunctorialOn (Dual p) p Function b, p ~ b) => Categorical (Transport2 (iso :: IsoK (Dual p ==> p ==> Function) a b)) where 378 -- type Obj (Transport2 (_ :: IsoK _ _ b)) = Obj b 379 -- 380 -- -- identity @x = transport2 iso (identity @b @x) 381 -- -- witnessMor = transport2 iso (witnessMor @b) 382 -- identity = MkTransport2 (bwd iso $^^ identity) 383 -- compose (MkTransport2 f) (MkTransport2 g) = MkTransport2 (bwd iso $^^ (compose (fwd iso $^^ f) (fwd iso $^^ g))) 384 -- witnessMor (MkTransport2 f) = MkEvidence \\ witnessMor (fwd iso $^^ f) 385 386 -------------------------------------------------------------------------------- 387 388 -- type Pointwise :: forall {i} {j}. Cat j -> Cat (i -> j) 389 -- newtype Pointwise q f g = MkPointwise (forall a. f a `q` g a) 390 -- 391 -- instance (Categorical q, Obj q ~ Always) => Categorical (Pointwise q) where 392 -- identity = MkPointwise identity 393 -- compose (MkPointwise a) (MkPointwise b) = MkPointwise (compose a b) 394 395 -- data Iso_Hom :: forall {i}. forall (p :: Cat i) -> IsoK (Dual p ==> p ==> Function) p (Hom p) 396 -- instance (Categorical p) => IsIso (Iso_Hom p) where 397 -- fwd _ = Binaturally \ @x @y -> () 398 399 -- data Iso_Naturally :: forall {i} {j} (p :: Cat i) (q :: Cat j) (a :: i -> j) (b :: i -> j). (forall (x :: i). IsoK q (a x) (b x)) -> IsoK (p ==> q) a b 400 -- instance IsIso (Iso_Naturally iso) where 401 402 -- deriving via Transport2 (Iso_Coerce @(q x) @(Hom q x)) instance (Categorical q, Obj q ~ Always) => Functorial (Pointwise q x) 403 404 type Stupid :: forall {i}. Cat i 405 data Stupid _ _ = MkStupid 406 407 instance Categorical Stupid where 408 identity = MkStupid 409 compose MkStupid MkStupid = MkStupid 410 411 -- type Whoa0 a = Iso_Coerce1 @(Hom Stupid) (Stupid a) (Hom Stupid a) 412 -- type Whoa1 = Iso_RelabelHom Stupid 413 -- type Whoa2 a = Iso_Transfer Whoa1 (Whoa0 a) 414 415 -- deriving via Transport1 (Iso_Transfer (Iso_RelabelHom Stupid) (Iso_Coerce1 @(Hom Stupid) (Stupid a) (Hom Stupid a))) instance Functorial (Stupid a) 416 417 -- deriving via Transport2 (Iso_Coerce2 @(Dual (Hom Stupid)) @(Hom Stupid) Stupid (Hom Stupid)) instance Functorial Stupid