Skip to content

Instantly share code, notes, and snippets.

@copumpkin

copumpkin/Scratch.agda

Last active October 6, 2015 00:57
Download ZIP

Revisions

  1. copumpkin renamed this gist Feb 15, 2014. 1 changed file with 0 additions and 0 deletions.
    0 gistfile1.hs → Scratch.agda
    View file
    File renamed without changes.
  2. copumpkin renamed this gist Jun 10, 2012. 1 changed file with 0 additions and 0 deletions.
    0 gistfile1.txt → gistfile1.hs
    View file
    File renamed without changes.
  3. copumpkin created this gist Jun 10, 2012.
    20 changes: 20 additions & 0 deletions gistfile1.txt
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,20 @@
    module Scratch where

    open import Level
    open import Function
    open import Relation.Binary.PropositionalEquality
    import Relation.Binary.EqReasoning as EqReasoning

    -- Legend has it that parametricity is just dinaturality
    module Parametricity {a} {F G : Set a → Set a → Set a}
    (mapF : ∀ {A B C D} → (A → B) → (C → D) → F B C → F A D)
    (mapG : ∀ {A B C D} → (A → B) → (C → D) → G B C → G A D)
    where
    postulate
    -- Agda doesn't know that its own polymorphic functions are dinatural, so we must teach it about itself
    dinatural : ∀ (f : ∀ {A} → F A A → G A A) {A B : Set a} (g : A → B) → ∀ x → mapG id g (f (mapF g id x)) ≡ mapG g id (f (mapF id g x))

    open Parametricity {zero} {λ A B → A → B} {λ _ A → A} (λ f g h → g ∘ h ∘ f) (λ _ f → f)

    definition : (fix : {A : Set} → (A → A) → A) {A : Set} (g : A → A) → fix g ≡ g (fix g)
    definition fix g = sym (dinatural fix g id)