Skip to content

Instantly share code, notes, and snippets.

@jozefg

jozefg/J.agda

Created March 1, 2021 20:55
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save jozefg/ebf70542a299200b483340287340913e to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save jozefg/ebf70542a299200b483340287340913e to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. jozefg created this gist Mar 1, 2021.
    13 changes: 13 additions & 0 deletions J.agda
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,13 @@
    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