Skip to content

Instantly share code, notes, and snippets.

@andrevidela

andrevidela/NaturalTransformation.idr

Created February 16, 2025 11:16
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save andrevidela/9f0d16c2b7dc4d75a6c30a22944263c5 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save andrevidela/9f0d16c2b7dc4d75a6c30a22944263c5 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
NaturalTransformation.idr
module Data.Category.NaturalTransformation
import public Data.Category.Functor
import Data.Category.Iso
import Syntax.PreorderReasoning
import Proofs.Congruence
import Proofs.Extensionality
import Proofs.UIP
import Control.Order
import Control.Relation
%hide Prelude.Functor
%hide Prelude.(|>)
%hide Prelude.Ops.infixl.(|>)
%unbound_implicits off
universal_property : (a : Type) -> (b : Type) -> (p : a -> b -> Type) -> Type
universal_property a b p = (x : a) -> (y : b ** (p x y
, (z : b) -> (p x z, z === y)))
-- A natural transformation between functors f and g between categories c and d
-- it is defined by it's component (x : c) -> F x -> G x
public export
record (=>>) {0 cObj, dObj : Type} {0 c : Category cObj} {0 d : Category dObj}
(f, g : Functor c d) where
constructor MkNT
component : (v : cObj) -> (f.mapObj v) ~> (g.mapObj v)
-- component x
-- x F x ───────> G x
-- │ │ │
-- m│ F m │ │ G m
-- │ │ │
-- v v v
-- y F y ───────> G y
-- component y
0 commutes : (0 x, y : cObj) -> (m : x ~> y) ->
let 0 top : f.mapObj x ~> g.mapObj x
top = component x
0 bot : f.mapObj y ~> g.mapObj y
bot = component y
0 left : f.mapObj x ~> f.mapObj y
left = f.mapHom _ _ m
0 right : g.mapObj x ~> g.mapObj y
right = g.mapHom _ _ m
0 comp1 : f.mapObj x ~> g.mapObj y
comp1 = top |> right
0 comp2 : f.mapObj x ~> g.mapObj y
comp2 = left |> bot
in comp1 === comp2
-- two natural transformations are equal if their components are equal
public export
record NTEq {0 o1, o2 : Type} {0 c1 : Category o1} {0 c2 : Category o2} {a, b : Functor c1 c2} (n1, n2 : a =>> b) where
constructor MkNTEq
0 sameComponent : (v : o1) -> n1.component v === n2.component v
public export
0 ntEqToEq : {0 o1, o2 : Type} -> {c1 : Category o1} -> {c2 : Category o2} -> {f, g : Functor c1 c2} -> {n1, n2 : f =>> g} ->
NTEq n1 n2 -> n1 === n2
ntEqToEq (MkNTEq sameComponent) {n1 = MkNT n1 p1} {n2 = MkNT n2 p2} =
cong2Dep0
{t3 = f =>> g}
MkNT
(funExtDep $ sameComponent)
(funExtDep0 $ \x => funExtDep0 $ \y => funExtDep $ \z => UIP _ _)
public export
ntTrans : {c1, c2 : _} -> {f1, f2 : Functor c1 c2} -> {a, b, c : f1 =>> f2} ->
NTEq a b -> NTEq b c -> NTEq a c
ntTrans x y = MkNTEq $ \vx => x.sameComponent vx `trans` y.sameComponent vx
public export
ntRefl : {c1, c2 : Category _} -> {f1, f2 : Functor c1 c2} -> {a : f1 =>> f2} -> NTEq a a
ntRefl = MkNTEq (\_ => Refl)
public export
ntsym : {c1, c2 : Category _} -> {f1, f2 : Functor c1 c2} -> {a, b : f1 =>> f2} -> NTEq a b -> NTEq b a
ntsym (v) = MkNTEq (\vx => sym (v.sameComponent vx))
public export
[NTETrans] {c1, c2 : Category _} -> {f1, f2 : Functor c1 c2} -> Transitive (f1 =>> f2) NTEq where
transitive = ntTrans
public export
[NTESym] {c1, c2 : Category _} -> {f1, f2 : Functor c1 c2} -> Symmetric (f1 =>> f2) NTEq where
symmetric = ntsym
public export
[NTERefl] {c1, c2 : Category _} -> {f1, f2 : Functor c1 c2} -> Reflexive (f1 =>> f2) NTEq where
reflexive = ntRefl
public export
[NTEQ] {c1, c2 : Category _} -> {f1, f2 : Functor c1 c2} ->
Preorder (f1 =>> f2) NTEq using NTERefl NTETrans where
-- Horizontal composition of natural transformations
public export
(!!>) : {0 cObj, dObj : Type} -> {0 c : Category cObj} -> {d : Category dObj}
-> {f, g, h : Functor c d}
-> f =>> g -> g =>> h -> f =>> h
(!!>) nat1 nat2 = MkNT (\x => nat1.component x |> nat2.component x) compProof
where
0 compProof : (0 x, y : cObj) -> (m : x ~> y) ->
let 0 n1, n2 : f.mapObj x ~> h.mapObj y
n1 = f.mapHom x y m |> (nat1.component y |> nat2.component y)
n2 = (nat1.component x |> nat2.component x) |> h.mapHom x y m
in n2 === n1
compProof x y m = sym (d.compAssoc _ _ _ _ _ _ _) `trans`
glueSquares (nat1.commutes x y m) (nat2.commutes x y m)
public export
identity : {0 o1, o2 : Type} -> {c1 : Category o1} -> {c2 : Category o2} ->
{f : Functor c1 c2} -> f =>> f
identity = MkNT
(\x => f.mapHom x x (c1.id x) )
(\x, y, m => let 0 mh = presComp f x x y (c1.id x) m
0 idr := c1.idRight _ _ m
0 idl := c1.idLeft _ _ m
0 mh2 := presComp f x y y m (c1.id y)
in Calc $
|~ (F_m (c1.id x)) |> F_m m
~~ F_m ((c1.id x) |> m) ..< mh
~~ F_m m ... (cong F_m idl)
~~ F_m (m |> c1.id y) ..< (cong F_m idr)
~~ F_m m |> F_m (c1 .id y) ... mh2)
||| Vetical composition of natural transformations
public export
(-*-) : {0 o1, o2, o3 : Type} ->
{0 a : Category o1} -> {0 b : Category o2} -> {c : Category o3} ->
{l, k : Functor a b} ->
{g, h : Functor b c} ->
k =>> l ->
g =>> h ->
(k !*> g) =>> (l !*> h)
(-*-) (MkNT n2 n2p) (MkNT n1 n1p) = MkNT
(\v => n1 (k.mapObj v) |> h.mapHom (k.mapObj v) (l.mapObj v) (n2 v))
(\x, y, m => let
H : {a, b : o2} -> a ~> b -> (h.mapObj a) ~> (h.mapObj b)
H = h.mapHom _ _
L : {a, b : o1} -> a ~> b -> (l.mapObj a) ~> (l.mapObj b)
L = l.mapHom _ _
G : {a, b : o2} -> a ~> b -> (g.mapObj a) ~> (g.mapObj b)
G = g.mapHom _ _
K : {a, b : o1} -> a ~> b -> (k.mapObj a) ~> (k.mapObj b)
K = k.mapHom _ _
in Calc $
|~ ((n1 (k.mapObj x) |> H (n2 x)) |> H (L m))
~~ (n1 (k.mapObj x) |> (H (n2 x) |> H (L m))) ..<(c.compAssoc _ _ _ _ (n1 (k.mapObj x)) (H (n2 x)) (H (L m)))
~~ (n1 (k.mapObj x) |> (H (n2 x |> L m))) ..<(cong (n1 (k.mapObj x) |> ) (h.presComp _ _ _ (n2 x) (L m)))
~~ (G (n2 x |> L m) |> n1 (l.mapObj y)) ...(n1p (k.mapObj x) (l.mapObj y) (n2 x |> L m))
~~ (G (K m |> n2 y) |> n1 (l.mapObj y)) ...(cong (\xn => G xn |> n1 (l.mapObj y)) (n2p _ _ m))
~~ ((G (K m) |> G (n2 y)) |> n1 (l.mapObj y)) ...(cong (\x => x |> n1 (l.mapObj y)) (g.presComp _ _ _ (K m) (n2 y)))
~~ (G (K m) |> (G (n2 y) |> n1 (l.mapObj y))) ..<(c.compAssoc _ _ _ _ (G (K m)) (G (n2 y)) (n1 (l.mapObj y)))
~~ (G (K m) |> (n1 (k.mapObj y) |> H (n2 y))) ..<(cong (G (K m) |> ) (n1p _ _ (n2 y)))
)
parameters {0 o1, o2 : Type} {0 c : Category o1} {0 d : Category o2} {f, g : Functor c d}
public export
ntIdentityRight : (n : f =>> g) ->
NTEq (n !!> identity {f = g}) n
ntIdentityRight nt = MkNTEq $ \vx => Calc $
|~ (|:>) d (nt.component vx) (g.mapHom vx vx (c.id vx))
~~ (|:>) d (nt.component vx) (d.id (g.mapObj vx))
...(cong ((|:>) d (nt.component vx)) (g.presId vx))
~~ nt.component vx
...((d.idRight _ _ _))
public export
ntIdentityLeft : (n : f =>> g) ->
NTEq (identity {f = f} !!> n) n
ntIdentityLeft nt = MkNTEq $ \vx => Calc $
|~ (|:>) d (f.mapHom vx vx (c.id vx)) (nt .component vx)
~~ (|:>) d (d.id (f.mapObj vx)) (nt.component vx)
...(cong (\nx => (|:>) d nx (nt.component vx)) (f.presId vx))
~~ nt.component vx ...(d.idLeft _ _ _)
public export
ntAssoc : {h, i : Functor c d} -> (n1 : f =>> g) -> (n2 : g =>> h) -> (n3 : h =>> i) ->
NTEq (n1 !!> (n2 !!> n3)) ((n1 !!> n2) !!> n3)
ntAssoc a b c = MkNTEq $ \vx => d.compAssoc _ _ _ _ (a.component vx) (b.component vx) (c.component vx)
public export
ntProd : {h : Functor c d} ->
{n1, n2: f =>> g} -> {n1', n2' : g =>> h} ->
NTEq n1 n2 -> NTEq n1' n2' -> NTEq (n1 !!> n1') (n2 !!> n2')
ntProd (MkNTEq comp1) (MkNTEq comp2) = MkNTEq $ \vx => Calc $
|~ (n1.component vx) |> (n1'.component vx)
~~ (n2.component vx) |> (n1'.component vx) ...(cong (|> n1'.component vx) (comp1 vx))
~~ (n2.component vx) |> (n2'.component vx) ...(cong (n2.component vx |>) (comp2 vx))
public export
distribute : {c : Category _} -> {f1, f2, f3 : Functor c c} ->
{a : f1 =>> f2} -> {b : f2 =>> f3} ->
NTEq ((a -*- a) !!> (b -*- b)) ((a !!> b) -*- (a !!> b))
distribute {a = a@(MkNT acomponent asq)} {b = b@(MkNT bcomponent bsq)} = MkNTEq $ \vx => Calc $
|~ (a -*- a).component vx |> (b -*- b).component vx
~= (a.component (f1.mapObj vx) |> f2.mapHom (f1.mapObj vx) (f2.mapObj vx) (a.component vx)) |> (b -*- b).component vx
~= (a.component (f1.mapObj vx) |> f2.mapHom (f1.mapObj vx) (f2.mapObj vx) (a.component vx)) |> (b.component _ |> f3.mapHom _ _ (b.component vx))
~~ (a.component (f1.mapObj vx) |> f2.mapHom (f1.mapObj vx) (f2.mapObj vx) (a.component vx)) |> ((f2.mapHom _ _ (b.component vx)) |> (b.component (f3.mapObj vx)))
...(cong ((a.component (f1.mapObj vx) |> f2.mapHom (f1.mapObj vx) (f2.mapObj vx) (a.component vx)) |>) (bsq _ _ (b.component vx)))
~~ (a.component (f1.mapObj vx)) |> ((f2.mapHom (f1.mapObj vx) (f2.mapObj vx) (a.component vx)) |> ((f2.mapHom (f2.mapObj vx) (f3.mapObj vx) (b.component vx)) |> (b.component (f3.mapObj vx))))
..<(c.compAssoc _ _ _ _ (a.component (f1.mapObj vx))(f2.mapHom (f1.mapObj vx) (f2.mapObj vx) (a.component vx))((f2.mapHom (f2.mapObj vx) (f3.mapObj vx) (b.component vx)) |> (b.component (f3.mapObj vx))))
~~ (a.component (f1.mapObj vx)) |> (((f2.mapHom (f1.mapObj vx) (f2.mapObj vx) (a.component vx)) |> (f2.mapHom (f2.mapObj vx) (f3.mapObj vx) (b.component vx))) |> (b.component (f3.mapObj vx)))
...(cong ((a.component (f1.mapObj vx)) |>) (c.compAssoc _ _ _ _ (f2.mapHom (f1.mapObj vx) (f2.mapObj vx) (a.component vx)) (f2.mapHom (f2.mapObj vx) (f3.mapObj vx) (b.component vx)) (b.component (f3.mapObj vx))))
~~ (a.component (f1.mapObj vx)) |> ((f2.mapHom (f1.mapObj vx) (f3.mapObj vx) (a.component vx |> b.component vx)) |> (b.component (f3.mapObj vx)))
..<(cong (\nx => (a.component (f1.mapObj vx) |> (nx |> b.component (f3.mapObj vx)))) (f2.presComp (f1.mapObj vx) (f2.mapObj vx) (f3.mapObj vx) (a.component vx) (b.component vx)))
~~ (a.component (f1.mapObj vx)) |> ((b.component (f1.mapObj vx)) |> (f3.mapHom (f1.mapObj vx) (f3.mapObj vx) ((a.component vx) |> (b.component vx))))
..<(let bb = bsq (f1.mapObj vx) (f3.mapObj vx) (acomponent vx |> bcomponent vx) in cong (a.component (f1.mapObj vx) |>) bb)
~~ ((a.component (f1.mapObj vx)) |> (b.component (f1.mapObj vx))) |> (f3.mapHom (f1.mapObj vx) (f3.mapObj vx) ((a.component vx) |> (b.component vx)))
...(c.compAssoc _ _ _ _ (a.component (f1.mapObj vx)) (b.component (f1.mapObj vx)) (f3.mapHom (f1.mapObj vx) (f3.mapObj vx) ((a.component vx) |> (b.component vx))))
~= ((a !!> b) -*- (a !!> b)).component vx
-- whiskering is a special case of the above
public export
(*-) : {a : Category _} -> {b : Category _} -> {c : Category _} ->
(f : Functor a b) -> {g, h : Functor b c} -> g =>> h -> (f !*> g) =>> (f !*> h)
(*-) f n = identity {f} -*- n
public export
(-*) : {0 b : Category _} -> {c : Category _} -> {d : Category _} ->
{g, h : Functor b c} -> g =>> h -> (f : Functor c d) -> (g !*> f) =>> (h !*> f)
(-*) n f = n -*- identity {f}
-- A Natural isomophism is a natural transformation which component is a bijection
public export
record (=~=) {0 cObj, dObj : Type} {0 c : Category cObj} {0 d : Category dObj} (f, g : Functor c d) where
constructor MkNaturalIsomorphism
nat : f =>> g
φ : (v : cObj) -> (~:>) d (g.mapObj v) (f.mapObj v)
0 η_φ : (v : cObj) -> (nat.component v |> φ v) {a = (f.mapObj v), b = (g.mapObj v), c = (f.mapObj v)}
=== d.id (f.mapObj v)
0 φ_η : (v : cObj) -> (φ v |> nat.component v) {a = (g.mapObj v), b = (f.mapObj v), c = (g.mapObj v)}
=== d.id (g.mapObj v)
-- for each natural isomorphism extract the isomorphism
public export
getIso : {0 cObj, dObj : Type} -> {0 c : Category cObj} -> {0 d : Category dObj} ->
{f, g : Functor c d} ->
f =~= g -> (v : cObj) -> Iso d (f.mapObj v) (g.mapObj v)
getIso nat v = MkIso (nat.nat.component v) (nat.φ v) (nat.η_φ v) (nat.φ_η v)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment