Skip to content

Instantly share code, notes, and snippets.

@jcreedcmu

jcreedcmu/gist:576e0e42ecdd5d4a2526c39ce307a3ca

Created December 11, 2017 00:04
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save jcreedcmu/576e0e42ecdd5d4a2526c39ce307a3ca to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save jcreedcmu/576e0e42ecdd5d4a2526c39ce307a3ca to your computer and use it in GitHub Desktop.
Download ZIP
Internalized parametricity
Raw
gistfile1.txt
{-# OPTIONS --without-K --rewriting #-}
module Sharp where
open import HoTT hiding ( O; Path; _*_ )
module WithArity (C : Set) where
postulate
𝕀 : Set
Ξ· : C β†’ 𝕀
Path : βˆ€ {β„“} (A : 𝕀 β†’ Set β„“) (a : (c : C) β†’ A (Ξ· c)) β†’ Set β„“
_*_ : βˆ€ {β„“} {A : 𝕀 β†’ Set β„“} {a : (c : C) β†’ A (Ξ· c)}
β†’ Path A a β†’ (i : 𝕀) β†’ A i
lam : βˆ€ {β„“} {A : 𝕀 β†’ Set β„“} (f : (i : 𝕀) β†’ A i)
β†’ Path A (f ∘ Ξ·)
Ξ·-rewrite : βˆ€ {β„“} {A : 𝕀 β†’ Set β„“} {a : (c : C) β†’ A (Ξ· c)}
(p : Path A a) (c : C) β†’ (p * (Ξ· c)) ↦ a c
{-# REWRITE Ξ·-rewrite #-}
syntax Path (λ i -> A) a = a ∈ i · A
embu : βˆ€ {β„“} {A : C β†’ Set β„“} (p : A ∈ i Β· Set β„“)
(a : (c : C) β†’ A c) β†’ Set β„“
embu {β„“} {A} p a = a ∈ i Β· (p * i)
embf : βˆ€ {β„“} {A : 𝕀 β†’ Set β„“} {B : (i : 𝕀) (x : A i) β†’ Set β„“}
{f : (c : C) β†’ (x : A (Ξ· c)) β†’ B (Ξ· c) x}
β†’ (f ∈ i Β· Ξ  (A i) (B i))
β†’ ((x : (i : 𝕀) β†’ A i) β†’ (Ξ» c β†’ f c (x (Ξ· c))) ∈ i Β· B i (x i))
embf p x = lam (Ξ» i β†’ (p * i) (x i))
postulate
embu-equiv : βˆ€ {β„“} {A : C β†’ Set β„“} β†’ is-equiv (embu {β„“} {A})
embf-equiv : βˆ€ {β„“} {A : 𝕀 β†’ Set β„“} {B : (i : 𝕀) (x : A i) β†’ Set β„“}
{f : (c : C) (x : A (Ξ· c)) β†’ B (Ξ· c) x}
β†’ is-equiv (embf {β„“} {A} {B} {f})
@JacquesCarette
Copy link

JacquesCarette commented Dec 11, 2017

Some comments might be a nice addition to this code...

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment