4

Ld Nclusion (4) -- η-rules and codata

 3 years ago
source link: https://ice1000.org/2020/09-11-Cutt4.html
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
η-rules and codata

Fortunately, this time we won’t need these complicated operations. We won’t need any SVG pictures either, because you’ve got enough of them (and should be able to draw them by yourself), and I’ve got enough with inkscape’s shitty display on hi-dpi screens!

{-# OPTIONS --cubical --allow-unsolved-metas #-}
module 2020-9-11-Cutt4 where
open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude

variable A B : Set

So, recall the proof of function extensionality:

functionExt : (f g : A -> B) (p : ∀ a -> f a ≡ g a) -> f ≡ g
functionExt _ _ p i a = p a i

Why does this proof type-check? Well, during type-checking, Agda first obtain the expression λ i a -> p a i, which is of a path type, and checks the following equalities:

That the path’s LHS is convertible to f

  • To check it, we apply i0 to the expression, and we get λ a -> p a i0, and p a : f a ≡ g a will reduce to f a when applied by i0 due to the property of the path type, so it reduces to λ a -> f a

report

Recommend

About Joyk


Aggregate valuable and interesting links.
Joyk means Joy of geeK