------------------------------------------------------------------------
-- Higher lenses, defined using the requirement that the remainder
-- function should be surjective
------------------------------------------------------------------------

import Equality.Path as P

module Lens.Non-dependent.Higher.Surjective-remainder
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Prelude

open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J hiding (_∘_)
open import H-level.Truncation.Propositional eq

open import Lens.Non-dependent eq
import Lens.Non-dependent.Higher eq as Higher

private
  variable
    a b : Level
    A B : Type a

-- A variant of the lenses defined in Lens.Non-dependent.Higher. In
-- this definition the function called inhabited is replaced by a
-- requirement that the remainder function should be surjective.

record Lens (A : Type a) (B : Type b) : Type (lsuc (a ⊔ b)) where
  field
    -- Remainder type.
    R : Type (a ⊔ b)

    -- Equivalence.
    equiv : A ≃ (R × B)

  -- Remainder.

  remainder : A → R
  remainder a = proj₁ (_≃_.to equiv a)

  field
    -- The remainder function is surjective.
    remainder-surjective : Surjective remainder

  -- Getter.

  get : A → B
  get a = proj₂ (_≃_.to equiv a)

  -- Setter.

  set : A → B → A
  set a b = _≃_.from equiv (remainder a , b)

instance

  -- The lenses defined above have getters and setters.

  has-getter-and-setter :
    Has-getter-and-setter (Lens {a = a} {b = b})
  has-getter-and-setter = record
    { get = Lens.get
    ; set = Lens.set
    }

-- Lens can be expressed as a nested Σ-type.

Lens-as-Σ :
  {A : Type a} {B : Type b} →
  Lens A B ≃
  ∃ λ (R : Type (a ⊔ b)) →
  ∃ λ (equiv : A ≃ (R × B)) →
    Surjective (proj₁ ∘ _≃_.to equiv)
Lens-as-Σ = Eq.↔→≃
  (λ l → R l , equiv l , remainder-surjective l)
  (λ (R , equiv , remainder-surjective) → record
     { R                    = R
     ; equiv                = equiv
     ; remainder-surjective = remainder-surjective
     })
  refl
  refl
  where
  open Lens

-- Higher.Lens A B is equivalent to Lens A B.

Higher-lens≃Lens : Higher.Lens A B ≃ Lens A B
Higher-lens≃Lens {A = A} {B = B} =
  Higher.Lens A B                              ↔⟨ Higher.Lens-as-Σ ⟩

  (∃ λ (R : Type _) →
     (A ≃ (R × B)) ×
     (R → ∥ B ∥))                              ↝⟨ (∃-cong λ _ → ∃-cong Higher.inhabited≃remainder-surjective) ⟩
  (∃ λ (R : Type _) →
   ∃ λ (equiv : A ≃ (R × B)) →
     Surjective (proj₁ ∘ _≃_.to equiv))        ↝⟨ inverse Lens-as-Σ ⟩□

  Lens A B                                     □

-- The equivalence preserves getters and setters.

Higher-lens≃Lens-preserves-getters-and-setters :
  Preserves-getters-and-setters-⇔ A B
    (_≃_.logical-equivalence Higher-lens≃Lens)
Higher-lens≃Lens-preserves-getters-and-setters =
    (λ _ → refl _ , refl _)
  , (λ _ → refl _ , refl _)