    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- This module is DEPRECATED.
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}
    {-# OPTIONS --warning=noUserWarning #-}

    module Function.HalfAdjointEquivalence where

    {-# WARNING_ON_IMPORT
    "Function.HalfAdjointEquivalence was deprecated in v2.0.
    Use Function.Properties.Inverse.HalfAdjointEquivalence instead."
    #-}

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

    infix 4 _≃_

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