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

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

module Function.Properties.Inverse.HalfAdjointEquivalence where

open import Function.Base
open import Function
open import Level
open import Relation.Binary.PropositionalEquality

private
  variable
    a b : Level
    A B : Set a

-- Half adjoint equivalences (see the HoTT book).
--
-- They are inverses with an extra coherence condition that the left
-- and right inversion proofs interact the right way with `cong`.

infix 4 _≃_

record _≃_ (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)

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

-- Half adjoint equivalences can be turned into inverses.

≃⇒↔ : A  B  A  B
≃⇒↔ A≃B = mk↔ₛ′ to from right-inverse-of left-inverse-of
  where open _≃_ A≃B

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

↔⇒≃ : A  B  A  B
↔⇒≃ A↔B = record
  { to               = to
  ; from             = from
  ; left-inverse-of  = strictlyInverseʳ
  ; right-inverse-of = right-inverse-of
  ; left-right       = left-right
  }
  where
  open ≡-Reasoning
  open module A↔B = Inverse A↔B

  right-inverse-of :  x  to (from x)  x
  right-inverse-of x =
    to (from x)               ≡⟨ sym (A↔B.strictlyInverseˡ _) 
    to (from (to (from x)))   ≡⟨ cong to (strictlyInverseʳ  _) 
    to (from x)               ≡⟨ A↔B.strictlyInverseˡ _ 
    x                         

  left-right :
     x 
    cong to (strictlyInverseʳ x)  right-inverse-of (to x)
  left-right x =
    cong to (strictlyInverseʳ x)               ≡⟨⟩

    trans refl (cong to (strictlyInverseʳ _))  ≡⟨ cong  p  trans p (cong to (strictlyInverseʳ _)))
                                                          (sym (trans-symˡ (A↔B.strictlyInverseˡ _))) 
    trans (trans (sym (A↔B.strictlyInverseˡ _))
               (A↔B.strictlyInverseˡ _))
      (cong to (strictlyInverseʳ _))           ≡⟨ trans-assoc (sym (A↔B.strictlyInverseˡ _)) 

    trans (sym (A↔B.strictlyInverseˡ _))
      (trans (A↔B.strictlyInverseˡ _)
         (cong to (strictlyInverseʳ _)))       ≡⟨ cong (trans (sym (A↔B.strictlyInverseˡ _))) lemma 

    trans (sym (A↔B.strictlyInverseˡ _))
      (trans (cong to (strictlyInverseʳ _))
         (trans (A↔B.strictlyInverseˡ _) refl))      ≡⟨⟩

    right-inverse-of (to x)                      
    where
    lemma =
      trans (A↔B.strictlyInverseˡ _)
        (cong to (strictlyInverseʳ _))             ≡⟨ cong (trans (A↔B.strictlyInverseˡ _)) (sym (cong-id _)) 

      trans (A↔B.strictlyInverseˡ _)
        (cong id (cong to (strictlyInverseʳ _)))   ≡⟨ sym (naturality A↔B.strictlyInverseˡ) 

      trans (cong (to  from)
                 (cong to (strictlyInverseʳ _)))
        (A↔B.strictlyInverseˡ _)                         ≡⟨ cong  p  trans p (A↔B.strictlyInverseˡ _))
                                                              (sym (cong-∘ _)) 
      trans (cong (to  from  to)
                      (strictlyInverseʳ _))
        (A↔B.strictlyInverseˡ _)                         ≡⟨ cong  p  trans p (A↔B.strictlyInverseˡ _))
                                                              (cong-∘ _) 
      trans (cong to
                 (cong (from  to)
                    (strictlyInverseʳ _)))
        (A↔B.strictlyInverseˡ _)                         ≡⟨ cong  p  trans (cong to p) (strictlyInverseˡ (to x)))
                                                              (cong-≡id strictlyInverseʳ) 
      trans (cong to (strictlyInverseʳ _))
        (A↔B.strictlyInverseˡ _)                         ≡⟨ cong (trans (cong to (strictlyInverseʳ _)))
                                                              (sym (trans-reflʳ _)) 
      trans (cong to (strictlyInverseʳ _))
        (trans (A↔B.strictlyInverseˡ _) refl)