Initial commit

2.typ

@@ -0,0 +1,811 @@
+#import "template/lib.typ": *
+#import "template/math.typ": *
+#import "@preview/fletcher:0.5.8" as fletcher: diagram, node, edge
+#import "@preview/curryst:0.6.0": rule, prooftree
+#import "@preview/pinit:0.2.2": *
+
+#let scheme = dark
+#let edge = edge.with(stroke: scheme.fg, crossing-fill: scheme.bg)
+#let prooftree = prooftree.with(stroke: stroke(thickness: 0.05em, paint: scheme.fg))
+
+#show: paper.with(scheme: scheme, title: "SEMPL", subtitle: "Lesson 1")
+
+#let environment = environment.with(scheme: scheme)
+#let environment_ = environment_.with(scheme: scheme)
+#let theorem = environment.with(name: "Theorem")
+#let proposition = environment.with(name: "Proposition")
+#let definition = environment.with(name: "Definition")
+#let remark = environment.with(name: "Remark", counter: none)
+#let exercise = environment.with(name: "Exercise")
+#let proof = environment_.with(name: "Proof of", follows: true)
+#let solution = environment_.with(name: "Solution of", follows: true)
+#let example = environment_.with(name: "Example")
+#let notation = environment_.with(name: "Notation", counter: none)
+
+`guillaume.geoffroy@irif.fr`
+
+#outline()
+
+= (Some) Universal algrebra with binders
+
+E.g. monoid = "Structure" over signature $(⋅, 1)$ satisfying some equations
+
+Idea :
+- Model of the $lambda$-calculus
+- Structure over signature $("Lambda", "App")$ satisfying
+  $
+    &beta : "App"("Lambda"(x . t), u) = t[x := u]\
+    &eta : "Lambda"(x . "App"(t, x)) = t
+  $
+
+== Algrebraic syntax with binders
+
+For a formal and abstract presentation
+- #link("https://lics.siglog.org/archive/1999/GabbayPitts-ANewApproachtoAbstr.html")[Gabbay & Pitts (LICS 1999)]
+- #link("https://lics.siglog.org/1999/FiorePlotkinTuri-AbstractSyntaxandVa.html")[Fiore, Plotkin & Tury (LICS 1999)]
+
+An algebraic signature with binders is a pair $Sigma = ("Op"_Sigma, "Ar"_Sigma)$ with
+- $"Op"_Sigma$ is a set (operations)
+- $"Ar"_Sigma$ is $in "Op"_Sigma --> "List"(NN)$ (arity)
+
+#example[
+  $
+    Sigma_1 = ({"Lam", "App"}, cases("Lam" mapsto (1), "App" mapsto (0, 0))})
+  $
+]
+
+#definition[
+  Let $Sigma$ be an algebraic signature.
+
+  The set of terms over $Lambda$ is defined by the following grammar, modulo
+  $alpha$-renaming.
+
+  $
+    t := &x " (variable)"\
+         &alpha((x_(1, 1), ..., x_(1, n_1))⋅t_1, ..., (x_(k, 1), ..., x_(k, n_k))⋅t_k)\
+         &"Where " alpha in "Op"_Sigma " and " (n_1, ..., n_k) = "Ar"_Sigma (alpha)
+         &"and " forall i, x_(i, 1), ..., x_(i, n_i) " are pairwise " eq.not
+  $
+]
+
+#example[
+  $"Term"(Sigma_Lambda)$ is the set of pure $lambda$-terms (modulo $alpha$)
+]
+
+#exercise[
+  Find a construction in an actual programming language that has arity $(1, 2)$.
+
+]
+#solution[
+  ```
+  function [] -> e
+           | h::t -> f      -> (0, 2)
+  function Leaf(x) -> e
+           | Node(l, r) -> f
+  ```
+]
+
+#notation[
+  Let $Sigma$ be a signature, $x_1, ..., x_n$ pairwise $eq.not$ variables and
+  t, u_1, ..., u_n terms over $Lambda$.
+
+  We write $t[x_1 := u_1, ..., x_n := u_1]$ for the simultaneous capture-avoiding
+  (#sym.arrow.l.r.double compatible with $eq.not$) substitution of each free
+  occurrence of $x_i$ with $u_i$.
+]
+
+#let Lam = $"Lam"$
+#let App = $"App"$
+#let Op = $"Op"$
+#let Ar = $"Ar"$
+#let Type = $"Type"$
+#let Rule = $"Rule"$
+
+#exercise[
+  - $(Lam(x ⋅ App(x, y)))[x := a, y := b] = Lam(x ⋅ App(x, b))$
+  - $(App(x, y))[x := y, y := x] = App(y, x)$
+  - $(Lam(x ⋅ App(y, x)))[y := x] = Lam(z ⋅ App(x, z))$
+]
+
+#exercise[
+  $Sigma$ signature, $t$, $u$, $v$ terms, $x$, $y$ variables.
+
+  If $y$ not free in $t$, prove $t[x := u[y := v]] = t[x := u][y := v]$
+]
+
+#solution[
+  $
+    y[x := u[y := z]] := y\
+    y[x := u][y := z] := z
+  $
+]
+
+#proposition[
+  Let $Sigma$ signature, $t, u_1, ..., u_n, v_1, ..., v_n$ terms over $Sigma$
+  $x_1, ..., x_n, y_1, ..., y_n$ variables. If no $y_i$ is free in $t$ then
+
+  $t[x_1 := u_1[overline(y) := overline(v)], ..., x_n := u_m [overline(y) := overline(v)]]
+  = t[overline(x) := overline(u)][overline(y) := overline(v)]$
+]
+
+#remark[
+  Also true if the list $overline(x)$ contains all of the free variables of $t$,
+  regardless of whether any $y_i$ is free in $t$.
+]
+
+#definition[
+  Given a signature $Sigma$, a simple type system over $Sigma$ is a pair
+  $tau = ("Type"_tau, "Rule"_tau)$ where :
+  - $"Type"_tau$ is a set
+  - $"Rule"_tau in product_cases(delim: #none, alpha in "Op"_Sigma, (n_1, ..., n_k)=Ar_Sigma(alpha))$
+]
+
+Intuitively :
+#prooftree(
+  rule(
+    $Gamma, x_(1, 1) : A_(1, 1), ..., x_(1, n_1) : A_(1, n_1) tack t_1 : B_1$,
+    $...$,
+    $Gamma, x_(k, 1) : A_(k, 1), ..., x_(k, n_k) : A_(k, n_k) tack t_k : B_k$,
+    $Gamma tack alpha((overline(x_1))⋅t_1, ..., (overline(x_k))⋅t_k) : C$
+  ),
+)
+$
+  <=> Rule_tau (alpha) = (overline(A_1), B_1, ..., overline(A_k), B_k, C)
+$
+
+#example[
+  Let $Type_tau_(S T)$ be generated by
+  $
+    A, b ::= &a | b | ... " (atomic types)"\
+             | &A -> B
+  $
+  $
+    Sigma_S T = (union_(A, B) {Lam_(A, B), App_(A, B)}, cases(Lam_(A, B) mapsto (1), App_(A, B) mapsto (0, 0))})
+  $
+
+  $Rule_tau_(S T) (App_(A, B)) = (A -> B, A, B)$
+  #prooftree(
+    rule(
+      $Gamma tack t : A -> B$,
+      $Gamma tack u : B$,
+      $Gamma tack App_(A, B)(t, u) : B$
+    ),
+  )
+
+  $Rule_tau_(S T) (Lam_(A, B)) = (A, B, A -> B)$
+  #prooftree(
+    rule(
+      $Gamma tack t : A$,
+      $Gamma tack u : B$,
+      $Gamma tack Lam(A, B)(x⋅t) : A -> B$
+    ),
+  )
+]
+
+#definition[
+  Let $Sigma, tau$ be a simply typed algebraic signature (STAS).
+  - A context is a tuple $((x_1 : A_1), ..., (x_n : A_n))$ (written $x_1 : A_1, ..., x_n : A_n$) when the $x_i$ are
+    pairwise $eq.not$ variables and the $A_i$ are types.
+  - The context $Gamma = x_i : A_i, ..., x_n : A_n$ binds the variables $x_1, ..., x_n : B_k$
+  - A context $Gamma$ _closes_ a term $t$ if it binds all its free variables
+  - A _term with context_ is a pair $(Gamma, t)$ (written $Gamma tack t$) where
+    $t$ is a term and $Gamma$ is a context that closes $t$.
+  - A _typing judgement_ is a triple $(Gamma, t, B)$ (written $Gamma tack t : B$)
+    where $Gamma tack t$ is a term with context and $B$ is a type.
+]
+
+#let ol = overline
+
+#definition[
+  Let $(Sigma, tau)$ be a STAS. The set of (intuistionistically) valid judgements
+  for $(Sigma, tau)$ is the least set of typing judgements s.t :
+  - $forall x, A quad x : A tack x : A$ is valid
+  - $forall alpha in Op_Sigma$ with $(n_1, ..., n_k) = Ar_Sigma(alpha)$ and
+    $(overline(A_1), B_1, ..., overline(A_k), ..., B_k, C) = Rule_Sigma (alpha)$
+    $
+      forall Gamma, overline(x_1) : overline(A_1) tack t_1, B_1, ..., Gamma, ol(x_k) : ol(A_k) tack t_k : B_k "valid"\
+      forall Gamma tack alpha((ol(x_1))⋅t_1, ..., (ol(x_k))⋅t_k) : C "is valid"
+    $
+  - permutation
+    $ &forall m in NN quad forall sigma : {1, ..., m} --> {1, ..., m} "bijection"\
+      &forall A_1, ..., A_m "types"\
+      &forall x_1 : A_(sigma(1)), ..., x_m : A_(sigma(m)) tack t : B "valid"\
+      &forall y_1, ..., y_m "pairwise" eq.not "variables"
+      y_1 : A_1, ..., y_m : A_m tack t[x_1 := y_(sigma(1)), ..., x_m := y_(sigma(m))] : B "is valid"
+    $
+  - contraction
+    $ &forall m in NN quad forall sigma : {1, ..., m} --> {1, ..., n}\
+      &forall A_1, ..., A_n "types"\
+      &forall x_1 : A_(sigma(1)), ..., x_m : A_(sigma(m)) tack t : B "valid"\
+      &forall y_1, ..., y_n "pairwise" eq.not "variables"
+      y_1 : A_1, ..., y_n : A_n tack t[x_1 := y_(sigma(1)), ..., x_m := y_(sigma(m))] : B "is valid"
+    $
+]
+
+#exercise[
+  State the cut rule
+]
+
+== Cartesian models
+
+Intuition :
+$
+  A &~> [[A]] "Set with structure"\
+  t: A &~> [[t : A]] in [[A]]
+$
+
+2 paths :
+- « Objects = Types, Morphims = Terms »
+  $
+    "(valid)" x_1 : A_1, ..., x_n : A_n tack t : B ~> [[Gamma tack t : B]] in space ??? [[A_1]], ..., [[A_n]]; [[B]] eq.not cal(C)([[A]], [[B]])
+  $
+- « Objects = Contexts = Lists of types, Morphisms = Substitutions = Lists of terms »
+  $
+    "(valid)" underbrace(underbrace(x_1 : A_1\, ...\, x_n : A_n, Gamma) tack t_1 : B_B ... Gamma tack t_n : B_n, Gamma : overline(A) tack Delta : overline(B))
+     ~> cases(
+          delim: "|",
+          overline(A) |-> [|overline(A)|],
+          Gamma : overline(A) |- Delta : overline(B) |->
+          [|Gamma |- Delta|] in ???_[|overline(A), overline(B)|]
+        )
+  $
+
+#let List = "List"
+
+#let lA = $overline(A)$
+#let lB = $overline(B)$
+#let lC = $overline(C)$
+#let lD = $overline(D)$
+#let lx = $overline(x)$
+#let ly = $overline(y)$
+#let lz = $overline(z)$
+#let cC = $cal(C)$
+#let lC = $overline(cC)$
+#let lt = $overline(t)$
+#let lu = $overline(u)$
+#let lv = $overline(v)$
+#let pair(r, l) = $chevron.l #r, #l chevron.r$
+#let Types = $"Types"$
+
+#exercise[
+  Let $(Sigma, tau)$ be a simply typed algebraic signature.\
+
+  - For all $overline(A), overline(B)$ list of types, let $cal(C)(overline(A), overline(B))$ be a set.\
+
+  - For all $Gamma : overline(A) |- Delta : overline(B)$ valid,
+    let $[|Gamma |- Delta|] in cal(C)(overline(A), overline(B))$
+
+  - For all $overline(A), overline(B), overline(C)$ and all
+    $b in cal(C)(overline(A), overline(B)),
+    c in cal(C)(overline(B), overline(C))$,
+    let $c[b] in cal(C)(overline(A), overline(C))$
+  Assume that
+  - $
+      &forall overline(A), overline(B), overline(C),\
+      &forall
+      Gamma_1 : overline(A) |- Delta_1 : overline(B) "and" Gamma_2 : overline(B) |- Delta_2 : overline(C) "valid",\
+      &[|Gamma_1 |- Delta_1|][[|Gamma_2 |- Delta_2|]] = [|Gamma_1 |- Delta_1[Gamma_2 |- Delta_2]|]
+    $
+  - $forall overline(A) overline(B), [| - |]_(overline(A), overline(B))$ is surjective
+  - $
+      forall "types" lA, B_1, ..., B_n\
+      forall "valid judgements"\
+      cases(delim: "(",
+        lz : lA tack t_1 : B_1,
+        lz : lA tack t_n : B_n
+      )\
+      cases(delim: "(",
+        lz : lA tack u_1 : B_1,
+        lz : lA tack u_n : B_n
+      )
+    $
+  - $[| lz |- alpha(lx_1 ⋅ t_1, ..., lx_n ⋅ t_n) |]$ depends only on $[| |- t_1 |], ..., [| |- t_n |]$
+  Prove that:
+  - $(List(Type), cal(C))$ defines a category with all finite products
+  - It is cartesian
+  - each $alpha in Op_Sigma$ is interpreted by a natural transformation (natural wrt the context)
+]
+
+#environment(name: "Erratum", counter: none)[
+  Terms in context are defined up to renaming :
+  $
+    x: A, y: B &tack t\
+    x': A, y': B &tack t[x := x', y := y']
+  $
+]
+
+#solution[
+  $"Id"$ morphism : $A_1, ..., A_n = overline(A)$
+  $
+    id_overline(A) = [[ overline(x) : overline(A) tack x_1 : A_1 ]], ..., [[ overline(x) : overline(A) tack x_n : A_n ]]
+  $
+
+  Composition : $overline(A), overline(B), overline(C)$
+  $
+    b in cal(C)(overline(A), overline(B)) quad c in cal(C)(overline(B), overline(C))\
+    c compose b = ? quad c[b]
+  $
+
+  Associativity : $overline(A), overline(B), overline(C), overline(D)$
+  $
+    b in cal(C)(overline(A), overline(B)) quad c in cal(C)(overline(B), overline(C)) quad d in cal(C)(overline(C), overline(D))\
+    "surjective : " b = [[overline(x) tack overline(t)]] quad c = [[overline(y) tack overline(u)]] quad d = [[overline(z) tack overline(v)]]\
+    d compose (c compose b) &= d[c[b]] \
+        &= [|overline(z) |- overline(v)|][[|overline(y) |- overline(u)|][[|overline(x) |- overline(t)|]]] \
+        &= [|overline(z) |- overline(v)|][[|overline(x) |- overline(u)[overline(y) := overline(t)]|]] \
+        &= [|overline(x) |- overline(v)[overline(z) := overline(u)[overline(y) := overline(t)]]|] \
+        &= [|overline(x) |- overline(v)[overline(z) := overline(u)][overline(y) := overline(t)]|] \
+        &= d[c][b] quad #[by unrolling in the other way]\
+        &= (d compose c) compose b
+  $
+
+  Unit : $overline(A), overline(B) quad b = [|overline(x) tack overline(t) in cal(C)(overline(A), overline(B))|]$
+  $
+    id_overline(B) &= [| overline(y) tack overline(y) |]\
+    id_overline(B) compose b &= [| overline(y) tack overline(y) |] compose [| overline(x) tack overline(t) |]\
+                             &= [| overline(x) tack overline(y)[ overline(y) := overline(t) ]|]
+                             &= [| overline(x) tack overline(t) |]
+                             &= b
+    id_overline(A) &= [| overline(x') tack overline(x') |]\
+    b compose id_overline(A) &= [| overline(x) tack overline(t) |] compose [| overline(x') tack overline(x') |]\
+                             &= [| overline(x') tack overline(t)[ overline(x) := overline(x') ]|]
+                             &= [| overline(x) tack overline(t) |]
+                             &= b
+  $
+
+
+  It is cartesian
+  - Terminal object : $[]$
+  - Product of $lA, lB$:
+    $
+      lA times lB & := [lA, lB] && quad ("concatenation") \
+      pi_lA & := [|lx : lA, ly : lB |- lx : lA|] \
+      pi_lB & := [|lx : lA, ly : lB |- ly : lB|] \
+    $
+    For $f := [|lz |- lt|] in cC(lC, lA), g := [|lz |- lu|] in cC(lC, lA)$,
+    $
+      pair(f, g) := [|z |- lt, lu|] quad (= [| [lz |- t_1, ..., lz |- t_m, lz |- u_1, ..., lz |- u_n] |])
+    $
+    Uniqueness:
+    Let $h = [|lz |- lv : lA, lB|] in cC(lC, [lA, lB])$.
+    $
+      lv &= [lv_lA, lv_lB] \
+      f &= pi_A compose h = [|lx, ly |- lx|] compose [|lz |- lv_lA, lv_lB|] \
+      &= [|lz |- lx[lx := lv_lA, ly := lv_lB]|] \
+      &= [|lz |- lv_lA|] \
+      g &= [|lz |- lv_lB|]
+    $
+    $h = pair(f, g)$ now follows from (3)
+
+  Prove that for all $alpha in Op_Sigma$ where $Rule(alpha) = (lA_1, B_1..., lA_n, B_n, C)$
+  the map $lD in List(Types) t-> cases(delim: "(",
+    b_1 = [| lz, lx_1 in cC((lD, lA_1), B_1) |],
+    ...,
+    b_n = [| lz, lx_n in cC((lD, lA_n), B_n) |],
+  ) t-> [| lz |- alpha(lx_1 ⋅ t_1, ..., lx_n ⋅ t_n) |]$ is a natural transformation (wrt $lD$).
+
+  $
+    cC((-, lA_1), B_1) times ... times cC((-, lA_n), B_n) => cC(-, C)
+  $
+
+  $
+    underbrace([| ly : lE |- lu : lD |], d) in cC(lE, lD)\
+
+    [| ly |- alpha(lx_1 ⋅ t_1[lz := lu], ..., lx_n ⋅ t_n[lz := lu]) |]
+    = [| lz |- alpha(lx_1 ⋅ t_1, ..., lx_n ⋅ t_n) |] compose [| ly |- lu |]
+  $
+]
+
+#show "STAS": "Simply Typed Algebraic Signature (STAS)"
+
+#let Ob = $"Ob"$
+#let Set = $"Set"$
+
+#definition[
+  Let $(Sigma, tau)$ be a STAS.
+  A structure on $(Sigma, tau)$ is :
+  - A locally small#footnote[$forall A, B, cC(A, B) "is a set"$] cartesian category $cC$. Notation :
+    - $(A times B, pi_1 "or" pi_A, pi_2 "or" pi_B)$ product
+    - $pair(f, g) in cC(C, A times B)$ universal map
+    - $T$ terminal object
+    - $T_A in cC(A, T)$
+  - A function $[| ... |] : Types --> Ob(cC)$
+  - $forall alpha in Op_Sigma$ with $Rule(alpha) = (lA_1, B_1, ..., lA_n, B_n, C)$
+    a natural transformation (wrt $D$)
+    $[| alpha |] : D in Ob(cC) t-> [| alpha |]_D in Set(cC(D times [| lA_1 |], [[B_1]]) times ... times cC(D times [| lA_n |], [[B_n]]), cC(D, [|C|]))$ ($[|A_1|]$ meaning $[|A_(1, 1)|] times ... times [|A_(1, m_1)|]$)
+]
+
+#example[
+  $AA$ set of atomic types $~> Lambda_("ST", AA) = (Sigma_(Lambda_("ST", AA)), tau_(Lambda_("ST", AA)))$.
+  $cC = Set$. $forall a in AA "choose" [|a|] "set"$. Let $[| A --> B |] = cC([|A|], [|B|])$.
+
+  $
+    [|Lam_(A, B)|]_D = f t-> (x t-> y t-> f(x, y)) in Set(cC(D times [|A|], [|B|]), cC(D, cC([|A|], [|B|])))
+  $
+]
+
+#exercise[
+  Given $Gamma : lA |- lt : lB$ valid typing judgements.
+
+  Define $[| Gamma : lA |- lt : lB |] in tau([|lA|], [|lB|])$.
+
+  Such that $[| Gamma_1 |- Delta_2[Gamma_2 := Delta_1] |] = [| Gamma_2 |- Delta_2 |] compose [| Gamma_1 |- Delta_1 |] in cC(D, A) => cC(D, B)$
+
+  $cC(A, B)$
+]
+
+== Models of the Simply-Typed $lambda$-Calculus
+
+#let ST = "ST"
+#let app = "app"
+#let lam = "lam"
+
+Interpret $Lambda_(ST, AA)$ so that
+$beta : [| lz : D |- app_(A, B)(lam_(A, B)(x⋅t), u) : B |] = [| z |- t[x := u] |]$
+and $eta : [| lz : D |- lam_(A, B)(x ⋅ app_(A, B)(t, x)) : A -> B |] = [| lz : D |- t : A -> B |]$
+
+Equivalently, so that $t =_(beta, eta) u => [| Gamma |- t |] = [| Gamma |- u |]$.
+
+Take $cC$ locally small category.
+
+Let $A -> B in Ob(cC), forall A, B in Ob(cC)$.
+
+Let $cC(D times A, B) <--_(lam_(A, B, D)) cC(D, A -> B)$,
+$cC(D, A -> B) times cC(D, A), -->_(app_(A, B, D)) cC(D, B)$ be a natural
+transformation wrt D.
+
+Assume that $forall t in cC(D times A, B), forall u in cC(D, u)$.
+
+$beta : app(lam(t), u) = t compose pair(id_D, u)$
+
+$eta : forall t e cC(D, A -> B)$
+
+$t = lam(app(t compose pi_D, pi_A))$
+
+Then $cC$ is cartesian closed (and this is equivalent).
+
+#exercise[
+  Given $Gamma : lA |- lt : lB$ valid typing judgements.
+
+  Define $[| Gamma : lA |- lt : lB |] in tau([|lA|], [|lB|])$.
+]
+
+In Ocaml, is it true that $("fun" x -> t) u eq.triple t[x := u]$ ?
+- find a sufficient condition on $f$ : if $f$ "uses $x$ exactly once"
+- find a sufficient condition on $e$ : if $e$ has no side-effects
+
+Attention : Non-commutative side-effects
+
+== Interlude : Yoneda's Lemma
+
+#let Cat = $cal("C")"at"$
+
+#definition[
+  Let $cC$, $cD$ be locally small categories.
+  The category of functions $Cat(cC, cD)$ defined by:
+]
+
+#proposition[
+  Let $cC$ be a locally small category.
+  Then $Cat(cC^"op", Set)$ is a Grothendieck topos, in particular:
+  - It has all small limits and colimits
+  - It is cartesian closed
+]
+
+#let yo = $よ$
+
+#definition(subtitle: "The Yoneda embedding")[
+  Let $cC$ a locally small category, we define a functor:
+  $
+    よ : cC --> Cat(cC^op, Set)
+  $
+
+  - On objects : $forall A in Ob(cC)$, $yo(A) : cC^"op" --> Set$ is defined by :
+    - $forall B in Ob(cC), yo(A)(B) = cC(B, A)$
+    - $forall f in cC(B_2, B_1), yo(A)(f) = cases(cC(B_1, A) &--> cC(B_2, A), g &t--> g compose f)$
+    $
+      yo(A)(f_1)(y(A)(f_2)(g)) &= (g compose f_2) compose f_1\
+                               &= g compose (f_2 compose f_1)\
+                               &= yo(A) (f_2 compose f_1) (g)
+    $
+  - On morphisms : $forall h in cC(A_1, A_2), yo(h) : yo(A_1) => y(A_2)$ is defined by :
+    $
+      forall B in Ob(cC), yo(h)(B) = cases(underbrace(yo(A_1)(B), cC(B, A_1)) &-->^(Set) underbrace(yo(A_2)(B), cC(B, A_2)),
+                                           g &t--> h compose g)
+    $
+]
+
+#exercise[
+  Prove that $forall h, yo(h)$ is natural : $forall f in cC^(B_1, B_2) = cC(B_2, B_1)$
+  #align(center, diagram({
+  	node((-1, -1), [$cC(B_1, A_1)$])
+  	node((-1, 1), [$cC(B_1, A_2)$])
+  	node((3, -1), [$cC(B_2, A_1)$])
+  	node((3, 1), [$cC(B_2, A_2)$])
+  	edge((-1, -1), (-1, 1), [$h compose -$], label-side: right, "->")
+  	edge((-1, -1), (-1, 1), [$yo(h)(B_1)$], label-side: left, " ")
+  	edge((-1, -1), (3, -1), [$- compose f$], label-side: left, "->")
+  	edge((3, -1), (3, 1), [$h compose -$], label-side: left, "->")
+  	edge((3, -1), (3, 1), [$yo(h)(B_2)$], label-side: right, " ")
+  	edge((-1, 1), (3, 1), [$- compose f$], label-side: right, "->")
+  	edge((-1, 1), (3, 1), [$yo(A_2)(f)$], label-side: left, "->")
+  	edge((-1, -1), (3, -1), [$yo(A_1)(f)$], label-side: right, " ")
+  }))
+]
+
+#theorem(subtitle: "Yoneda")[
+  For all $F in Cat(cC^"op", Set)$, the natural transformation :
+  $
+    cases(
+      Cat(cC^"op", Set)(yo(-), F) &==> F(-),
+      underbrace(A, in Ob(cC)) t-> underbrace(alpha, in yo(A) => F = Cat(cC^"op", Set)(yo(A), F)) &t--> underbrace(underbrace(alpha_A, in Set(yo(A)(A), F(A)))(underbrace(id_A, in cC(A, A) = yo(A)(A))), in F(A)),
+    )
+  $
+
+  is a bijection.
+]
+
+#exercise[
+  - Prove naturality
+  - Prove Yoneda (i.e. bijection)
+  - Prove that $yo : cC --> Cat(cC^"op", Set)$ which is full & faithful (Apply
+    yoneda to $F = yo(B)$)
+  - Prove that $yo$ is continuous (= preserves all small limits that exists in $cC$)
+]
+
+= Models of linear logic
+
+== Nomenclature the various fragments of linear logic
+
+$
+  #pin(1)&(times) quad &-o quad &1 quad &    quad &par quad &bot quad &"multiplicative"\
+  &(+)     quad &\& quad &0 quad &top quad &    quad &&"additive"\
+  &!       quad &   quad &  quad &    #pin(2) quad &    quad &&"exponential"\
+$
+$
+  "intuitionistic fragment"
+$
+
+// #pinit-highlight(1, 2)
+
+- MALL : $(times) (+) \& par 1 space 0 space top bot -o$
+- ILL : $(times) (+) \& space 1 space 0 space top -o !$
+- MEILL : $(times) (+) \& par 1 space 0 space top bot -o ! space ?$
+
+== Standard notions of models for fragments of MALL
+
+$(times) 1$ : Symmetric monoidal category
+- adding $-o$ : Symmetrict monoidal closed category
+  - adding $par bot$ : \*-autonomous
+- adding $& top$ : Finite products
+- adding $(+) 0$ : Finite coproducts
+
+#definition[
+  Let $cC$ be a category and $A, B in Ob(cC)$.
+
+  A coproduct of A and B is:
+  - An object $A (+) B$
+  - Two morphisms $i_A in cC(A, A (+) B), i_B in cC(B, A(+) B)$
+    such that $forall C in Ob(cC), forall f in cC(A, C), forall g in cC(B, C)$
+
+    $exists ! [f, g] in cC(A (+) B, C)$ such that
+    #align(center, diagram({
+    	node((-1, -1), [$A (+) B$])
+    	node((0, -1), [$B$])
+    	node((-2, -1), [$A$])
+    	node((-1, 0), [$C$])
+    	edge((0, -1), (-1, -1), [$iota_B$], label-side: right, "->")
+    	edge((-2, -1), (-1, -1), [$iota_A$], label-side: left, "->")
+    	edge((-1, -1), (-1, 0), [$[f, g]$], label-side: right, "->")
+    	edge((0, -1), (-1, 0), [$g$], label-side: left, "->", bend: 18deg)
+    	edge((-2, -1), (-1, 0), [$f$], label-side: right, "->", bend: -18deg)
+    }))
+]
+
+#let FinBan = $"FinBan"$
+
+#example[
+  Let $FinBan$ (finite Banard) be the category defined by :
+  - $Ob(FinBan)$ : All finite-dimensional normed ($RR$-)vector spaces 
+  - $FinBan(A, B)$ =
+    ${ &f : A --> B "linear"\ &"s.t." forall ||f(a)|| <= ||a|| }$ 
+  - $FinBan(A_1, ..., A_n, B)$ =
+    ${ &f : A_1 times ... times A_n --> B space n"-linear (linear wrt each variable)"\ &"s.t." forall ||f(a_1, ..., a_n)|| <= ||a_1|| ... ||a_n|| }$ 
+  - $top = 0 = { 0 }$
+  - $A & B = A times B space (= A + B)$, $||(a, b)|| = max(||a||, ||b||)$\
+    Exercise : Prove that product\
+    $||pi_A(a, b)||  = ||a|| <= max(||a||, ||b||)$\
+    $||pi_B(a, b)||  = ||b|| <= max(||a||, ||b||)$
+
+    Let $f in FinBan(C, A)$, $g in FinBan(C, B)$.
+
+    $<f, g>$ must be defined by $<f, g>(c) = (f(c), g(c))$
+
+    let $c in C$, $underbrace(||f(c)|| <= c quad ||g(c)|| <= c, ||(f(c), g(c))|| <= c)$
+
+  - $A (+) B = A + B space (= A times B)$\
+    $||inj_A(a, b)||  = ||(a, 0)|| "and" ||(a, 0)||, ||a||$\
+    $||inj_B(a, b)||  = ||(0, b)|| "and" ||(0, b)||, ||b||$
+
+    Let $f in FinBan(A, C)$, $g in FinBan(B, C)$.
+
+    $exists ! h : A (+) B --> C$ linear s.t $h compose inj_1 = f$ ($h(a, 0) = f(a)$) and $h compose inj_2 = g$ ($f(0, b) = g(b)$)
+
+    So, $h(a, b) = h((a, 0) + (0, b)) = f(a) + g(b)$.
+
+    $||h(a, b)|| = ||f(a) + g(b)|| <= ||f(a)|| + ||g(b)|| <= ||a|| + ||b||$
+  - $A -o B$ = Linear maps $A -> B$
+    $||f|| = sup_"max" {||f(a)||, ||a|| <= 1}$
+  - $bot = 1 = (RR, |.|)$
+
+    $
+      1 -o B &arrow.r.double^~ B\
+      underbrace(f, ||f|| = ||f(1)|| = ||f(-1)||) &t-> f(1) quad quad (|r| <= 1)
+    $
+
+    $((a -o bot) -o bot) tilde.eq A$
+  - $(A (*) B, (a, b) t-> a (*) b)$ is characterised by the following universal property.
+    #align(center, diagram({
+    	node((-2, -1), [$(A, B)$])
+    	node((0, -1), [$FinBan(A, B\; C)$])
+    	node((-1, -1), [$C$])
+    	node((-2, 0), [$A (times) B$])
+    	node((-2, 1), [$FinBan(A, B\; A (times) B)$])
+    	edge((-2, 0), (-1, -1), [$exists !$], label-side: right, "-->")
+    	edge((-2, -1), (-1, -1), [$forall$], label-side: left, "->")
+    	edge((-2, -1), (-2, 0), [$(a, b) t-> a (times) b$], label-side: right, "->")
+    	edge((-2, 1), (-2, 0), [$in$], label-side: center, " ")
+    	edge((-1, -1), (0, -1), [$in$], label-side: center, " ")
+    	edge((-2, -1), (-2, -1), "->", bend: 140deg, loop-angle: 135deg)
+    }))
+]
+
+#exercise[
+  Find a symmetrical monoidal category $(cC, (*), 1)$
+  s.t. $cC$ has finite coproducts but $(*)$ does not distribute over them.
+  i.e., in general :
+  - $A (*) (B (+) C) tilde.eq.not (A (*) B) (+) (B (*) C)$
+  - $A (*) 0 tilde.eq.not 0$
+]
+
+#solution[
+  $cC = FinBan$
+
+  $(*) = \&$
+
+  $I = top$
+
+  $(1 (+) 1) \& 1 tilde.eq.not (1 \& 1) (+) (1 \& 1)$
+]
+
+== Interpreting $!$ Linean/Non-Linear adjunctions
+
+#definition[
+  Let $(cC, ⋅, I) space (cD, (x), 1)$ be symmetric monoidal categories.
+
+  A _symmetric lax monoidal functor_ from $cC$ to $cD$ is a functor
+  $F : cC --> cD$ equipped with :
+  - A natural transformation (wrt $A, B$) :
+    $m^2_(A, B) in cD(F A (*) F B, F (A ⋅ B)), forall A, B in Ob(cC)$
+  - A morphism $m^0 in cD(1, F I)$
+
+  Such that :
+  1.
+    #align(center, diagram({
+    	node((0, 0), [$(F A (*) F B) (*) F C$])
+    	node((1, 0), [$F A (*) (F B (*) F C)$])
+    	node((0, 1), [$F(A⋅B) (*) F C$])
+    	node((0, 2), [$F((A⋅B)⋅C)$])
+    	node((1, 1), [$F A (*) F (B ⋅ C)$])
+    	node((1, 2), [$F (A ⋅ (B ⋅ C))$])
+    	edge((0, 0), (1, 0), [$"assoc"^cD$], label-side: left, "->")
+    	edge((0, 2), (1, 2), [$"assoc"^cD$], label-side: left, "->")
+    	edge((0, 0), (0, 1), [$m^2_(A, B) (*) F C$], label-side: right, "->")
+    	edge((0, 1), (0, 2), [$m^2_(A⋅B, C)$], label-side: right, "->")
+    	edge((1, 0), (1, 1), [$F A (*) m^2_(B, C)$], label-side: left, "->")
+    	edge((1, 1), (1, 2), [$m^2_(A, B⋅C)$], label-side: left, "->")
+    }))
+  2.
+    // https://q.uiver.app/#r=typst&q=WzAsNCxbMCwwLCJGIEEgKCopIDEiXSxbMSwwLCJGIEEiXSxbMCwxLCJGIEEgKCopIEYgSSJdLFsxLDEsIkYgKEEg4ouF4oCvSSkiXSxbMCwxLCJcInVuaXRcIl5jRCJdLFswLDIsImlkXyhGIEEpICgqKSBtXjAiLDJdLFszLDEsIkYgKFwidW5pdFwiXmNDKSIsMl0sWzIsMywibV4yIiwyXV0=
+    #align(center, diagram({
+    	node((-2, -2), [$F A (*) 1$])
+    	node((-1, -2), [$F A$])
+    	node((-2, -1), [$F A (*) F I$])
+    	node((-1, -1), [$F (A ⋅ I)$])
+    	edge((-2, -2), (-1, -2), [$"unit"^cD$], label-side: left, "->")
+    	edge((-2, -2), (-2, -1), [$id_(F A) (*) m^0$], label-side: right, "->")
+    	edge((-1, -1), (-1, -2), [$F ("unit"^cC)$], label-side: right, "->")
+    	edge((-2, -1), (-1, -1), [$m^2$], label-side: right, "->")
+    }))
+  3.
+    // https://q.uiver.app/#r=typst&q=WzAsNCxbMCwwLCJGIEEgKCopIEYgQiJdLFsxLDAsIkYgQiAoKikgRiBBIl0sWzAsMSwiRiAoQSDii4UgQikiXSxbMSwxLCJGIChCIOKLhSBBKSJdLFswLDIsIm1fMiJdLFsxLDMsIm1eMiJdLFswLDEsIlwiU3dhcFwiXmNEIiwxXSxbMiwzLCJGIChcIlN3YXBcIl5jQykiLDFdXQ==
+    #align(center, diagram({
+    	node((-2, -1), [$F A (*) F B$])
+    	node((-1, -1), [$F B (*) F A$])
+    	node((-2, 0), [$F (A ⋅ B)$])
+    	node((-1, 0), [$F (B ⋅ A)$])
+    	edge((-2, -1), (-2, 0), [$m^2$], label-side: right, "->")
+    	edge((-1, -1), (-1, 0), [$m^2$], label-side: left, "->")
+    	edge((-2, -1), (-1, -1), [$"Swap"^cD$], label-side: center, "->")
+    	edge((-2, 0), (-1, 0), [$F ("Swap"^cC)$], label-side: center, "->")
+    }))
+
+  A _strong monoidal functor_ is a lax monoidal functor (F, m) s.t. $m^2$ and
+  $m^0$ are isomophisms.
+]
+
+#definition[
+  A _symmetric monoidal adjunction_ :
+  #align(center, diagram({
+  	node((-1, 0), [$(cal(C), dot, I)$])
+  	node((1, 0), [$(cal(D), (*), 1)$])
+  	node((0, 0), [$bot_(underline(m), underline(eta), underline(epsilon))$])
+  	edge((-1, 0), (1, 0), [$L$], label-side: left, "->", bend: 40deg)
+  	edge((1, 0), (-1, 0), [$B$], label-side: left, "->", bend: 40deg)
+  }))
+
+  Is the data of :
+  - A strong monoidal functor $(L, m) : (cC, ⋅, I) --> (cD, (*), 1)$
+  - A functor $R : cD --> cC$
+  - An adjunction $L attach(tack.l, br:(eta, epsilon)) R$
+    $
+    // https://q.uiver.app/#r=typst&q=WzAsMixbMCwwLCJjQyJdLFsxLDAsImNEIl0sWzAsMSwiTCIsMCx7Im9mZnNldCI6LTN9XSxbMSwwLCJSIiwwLHsib2Zmc2V0IjotM31dLFswLDEsImJvdF8oZXRhLCBlcHNpbG9uKSIsMSx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6Im5vbmUifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dXQ==
+    #align(center, diagram({
+    	node((0, 0), [$cC$])
+    	node((1, 0), [$cD$])
+    	edge((0, 0), (1, 0), [$L$], label-side: left, shift: 0.3, "->")
+    	edge((1, 0), (0, 0), [$R$], label-side: left, shift: 0.3, "->")
+    	edge((0, 0), (1, 0), [$bot_(eta, epsilon)$], label-side: center, " ")
+    }))
+    $
+]
+
+#definition[
+  A _linear/non-linear adjunction_ is a summetric monoidal adjunction
+  #align(center, diagram({
+  	node((-1, 0), [$(VV, times, I)$])
+  	node((1, 0), [$(LL, (*), 1)$])
+  	node((0, 0), [$bot_(m, eta, epsilon)$])
+  	edge((-1, 0), (1, 0), [$L$], label-side: left, "->", bend: 40deg)
+  	edge((1, 0), (-1, 0), [$V$], label-side: left, "->", bend: 40deg)
+  }))
+]
+
+=== The exponential comonoad $!$
+
+Let $! = L compose V : bb(L) -> bb(L)$.
+$forall a in "OB" bb(L), $ let $mu_A = L(  eta_(V A)) in bb(L)(L V A, L V L V A)$ \
+($L V A "is" !A$, $L V L V A "is" !!A$,) \
+Then $(!, epsilon, mu)$ is a comonad.
+We then have
+
+#diagram({
+  node((0, 0), [$(LL_!, par, T)$])
+  node((2, 0), [$(LL, (*), 1)$])
+  node((1, 0), [$bot$])
+  edge((0, 0), (2, 0), [$!$], label-side: left, "->", bend: 18deg)
+  edge((2, 0), (0, 0), [$id$], label-side: left, "->", bend: 18deg)
+})
+
+where $bb(L)_!(A,B) := bb(L)(!A, B)$
+
+#let big_adjunction(L, R, f, g, a: $bot$) = diagram({
+	node((-1, 0), L)
+	node((1, 0), R)
+	node((0, 0), a)
+	edge((-1, 0), (1, 0), f, label-side: left, "->", bend: 18deg)
+	edge((1, 0), (-1, 0), g, label-side: left, "->", bend: 18deg)
+})
+
+#big_adjunction($(LL^!, (*), 1)$, $(LL, (*), 1)$, $"forget"$, $!$)
+
+#definition[
+  Let $cC$ be a category and $(!, epsilon, nu)$ a command on $cC$
+  - The Kleisli category $cC_!$ is defined by
+    $ &Ob(cC_!) = Ob(cC)\
+      &cC_! (A, B) = cC(!A, B)\
+      &"for" f in cC_! (A, B), g in cC_! (B, C)\
+      &g << f in cC_!(A, C) "is defined by"\
+      &g << f = f compose !f compose nu_A
+    $
+]