Skip to content

Instantly share code, notes, and snippets.

@Lysxia

Lysxia/I.agda

Created February 9, 2023 15:13
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 Lysxia/c5edf02b2ac4698ee617709fe1ccc745 to your computer and use it in GitHub Desktop.
Save Lysxia/c5edf02b2ac4698ee617709fe1ccc745 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
I.agda
module I where
open import Data.Unit
open import Relation.Binary.PropositionalEquality
private variable
A : Set
to : (⊤ → A) → A
to f = f tt
from : A → ⊤ → A
from x _ = x
to∘from : ∀ {A} (x : A) → to (from x) ≡ x
to∘from _ = refl
from∘to : ∀ {A} (x : ⊤ → A) → from (to x) ≡ x
from∘to _ = refl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment