commit 50bd5370c4f80bfddce38197a7d443108c416ca9
parent 14be6a03279b09647779ed8c8dd2b698c28253c8
Author: Robert Russell <robert@rr3.xyz>
Date: Fri, 9 Oct 2026 12:47:50 -0700
Todo: add experiment
Diffstat:
| A | src/Todo/HomIso.hs | | | 415 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
1 file changed, 415 insertions(+), 0 deletions(-)
diff --git a/src/Todo/HomIso.hs b/src/Todo/HomIso.hs
@@ -0,0 +1,415 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Todo.HomIso where
+
+import Data.Coerce
+import Lude
+
+--------------------------------------------------------------------------------
+
+-- mapIso
+-- :: forall {i} {j} (f :: i -> j) (a :: i) (b :: i)
+-- . (Functorial f) => Iso (Dom f) a b -> Iso (Cod f) (f a) (f b)
+-- mapIso = fork MkIso (map . to) (map . fro)
+
+--------------------------------------------------------------------------------
+-- Haskell
+
+type Pointwise :: forall {i} {j}. Cat j -> Cat (i -> j)
+newtype Pointwise q f g = MkPointwise (forall a. f a `q` g a)
+
+instance (Categorical q, Obj q ~ Always) => Categorical (Pointwise q) where
+ identity = MkPointwise identity
+ compose (MkPointwise a) (MkPointwise b) = MkPointwise (compose a b)
+
+instance (Categorical q, Obj q ~ Always) => Functorial (Pointwise q f) where
+ type Dom (Pointwise q f) = Pointwise q
+ type Cod (Pointwise q f) = Function
+ map = compose
+
+instance (Categorical q, Obj q ~ Always) => Functorial (Pointwise q) where
+ type Dom (Pointwise q) = Dual (Pointwise q)
+ type Cod (Pointwise q) = Pointwise q ==> Function
+ map (MkDual f) = Naturally (. f)
+
+type (<->) :: forall (r :: Repr). Cat (Type# r)
+type (<->) @r = Iso (Function# r)
+
+type (:-:) :: Cat Constraint
+type (:-:) = Iso Entailment
+
+type (<~>) :: forall i (r :: Repr). Cat (i -> Type# r)
+type (<~>) @i @r = Iso (Pointwise (Function# r))
+
+type (:~:) :: forall i. Cat (i -> Constraint)
+type (:~:) @i = Iso (Pointwise Entailment)
+
+--------------------------------------------------------------------------------
+
+data FunctorB :: forall i j. Cat i -> Cat j -> Brand
+type FunctorK :: forall i j. Cat i -> Cat j -> Kind
+type FunctorK p q = OpenKind (FunctorB p q)
+
+type IsFunctor :: forall {i} {j} (p :: Cat i) (q :: Cat j). FunctorK p q -> Constraint
+class (Categorical p, Categorical q) => IsFunctor (f :: FunctorK @i @j p q) where
+ type Omap (f :: FunctorK @i @j p q) (_ :: i) :: j
+ mmap :: For f (forall (a :: i) (b :: i). a `p` b -> Omap f a `q` Omap f b)
+
+data IdF :: forall i. forall (p :: Cat i) -> FunctorK p p
+instance (Categorical p) => IsFunctor (IdF p) where
+ type Omap (IdF p) a = a
+ mmap _ h = h
+
+data ComposeF :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k). FunctorK q r -> FunctorK p q -> FunctorK p r
+instance (IsFunctor f, IsFunctor g) => IsFunctor (ComposeF f g) where
+ type Omap (ComposeF f g) a = (Omap f . Omap g) a
+ mmap _ = mmap f . mmap g
+
+data NominalF :: forall i j. forall (p :: Cat i) (q :: Cat j) (f :: i -> j) -> FunctorK p q
+instance (FunctorialOn p q f) => IsFunctor (NominalF p q f) where
+ type Omap (NominalF _ _ f) a = f a
+ mmap _ = map
+
+data CoerceF :: forall i. forall (p :: Cat i) (q :: Cat i) -> FunctorK p q
+instance (Categorical p, Categorical q, Coercible p q) => IsFunctor (CoerceF p q) where
+ type Omap (CoerceF _ _) a = a
+ mmap _ = coerce
+
+type SomeCat :: Kind
+data SomeCat = forall i. MkSomeCat (Cat i)
+type Funct :: Cat SomeCat
+data Funct _ _ where
+ MkFunct :: forall {i} {j} (p :: Cat i) (q :: Cat j). forall (f :: FunctorK p q) -> (IsFunctor f) => Funct (MkSomeCat p) (MkSomeCat q)
+type IsCat :: Predicate SomeCat
+class IsCat sp where isCat :: forall r. (forall {i}. forall (p :: Cat i) -> (MkSomeCat p ~ sp, Categorical p) => r) -> r
+instance (Categorical p) => IsCat (MkSomeCat p) where isCat k = k p
+instance Categorical Funct where
+ type Obj Funct = IsCat
+ identity @sp = isCat @sp \p -> MkFunct (IdF p)
+ compose (MkFunct f) (MkFunct g) = MkFunct (ComposeF f g)
+ witnessMor (MkFunct _) = MkEvidence
+
+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
+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
+ fwd _ = mmap f (fwd iso)
+ bwd _ = mmap f (bwd iso)
+
+type Relabel :: forall i. Cat (Cat i)
+data Relabel p q = (Categorical p, Categorical q) => MkRelabel {relabel :: forall a b. a `p` b -> a `q` b}
+instance Categorical Relabel where
+ type Obj Relabel = Categorical
+ identity = MkRelabel identity
+ compose (MkRelabel f) (MkRelabel g) = MkRelabel (compose f g)
+ witnessMor (MkRelabel _) = MkEvidence
+
+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
+instance (Categorical p, Categorical q, IsIso rel, IsIso iso) => IsIso (Iso_Transfer (rel :: IsoK Relabel p q) (iso :: IsoK p a b)) where
+ fwd _ = relabel (fwd rel) (fwd iso)
+ bwd _ = relabel (fwd rel) (bwd iso)
+
+data Iso_RelabelHom :: forall {i}. forall (p :: Cat i) -> IsoK Relabel (Hom p) p
+instance (Categorical p) => IsIso (Iso_RelabelHom p) where
+ fwd _ = MkRelabel unHom
+ bwd _ = MkRelabel MkHom
+
+-- 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')
+-- instance (IsIso relp, IsIso rel) => IsIso (Iso_RelabelNT relp rel) where
+-- fwd _ = MkRelabel \(Naturally f) -> Naturally (relabel (fwd rel) f)
+
+--------------------------------------------------------------------------------
+
+data MorphB :: forall i. Cat i -> i -> i -> Brand
+type MorphK :: forall i. Cat i -> i -> i -> Kind
+type MorphK p a b = OpenKind (MorphB p a b)
+
+type IsMorph :: forall {i} (p :: Cat i) (a :: i) (b :: i). MorphK p a b -> Constraint
+class (Categorical p) => IsMorph (this :: MorphK p a b) where
+ morph :: For this (a `p` b)
+
+type Morph :: forall i. Cat i -> i -> i -> Kind
+data Morph _ _ _ where
+ MkMorph :: forall {i} (p :: Cat i) (a :: i) (b :: i). forall (rw :: MorphK p a b) -> (IsMorph rw) => Morph p a b
+
+instance (Categorical p) => Categorical (Morph p) where
+ type Obj (Morph p) = Obj p
+ identity = MkMorph (Morph_Identity p)
+ compose (MkMorph f) (MkMorph g) = MkMorph (Morph_Compose f g)
+ witnessMor (MkMorph f) = MkEvidence \\ witnessMor (morph f)
+
+data Morph_Identity :: forall {i}. forall (p :: Cat i) -> forall (a :: i). MorphK p a a
+instance forall i (p :: Cat i) (a :: i). (Categorical p, Obj p a) => IsMorph (Morph_Identity p @a) where
+ morph _ = identity
+ {-# INLINE morph #-}
+
+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
+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
+ morph _ = morph t . morph s
+ {-# INLINE morph #-}
+
+data Morph_Dual :: forall {i} (p :: Cat i) (a :: i) (b :: i). MorphK p b a -> MorphK (Dual p) a b
+instance forall i (p :: Cat i) (a :: i) (b :: i) (s :: MorphK p b a). (IsMorph s) => IsMorph (Morph_Dual s) where
+ morph _ = MkDual (morph s)
+ {-# INLINE morph #-}
+
+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)
+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
+ morph _ = (comp (morph s) \\ witnessMor (morph t)) . (map (morph t) \\ witnessMor (morph s))
+ {-# INLINE morph #-}
+
+data Morph_IsoFwd :: forall {i} (p :: Cat i) (a :: i) (b :: i). IsoK p a b -> MorphK p a b
+instance forall i (p :: Cat i) (a :: i) (b :: i) (iso :: IsoK p a b). (IsIso iso) => IsMorph (Morph_IsoFwd iso) where
+ morph _ = fwd iso
+ {-# INLINE morph #-}
+
+data Morph_IsoBwd :: forall {i} (p :: Cat i) (a :: i) (b :: i). IsoK p a b -> MorphK p b a
+instance forall i (p :: Cat i) (a :: i) (b :: i) (iso :: IsoK p a b). (IsIso iso) => IsMorph (Morph_IsoBwd iso) where
+ morph _ = bwd iso
+ {-# INLINE morph #-}
+
+--------------------------------------------------------------------------------
+
+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
+type family Rewrite _ _ _ _ where
+ Rewrite (iso :: IsoK p a b) p a b = Morph_IsoFwd iso
+ Rewrite iso (Dual q) x y = Morph_Dual (Rewrite (Iso_Inv iso) q y x)
+ Rewrite iso q x y = Rewrite' iso q x y (RewriteTouches iso x y)
+
+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
+type family Rewrite' _ _ _ _ _ where
+ -- We check these two cases *after* checking for direct applicability of the
+ -- iso, so either (a) we need to recurse to apply the iso at some location
+ -- deep in the input, or (b) the iso doesn't apply at all. These two cases
+ -- are distinguished by the bool computed by `RewriteTouches`. By only
+ -- recursing when the bool is true, we avoid needlessly requiring *all*
+ -- types of function kind to be functors, and we avoid getting stuck on
+ -- type variables in some circumstances.
+ Rewrite' iso q (f x) (g y) True = RewriteApp iso q f (Dom f) (Cod f) x g (Dom g) (Cod g) y
+ Rewrite' _ q x x False = Morph_Identity q
+ Rewrite' iso q x y _ =
+ TypeError
+ ( ErrText "Could not rewrite type "
+ !// ErrType x
+ !// ErrText " to type "
+ !// ErrType y
+ !// ErrText " along isomorphism "
+ !// ErrType iso
+ !// ErrText " in category "
+ !// ErrType q
+ )
+
+type RewriteTouches :: forall {i} (p :: Cat i) (a :: i) (b :: i). IsoK p a b -> forall {k}. k -> k -> Bool
+type family RewriteTouches _ _ _ where
+ RewriteTouches (_ :: IsoK _ a b) a b = True
+ RewriteTouches iso (f x) (g y) = RewriteTouches iso f g || RewriteTouches iso x y
+ RewriteTouches _ _ _ = False
+
+-- | Helper for `Rewrite'` to ensure functor (co)domains align
+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)
+type family RewriteApp _ _ _ _ _ _ _ _ _ _ where
+ RewriteApp iso q f r q x g r q y = Morph_App (Rewrite iso (r ==> q) f g) (Rewrite iso r x y)
+ RewriteApp _ _ f fdom fcod _ g gdom gcod _ =
+ TypeError
+ ( ErrText "Could not rewrite type application between (functor, dom, cod) triples "
+ !// ErrType (f, fdom, fcod)
+ !// ErrText " and "
+ !// ErrType (g, gdom, gcod)
+ !// ErrText " because the (co)domains do not match"
+ )
+
+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
+rewrite iso = morph (Rewrite iso _ _ _)
+{-# INLINE rewrite #-}
+
+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
+x `rewrittenAlong` iso = rewrite iso x
+{-# INLINE rewrittenAlong #-}
+
+--------------------------------------------------------------------------------
+
+data IsoB :: forall i. Cat i -> i -> i -> Brand
+type IsoK :: forall i. Cat i -> i -> i -> Kind
+type IsoK p a b = OpenKind (IsoB p a b)
+
+type IsIso :: forall {i} (p :: Cat i) (a :: i) (b :: i). IsoK p a b -> Constraint
+class (Categorical p) => IsIso (this :: IsoK p a b) where
+ fwd :: For this (a `p` b)
+ bwd :: For this (b `p` a)
+
+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
+fwd1 iso = comp (fwd iso)
+
+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
+bwd1 iso = comp (bwd iso)
+
+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
+fwd2 iso = bicomp (fwd iso)
+
+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
+bwd2 iso = bicomp (bwd iso)
+
+-- type Fwd :: forall {i} (p :: Cat i) (a :: i) (b :: i). IsoK p a b -> forall {k}. k -> k
+-- type family Fwd _ _ where
+-- Fwd (_ :: IsoK _ a b) a = b
+-- Fwd iso (x y) = (Fwd iso x) (Fwd iso y)
+-- Fwd _ x = x
+
+-- type Bwd :: forall {i} (p :: Cat i) (a :: i) (b :: i). IsoK p a b -> forall {k}. k -> k
+-- type family Bwd _ _ where
+-- Bwd (_ :: IsoK _ a b) b = a
+-- Bwd iso (x y) = (Bwd iso x) (Bwd iso y)
+-- Bwd _ x = x
+
+-- TODO: Iso type, analogous to Morph
+
+--------------------------------------------------------------------------------
+
+data Iso_Identity :: forall {i}. forall (p :: Cat i) -> forall (a :: i). IsoK p a a
+instance (Categorical p, Obj p a) => IsIso (Iso_Identity p @a) where
+ fwd _ = identity
+ bwd _ = identity
+
+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
+instance (IsIso iso0, IsIso iso1) => IsIso (Iso_Compose iso0 iso1) where
+ fwd _ = fwd iso0 . fwd iso1
+ bwd _ = bwd iso1 . bwd iso0
+
+data Iso_Inv :: forall {i} (p :: Cat i) (a :: i) (b :: i). IsoK p b a -> IsoK p a b
+instance (IsIso iso) => IsIso (Iso_Inv iso) where
+ fwd _ = bwd iso
+ bwd _ = fwd iso
+
+data Iso_Coerce :: forall (a :: Type) (b :: Type) -> IsoK Function a b
+instance (Coercible a b) => IsIso (Iso_Coerce a b) where
+ fwd _ = coerce
+ bwd _ = coerce
+
+data Iso_Coerce1 :: forall {i} (p :: Cat i). forall (a :: i -> Type) (b :: i -> Type) -> IsoK (p ==> Function) a b
+instance (Categorical p, FunctorialOn p Function a, FunctorialOn p Function b, Coercible a b) => IsIso (Iso_Coerce1 @p a b) where
+ fwd _ = Naturally coerce
+ bwd _ = Naturally coerce
+
+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
+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
+ fwd _ = Binaturally coerce
+ bwd _ = Binaturally coerce
+
+data Iso_Swap :: forall (a :: Type) (b :: Type) -> IsoK Function (Tuple2 a b) (Tuple2 b a)
+instance IsIso (Iso_Swap a b) where
+ fwd _ (x, y) = (y, x)
+ bwd _ (y, x) = (x, y)
+
+data Iso_Assoc :: forall (a :: Type) (b :: Type) (c :: Type) -> IsoK Function (Tuple2 (Tuple2 a b) c) (Tuple2 a (Tuple2 b c))
+instance IsIso (Iso_Assoc a b c) where
+ fwd _ ((x, y), z) = (x, (y, z))
+ bwd _ (x, (y, z)) = ((x, y), z)
+
+--------------------------------------------------------------------------------
+
+type Transport :: forall (a :: Type) (b :: Type). IsoK Function a b -> Type
+newtype Transport @a @_ _ = MkTransport {unTransport :: a}
+
+data Iso_Transport :: forall (a :: Type) (b :: Type). forall (iso :: IsoK Function a b) -> IsoK Function b (Transport iso)
+instance (IsIso iso) => IsIso (Iso_Transport iso) where
+ fwd _ = MkTransport . bwd iso
+ bwd _ = fwd iso . unTransport
+
+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
+transport iso = rewrite (Iso_Transport iso)
+{-# INLINE transport #-}
+
+--------------------------------------------------------------------------------
+
+class Sg a where (++) :: Biendo a
+
+instance (Sg a, Sg b, Sg c) => Sg (Tuple2 (Tuple2 a b) c) where
+ ((a1, b1), c1) ++ ((a2, b2), c2) = ((a1 ++ a2, b1 ++ b2), c1 ++ c2)
+
+-- instance (Sg a, Sg b, Sg c) => Sg (Tuple2 a (Tuple2 b c)) where
+-- (++) = rewrite (Iso_Assoc a b c) ((++) @(Tuple2 (Tuple2 a b) c))
+
+instance (IsIso iso, Sg b) => Sg (Transport (iso :: IsoK Function a b)) where
+ (++) = transport iso ((++) @b)
+
+deriving via Transport (Iso_Inv (Iso_Assoc a b c)) instance (Sg a, Sg b, Sg c) => Sg (Tuple2 a (Tuple2 b c))
+
+--------------------------------------------------------------------------------
+
+type Transport1 :: forall {i} (p :: Cat i) (a :: i -> Type) (b :: i -> Type). IsoK (p ==> Function) a b -> i -> Type
+newtype Transport1 @_ @a @_ _ x = MkTransport1 {unTransport1 :: a x}
+
+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
+ type Dom (Transport1 @p _) = p
+ type Cod (Transport1 @_ _) = Function
+ map f = coerce $ bwd1 iso . map f . fwd1 iso \\ witnessMor f
+
+--------------------------------------------------------------------------------
+
+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
+newtype Transport2 @_ @_ @a @_ _ x y = MkTransport2 {unTransport2 :: a x y}
+
+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
+ type Dom (Transport2 @_ @q _ _) = q
+ type Cod (Transport2 @_ @_ _ _) = Function
+ map f = coerce $ bwd2 iso . map f . fwd2 iso \\ witnessMor f
+
+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
+ type Dom (Transport2 @p @_ _) = p
+ type Cod (Transport2 @_ @q _) = q ==> Function
+ map @x @y f =
+ Naturally (coerce $ bwd2 iso . nmap f . fwd2 iso)
+ \\ (b `preservesObj` x)
+ \\ (b `preservesObj` y)
+ \\ witnessMor f
+
+-- 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)
+-- 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
+-- fwd _ = Binaturally MkTransport2 . bwd iso
+-- bwd _ = fwd iso . Binaturally unTransport2
+--
+-- 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
+-- transport2 iso = rewrite (Iso_Transport2 iso)
+-- {-# INLINE transport2 #-}
+
+--------------------------------------------------------------------------------
+
+-- 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
+-- type Obj (Transport2 (_ :: IsoK _ _ b)) = Obj b
+--
+-- -- identity @x = transport2 iso (identity @b @x)
+-- -- witnessMor = transport2 iso (witnessMor @b)
+-- identity = MkTransport2 (bwd iso $^^ identity)
+-- compose (MkTransport2 f) (MkTransport2 g) = MkTransport2 (bwd iso $^^ (compose (fwd iso $^^ f) (fwd iso $^^ g)))
+-- witnessMor (MkTransport2 f) = MkEvidence \\ witnessMor (fwd iso $^^ f)
+
+--------------------------------------------------------------------------------
+
+-- type Pointwise :: forall {i} {j}. Cat j -> Cat (i -> j)
+-- newtype Pointwise q f g = MkPointwise (forall a. f a `q` g a)
+--
+-- instance (Categorical q, Obj q ~ Always) => Categorical (Pointwise q) where
+-- identity = MkPointwise identity
+-- compose (MkPointwise a) (MkPointwise b) = MkPointwise (compose a b)
+
+-- data Iso_Hom :: forall {i}. forall (p :: Cat i) -> IsoK (Dual p ==> p ==> Function) p (Hom p)
+-- instance (Categorical p) => IsIso (Iso_Hom p) where
+-- fwd _ = Binaturally \ @x @y -> ()
+
+-- 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
+-- instance IsIso (Iso_Naturally iso) where
+
+-- deriving via Transport2 (Iso_Coerce @(q x) @(Hom q x)) instance (Categorical q, Obj q ~ Always) => Functorial (Pointwise q x)
+
+type Stupid :: forall {i}. Cat i
+data Stupid _ _ = MkStupid
+
+instance Categorical Stupid where
+ identity = MkStupid
+ compose MkStupid MkStupid = MkStupid
+
+-- type Whoa0 a = Iso_Coerce1 @(Hom Stupid) (Stupid a) (Hom Stupid a)
+-- type Whoa1 = Iso_RelabelHom Stupid
+-- type Whoa2 a = Iso_Transfer Whoa1 (Whoa0 a)
+
+-- deriving via Transport1 (Iso_Transfer (Iso_RelabelHom Stupid) (Iso_Coerce1 @(Hom Stupid) (Stupid a) (Hom Stupid a))) instance Functorial (Stupid a)
+
+-- deriving via Transport2 (Iso_Coerce2 @(Dual (Hom Stupid)) @(Hom Stupid) Stupid (Hom Stupid)) instance Functorial Stupid
