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

-- An equality characterisation lemma.

@0 equality-characterisation₁ :
  {A : Type a} {B : Type b} {l₁ l₂ : Lens A B} 
  Block "equality-characterisation" 
  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} {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₁′ = _≃_.to Lens≃Variant-lens l₁
  l₂′ = _≃_.to Lens≃Variant-lens l₂

-- Another equality characterisation lemma.

@0 equality-characterisation₂ :
  {l₁ l₂ : Lens A B} 
  Block "equality-characterisation" 
  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

-- Yet another equality characterisation lemma.

@0 equality-characterisation₃ :
  {A : Type a} {B : Type b}
  {l₁ l₂ : Lens A B} 
  Block "equality-characterisation" 
  Univalence (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₂}  univ =
  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

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

Lens⇔Higher-lens :
  Block "conversion" 
  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))
  }

-- The conversion preserves getters and setters.

Lens⇔Higher-lens-preserves-getters-and-setters :
  (bl : Block "conversion") 
  Preserves-getters-and-setters-⇔ A B (Lens⇔Higher-lens bl)
Lens⇔Higher-lens-preserves-getters-and-setters bl@ =
     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 bl) 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,
-- assuming univalence).

Lens≃ᴱHigher-lens :
  {A : Type a} {B : Type b} 
  Block "conversion" 
  @0 Univalence (a  b) 
  Lens A B ≃ᴱ Higher.Lens A B
Lens≃ᴱHigher-lens {A = A} {B = B} bl univ =
  EEq.↔→≃ᴱ
    (_⇔_.to (Lens⇔Higher-lens bl))
    (_⇔_.from (Lens⇔Higher-lens bl))
    (to∘from bl)
    (from∘to bl)
  where
  @0 to∘from :
    (bl : Block "conversion") 
     l 
    _⇔_.to (Lens⇔Higher-lens bl) (_⇔_.from (Lens⇔Higher-lens bl) l)  l
  to∘from  l = _↔_.from (Higher.equality-characterisation₂ univ)
    ( ( 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 :
    (bl : Block "conversion") 
     l 
    _⇔_.from (Lens⇔Higher-lens bl) (_⇔_.to (Lens⇔Higher-lens bl) l)  l
  from∘to bl@ l = _≃_.from (equality-characterisation₃  univ)
    (  _  refl _)
    , Σ∥B∥H≃H
    ,  b p@(a , [ get-a≡b ]) 
         _≃_.to (Σ∥B∥H≃H  b )
           (_≃ᴱ_.from (Higher.remainder≃ᴱget⁻¹ᴱ
                         (_⇔_.to (Lens⇔Higher-lens bl) l) b)
              (subst (_⁻¹ᴱ b) (sym (⟨ext⟩ λ _  refl _)) p))       ≡⟨ cong (_≃_.to (Σ∥B∥H≃H  b ) 
                                                                            _≃ᴱ_.from (Higher.remainder≃ᴱget⁻¹ᴱ
                                                                                         (_⇔_.to (Lens⇔Higher-lens bl) 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 bl) l) b)
              p)                                                   ≡⟨⟩

         _≃_.to (Σ∥B∥H≃H  b )
           (Higher.Lens.remainder
              (_⇔_.to (Lens⇔Higher-lens bl) 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  ↔⟨ (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 :
  {A : Type a} {B : Type b}
  (bl : Block "conversion")
  (@0 univ : Univalence (a  b)) 
  Preserves-getters-and-setters-⇔ A B
    (_≃ᴱ_.logical-equivalence (Lens≃ᴱHigher-lens bl univ))
Lens≃ᴱHigher-lens-preserves-getters-and-setters bl univ =
  Lens⇔Higher-lens-preserves-getters-and-setters bl