Morphisms and transformations

Okei, det ser ut som noke har løsna her. Den store skurken i det siste har vore å gå fra ein naturlig transformasjon, til morfi og tilbake att. Eg har ei løysing som ser ut til å gje meining, som heller ikkje brukar noke trunkering - vi kan kikke på det i møtet i morgon :)

Løysinga

Vi nyttar naturalitet av α over map-⟦_⟧ og s , id. Når vi køyrer α gjennom begge omformingane, får vi denne transformasjonen (β):

β (s , v) =
  pr1 (α (s , id)) ,
  v ∘ pr2 (α (s , id))

Då må vi berre vise at α (s , id) == β (s , id), som er gjennomførbart sidan begge deler er lik map-⟦ D ⟧ v (α (s , id))!

Diagram

            map-⟦ C ⟧ v
s , id ------------------> s , v ∘ id (＝ s , v)
  |                             |
  |                             |
α |                             |
  |                             |
  |                             |
  V                             V
α (s , id) ---------------> α (s , v ∘ id) (＝ α (s , v))
             map-⟦ D ⟧ v