------------------------------------------------------------------------
-- The lens type in Lens.Non-dependent.Higher.Capriotti.Variant, but
-- with erased "proofs"
------------------------------------------------------------------------

import Equality.Path as P

module Lens.Non-dependent.Higher.Capriotti.Variant.Erased
  {e⁺} (eq :  {a p}  P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J using (_↔_)
open import Equality.Path.Isomorphisms eq
open import Equality.Path.Isomorphisms.Univalence eq
  using () renaming (opaque-univ to univ)
open import Equivalence equality-with-J as Eq using (_≃_)
open import Equivalence.Erased.Cubical eq as EEq using (_≃ᴱ_)
open import Equivalence.Erased.Contractible-preimages.Cubical eq as ECP
  using (_⁻¹ᴱ_)
open import Erased.Cubical eq
open import Extensionality equality-with-J
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as T using (∥_∥; ∣_∣)
open import Preimage equality-with-J using (_⁻¹_)
open import Univalence-axiom equality-with-J

open import Lens.Non-dependent eq
import Lens.Non-dependent.Higher.Erased eq as Higher
import Lens.Non-dependent.Higher.Capriotti.Variant eq as V

private
  variable
    a b p : Level
    A B   : Type a

------------------------------------------------------------------------
-- The lens type family

-- Coherently constant type-valued functions.

Coherently-constant :
  {A : Type a}  (A  Type p)  Type (a  lsuc p)
Coherently-constant {p = p} {A = A} P =
   λ (Q :  A   Type p)   x  P x ≃ᴱ Q  x 

-- Higher lenses with erased "proofs".

Lens : Type a  Type b  Type (lsuc (a  b))
Lens A B =  λ (get : A  B)  Coherently-constant (get ⁻¹ᴱ_)

-- In erased contexts Lens A B is equivalent to V.Lens A B.

@0 Lens≃Variant-lens : Lens A B  V.Lens A B
Lens≃Variant-lens =
  ( λ get   λ Q   x  get ⁻¹ᴱ x ≃ᴱ Q  x )  ↝⟨ (∃-cong λ _  ∃-cong λ _  ∀-cong ext λ _  inverse
                                                      EEq.≃≃≃ᴱ) 
  ( λ get   λ Q   x  get ⁻¹ᴱ x   Q  x )  ↝⟨ (∃-cong λ _  ∃-cong λ _  ∀-cong ext λ _ 
                                                      Eq.≃-preserves ext (inverse ECP.⁻¹≃⁻¹ᴱ) F.id) ⟩□
  ( λ get   λ Q   x  get ⁻¹  x   Q  x )  

-- Some derived definitions.

module Lens {A : Type a} {B : Type b} (l : Lens A B) where

  -- A getter.

  get : A  B
  get = proj₁ l

  -- A predicate.

  H : Pow a  B 
  H = proj₁ (proj₂ l)

  -- An equivalence (with erased proofs).

  get⁻¹ᴱ-≃ᴱ :  b  get ⁻¹ᴱ b ≃ᴱ H  b 
  get⁻¹ᴱ-≃ᴱ = proj₂ (proj₂ l)

  -- All the getter's "preimages" are equivalent (with erased proofs).

  get⁻¹ᴱ-constant : (b₁ b₂ : B)  get ⁻¹ᴱ b₁ ≃ᴱ get ⁻¹ᴱ b₂
  get⁻¹ᴱ-constant b₁ b₂ =
    get ⁻¹ᴱ b₁  ↝⟨ get⁻¹ᴱ-≃ᴱ b₁ 
    H  b₁     ↔⟨ ≡⇒≃ $ cong H $ T.truncation-is-proposition _ _ 
    H  b₂     ↝⟨ inverse $ get⁻¹ᴱ-≃ᴱ b₂ ⟩□
    get ⁻¹ᴱ b₂  

  -- The two directions of get⁻¹ᴱ-constant.

  get⁻¹ᴱ-const : (b₁ b₂ : B)  get ⁻¹ᴱ b₁  get ⁻¹ᴱ b₂
  get⁻¹ᴱ-const b₁ b₂ = _≃ᴱ_.to (get⁻¹ᴱ-constant b₁ b₂)

  get⁻¹ᴱ-const⁻¹ᴱ : (b₁ b₂ : B)  get ⁻¹ᴱ b₂  get ⁻¹ᴱ b₁
  get⁻¹ᴱ-const⁻¹ᴱ b₁ b₂ = _≃ᴱ_.from (get⁻¹ᴱ-constant b₁ b₂)

  -- Some coherence properties.

  @0 get⁻¹ᴱ-const-∘ :
    (b₁ b₂ b₃ : B) (p : get ⁻¹ᴱ b₁) 
    get⁻¹ᴱ-const b₂ b₃ (get⁻¹ᴱ-const b₁ b₂ p)  get⁻¹ᴱ-const b₁ b₃ p
  get⁻¹ᴱ-const-∘ b₁ b₂ b₃ p =
    _≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b₃)
      (≡⇒→ (cong H $ T.truncation-is-proposition _ _)
         (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b₂)
            (_≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b₂)
               (≡⇒→ (cong H $ T.truncation-is-proposition _ _)
                  (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b₁) p)))))                ≡⟨ cong (_≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ _)  ≡⇒→ _) $
                                                                   _≃ᴱ_.right-inverse-of (get⁻¹ᴱ-≃ᴱ _) _ 
    _≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b₃)
      (≡⇒→ (cong H $ T.truncation-is-proposition _ _)
         (≡⇒→ (cong H $ T.truncation-is-proposition _ _)
            (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b₁) p)))                        ≡⟨ cong  eq  _≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ _) (_≃_.to eq (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ _) _))) $ sym $
                                                                   ≡⇒≃-trans ext _ _ 
    _≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b₃)
      (≡⇒→ (trans (cong H $ T.truncation-is-proposition _ _)
              (cong H $ T.truncation-is-proposition _ _))
            (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b₁) p))                         ≡⟨ cong  eq  _≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b₃) (≡⇒→ eq _)) $
                                                                   trans (sym $ cong-trans _ _ _) $
                                                                   cong (cong H) $ mono₁ 1 T.truncation-is-proposition _ _ ⟩∎
    _≃ᴱ_.from (get⁻¹ᴱ-≃ᴱ b₃)
      (≡⇒→ (cong H $ T.truncation-is-proposition _ _)
         (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b₁) p))                            

  @0 get⁻¹ᴱ-const-id :
    (b : B) (p : get ⁻¹ᴱ b)  get⁻¹ᴱ-const b b p  p
  get⁻¹ᴱ-const-id b p =
    get⁻¹ᴱ-const b b p                                           ≡⟨ sym $ _≃ᴱ_.left-inverse-of (get⁻¹ᴱ-constant _ _) _ 
    get⁻¹ᴱ-const⁻¹ᴱ b b (get⁻¹ᴱ-const b b (get⁻¹ᴱ-const b b p))  ≡⟨ cong (get⁻¹ᴱ-const⁻¹ᴱ b b) $ get⁻¹ᴱ-const-∘ _ _ _ _ 
    get⁻¹ᴱ-const⁻¹ᴱ b b (get⁻¹ᴱ-const b b p)                     ≡⟨ _≃ᴱ_.left-inverse-of (get⁻¹ᴱ-constant _ _) _ ⟩∎
    p                                                            

  @0 get⁻¹ᴱ-const-inverse :
    (b₁ b₂ : B) (p : get ⁻¹ᴱ b₁) 
    get⁻¹ᴱ-const b₁ b₂ p  get⁻¹ᴱ-const⁻¹ᴱ b₂ b₁ p
  get⁻¹ᴱ-const-inverse b₁ b₂ p =
    sym $ _≃_.to-from (EEq.≃ᴱ→≃ (get⁻¹ᴱ-constant _ _)) (
      get⁻¹ᴱ-const b₂ b₁ (get⁻¹ᴱ-const b₁ b₂ p)  ≡⟨ get⁻¹ᴱ-const-∘ _ _ _ _ 
      get⁻¹ᴱ-const b₁ b₁ p                       ≡⟨ get⁻¹ᴱ-const-id _ _ ⟩∎
      p                                          )

  -- A setter.

  set : A  B  A
  set a b =                      $⟨ get⁻¹ᴱ-const _ _ 
    (get ⁻¹ᴱ get a  get ⁻¹ᴱ b)  ↝⟨ _$ (a , [ refl _ ]) 
    get ⁻¹ᴱ b                    ↝⟨ proj₁ ⟩□
    A                            

  -- Lens laws.

  @0 get-set :  a b  get (set a b)  b
  get-set a b =
    get (proj₁ (get⁻¹ᴱ-const (get a) b (a , [ refl _ ])))  ≡⟨ erased (proj₂ (get⁻¹ᴱ-const (get a) b (a , [ refl _ ]))) ⟩∎
    b                                                      

  @0 set-get :  a  set a (get a)  a
  set-get a =
    proj₁ (get⁻¹ᴱ-const (get a) (get a) (a , [ refl _ ]))  ≡⟨ cong proj₁ $ get⁻¹ᴱ-const-id _ _ ⟩∎
    a                                                      

  @0 set-set :  a b₁ b₂  set (set a b₁) b₂  set a b₂
  set-set a b₁ b₂ =
    proj₁ (get⁻¹ᴱ-const (get (set a b₁)) b₂ (set a b₁ , [ refl _ ]))  ≡⟨ elim¹
                                                                            {b} eq 
                                                                              proj₁ (get⁻¹ᴱ-const (get (set a b₁)) b₂ (set a b₁ , [ refl _ ])) 
                                                                              proj₁ (get⁻¹ᴱ-const b b₂ (set a b₁ , [ eq ])))
                                                                           (refl _)
                                                                           (get-set a b₁) 
    proj₁ (get⁻¹ᴱ-const b₁ b₂ (set a b₁ , [ get-set a b₁ ]))          ≡⟨⟩

    proj₁ (get⁻¹ᴱ-const b₁ b₂
             (get⁻¹ᴱ-const (get a) b₁ (a , [ refl _ ])))              ≡⟨ cong proj₁ $ get⁻¹ᴱ-const-∘ _ _ _ _ ⟩∎

    proj₁ (get⁻¹ᴱ-const (get a) b₂ (a , [ refl _ ]))                  

  -- TODO: Can get-set-get and get-set-set be proved for the lens laws
  -- given above?

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
    }

------------------------------------------------------------------------
-- Equality characterisation lemmas

opaque

  -- An equality characterisation lemma.

  @0 equality-characterisation₁ :
    {l₁ l₂ : Lens A B} 
    let open Lens in

    (l₁  l₂)
      
    ( λ (g : get l₁  get l₂) 
      λ (h : H l₁  H l₂) 
        b p 
       subst (_$  b ) h
         (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym g) p)) 
       _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)
  equality-characterisation₁ {A = A} {B = B} {l₁ = l₁} {l₂ = l₂} =
    l₁  l₂                                                           ↝⟨ inverse $ Eq.≃-≡ Lens≃Variant-lens 

    l₁′  l₂′                                                         ↝⟨ V.equality-characterisation₁ 

    ( λ (g : get l₁  get l₂) 
      λ (h : H l₁  H l₂) 
        b p 
       subst (_$  b ) h
         (_≃_.to (V.Lens.get⁻¹-≃ l₁′ b) (subst (_⁻¹ b) (sym g) p)) 
       _≃_.to (V.Lens.get⁻¹-≃ l₂′ b) p)                               ↝⟨ (∃-cong λ g  ∃-cong λ h  ∀-cong ext λ b 
                                                                          Π-cong ext ECP.⁻¹≃⁻¹ᴱ λ p 
                                                                          ≡⇒↝ _ $ cong  p′  subst (_$ _) h (_≃_.to (V.Lens.get⁻¹-≃ l₁′ _) p′) 
                                                                                               _≃_.to (V.Lens.get⁻¹-≃ l₂′ _) p)
                                                                            (
       subst (_⁻¹ b) (sym g) p                                               ≡⟨ elim₁
                                                                                   g  subst (_⁻¹ b) (sym g) p 
                                                                                         Σ-map id erased (subst (_⁻¹ᴱ b) (sym g) (Σ-map id [_]→ p)))
                                                                                  (
         subst (_⁻¹ b) (sym (refl _)) p                                            ≡⟨ trans (cong (flip (subst (_⁻¹ b)) _) sym-refl) $
                                                                                      subst-refl _ _ 

         p                                                                         ≡⟨ cong (Σ-map id erased) $ sym $
                                                                                      trans (cong (flip (subst (_⁻¹ᴱ b)) _) sym-refl) $
                                                                                      subst-refl _ _ ⟩∎
         Σ-map id erased
           (subst (_⁻¹ᴱ b) (sym (refl _)) (Σ-map id [_]→ p))                       )
                                                                                  _ 
       Σ-map id erased (subst (_⁻¹ᴱ b) (sym g) (Σ-map id [_]→ p))            ≡⟨⟩

       _≃_.from ECP.⁻¹≃⁻¹ᴱ
         (subst (_⁻¹ᴱ b) (sym g) (_≃_.to ECP.⁻¹≃⁻¹ᴱ p))                      )) ⟩□

    ( λ (g : get l₁  get l₂) 
      λ (h : H l₁  H l₂) 
        b p 
       subst (_$  b ) h
         (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym g) p)) 
       _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                    
    where
    open Lens

    l₁′ l₂′ : V.Lens A B
    l₁′ = _≃_.to Lens≃Variant-lens l₁
    l₂′ = _≃_.to Lens≃Variant-lens l₂

opaque

  -- Another equality characterisation lemma.

  @0 equality-characterisation₂ :
    {l₁ l₂ : Lens A B} 
    let open Lens in

    (l₁  l₂)
      
    ( λ (g :  a  get l₁ a  get l₂ a) 
      λ (h :  b  H l₁ b  H l₂ b) 
        b p 
       subst id (h  b )
         (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) 
       _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)
  equality-characterisation₂ {l₁ = l₁} {l₂ = l₂} =
    l₁  l₂                                                               ↝⟨ equality-characterisation₁ 

    ( λ (g : get l₁  get l₂) 
      λ (h : H l₁  H l₂) 
        b p 
       subst (_$  b ) h
         (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym g) p)) 
       _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                        ↝⟨ (Σ-cong-contra (Eq.extensionality-isomorphism ext) λ _ 
                                                                              Σ-cong-contra (Eq.extensionality-isomorphism ext) λ _ 
                                                                              F.id) 
    ( λ (g :  a  get l₁ a  get l₂ a) 
      λ (h :  b  H l₁ b  H l₂ b) 
        b p 
       subst (_$  b ) (⟨ext⟩ h)
         (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) 
       _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                        ↝⟨ (∃-cong λ _  ∃-cong λ _  ∀-cong ext λ _  ∀-cong ext λ _ 
                                                                              ≡⇒↝ _ $ cong (_≡ _) $
                                                                              subst-ext ext) ⟩□
    ( λ (g :  a  get l₁ a  get l₂ a) 
      λ (h :  b  H l₁ b  H l₂ b) 
        b p 
       subst id (h  b )
         (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) 
       _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                        
    where
    open Lens

opaque

  -- Yet another equality characterisation lemma.

  @0 equality-characterisation₃ :
    {l₁ l₂ : Lens A B} 
    let open Lens in

    (l₁  l₂)
      
    ( λ (g :  a  get l₁ a  get l₂ a) 
      λ (h :  b  H l₁ b  H l₂ b) 
        b p 
       _≃_.to (h  b )
         (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) 
       _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)
  equality-characterisation₃ {l₁ = l₁} {l₂ = l₂} =
    l₁  l₂                                                               ↝⟨ equality-characterisation₂ 

    ( λ (g :  a  get l₁ a  get l₂ a) 
      λ (h :  b  H l₁ b  H l₂ b) 
        b p 
       subst id (h  b )
         (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) 
       _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                        ↝⟨ (∃-cong λ _ 
                                                                              Σ-cong-contra (∀-cong ext λ _  inverse $ ≡≃≃ univ) λ _  F.id) 
    ( λ (g :  a  get l₁ a  get l₂ a) 
      λ (h :  b  H l₁ b  H l₂ b) 
        b p 
       subst id (≃⇒≡ univ (h  b ))
         (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) 
       _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                        ↝⟨ (∃-cong λ _  ∃-cong λ _  ∀-cong ext λ _  ∀-cong ext λ _ 
                                                                              ≡⇒↝ _ $ cong (_≡ _) $
                                                                              trans (subst-id-in-terms-of-≡⇒↝ equivalence) $
                                                                              cong  eq  _≃_.to eq _) $
                                                                              _≃_.right-inverse-of (≡≃≃ univ) _) ⟩□
    ( λ (g :  a  get l₁ a  get l₂ a) 
      λ (h :  b  H l₁ b  H l₂ b) 
        b p 
       _≃_.to (h  b )
         (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₁ b) (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ g)) p)) 
       _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ l₂ b) p)                                        
    where
    open Lens

------------------------------------------------------------------------
-- Conversion functions

opaque

  -- The lenses defined above can be converted to and from the lenses
  -- defined in Higher.

  Lens⇔Higher-lens : Lens A B  Higher.Lens A B
  Lens⇔Higher-lens {A = A} {B = B} = record
    { to = λ (g , H , eq)  record
             { R = Σ  B  H

             ; equiv =
                 A                                               ↝⟨ (inverse $ drop-⊤-right λ _  _⇔_.to EEq.Contractibleᴱ⇔≃ᴱ⊤
                                                                     Contractibleᴱ-Erased-other-singleton) 
                 ( λ (a : A)   λ (b : B)  Erased (g a  b))  ↔⟨ ∃-comm 
                 ( λ (b : B)  g ⁻¹ᴱ b)                         ↝⟨ ∃-cong eq 
                 ( λ (b : B)  H  b )                         ↔⟨ (Σ-cong (inverse T.∥∥×≃) λ _  ≡⇒≃ $ cong H $ T.truncation-is-proposition _ _) 
                 ( λ ((b , _) :  B  × B)  H b)               ↔⟨ Σ-assoc F.∘
                                                                    (∃-cong λ _  ×-comm) F.∘
                                                                    inverse Σ-assoc ⟩□
                 Σ  B  H × B                                   

             ; inhabited = proj₁
             }
    ; from = λ l 
                 Higher.Lens.get l
               ,  _  Higher.Lens.R l)
               ,  b  inverse (Higher.remainder≃ᴱget⁻¹ᴱ l b))
    }

opaque
  unfolding Lens⇔Higher-lens

  -- The conversion preserves getters and setters.

  Lens⇔Higher-lens-preserves-getters-and-setters :
    Preserves-getters-and-setters-⇔ A B Lens⇔Higher-lens
  Lens⇔Higher-lens-preserves-getters-and-setters =
       l@(g , H , eq) 
           refl _
         , ⟨ext⟩ λ a  ⟨ext⟩ λ b 
           let h₁ = _≃ᴱ_.to (eq (g a)) (a , [ refl _ ])

               h₂ =
                 _≃_.from (≡⇒≃ (cong H _))
                   (subst (H  proj₁) (sym (_≃_.left-inverse-of T.∥∥×≃ _))
                      (≡⇒→ (cong H _) h₁))

               h₃ = ≡⇒→ (cong H _) h₁

               lemma =
                 h₂                                         ≡⟨ sym $ subst-in-terms-of-inverse∘≡⇒↝ equivalence _ _ _ 

                 subst H _
                   (subst (H  proj₁)
                      (sym (_≃_.left-inverse-of T.∥∥×≃ _))
                      (≡⇒→ (cong H _) h₁))                  ≡⟨ cong  x  subst H (sym $ T.truncation-is-proposition _ _)
                                                                             (subst (H  proj₁)
                                                                                (sym (_≃_.left-inverse-of T.∥∥×≃ ( g a  , b)))
                                                                                x)) $ sym $
                                                               subst-in-terms-of-≡⇒↝ equivalence _ _ _ 
                 subst H _
                   (subst (H  proj₁)
                      (sym (_≃_.left-inverse-of T.∥∥×≃ _))
                      (subst H _ h₁))                       ≡⟨ cong  x  subst H (sym $ T.truncation-is-proposition _ _) x) $
                                                               subst-∘ _ _ _ 

                 subst H _ (subst H _ (subst H _ h₁))       ≡⟨ cong  x  subst H (sym $ T.truncation-is-proposition _ _) x) $
                                                               subst-subst _ _ _ _ 

                 subst H _ (subst H _ h₁)                   ≡⟨ subst-subst _ _ _ _ 

                 subst H _ h₁                               ≡⟨ cong  eq  subst H eq h₁) $
                                                               mono₁ 1 T.truncation-is-proposition _ _ 

                 subst H _ h₁                               ≡⟨ subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩∎

                 ≡⇒→ (cong H _) h₁                          
           in
           proj₁ (_≃ᴱ_.from (eq b) h₂)  ≡⟨ cong  h  proj₁ (_≃ᴱ_.from (eq b) h)) lemma ⟩∎
           proj₁ (_≃ᴱ_.from (eq b) h₃)  )
    ,  l 
           refl _
         , ⟨ext⟩ λ a  ⟨ext⟩ λ b 
           Lens.set (_⇔_.from Lens⇔Higher-lens l) a b        ≡⟨⟩

           _≃ᴱ_.from (Higher.Lens.equiv l)
             ( ≡⇒→ (cong  _  Higher.Lens.R l) _)
                 (Higher.Lens.remainder l a)
             , b
             )                                               ≡⟨ cong  eq  _≃ᴱ_.from (Higher.Lens.equiv l) (≡⇒→ eq _ , b)) $
                                                                cong-const _ 
           _≃ᴱ_.from (Higher.Lens.equiv l)
             (≡⇒→ (refl _) (Higher.Lens.remainder l a) , b)  ≡⟨ cong  f  _≃ᴱ_.from (Higher.Lens.equiv l) (f _ , b)) $
                                                                ≡⇒→-refl 
           _≃ᴱ_.from (Higher.Lens.equiv l)
             (Higher.Lens.remainder l a , b)                 ≡⟨⟩

           Higher.Lens.set l a b                             )

-- Lens A B is equivalent to Higher.Lens A B (with erased proofs).

Lens≃ᴱHigher-lens : Lens A B ≃ᴱ Higher.Lens A B
Lens≃ᴱHigher-lens {A = A} {B = B} =
  EEq.↔→≃ᴱ
    (_⇔_.to Lens⇔Higher-lens)
    (_⇔_.from Lens⇔Higher-lens)
    to∘from
    from∘to
  where
  opaque
    unfolding Lens⇔Higher-lens

    @0 to∘from :
      (l : Higher.Lens A B) 
      _⇔_.to Lens⇔Higher-lens (_⇔_.from Lens⇔Higher-lens l)  l
    to∘from l = _↔_.from Higher.equality-characterisation₂
      ( ( B  × R  ↔⟨ (drop-⊤-left-× λ r  _⇔_.to contractible⇔↔⊤ $
                        propositional⇒inhabited⇒contractible
                          T.truncation-is-proposition
                          (inhabited r)) ⟩□
         R          )
      ,  a 
           ≡⇒→ (cong  _  R) (T.truncation-is-proposition _ _))
             (remainder a)                                         ≡⟨ cong  eq  ≡⇒→ eq _) $ cong-const _ 

           ≡⇒→ (refl _) (remainder a)                              ≡⟨ cong (_$ _) ≡⇒→-refl ⟩∎

           remainder a                                             )
      ,  _  refl _)
      )
      where
      open Higher.Lens l

    @0 from∘to :
      (l : Lens A B) 
      _⇔_.from Lens⇔Higher-lens (_⇔_.to Lens⇔Higher-lens l)  l
    from∘to l = _≃_.from equality-characterisation₃
      (  _  refl _)
      , Σ∥B∥H≃H
      ,  b p@(a , [ get-a≡b ]) 
           _≃_.to (Σ∥B∥H≃H  b )
             (_≃ᴱ_.from (Higher.remainder≃ᴱget⁻¹ᴱ
                           (_⇔_.to Lens⇔Higher-lens l) b)
                (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ λ _  refl _)) p))       ≡⟨ cong (_≃_.to (Σ∥B∥H≃H  b ) 
                                                                              _≃ᴱ_.from (Higher.remainder≃ᴱget⁻¹ᴱ
                                                                                           (_⇔_.to Lens⇔Higher-lens l) b)) $
                                                                        trans (cong (flip (subst (_⁻¹ᴱ b)) p) $
                                                                               trans (cong sym $ ext-refl ext) $
                                                                               sym-refl) $
                                                                        subst-refl _ _ 
           _≃_.to (Σ∥B∥H≃H  b )
             (_≃ᴱ_.from (Higher.remainder≃ᴱget⁻¹ᴱ
                           (_⇔_.to Lens⇔Higher-lens l) b)
                p)                                                   ≡⟨⟩

           _≃_.to (Σ∥B∥H≃H  b )
             (Higher.Lens.remainder (_⇔_.to Lens⇔Higher-lens l) a)   ≡⟨⟩

           subst H _
             (≡⇒→ (cong H _) (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a))
                                (a , [ refl _ ])))                   ≡⟨ cong (subst H _) $ sym $
                                                                        subst-in-terms-of-≡⇒↝ equivalence _ _ _ 

           subst H _ (subst H _ (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a))
                                   (a , [ refl _ ])))                ≡⟨ subst-subst _ _ _ _ 

           subst H _ (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a)) (a , [ refl _ ]))  ≡⟨ cong  eq  subst H eq (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a)) (a , [ refl _ ]))) $
                                                                        mono₁ 1 T.truncation-is-proposition _ _ 
           subst H (cong ∣_∣ get-a≡b)
             (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a)) (a , [ refl _ ]))          ≡⟨ elim¹
                                                                           {b} eq 
                                                                             subst H (cong ∣_∣ eq)
                                                                               (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a)) (a , [ refl _ ])) 
                                                                             _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b) (a , [ eq ]))
                                                                          (
             subst H (cong ∣_∣ (refl _))
               (_≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a)) (a , [ refl _ ]))              ≡⟨ trans (cong (flip (subst H) _) $ cong-refl _) $
                                                                              subst-refl _ _ 
             _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ (get a)) (a , [ refl _ ])                  )
                                                                          _ ⟩∎
           _≃ᴱ_.to (get⁻¹ᴱ-≃ᴱ b) p                                   )
      )
      where
      open Lens l

      Σ∥B∥H≃H :  b  Σ  B  H  H b
      Σ∥B∥H≃H b =
        Σ  B  H  ↔⟨ (drop-⊤-left-Σ $ _⇔_.to contractible⇔↔⊤ $
                       propositional⇒inhabited⇒contractible
                         T.truncation-is-proposition b) ⟩□
        H b        

-- The equivalence preserves getters and setters.

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