Skip to content

Instantly share code, notes, and snippets.

@jozefg

jozefg/J.agda

Created March 1, 2021 20:55
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save jozefg/ebf70542a299200b483340287340913e to your computer and use it in GitHub Desktop.
Save jozefg/ebf70542a299200b483340287340913e to your computer and use it in GitHub Desktop.
Download ZIP
Raw
J.agda
open import Data.Product
open import Relation.Binary.PropositionalEquality
singleton-contractible : {A : Set}(x : A) (p : Σ[ y ∈ A ] x ≡ y) → (x , refl) ≡ p
singleton-contractible x ( .x , refl )= refl
transport : {A : Set}(B : A → Set)(x y : A) → x ≡ y → B x → B y
transport B x .x refl b = b
J : {A : Set}(B : (x y : A) → x ≡ y → Set) → ((x : A) → B x x refl) → (x y : A)(p : x ≡ y) → B x y p
J {A} B base x y p = transport C (x , refl) (y , p) (singleton-contractible x (y , p)) (base x)
where C : Σ[ y ∈ A ] x ≡ y → Set
C (y , p) = B x y p
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment