Skip to content

Instantly share code, notes, and snippets.

@louisswarren louisswarren/lift.agda
Last active Jan 10, 2020

Embed
What would you like to do?
Lift types by instance resolution in Agda
data : Set where
zero :
suc :
data : Set where
nonneg :
negsuc :
data : Set where
frac_/suc_ :
record Embedding (A B : Set) : Set where
field
map : A B
open Embedding renaming (map to _$_)
instance trivial↪ : {A : Set} Embedding A A
trivial↪ $ x = x
-- Types can be lifted by finding their embedding via instance resolution
lift : {B : Set} {A : Set} ⦃ A↦B : Embedding A B ⦄ A B
lift ⦃ A↦B ⦄ x = A↦B $ x
instance
ℕ↪ℤ : Embedding ℕ ℤ
ℕ↪ℤ $ n = nonneg n
ℕ↪ℚ : Embedding ℕ ℚ
ℕ↪ℚ $ n = frac lift n /suc zero
ℤ↪ℚ : Embedding ℤ ℚ
ℤ↪ℚ $ a = frac a /suc zero
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.