flock_functors_natural_transformations.md

We need to consider (Cat..) as the outer category for push/pull cycle.

We need to define endofunctors for Cat, Dur, Lit, Nat. How can we do this?

Well it needs to be of the form:

f : CatX -> CatX
f : CatX(a) -> CatX(a)
f : CatX(a -> b) -> CatX(a -> b)

CatX is literally Mod-like when there are functors to and from Mod, some Lit:

f : CatX -> CatY is literally (ModX -> ModY)-like when there are natural transformations to and from ModX -> ModY, some LitX -> LitY.

Explicit definitions:

• CatX -> CatY is categorically ModX -> ModY-like when it is isomorphic to both ModX -> ModY and some CatZ -> CatW:

isofunctor'(functor'(CatX -> CatY) -> functor'(ModX -> ModY))

CatX -> CatY = ModX -> ModY

We may omit CatZ -> CatW without loss of generality.

• CatX -> CatY is durationally ModX -> ModY-like when there is a functor to ModX -> ModY and a functor from ModX -> ModY to some DurX -> DurY:

functor'(functor'(CatX -> CatY) -> functor'(ModX -> ModY))
functor'(functor'(ModX -> ModY) -> functor'(DurX -> DurY))

(CatX -> CatY) -> (ModX -> ModY) -> (DurX -> DurY) (-> (CatX -> CatY))

• CatX -> CatY is literally ModX -> ModY-like when there are functors to and from ModX -> ModY, some LitX -> LitY:

functor'(functor'(CatX -> CatY) -> functor'(ModX -> ModY))
functor'(functor'(ModX -> ModY) -> functor'(CatX -> CatY))

functor'(functor'(ModX -> ModY) -> functor'(LitX -> LitY))
functor'(functor'(LitX -> LitY) -> functor'(ModX -> ModY))

(CatX -> CatY) <-> (ModX -> ModY) <-> (LitX -> LitY) (<-> (DurX -> DurY) <-> (CatX -> CatY))

• CatX -> CatY is naturally ModX -> ModY-like when it is isomorphic to both the ModX -> ModY and some NatX -> NatY:

isofunctor'(functor'(CatX -> CatY) -> functor'(ModX -> ModY))
isofunctor'(functor'(ModX -> ModY) -> functor'(NatX -> NatY))

(CatX -> CatY) = (ModX -> ModY) = (NatX -> NatY) (= (LitX -> LitY) = (DurX -> DurY) = (CatX -> CatY))

Explicit definitions, dropped to morphisms:

• a -> b is categorically ModX -> ModY-like when it is isomorphic to both ModX -> ModY and some CatZ -> CatW:

iso'((a -> b) -> (mx -> my))

CatX -> CatY = ModX -> ModY

We may omit CatZ -> CatW without loss of generality.

• a -> b is durationally ModX -> ModY-like when there is a functor to ModX -> ModY and a functor from ModX -> ModY to some DurX -> DurY:

(a -> b) -> (mx -> my)
(mx -> my) -> (dx -> dy)

(a -> b) -> (mx -> my) -> (dx -> dy)

(CatX -> CatY) -> (ModX -> ModY) -> (DurX -> DurY) (-> (CatX -> CatY))

• a -> b is literally ModX -> ModY-like when there are functors to and from ModX -> ModY, some LitX -> LitY:

(a -> b) -> (mx -> my)
(mx -> my) -> (lx -> ly)
(lx -> ly) -> (mx -> my)
(mx -> my) -> (a -> b)

(a -> b) <-> (mx -> my) <-> (lx -> ly)

(CatX -> CatY) <-> (ModX -> ModY) <-> (LitX -> LitY) (<-> (DurX -> DurY) <-> (CatX -> CatY))

• CatX -> CatY is naturally ModX -> ModY-like when it is isomorphic to both the ModX -> ModY and some NatX -> NatY:

iso'((a -> b) -> (mx -> my))
iso'((mx -> my) -> (nx -> ny))

(a -> b) = (mx -> my) = (nx -> ny)

(CatX -> CatY) = (ModX -> ModY) = (NatX -> NatY) (= (LitX -> LitY) = (DurX -> DurY) = (CatX -> CatY))

Mod-dependent-endofunctor: (CatX : Mod-like)! => (f : functor'(CatX -> CatX)) "f is an endofunctor on any Mod-like category"

Mod-endofunctor: (CatX : Mod-like)? => (f : functor'(CatX -> CatX)) "Whether or not CatX is Mod-like, f is an endofunctor expression on CatX"

!?

()! forces uniqueness (there is a single option) (for booleans, truth, which is the default anyway)
()? forces optionality (there are multiple options) (for booleans, completeness)

(expr)! := expr :#  1
(expr)? := expr :# (2 + _)

In other words, `!` is the postfix (unary, operator) form of `_`.