Adventure in Oxford

我懶得寫了耶，反正看到很多東西，Oxford 的環境很不錯 XD。scm 老師的朋友寫了一張參觀路線給我，還借我他的職員證，所以我可以憑證進入各個學院（不然要繳錢或根本進不去）。中間 scm 老師的學妹帶我進她的學院吃中餐（就是 Harry Potter 電影裡的餐廳！）以及參觀。總之看了幾個學院、參觀兩個博物館、和 Oxford 一些其他的地標。Postcards 我剛剛弄好了，明天丟進郵筒裡。

回來突然想到 Jeremy 昨天講的話，試著改用 universal property（的一個方向）證明 fold fusion，果然一句話就解決了，因為 induction 現在藏在 universal property 的證明裡面。

foldr-univr : {A B : Set} -> (h : [ A ] -> B) -> forall f e ->
  (h [] ≡ e) -> (forall x xs -> h (x ∷ xs) ≡ f x (h xs)) ->
  (forall x -> h x ≡ foldr f e x)
foldr-univr h f e base-cond step-cond []       = base-cond
foldr-univr h f e base-cond step-cond (x ∷ xs) =
  ≡-trans (step-cond x xs)
          (≡-cong (f x) (foldr-univr h f e base-cond step-cond xs))

foldr-fusion : {A B C : Set} -> (h : B -> C) -> {f : A -> B -> B} ->
  {g : A -> C -> C} -> {e : B} -> (forall x y -> h (f x y) ≡ g x (h y)) ->
  forall x -> (h ∘ foldr f e) x ≡ foldr g (h e) x
foldr-fusion {_} {_} {_} h {f} {g} {e} fuse-cond =
  foldr-univr (h ∘ foldr f e) g (h e) ≡-refl
              (\x xs -> fuse-cond x (foldr f e xs))

--
快離開 Oxford 嘍。