------------------------------------------------------------------------
-- The Agda standard library
--
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Function.Base
open import Function.Equality using (_⟨\$⟩_)
open import Function.Inverse as Inv using (_↔_; module Inverse)
open import Level
open import Relation.Binary.PropositionalEquality

-- Half adjoint equivalences (see the HoTT book).

record _≃_ {a b} (A : Set a) (B : Set b) : Set (a  b) where
field
to               : A  B
from             : B  A
left-inverse-of  :  x  from (to x)  x
right-inverse-of :  x  to (from x)  x
left-right       :
x  cong to (left-inverse-of x)  right-inverse-of (to x)

-- Half adjoint equivalences can be turned into inverses.

inverse : A  B
inverse = Inv.inverse to from left-inverse-of right-inverse-of

-- The forward direction of a half adjoint equivalence is injective.

injective :  {x y}  to x  to y  x  y
injective {x} {y} to-x≡to-y =
x            ≡⟨ sym (left-inverse-of _)
from (to x)  ≡⟨ cong from to-x≡to-y
from (to y)  ≡⟨ left-inverse-of _
y
where
open ≡-Reasoning

-- Inverses can be turned into half adjoint equivalences.
--
-- (This proof is based on one in the HoTT book.)

↔→≃ :  {a b} {A : Set a} {B : Set b}  A  B  A  B
↔→≃ A↔B = record
{ to               = to   ⟨\$⟩_
; from             = from ⟨\$⟩_
; left-inverse-of  = left-inverse-of
; right-inverse-of = right-inverse-of
; left-right       = left-right
}
where
open ≡-Reasoning
open module A↔B = Inverse A↔B using (to; from; left-inverse-of)

right-inverse-of :  x  to ⟨\$⟩ (from ⟨\$⟩ x)  x
right-inverse-of x =
to ⟨\$⟩ (from ⟨\$⟩ x)                      ≡⟨ sym (A↔B.right-inverse-of _)
to ⟨\$⟩ (from ⟨\$⟩ (to ⟨\$⟩ (from ⟨\$⟩ x)))  ≡⟨ cong (to ⟨\$⟩_) (left-inverse-of _)
to ⟨\$⟩ (from ⟨\$⟩ x)                      ≡⟨ A↔B.right-inverse-of _
x

left-right :
x
cong (to ⟨\$⟩_) (left-inverse-of x)  right-inverse-of (to ⟨\$⟩ x)
left-right x =
cong (to ⟨\$⟩_) (left-inverse-of x)               ≡⟨⟩

trans refl (cong (to ⟨\$⟩_) (left-inverse-of _))  ≡⟨ cong  p  trans p (cong (to ⟨\$⟩_) _))
(sym (trans-symˡ (A↔B.right-inverse-of _)))
trans (trans (sym (A↔B.right-inverse-of _))
(A↔B.right-inverse-of _))
(cong (to ⟨\$⟩_) (left-inverse-of _))           ≡⟨ trans-assoc (sym (A↔B.right-inverse-of _))

trans (sym (A↔B.right-inverse-of _))
(trans (A↔B.right-inverse-of _)
(cong (to ⟨\$⟩_) (left-inverse-of _)))       ≡⟨ cong (trans (sym (A↔B.right-inverse-of _))) lemma

trans (sym (A↔B.right-inverse-of _))
(trans (cong (to ⟨\$⟩_) (left-inverse-of _))
(trans (A↔B.right-inverse-of _) refl))      ≡⟨⟩

right-inverse-of (to ⟨\$⟩ x)
where
lemma =
trans (A↔B.right-inverse-of _)
(cong (to ⟨\$⟩_) (left-inverse-of _))             ≡⟨ cong (trans (A↔B.right-inverse-of _)) (sym (cong-id _))

trans (A↔B.right-inverse-of _)
(cong id (cong (to ⟨\$⟩_) (left-inverse-of _)))   ≡⟨ sym (naturality A↔B.right-inverse-of)

trans (cong ((to ⟨\$⟩_)  (from ⟨\$⟩_))
(cong (to ⟨\$⟩_) (left-inverse-of _)))
(A↔B.right-inverse-of _)                         ≡⟨ cong  p  trans p (A↔B.right-inverse-of _))
(sym (cong-∘ _))
trans (cong ((to ⟨\$⟩_)  (from ⟨\$⟩_)  (to ⟨\$⟩_))
(left-inverse-of _))
(A↔B.right-inverse-of _)                         ≡⟨ cong  p  trans p (A↔B.right-inverse-of _))
(cong-∘ _)
trans (cong (to ⟨\$⟩_)
(cong ((from ⟨\$⟩_)  (to ⟨\$⟩_))
(left-inverse-of _)))
(A↔B.right-inverse-of _)                         ≡⟨ cong  p  trans (cong (to ⟨\$⟩_) p) _)
(cong-≡id left-inverse-of)
trans (cong (to ⟨\$⟩_) (left-inverse-of _))
(A↔B.right-inverse-of _)                         ≡⟨ cong (trans (cong (to ⟨\$⟩_) (left-inverse-of _)))
(sym (trans-reflʳ _))
trans (cong (to ⟨\$⟩_) (left-inverse-of _))
(trans (A↔B.right-inverse-of _) refl)