Skip to content

Instantly share code, notes, and snippets.

@laserbat

laserbat/equiv.hs

Created February 16, 2026 18:20
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save laserbat/4100ae3698c9e7b3170eba068c961a2f to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save laserbat/4100ae3698c9e7b3170eba068c961a2f to your computer and use it in GitHub Desktop.
Download ZIP
Raw
equiv.hs
data a <-> b = Arp (a -> b) (b -> a)
arp :: (a -> b) -> (b -> a) -> a <-> b
arp = Arp
(.>) :: (a <-> b) -> (a -> b)
(.>) (Arp a _) = a
(.<) :: (a <-> b) -> (b -> a)
(.<) (Arp _ b) = b
star :: p -> ((p <-> q) <-> q)
star a =
arp
(\b -> b .> a)
(\b -> arp (const b) (const a))
-- (star a) .> b = b .> a
-- ((star a) .< b) .> c = b
-- ((star a) .< b) .< c = a
(><) :: (q <-> p) -> (r <-> s) -> ((p <-> r) <-> (q <-> s))
a >< b =
arp
( \c ->
arp
(\d -> b .> (c .> (a .> d)))
(\d -> a .< (c .< (b .< d)))
)
( \c ->
arp
(\d -> b .< (c .> (a .< d)))
(\d -> a .> (c .< (b .> d)))
)
--- ((a >< b) .> c) .> d = b .> (c .> (a .> d))
--- ((a >< b) .> c) .< d = a .< (c .< (b .< d))
--- ((a >< b) .< c) .> d = b .< (c .> (a .< d))
--- ((a >< b) .< c) .< d = a .> (c .< (b .> d))
refl :: p <-> p
refl = arp id id
--- refl .> a = a
--- refl .< a = a
sym :: (p <-> q) <-> (q <-> p)
sym =
arp
(\a -> arp (\b -> a .< b) (\b -> a .> b))
(\a -> arp (\b -> a .< b) (\b -> a .> b))
--- (sym .> a) .> b = a .< b
--- (sym .> a) .< b = a .> b
--- (sym .< a) .> b = a .< b
--- (sym .< a) .< b = a .> b
(>~<) :: ((p <-> q) <-> (p <-> r)) -> (p <-> (q <-> r)) -> (q <-> r)
a >~< b =
arp
(\c -> (b .> ((a .< ((b >< star c) .> refl)) .< c)) .> c)
(\c -> (b .> ((a .> ((((refl >< sym) .> b) >< star c) .> refl)) .< c)) .< c)
--- (a >~< b) .> c = (b .> ((a .< ((b >< star c) .> refl)) .< c)) .> c
--- (a >~< b) .< c = (b .> ((a .> ((((refl >< sym) .> b) >< star c) .> refl)) .< c)) .< c
(>-<) ::
c ->
(((a <-> b) <-> b) <-> (((a <-> b) <-> b) <-> (a <-> c))) ->
(((a <-> b) <-> b) <-> (a <-> c))
a >-< b =
arp
(\c -> (b .> c) .> c)
(\c -> (b .> star (c .< a)) .< c)
--- (a >-< b) .> c = (b .> c) .> c
--- (a >-< b) .< c = (b .> star (c .< a)) .< c
----
dist :: (r <-> (r <-> (p <-> q))) <-> ((r <-> p) <-> (r <-> q))
dist =
arp
( \a ->
arp
( \b ->
arp
(\c -> ((a .> c) .> c) .> (b .> c))
(\c -> a .< ((refl >< sym) .> (((sym .> b) >< star c) .< refl)))
)
( \b ->
arp
(\c -> ((a .> c) .> c) .< (b .> c))
(\c -> a .< (((sym .> b) >< star c) .< refl))
)
)
( \a ->
arp
(\b -> star b .< (sym .> (((sym .> ((a >< star b) .> refl)) >< star b) .> refl)))
(\b -> b .< (a >~< b))
)
--- ((dist .> a) .> b) .> c = ((a .> c) .> c) .> (b .> c)
--- ((dist .> a) .> b) .< c = a .< ((refl >< sym) .> (((sym .> b) >< star c) .< refl))
--- ((dist .> a) .< b) .> c = ((a .> c) .> c) .< (b .> c)
--- ((dist .> a) .< b) .< c = a .< (((sym .> b) >< star c) .< refl)
--- (dist .< a) .> b = star b .< (sym .> (((sym .> ((a >< star b) .> refl)) >< star b) .> refl))
--- (dist .< a) .< b = b .< (a >~< b)
flap :: (p <-> q) <-> (((p <-> r) <-> r) <-> (((p <-> r) <-> r) <-> (p <-> q)))
flap =
arp
(\a -> (refl >< sym) .> (sym .> star a))
( \a ->
arp
(\b -> ((a .> star b) .> star b) .> b)
(\b -> ((a .> (a .< (b >-< a))) .> (a .< (b >-< a))) .< b)
)
--- flap .> a = (refl >< sym) .> (sym .> star a)
--- (flap .< a) .> b = ((a .> star b) .> star b) .> b
--- (flap .< a) .< b = ((a .> (a .< (b >-< a))) .> (a .< (b >-< a))) .< b
-----
refl' :: p <-> p
refl' =
flap
.< ( dist
.< ( ((dist .< sym) .> ((dist .> (flap .> (dist .< sym))) .< sym))
.> ((dist .> (flap .> (dist .< sym))) .< sym)
)
)
-----
compose :: (q <-> r) -> (r <-> s) -> q <-> s
compose a b = (a >< b) .> refl
contr :: (x <-> (x <-> (x <-> y))) <-> (x <-> y)
contr = (refl >< star refl) .> dist
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment