------------------------------------------------------------------------
-- The Agda standard library
--
-- Half adjoint equivalences
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Function.HalfAdjointEquivalence where

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)            ∎