------------------------------------------------------------------------
-- Traditional non-dependent lenses with erased lens laws
------------------------------------------------------------------------

import Equality.Path as P

module Lens.Non-dependent.Traditional.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 as P hiding (id; [_,_]) renaming (_∘_ to _⊚_)

import Bi-invertibility.Erased
open import Bijection equality-with-J as Bij using (_↔_)
open import Circle eq using (𝕊¹)
open import Circle.Erased eq as CE using (𝕊¹ᴱ)
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq
  using (_≃_; Is-equivalence)
open import Equivalence.Erased.Cubical eq as EEq
  using (_≃ᴱ_; Is-equivalenceᴱ)
open import Equivalence.Erased.Contractible-preimages equality-with-J
  as ECP using (Contractibleᴱ; _⁻¹ᴱ_)
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 as H-level
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as PT using (∥_∥)
open import H-level.Truncation.Propositional.Erased eq as TE
  using (∥_∥ᴱ; ∣_∣)
open import Preimage equality-with-J using (_⁻¹_)
open import Surjection equality-with-J as Surjection using (_↠_)
open import Univalence-axiom equality-with-J

open import Lens.Non-dependent eq as Non-dependent
  hiding (no-first-projection-lens)
import Lens.Non-dependent.Traditional eq as T
import Lens.Non-dependent.Traditional.Combinators eq as TC

private
  variable
    a b c p             : Level
    A A₁ A₂ B B₁ B₂ C D : Type a
    u v x₁ x₂ y₁ y₂     : A

------------------------------------------------------------------------
-- Traditional lenses

-- Lenses with erased lens laws.

record Lens (A : Type a) (B : Type b) : Type (a  b) where
  field
    -- Getter and setter.
    get : A  B
    set : A  B  A

    -- Lens laws.
    @0 get-set :  a b  get (set a b)  b
    @0 set-get :  a  set a (get a)  a
    @0 set-set :  a b₁ b₂  set (set a b₁) b₂  set a b₂

  -- A combination of get and set.

  modify : (B  B)  A  A
  modify f x = set x (f (get x))

instance

  -- Traditional lenses with erased laws 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 A B is isomorphic to a nested Σ-type.

Lens-as-Σ :
  Lens A B 
   λ (get : A  B) 
   λ (set : A  B  A) 
  Erased ((∀ a b  get (set a b)  b) ×
          (∀ a  set a (get a)  a) ×
          (∀ a b₁ b₂  set (set a b₁) b₂  set a b₂))
Lens-as-Σ = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ l  get l , set l
                   , [ get-set l , set-get l , set-set l ]
      ; from = λ { (get , set , [ get-set , set-get , set-set ]) 
                   record
                     { get     = get
                     ; set     = set
                     ; get-set = get-set
                     ; set-get = set-get
                     ; set-set = set-set
                     }
                 }
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  }
  where
  open Lens

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

@0 Lens≃Traditional-lens : Lens A B  T.Lens A B
Lens≃Traditional-lens {A = A} {B = B} =
  Lens A B                                               ↔⟨ Lens-as-Σ 

  ( λ (get : A  B) 
    λ (set : A  B  A) 
   Erased ((∀ a b  get (set a b)  b) ×
           (∀ a  set a (get a)  a) ×
           (∀ a b₁ b₂  set (set a b₁) b₂  set a b₂)))  ↔⟨ (∃-cong λ _  ∃-cong λ _  erased Erased↔) 

  ( λ (get : A  B) 
    λ (set : A  B  A) 
   (∀ a b  get (set a b)  b) ×
   (∀ a  set a (get a)  a) ×
   (∀ a b₁ b₂  set (set a b₁) b₂  set a b₂))           ↔⟨ inverse T.Lens-as-Σ ⟩□

  T.Lens A B                                             

-- Lenses without erased proofs can be turned into lenses with erased
-- proofs (in erased contexts).

@0 Traditional-lens→Lens : T.Lens A B  Lens A B
Traditional-lens→Lens = _≃_.from Lens≃Traditional-lens

private

  -- The forward direction of Lens≃Traditional-lens.

  @0 trad : Lens A B  T.Lens A B
  trad = _≃_.to Lens≃Traditional-lens

private
  variable
    l₁ l₂ : Lens A B

------------------------------------------------------------------------
-- Somewhat coherent lenses

-- Traditional lenses with erased lens laws that satisfy some extra
-- coherence properties (that are also erased).

record Coherent-lens (A : Type a) (B : Type b) : Type (a  b) where
  field
    lens : Lens A B

  open Lens lens public

  field
    @0 get-set-get :  a  cong get (set-get a)  get-set a (get a)
    @0 get-set-set :
       a b₁ b₂ 
      cong get (set-set a b₁ b₂) 
      trans (get-set (set a b₁) b₂) (sym (get-set a b₂))

instance

  -- Somewhat coherent lenses have getters and setters.

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

-- Coherent-lens A B is equivalent to a nested Σ-type.

Coherent-lens-as-Σ :
  Coherent-lens A B 
   λ (l : Lens A B) 
    let open Lens l in
    Erased
      ((∀ a  cong get (set-get a)  get-set a (get a)) ×
       (∀ a b₁ b₂ 
        cong get (set-set a b₁ b₂) 
        trans (get-set (set a b₁) b₂) (sym (get-set a b₂))))
Coherent-lens-as-Σ = Eq.↔→≃
   l  lens l , [ get-set-get l , get-set-set l ])
   (l , [ get-set-get , get-set-set ])  record
     { lens        = l
     ; get-set-get = get-set-get
     ; get-set-set = get-set-set
     })
  refl
  refl
  where
  open Coherent-lens

-- In erased contexts Coherent-lens A B is equivalent to
-- T.Coherent-lens A B.

@0 Coherent-lens≃Traditional-coherent-lens :
  Coherent-lens A B  T.Coherent-lens A B
Coherent-lens≃Traditional-coherent-lens {A = A} {B = B} =
  Coherent-lens A B                                           ↔⟨ Coherent-lens-as-Σ 

  ( λ (l : Lens A B) 
   let open Lens l in
   Erased
     ((∀ a  cong get (set-get a)  get-set a (get a)) ×
      (∀ a b₁ b₂ 
       cong get (set-set a b₁ b₂) 
       trans (get-set (set a b₁) b₂) (sym (get-set a b₂)))))  ↔⟨ (Σ-cong Lens≃Traditional-lens λ _  erased Erased↔) 

  ( λ (l : T.Lens A B) 
   let open T.Lens l in
   (∀ a  cong get (set-get a)  get-set a (get a)) ×
   (∀ a b₁ b₂ 
    cong get (set-set a b₁ b₂) 
    trans (get-set (set a b₁) b₂) (sym (get-set a b₂))))      ↔⟨ inverse T.Coherent-lens-as-Σ 

  T.Coherent-lens A B                                         

------------------------------------------------------------------------
-- Some lemmas

-- If two lenses have equal setters, then they also have equal
-- getters (in erased contexts).

@0 getters-equal-if-setters-equal :
  let open Lens in
  (l₁ l₂ : Lens A B) 
  set l₁  set l₂ 
  get l₁  get l₂
getters-equal-if-setters-equal l₁ l₂ =
  Lens.set l₁  Lens.set l₂                    ↔⟨⟩
  T.Lens.set (trad l₁)  T.Lens.set (trad l₂)  ↝⟨ T.getters-equal-if-setters-equal (trad l₁) (trad l₂) 
  T.Lens.get (trad l₁)  T.Lens.get (trad l₂)  ↔⟨⟩
  Lens.get l₁  Lens.get l₂                    

-- If the forward direction of an equivalence with erased proofs is
-- Lens.get l, then the setter of l can be expressed using the other
-- direction of the equivalence (in erased contexts).

@0 from≡set :
   (l : Lens A B) is-equiv 
  let open Lens
      A≃B = EEq.⟨ get l , is-equiv 
  in
   a b  _≃ᴱ_.from A≃B b  set l a b
from≡set l is-equiv =
  T.from≡set (trad l) (EEq.Is-equivalenceᴱ→Is-equivalence is-equiv)

-- If A and B are "very stable n levels up" (given certain
-- assumptions), then Lens A B is "very stable n levels up".

Very-stable-Lensⁿ :
   n 
  (A  B  For-iterated-equality n Very-stable A) 
  (A  For-iterated-equality n Very-stable B) 
  For-iterated-equality n Very-stable (Lens A B)
Very-stable-Lensⁿ {A = A} {B = B} n A-s B-s =
  Very-stable-congⁿ _ n (inverse Lens-as-Σ) $
  Very-stable-Σⁿ n (Very-stable-Πⁿ ext n λ a 
                    B-s a) λ _ 
  Very-stable-Σⁿ n (Very-stable-Πⁿ ext n λ a 
                    Very-stable-Πⁿ ext n λ b 
                    A-s a b) λ _ 
  Very-stable→Very-stableⁿ n
  Very-stable-Erased

------------------------------------------------------------------------
-- Some lens isomorphisms

-- Lens preserves equivalences.

Lens-cong : A₁  A₂  B₁  B₂  Lens A₁ B₁  Lens A₂ B₂
Lens-cong {A₁ = A₁} {A₂ = A₂} {B₁ = B₁} {B₂ = B₂} A₁≃A₂ B₁≃B₂ =
  Lens A₁ B₁                                             ↔⟨ Lens-as-Σ 

  ( λ (get : A₁  B₁) 
    λ (set : A₁  B₁  A₁) 
   Erased ((∀ a b  get (set a b)  b) ×
           (∀ a  set a (get a)  a) ×
           (∀ a b₁ b₂  set (set a b₁) b₂  set a b₂)))  ↝⟨ (Σ-cong (→-cong ext A₁≃A₂ B₁≃B₂) λ get 
                                                             Σ-cong (→-cong ext A₁≃A₂ $ →-cong ext B₁≃B₂ A₁≃A₂) λ set 
                                                             Erased-cong (
                                                             (Π-cong ext A₁≃A₂ λ a  Π-cong ext B₁≃B₂ λ b 
                                                              inverse (Eq.≃-≡ B₁≃B₂) F.∘
                                                              (≡⇒≃ $ cong (_≡ _)
      (get (set a b)                                            ≡⟨ sym $ cong₂  a b  get (set a b))
                                                                     (_≃_.left-inverse-of A₁≃A₂ _)
                                                                     (_≃_.left-inverse-of B₁≃B₂ _) 
       get (set (_≃_.from A₁≃A₂ (_≃_.to A₁≃A₂ a))
              (_≃_.from B₁≃B₂ (_≃_.to B₁≃B₂ b)))                ≡⟨ cong get $ sym $ _≃_.left-inverse-of A₁≃A₂ _ ⟩∎

       get (_≃_.from A₁≃A₂ (_≃_.to A₁≃A₂
              (set (_≃_.from A₁≃A₂ (_≃_.to A₁≃A₂ a))
                 (_≃_.from B₁≃B₂ (_≃_.to B₁≃B₂ b)))))           )))
                                                               ×-cong
                                                             (Π-cong ext A₁≃A₂ λ a 
                                                              inverse (Eq.≃-≡ A₁≃A₂) F.∘
                                                              (≡⇒≃ $ cong (_≡ _)
      (set a (get a)                                             ≡⟨ cong (set a) $ sym $ _≃_.left-inverse-of B₁≃B₂ _ 

       set a (_≃_.from B₁≃B₂ (_≃_.to B₁≃B₂ (get a)))             ≡⟨ cong  a  set a (_≃_.from B₁≃B₂ (_≃_.to B₁≃B₂ (get a)))) $ sym $
                                                                    _≃_.left-inverse-of A₁≃A₂ _ ⟩∎
       set (_≃_.from A₁≃A₂ (_≃_.to A₁≃A₂ a))
         (_≃_.from B₁≃B₂ (_≃_.to B₁≃B₂
            (get (_≃_.from A₁≃A₂ (_≃_.to A₁≃A₂ a)))))            )))
                                                               ×-cong
                                                             (inverse $ Π-cong ext (inverse A₁≃A₂) λ a 
                                                              inverse $ Π-cong ext B₁≃B₂ λ b₁ 
                                                              inverse $ Π-cong ext (inverse B₁≃B₂) λ b₂ 
                                                              (≡⇒≃ $ cong  a′  set a′ (_≃_.from B₁≃B₂ b₂) 
                                                                                  set (_≃_.from A₁≃A₂ a) (_≃_.from B₁≃B₂ b₂))
      (_≃_.from A₁≃A₂ (_≃_.to A₁≃A₂
         (set (_≃_.from A₁≃A₂ a)
            (_≃_.from B₁≃B₂ (_≃_.to B₁≃B₂ b₁))))                 ≡⟨ _≃_.left-inverse-of A₁≃A₂ _ 

       set (_≃_.from A₁≃A₂ a)
         (_≃_.from B₁≃B₂ (_≃_.to B₁≃B₂ b₁))                      ≡⟨ cong (set (_≃_.from A₁≃A₂ a)) $
                                                                    _≃_.left-inverse-of B₁≃B₂ _ ⟩∎

       set (_≃_.from A₁≃A₂ a) b₁                                 )) F.∘
                                                              Eq.≃-≡ A₁≃A₂))) 
  ( λ (get : A₂  B₂) 
    λ (set : A₂  B₂  A₂) 
   Erased ((∀ a b  get (set a b)  b) ×
           (∀ a  set a (get a)  a) ×
           (∀ a b₁ b₂  set (set a b₁) b₂  set a b₂)))  ↔⟨ inverse Lens-as-Σ ⟩□

  Lens A₂ B₂                                             

-- If B is a proposition (when A is inhabited), then Lens A B is
-- equivalent (with erased proofs) to
-- (A → B) × Erased ((a : A) → a ≡ a).

lens-to-proposition≃ᴱ :
  @0 (A  Is-proposition B) 
  Lens A B ≃ᴱ ((A  B) × Erased ((a : A)  a  a))
lens-to-proposition≃ᴱ {A = A} {B = B} B-prop =
  Lens A B                                                          ↔⟨ Lens-as-Σ 

  ( λ (get : A  B) 
    λ (set : A  B  A) 
     Erased
       ((∀ a b  get (set a b)  b) ×
        (∀ a  set a (get a)  a) ×
        (∀ a b₁ b₂  set (set a b₁) b₂  set a b₂)))                ↔⟨ (∃-cong λ _  ∃-cong λ _  Erased-cong (
                                                                        drop-⊤-left-× λ _ 
                                                                        _⇔_.to contractible⇔↔⊤ $
                                                                        Π-closure ext 0 λ a 
                                                                        Π-closure ext 0 λ _ 
                                                                        +⇒≡ (B-prop a))) 
  ( λ (get : A  B) 
    λ (set : A  B  A) 
     Erased
       ((∀ a  set a (get a)  a) ×
        (∀ a b₁ b₂  set (set a b₁) b₂  set a b₂)))                ↔⟨ (∃-cong λ get  ∃-cong λ set  Erased-cong (∃-cong λ _ 
                                                                        ∀-cong ext λ a  ∀-cong ext λ b₁  ∀-cong ext λ b₂ 
                                                                        ≡⇒≃ (
       (set (set a b₁)                         b₂  set a b₂)             ≡⟨ cong  b  set (set a b) b₂  _) (B-prop a _ _) 
       (set (set a (get a))                    b₂  set a b₂)             ≡⟨ cong  b  set (set a (get a)) b  _) (B-prop a _ _) 
       (set (set a (get a)) (get (set a (get a)))  set a b₂)             ≡⟨ cong  b  _  set a b) (B-prop a _ _) ⟩∎
       (set (set a (get a)) (get (set a (get a)))  set a (get a))        ))) 

  ( λ (get : A  B) 
    λ (set : A  B  A) 
     Erased
       ((∀ a  set a (get a)  a) ×
        (∀ a  B  B 
           set (set a (get a)) (get (set a (get a))) 
           set a (get a))))                                         ↝⟨ (∃-cong λ get 
                                                                        EEq.Σ-cong-≃ᴱ-Erased (A→B→A≃ᴱA→A get) λ _  F.id) 
  ((A  B) ×
    λ (f : A  A) 
     Erased
       ((∀ a  f a  a) ×
        (∀ a  B  B  f (f a)  f a)))                             ↝⟨ (∃-cong λ get  ∃-cong λ _  Erased-cong (∃-cong λ _ 
                                                                        ∀-cong [ ext ] λ a 
                                                                        EEq.drop-⊤-left-Π-≃ᴱ-Erased ext (B≃ᴱ⊤ get a) F.∘
                                                                        EEq.drop-⊤-left-Π-≃ᴱ-Erased ext (B≃ᴱ⊤ get a))) 
  ((A  B) ×
    λ (f : A  A) 
     Erased
       ((∀ a  f a  a) ×
        (∀ a  f (f a)  f a)))                                     ↔⟨ (∃-cong λ _  ∃-cong λ f  Erased-cong (
                                                                        Σ-cong (Eq.extensionality-isomorphism ext) λ f≡id 
                                                                        ∀-cong ext λ a 
                                                                        ≡⇒≃ (cong₂ _≡_ (trans (f≡id (f a)) (f≡id a)) (f≡id a)))) 
  ((A  B) ×
    λ (f : A  A) 
     Erased
       (f  P.id ×
        ((a : A)  a  a)))                                         ↔⟨ (∃-cong λ _  ∃-cong λ _  Erased-Σ↔Σ) 

  ((A  B) ×
    λ (f : A  A) 
     Erased (f  P.id) ×
     Erased ((a : A)  a  a))                                      ↔⟨ (∃-cong λ _  Σ-assoc) 

  (A  B) ×
  ( λ (f : A  A)  Erased (f  P.id)) ×
  Erased ((a : A)  a  a)                                          ↝⟨ (∃-cong λ _  EEq.drop-⊤-left-Σ-≃ᴱ-Erased $
                                                                        _⇔_.to EEq.Contractibleᴱ⇔≃ᴱ⊤ Contractibleᴱ-Erased-singleton) ⟩□
  (A  B) × Erased ((a : A)  a  a)                                
  where
  B≃ᴱ⊤ : (A  B)  A  B ≃ᴱ 
  B≃ᴱ⊤ get a = EEq.inhabited→Is-proposition→≃ᴱ⊤ (get a) (B-prop a)

  A→B→A≃ᴱA→A : (A  B)  (A  B  A) ≃ᴱ (A  A)
  A→B→A≃ᴱA→A get =
    (A  B  A)  ↝⟨ ∀-cong [ ext ]  a  EEq.drop-⊤-left-Π-≃ᴱ-Erased ext $ B≃ᴱ⊤ get a) ⟩□
    (A  A)      

-- If equality is very stable for A (when B is inhabited) and B is a
-- proposition (when A is inhabited), then Lens A B is equivalent to
-- (A → B) × Erased ((a : A) → a ≡ a).

Very-stable-≡→lens-to-proposition≃ :
  (B  Very-stable-≡ A) 
  (A  Is-proposition B) 
  Lens A B  ((A  B) × Erased ((a : A)  a  a))
Very-stable-≡→lens-to-proposition≃ {B = B} {A = A} A-s B-prop =
  Stable-≡→≃ᴱ→≃ stable₁ stable₂ (lens-to-proposition≃ᴱ B-prop)
  where
  stable₁ : Stable-≡ (Lens A B)
  stable₁ =
    Very-stable→Stable 1 $
    Very-stable-Lensⁿ 1
       _  A-s)
      (H-level→Very-stable 1  B-prop)

  stable₂ : Stable-≡ ((A  B) × Erased ((a : A)  a  a))
  stable₂ =
    Very-stable→Stable 1 $
    Very-stable-×ⁿ 1
      (Very-stable-Πⁿ ext 1 λ a 
       H-level→Very-stable 1 (B-prop a))
      (Very-stable→Very-stable-≡ 0
       Very-stable-Erased)

-- Lens A ⊤ is equivalent (with erased proofs) to
-- Erased ((a : A) → a ≡ a).

lens-to-⊤≃ᴱ : Lens A  ≃ᴱ Erased ((a : A)  a  a)
lens-to-⊤≃ᴱ {A = A} =
  Lens A                             ↝⟨ lens-to-proposition≃ᴱ  _  mono₁ 0 ⊤-contractible) 
  (A  ) × Erased ((a : A)  a  a)  ↔⟨ drop-⊤-left-×  _  →-right-zero) ⟩□
  Erased ((a : A)  a  a)            

-- Lens A ⊥ is equivalent to ¬ A.

lens-to-⊥≃ : Lens A ( { = b})  (¬ A)
lens-to-⊥≃ {A = A} =
  Lens A                             ↝⟨ Very-stable-≡→lens-to-proposition≃  ())  _  ⊥-propositional) 
  (A  ) × Erased ((a : A)  a  a)  ↔⟨ (×-cong₁ λ _  →-cong ext F.id (Bij.⊥↔uninhabited ⊥-elim)) 
  ¬ A × Erased ((a : A)  a  a)      ↔⟨ (drop-⊤-right λ ¬a 
                                          _⇔_.to contractible⇔↔⊤ $
                                          propositional⇒inhabited⇒contractible
                                            (H-level-Erased 1 (
                                             Π-closure ext 1 λ a 
                                             ⊥-elim (¬a a)))
                                            [ refl ]) ⟩□
  ¬ A                                 

-- See also lens-from-⊥≃⊤ and lens-from-⊤≃codomain-contractible below.

------------------------------------------------------------------------
-- Some lens results related to h-levels

-- If the domain of a lens is inhabited and has h-level n, then the
-- codomain also has h-level n (in erased contexts).

@0 h-level-respects-lens-from-inhabited :
   n  Lens A B  A  H-level n A  H-level n B
h-level-respects-lens-from-inhabited n l =
  T.h-level-respects-lens-from-inhabited n (trad l)

-- Lenses with contractible domains have contractible codomains (in
-- erased contexts).

@0 contractible-to-contractible :
  Lens A B  Contractible A  Contractible B
contractible-to-contractible l =
  T.contractible-to-contractible (trad l)

-- A variant for Contractibleᴱ.

Contractibleᴱ→Contractibleᴱ :
  Lens A B  Contractibleᴱ A  Contractibleᴱ B
Contractibleᴱ→Contractibleᴱ l c@(a , _) =
  ECP.Contractibleᴱ-respects-surjection
    (Lens.get l)
     b  Lens.set l a b
         , (Lens.get l (Lens.set l a b)  ≡⟨ Lens.get-set l _ _ ⟩∎
            b                            ))
    c

-- If A and B have h-level n given the assumption that A is inhabited,
-- then Lens A B also has h-level n.

lens-preserves-h-level :
   n  (A  H-level n A)  (A  H-level n B) 
  H-level n (Lens A B)
lens-preserves-h-level n hA hB =
  H-level.respects-surjection (_↔_.surjection (inverse Lens-as-Σ)) n $
  Σ-closure n (Π-closure ext n λ a 
               hB a) λ _ 
  Σ-closure n (Π-closure ext n λ a 
               Π-closure ext n λ _ 
               hA a) λ _ 
  H-level-Erased n
    (×-closure n (Π-closure ext n λ a 
                  Π-closure ext n λ _ 
                  +⇒≡ $ mono₁ n (hB a)) $
     ×-closure n (Π-closure ext n λ a 
                  +⇒≡ $ mono₁ n (hA a))
                 (Π-closure ext n λ a 
                  Π-closure ext n λ _ 
                  Π-closure ext n λ _ 
                  +⇒≡ $ mono₁ n (hA a)))

-- If A has positive h-level n, then Lens A B also has h-level n (in
-- erased contexts).

@0 lens-preserves-h-level-of-domain :
   n  H-level (1 + n) A  H-level (1 + n) (Lens A B)
lens-preserves-h-level-of-domain {A = A} {B = B} n =
  H-level (1 + n) A             ↝⟨ T.lens-preserves-h-level-of-domain n 
  H-level (1 + n) (T.Lens A B)  ↝⟨ H-level-cong _ (1 + n) (inverse Lens≃Traditional-lens) ⟩□
  H-level (1 + n) (Lens A B)    

-- Lens 𝕊¹ᴱ ⊤ is not propositional (assuming univalence).

¬-lens-to-⊤-propositional :
  @0 Univalence (# 0) 
  ¬ Is-proposition (Lens 𝕊¹ᴱ )
¬-lens-to-⊤-propositional univ =
  Stable-¬
    [ Is-proposition (Lens 𝕊¹ᴱ )   ↝⟨ H-level-cong _ 1 (Lens-cong (inverse CE.𝕊¹≃𝕊¹ᴱ) Eq.id) 
      Is-proposition (Lens 𝕊¹ )    ↝⟨ H-level-cong _ 1 Lens≃Traditional-lens 
      Is-proposition (T.Lens 𝕊¹ )  ↝⟨ T.¬-lens-to-⊤-propositional univ ⟩□
      ⊥₀                            
    ]

------------------------------------------------------------------------
-- Some equality characterisation lemmas

abstract

  -- An equality characterisation lemma.

  equality-characterisation₁ :
    let open Lens in

    l₁  l₂
      
     λ (g : get l₁  get l₂) 
     λ (s : set l₁  set l₂) 
      Erased
        ((∀ a b  subst  get  get (set l₂ a b)  b) g
                    (subst  set  get l₁ (set a b)  b) s
                       (get-set l₁ a b)) 
                  get-set l₂ a b)
           ×
         (∀ a  subst  get  set l₂ a (get a)  a) g
                  (subst  set  set a (get l₁ a)  a) s
                     (set-get l₁ a)) 
                set-get l₂ a)
           ×
         (∀ a b₁ b₂  subst  set  set (set a b₁) b₂  set a b₂) s
                        (set-set l₁ a b₁ b₂) 
                      set-set l₂ a b₁ b₂))

  equality-characterisation₁ {l₁ = l₁} {l₂ = l₂} =
    let l₁′ = _↔_.to Lens-as-Σ l₁
        l₂′ = _↔_.to Lens-as-Σ l₂
    in

    l₁  l₂                                                            ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ (inverse Lens-as-Σ)) 

    l₁′  l₂′                                                          ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ (inverse Σ-assoc)) 

    ((get l₁ , set l₁) , proj₂ (proj₂ l₁′))
      
    ((get l₂ , set l₂) , proj₂ (proj₂ l₂′))                            ↝⟨ inverse Bij.Σ-≡,≡↔≡ 

    ( λ (gs : (get l₁ , set l₁)  (get l₂ , set l₂)) 
     subst  (get , set) 
              Erased
                ((∀ a b  get (set a b)  b) ×
                 (∀ a  set a (get a)  a) ×
                 (∀ a b₁ b₂  set (set a b₁) b₂  set a b₂)))
           gs (proj₂ (proj₂ l₁′)) 
     proj₂ (proj₂ l₂′))                                                ↝⟨ Σ-cong (inverse ≡×≡↔≡)  gs  ≡⇒↝ _ $
                                                                          cong  (gs : (get l₁ , set l₁)  (get l₂ , set l₂)) 
                                                                                  subst  (get , set) 
                                                                                           Erased
                                                                                             ((∀ a b  get (set a b)  b) ×
                                                                                              (∀ a  set a (get a)  a) ×
                                                                                              (∀ a b₁ b₂  set (set a b₁) b₂  set a b₂)))
                                                                                        gs (proj₂ (proj₂ l₁′))
                                                                                    
                                                                                  proj₂ (proj₂ l₂′))
                                                                               (sym $ _↔_.right-inverse-of ≡×≡↔≡ gs)) 
    ( λ (gs : get l₁  get l₂ × set l₁  set l₂) 
     subst  (get , set) 
              Erased
                ((∀ a b  get (set a b)  b) ×
                 (∀ a  set a (get a)  a) ×
                 (∀ a b₁ b₂  set (set a b₁) b₂  set a b₂)))
           (_↔_.to ≡×≡↔≡ gs) (proj₂ (proj₂ l₁′)) 
     proj₂ (proj₂ l₂′))                                                ↝⟨ inverse Σ-assoc 

    ( λ (g : get l₁  get l₂) 
      λ (s : set l₁  set l₂) 
     subst  (get , set) 
              Erased
                ((∀ a b  get (set a b)  b) ×
                 (∀ a  set a (get a)  a) ×
                 (∀ a b₁ b₂  set (set a b₁) b₂  set a b₂)))
           (_↔_.to ≡×≡↔≡ (g , s)) (proj₂ (proj₂ l₁′)) 
     proj₂ (proj₂ l₂′))                                                ↝⟨ (∃-cong λ g  ∃-cong λ s  ≡⇒↝ _ $ cong (_≡ proj₂ (proj₂ l₂′))
                                                                           push-subst-[]) 
    ( λ (g : get l₁  get l₂) 
      λ (s : set l₁  set l₂) 
     [ subst  (get , set) 
                (∀ a b  get (set a b)  b) ×
                (∀ a  set a (get a)  a) ×
                (∀ a b₁ b₂  set (set a b₁) b₂  set a b₂))
             (_↔_.to ≡×≡↔≡ (g , s)) (erased (proj₂ (proj₂ l₁′))) ] 
     [ erased (proj₂ (proj₂ l₂′)) ])                                   ↝⟨ (∃-cong λ _  ∃-cong λ _  inverse Erased-≡↔[]≡[]) 

    ( λ (g : get l₁  get l₂) 
      λ (s : set l₁  set l₂) 
     Erased
       (subst  (get , set) 
                 (∀ a b  get (set a b)  b) ×
                 (∀ a  set a (get a)  a) ×
                 (∀ a b₁ b₂  set (set a b₁) b₂  set a b₂))
              (_↔_.to ≡×≡↔≡ (g , s)) (erased (proj₂ (proj₂ l₁′))) 
        erased (proj₂ (proj₂ l₂′))))                                   ↝⟨ (∃-cong λ g  ∃-cong λ s  Erased-cong (≡⇒↝ _ $
                                                                           cong  x  x  erased (proj₂ (proj₂ l₂′)))
                                                                                (push-subst-, {y≡z = _↔_.to ≡×≡↔≡ (g , s)} _ _))) 
    ( λ (g : get l₁  get l₂) 
      λ (s : set l₁  set l₂) 
     Erased
       (( subst  { (get , set)   a b  get (set a b)  b })
                (_↔_.to ≡×≡↔≡ (g , s)) (get-set l₁)
        , subst  { (get , set) 
                     (∀ a  set a (get a)  a) ×
                     (∀ a b₁ b₂  set (set a b₁) b₂  set a b₂) })
                (_↔_.to ≡×≡↔≡ (g , s))
                (proj₂ (erased (proj₂ (proj₂ l₁′))))
        ) 
        erased (proj₂ (proj₂ l₂′))))                                   ↝⟨ (∃-cong λ _  ∃-cong λ _  Erased-cong (inverse ≡×≡↔≡)) 

    ( λ (g : get l₁  get l₂) 
      λ (s : set l₁  set l₂) 
     Erased
       (subst  { (get , set)   a b  get (set a b)  b })
              (_↔_.to ≡×≡↔≡ (g , s)) (get-set l₁) 
        get-set l₂
          ×
        subst  { (get , set) 
                   (∀ a  set a (get a)  a) ×
                   (∀ a b₁ b₂  set (set a b₁) b₂  set a b₂) })
              (_↔_.to ≡×≡↔≡ (g , s))
              (proj₂ (erased (proj₂ (proj₂ l₁′)))) 
        proj₂ (erased (proj₂ (proj₂ l₂′)))))                           ↝⟨ (∃-cong λ g  ∃-cong λ s  Erased-cong (∃-cong λ _  ≡⇒↝ _ $
                                                                           cong  x  x  proj₂ (erased (proj₂ (proj₂ l₂′))))
                                                                                (push-subst-, {y≡z = _↔_.to ≡×≡↔≡ (g , s)} _ _))) 
    ( λ (g : get l₁  get l₂) 
      λ (s : set l₁  set l₂) 
     Erased
       (subst  { (get , set)   a b  get (set a b)  b })
              (_↔_.to ≡×≡↔≡ (g , s)) (get-set l₁) 
        get-set l₂
          ×
        ( subst  { (get , set)   a  set a (get a)  a })
                (_↔_.to ≡×≡↔≡ (g , s)) (set-get l₁)
        , subst  { (get , set) 
                      a b₁ b₂  set (set a b₁) b₂  set a b₂ })
                (_↔_.to ≡×≡↔≡ (g , s)) (set-set l₁)
        ) 
        proj₂ (erased (proj₂ (proj₂ l₂′)))))                           ↝⟨ (∃-cong λ _  ∃-cong λ _  Erased-cong (∃-cong λ _  inverse ≡×≡↔≡)) 

    ( λ (g : get l₁  get l₂) 
      λ (s : set l₁  set l₂) 
     Erased
       (subst  { (get , set)   a b  get (set a b)  b })
              (_↔_.to ≡×≡↔≡ (g , s)) (get-set l₁) 
        get-set l₂
          ×
        subst  { (get , set)   a  set a (get a)  a })
              (_↔_.to ≡×≡↔≡ (g , s)) (set-get l₁) 
        set-get l₂
          ×
        subst  { (get , set) 
                    a b₁ b₂  set (set a b₁) b₂  set a b₂ })
              (_↔_.to ≡×≡↔≡ (g , s)) (set-set l₁) 
          set-set l₂))                                                 ↝⟨ (∃-cong λ g  ∃-cong λ s  Erased-cong (
                                                                           lemma₁  { (get , set) a   b  get (set a b)  b })
                                                                                  (_↔_.to ≡×≡↔≡ (g , s))
                                                                             ×-cong
                                                                           lemma₁  { (get , set) a  set a (get a)  a })
                                                                                  (_↔_.to ≡×≡↔≡ (g , s))
                                                                             ×-cong
                                                                           lemma₁  { (get , set) a   b₁ b₂  set (set a b₁) b₂  set a b₂ })
                                                                                  (_↔_.to ≡×≡↔≡ (g , s)))) 
    ( λ (g : get l₁  get l₂) 
      λ (s : set l₁  set l₂) 
     Erased
       ((∀ a  subst  { (get , set)   b  get (set a b)  b })
                     (_↔_.to ≡×≡↔≡ (g , s)) (get-set l₁ a) 
               get-set l₂ a)
          ×
        (∀ a  subst  { (get , set)  set a (get a)  a })
                     (_↔_.to ≡×≡↔≡ (g , s)) (set-get l₁ a) 
               set-get l₂ a)
          ×
        (∀ a  subst  { (get , set) 
                           b₁ b₂  set (set a b₁) b₂  set a b₂ })
                     (_↔_.to ≡×≡↔≡ (g , s)) (set-set l₁ a) 
               set-set l₂ a)))                                         ↝⟨ (∃-cong λ g  ∃-cong λ s  Erased-cong (
                                                                           (∀-cong ext λ a 
                                                                              lemma₁  { (get , set) b  get (set a b)  b })
                                                                                     (_↔_.to ≡×≡↔≡ (g , s)))
                                                                             ×-cong
                                                                           F.id
                                                                             ×-cong
                                                                           (∀-cong ext λ a 
                                                                              lemma₁  { (get , set) b₁   b₂  set (set a b₁) b₂  set a b₂ })
                                                                                     (_↔_.to ≡×≡↔≡ (g , s))))) 
    ( λ (g : get l₁  get l₂) 
      λ (s : set l₁  set l₂) 
     Erased
       ((∀ a b  subst  { (get , set)  get (set a b)  b })
                       (_↔_.to ≡×≡↔≡ (g , s)) (get-set l₁ a b) 
                 get-set l₂ a b)
          ×
        (∀ a  subst  { (get , set)  set a (get a)  a })
                     (_↔_.to ≡×≡↔≡ (g , s)) (set-get l₁ a) 
               set-get l₂ a)
          ×
        (∀ a b₁  subst  { (get , set) 
                              b₂  set (set a b₁) b₂  set a b₂ })
                        (_↔_.to ≡×≡↔≡ (g , s)) (set-set l₁ a b₁) 
                  set-set l₂ a b₁)))                                   ↝⟨ (∃-cong λ g  ∃-cong λ s  Erased-cong (∃-cong λ _  ∃-cong λ _ 
                                                                           ∀-cong ext λ a  ∀-cong ext λ b₁ 
                                                                             lemma₁  { (get , set) b₂  set (set a b₁) b₂  set a b₂ })
                                                                                    (_↔_.to ≡×≡↔≡ (g , s)))) 
    ( λ (g : get l₁  get l₂) 
      λ (s : set l₁  set l₂) 
     Erased
       ((∀ a b  subst  { (get , set)  get (set a b)  b })
                       (_↔_.to ≡×≡↔≡ (g , s)) (get-set l₁ a b) 
                 get-set l₂ a b)
          ×
        (∀ a  subst  { (get , set)  set a (get a)  a })
                     (_↔_.to ≡×≡↔≡ (g , s)) (set-get l₁ a) 
               set-get l₂ a)
          ×
        (∀ a b₁ b₂  subst  { (get , set) 
                                set (set a b₁) b₂  set a b₂ })
                           (_↔_.to ≡×≡↔≡ (g , s)) (set-set l₁ a b₁ b₂) 
                     set-set l₂ a b₁ b₂)))                             ↝⟨ (∃-cong λ g  ∃-cong λ s  Erased-cong (
                                                                           (∀-cong ext λ a  ∀-cong ext λ b 
                                                                            lemma₂  { (get , set)  get (set a b)  b }) g s)
                                                                             ×-cong
                                                                           (∀-cong ext λ a 
                                                                            lemma₂  { (get , set)  set a (get a)  a }) g s)
                                                                             ×-cong
                                                                           (∀-cong ext λ a  ∀-cong ext λ b₁  ∀-cong ext λ b₂ 
                                                                            lemma₂  { (get , set)  set (set a b₁) b₂  set a b₂ }) g s))) 
    ( λ (g : get l₁  get l₂) 
      λ (s : set l₁  set l₂) 
     Erased
       ((∀ a b  subst  get  get (set l₂ a b)  b) g
                   (subst  set  get l₁ (set a b)  b) s
                      (get-set l₁ a b)) 
                 get-set l₂ a b)
          ×
        (∀ a  subst  get  set l₂ a (get a)  a) g
                 (subst  set  set a (get l₁ a)  a) s
                    (set-get l₁ a)) 
               set-get l₂ a)
          ×
        (∀ a b₁ b₂ 
           subst  get  set l₂ (set l₂ a b₁) b₂  set l₂ a b₂) g
             (subst  set  set (set a b₁) b₂  set a b₂) s
                (set-set l₁ a b₁ b₂)) 
           set-set l₂ a b₁ b₂)))                                       ↝⟨ (∃-cong λ g  ∃-cong λ _  Erased-cong (∃-cong λ _  ∃-cong λ _ 
                                                                           ∀-cong ext λ _  ∀-cong ext λ _  ∀-cong ext λ _ 
                                                                           ≡⇒↝ _ $ cong  x  x  _) $ subst-const g)) ⟩□
    ( λ (g : get l₁  get l₂) 
      λ (s : set l₁  set l₂) 
     Erased
       ((∀ a b  subst  get  get (set l₂ a b)  b) g
                   (subst  set  get l₁ (set a b)  b) s
                      (get-set l₁ a b)) 
                 get-set l₂ a b)
          ×
        (∀ a  subst  get  set l₂ a (get a)  a) g
                 (subst  set  set a (get l₁ a)  a) s
                    (set-get l₁ a)) 
               set-get l₂ a)
          ×
        (∀ a b₁ b₂  subst  set  set (set a b₁) b₂  set a b₂) s
                       (set-set l₁ a b₁ b₂) 
                     set-set l₂ a b₁ b₂)))                             
    where
    open Lens

    abstract

      lemma₁ :
         (C : A  B  Type c) (eq : u  v) {f g} 
        (subst  x   y  C x y) eq f  g)
          
        (∀ y  subst  x  C x y) eq (f y)  g y)
      lemma₁ C eq {f} {g} =
        subst  x   y  C x y) eq f  g              ↔⟨ inverse $ Eq.extensionality-isomorphism ext 
        (∀ y  subst  x   y  C x y) eq f y  g y)  ↝⟨ (∀-cong ext λ y  ≡⇒↝ _ $
                                                            cong  x  x  _) (sym $ push-subst-application eq _)) ⟩□
        (∀ y  subst  x  C x y) eq (f y)  g y)      

    lemma₂ :
      (P : A × B  Type p) (x₁≡x₂ : x₁  x₂) (y₁≡y₂ : y₁  y₂) 
       {p p′} 
      (subst P (_↔_.to ≡×≡↔≡ (x₁≡x₂ , y₁≡y₂)) p  p′)
        
      (subst  x  P (x , y₂)) x₁≡x₂ (subst  y  P (x₁ , y)) y₁≡y₂ p)
         
       p′)
    lemma₂ P x₁≡x₂ y₁≡y₂ {p = p} = ≡⇒↝ _ $ cong (_≡ _) $ elim¹
       y₁≡y₂ 
         subst P (_↔_.to ≡×≡↔≡ (x₁≡x₂ , y₁≡y₂)) p 
         subst  x  P (x , _)) x₁≡x₂
           (subst  y  P (_ , y)) y₁≡y₂ p))
      (subst P (_↔_.to ≡×≡↔≡ (x₁≡x₂ , refl _)) p                     ≡⟨⟩

       subst P (cong₂ _,_ x₁≡x₂ (refl _)) p                          ≡⟨⟩

       subst P (trans (cong (_, _) x₁≡x₂) (cong (_ ,_) (refl _))) p  ≡⟨ cong  eq  subst P (trans (cong (_, _) x₁≡x₂) eq) p) $ cong-refl _ 

       subst P (trans (cong (_, _) x₁≡x₂) (refl _)) p                ≡⟨ cong  eq  subst P eq p) $ trans-reflʳ _ 

       subst P (cong (_, _) x₁≡x₂) p                                 ≡⟨ sym $ subst-∘ _ _ _ 

       subst  x  P (x , _)) x₁≡x₂ p                               ≡⟨ cong (subst  x  P (x , _)) x₁≡x₂) $ sym $ subst-refl _ _ ⟩∎

       subst  x  P (x , _)) x₁≡x₂
         (subst  y  P (_ , y)) (refl _) p)                        )
      _

  -- Another equality characterisation lemma.

  equality-characterisation₂ :
    let open Lens in

    l₁  l₂
      
     λ (g : get l₁  get l₂) 
     λ (s : set l₁  set l₂) 
      Erased
        ((∀ a b 
            trans (sym (cong₂  set get  get (set a b)) s g))
              (get-set l₁ a b) 
            get-set l₂ a b) ×
         (∀ a 
            trans (sym (cong₂  set get  set a (get a)) s g))
              (set-get l₁ a) 
            set-get l₂ a) ×
         (∀ a b₁ b₂ 
            subst  set  set (set a b₁) b₂  set a b₂) s
              (set-set l₁ a b₁ b₂) 
            set-set l₂ a b₁ b₂))

  equality-characterisation₂ {l₁ = l₁} {l₂ = l₂} =
    l₁  l₂                                                           ↝⟨ equality-characterisation₁ 

    ( λ (g : get l₁  get l₂) 
      λ (s : set l₁  set l₂) 
     Erased
       ((∀ a b  subst  get  get (set l₂ a b)  b) g
                   (subst  set  get l₁ (set a b)  b) s
                      (get-set l₁ a b)) 
                 get-set l₂ a b)
          ×
        (∀ a  subst  get  set l₂ a (get a)  a) g
                 (subst  set  set a (get l₁ a)  a) s
                    (set-get l₁ a)) 
               set-get l₂ a)
          ×
        (∀ a b₁ b₂  subst  set  set (set a b₁) b₂  set a b₂) s
                       (set-set l₁ a b₁ b₂) 
                     set-set l₂ a b₁ b₂)))                            ↝⟨ (∃-cong λ g  ∃-cong λ s  Erased-cong (
                                                                          (∀-cong ext λ a  ∀-cong ext λ b  ≡⇒↝ _ $ cong (_≡ _) $
                                                                           lemma₁ g s a b)
                                                                            ×-cong
                                                                          (∀-cong ext λ a  ≡⇒↝ _ $ cong (_≡ _) $
                                                                           lemma₂ g s a)
                                                                            ×-cong
                                                                          F.id)) ⟩□
    ( λ (g : get l₁  get l₂) 
      λ (s : set l₁  set l₂) 
     Erased
       ((∀ a b  trans (sym (cong₂  set get  get (set a b)) s g))
                   (get-set l₁ a b) 
                 get-set l₂ a b) ×
        (∀ a  trans (sym (cong₂  set get  set a (get a)) s g))
                 (set-get l₁ a) 
               set-get l₂ a) ×
        (∀ a b₁ b₂ 
           subst  set  set (set a b₁) b₂  set a b₂) s
             (set-set l₁ a b₁ b₂) 
           set-set l₂ a b₁ b₂)))                                      
    where
    open Lens

    @0 lemma₁ :
      (g : get l₁  get l₂) (s : set l₁  set l₂) 
       a b 
      subst  get  get (set l₂ a b)  b) g
        (subst  set  get l₁ (set a b)  b) s
           (get-set l₁ a b)) 
      trans (sym (cong₂  set get  get (set a b)) s g))
        (get-set l₁ a b)
    lemma₁ g s a b =
      subst  get  get (set l₂ a b)  b) g
        (subst  set  get l₁ (set a b)  b) s
           (get-set l₁ a b))                                     ≡⟨ cong  eq  subst  get  get (set l₂ a b)  b) g eq) $
                                                                    subst-in-terms-of-trans-and-cong
                                                                      {f = λ set  get l₁ (set a b)} {g = λ _  b}
                                                                      {x≡y = s} {fx≡gx = (get-set l₁ a b)} 
      subst  get  get (set l₂ a b)  b) g
        (trans (sym (cong  set  get l₁ (set a b)) s))
           (trans (get-set l₁ a b) (cong (const b) s)))          ≡⟨ cong  eq  subst  get  get (set l₂ a b)  b) g
                                                                                   (trans (sym (cong  set  get l₁ (set a b)) s))
                                                                                      (trans _ eq))) $
                                                                    cong-const s 
      subst  get  get (set l₂ a b)  b) g
        (trans (sym (cong  set  get l₁ (set a b)) s))
           (trans (get-set l₁ a b) (refl _)))                    ≡⟨ cong  eq  subst  get  get (set l₂ a b)  b) g
                                                                                   (trans (sym (cong  set  get l₁ (set a b)) s)) eq)) $
                                                                    trans-reflʳ _ 
      subst  get  get (set l₂ a b)  b) g
        (trans (sym (cong  set  get l₁ (set a b)) s))
           (get-set l₁ a b))                                     ≡⟨ subst-in-terms-of-trans-and-cong {x≡y = g}
                                                                      {fx≡gx = trans _ (get-set l₁ a b)} 
      trans (sym (cong  get  get (set l₂ a b)) g))
        (trans (trans (sym (cong  set  get l₁ (set a b)) s))
                  (get-set l₁ a b))
           (cong (const b) g))                                   ≡⟨ cong  eq  trans (sym (cong  get  get (set l₂ a b)) g))
                                                                                   (trans (trans (sym (cong  set  get l₁ (set a b)) s))
                                                                                             (get-set l₁ a b))
                                                                                      eq)) $
                                                                    cong-const g 
      trans (sym (cong  get  get (set l₂ a b)) g))
        (trans (trans (sym (cong  set  get l₁ (set a b)) s))
                  (get-set l₁ a b))
           (refl _))                                             ≡⟨ cong (trans _) $
                                                                    trans-reflʳ _ 
      trans (sym (cong  get  get (set l₂ a b)) g))
        (trans (sym (cong  set  get l₁ (set a b)) s))
           (get-set l₁ a b))                                     ≡⟨ sym $ trans-assoc _ _ (get-set l₁ a b) 

      trans (trans (sym (cong  get  get (set l₂ a b)) g))
               (sym (cong  set  get l₁ (set a b)) s)))
        (get-set l₁ a b)                                         ≡⟨ cong  eq  trans eq (get-set l₁ a b)) $ sym $
                                                                    sym-trans _ (cong  get  get (set l₂ a b)) g) 
      trans (sym (trans (cong  set  get l₁ (set a b)) s)
                    (cong  get  get (set l₂ a b)) g)))
        (get-set l₁ a b)                                         ≡⟨⟩

      trans (sym (cong₂  set get  get (set a b)) s g))
        (get-set l₁ a b)                                         

    @0 lemma₂ :
      (g : get l₁  get l₂) (s : set l₁  set l₂) 
       a 
      subst  get  set l₂ a (get a)  a) g
        (subst  set  set a (get l₁ a)  a) s
           (set-get l₁ a)) 
      trans (sym (cong₂  set get  set a (get a)) s g))
        (set-get l₁ a)
    lemma₂ g s a =
      subst  get  set l₂ a (get a)  a) g
        (subst  set  set a (get l₁ a)  a) s
           (set-get l₁ a))                                       ≡⟨⟩

      subst  get  set l₂ a (get a)  a) g
        (subst  set  set a (get l₁ a)  a) s
           (set-get l₁ a))                                       ≡⟨ cong (subst  get  set l₂ a (get a)  a) g) $
                                                                    subst-in-terms-of-trans-and-cong {x≡y = s} {fx≡gx = set-get l₁ a} 
      subst  get  set l₂ a (get a)  a) g
        (trans (sym (cong  set  set a (get l₁ a)) s))
           (trans (set-get l₁ a) (cong (const a) s)))            ≡⟨ cong  eq  subst  get  set l₂ a (get a)  a) g
                                                                                    (trans (sym (cong  set  set a (get l₁ a)) s))
                                                                                       (trans _ eq))) $
                                                                    cong-const s 
      subst  get  set l₂ a (get a)  a) g
        (trans (sym (cong  set  set a (get l₁ a)) s))
           (trans (set-get l₁ a) (refl _)))                      ≡⟨ cong  eq  subst  get  set l₂ a (get a)  a) g
                                                                                   (trans (sym (cong  set  set a (get l₁ a)) s)) eq)) $
                                                                    trans-reflʳ _ 
      subst  get  set l₂ a (get a)  a) g
        (trans (sym (cong  set  set a (get l₁ a)) s))
           (set-get l₁ a))                                       ≡⟨ subst-in-terms-of-trans-and-cong {x≡y = g}
                                                                      {fx≡gx = trans (sym (cong  set  set a (get l₁ a)) s)) (set-get l₁ a)} 
      trans (sym (cong  get  set l₂ a (get a)) g))
        (trans (trans (sym (cong  set  set a (get l₁ a)) s))
                  (set-get l₁ a))
           (cong (const a) g))                                   ≡⟨ cong  eq  trans (sym (cong  get  set l₂ a (get a)) g))
                                                                                   (trans (trans (sym (cong  set  set a (get l₁ a)) s))
                                                                                             (set-get l₁ a))
                                                                                      eq)) $
                                                                    cong-const g 
      trans (sym (cong  get  set l₂ a (get a)) g))
        (trans (trans (sym (cong  set  set a (get l₁ a)) s))
                  (set-get l₁ a))
           (refl _))                                             ≡⟨ cong (trans _) $
                                                                    trans-reflʳ _ 
      trans (sym (cong  get  set l₂ a (get a)) g))
        (trans (sym (cong  set  set a (get l₁ a)) s))
           (set-get l₁ a))                                       ≡⟨ sym $ trans-assoc _ _ (set-get l₁ a) 

      trans (trans (sym (cong  get  set l₂ a (get a)) g))
               (sym (cong  set  set a (get l₁ a)) s)))
        (set-get l₁ a)                                           ≡⟨ cong  eq  trans eq (set-get l₁ a)) $ sym $
                                                                    sym-trans _ (cong  get  set l₂ a (get a)) g) 
      trans (sym (trans (cong  set  set a (get l₁ a)) s)
                    (cong  get  set l₂ a (get a)) g)))
        (set-get l₁ a)                                           ≡⟨⟩

      trans (sym (cong₂  set get  set a (get a)) s g))
        (set-get l₁ a)                                           

  -- And another one.

  equality-characterisation₃ :
    let open Lens in

    l₁  l₂
      
     λ (g : get l₁  get l₂) 
     λ (s : set l₁  set l₂) 
      Erased
        ((∀ a b 
            trans (sym (cong₂  set get  get (set a b)) s g))
              (get-set l₁ a b) 
            get-set l₂ a b) ×
         (∀ a 
            trans (sym (cong₂  set get  set a (get a)) s g))
              (set-get l₁ a) 
            set-get l₂ a) ×
         (∀ a b₁ b₂ 
            trans (set-set l₁ a b₁ b₂) (cong  set  set a b₂) s) 
            trans (cong  set  set (set a b₁) b₂) s)
              (set-set l₂ a b₁ b₂)))

  equality-characterisation₃ {l₁ = l₁} {l₂ = l₂} =
    l₁  l₂                                                           ↝⟨ equality-characterisation₂ 

    ( λ (g : get l₁  get l₂) 
      λ (s : set l₁  set l₂) 
     Erased
       ((∀ a b  trans (sym (cong₂  set get  get (set a b)) s g))
                   (get-set l₁ a b) 
                 get-set l₂ a b) ×
        (∀ a  trans (sym (cong₂  set get  set a (get a)) s g))
                 (set-get l₁ a) 
               set-get l₂ a) ×
        (∀ a b₁ b₂ 
           subst  set  set (set a b₁) b₂  set a b₂) s
             (set-set l₁ a b₁ b₂) 
           set-set l₂ a b₁ b₂)))                                      ↝⟨ (∃-cong λ g  ∃-cong λ s  Erased-cong (∃-cong λ _  ∃-cong λ _ 
                                                                          ∀-cong ext λ a  ∀-cong ext λ b₁  ∀-cong ext λ b₂  ≡⇒↝ _ $
                                                                          lemma g s a b₁ b₂)) ⟩□
    ( λ (g : get l₁  get l₂) 
      λ (s : set l₁  set l₂) 
     Erased
       ((∀ a b  trans (sym (cong₂  set get  get (set a b)) s g))
                   (get-set l₁ a b) 
                 get-set l₂ a b) ×
        (∀ a  trans (sym (cong₂  set get  set a (get a)) s g))
                 (set-get l₁ a) 
               set-get l₂ a) ×
        (∀ a b₁ b₂ 
           trans (set-set l₁ a b₁ b₂) (cong  set  set a b₂) s) 
           trans (cong  set  set (set a b₁) b₂) s)
             (set-set l₂ a b₁ b₂))))                                  
    where
    open Lens

    @0 lemma :
      (g : get l₁  get l₂) (s : set l₁  set l₂) 
       a b₁ b₂ 
      (subst  set  set (set a b₁) b₂  set a b₂) s
         (set-set l₁ a b₁ b₂) 
       set-set l₂ a b₁ b₂) 
      (trans (set-set l₁ a b₁ b₂) (cong  set  set a b₂) s) 
       trans (cong  set  set (set a b₁) b₂) s)
         (set-set l₂ a b₁ b₂))
    lemma g s a b₁ b₂ =
      subst  set  set (set a b₁) b₂  set a b₂) s
        (set-set l₁ a b₁ b₂) 
      set-set l₂ a b₁ b₂                                        ≡⟨ cong (_≡ _) $
                                                                   subst-in-terms-of-trans-and-cong {x≡y = s} {fx≡gx = set-set l₁ a b₁ b₂} 
      trans (sym (cong  set  set (set a b₁) b₂) s))
        (trans (set-set l₁ a b₁ b₂)
           (cong  set  set a b₂) s)) 
      set-set l₂ a b₁ b₂                                        ≡⟨ [trans≡]≡[≡trans-symˡ] _ _ _ 

      trans (set-set l₁ a b₁ b₂) (cong  set  set a b₂) s) 
      trans (sym (sym (cong  set  set (set a b₁) b₂) s)))
        (set-set l₂ a b₁ b₂)                                    ≡⟨ cong  eq  trans _ (cong  set  set a b₂) s) 
                                                                                trans eq (set-set l₂ a b₁ b₂)) $
                                                                   sym-sym (cong  set  set (set a b₁) b₂) s) 
      trans (set-set l₁ a b₁ b₂) (cong  set  set a b₂) s) 
      trans (cong  set  set (set a b₁) b₂) s)
        (set-set l₂ a b₁ b₂)                                    

  -- And yet another one.

  equality-characterisation₄ :
    let open Lens in

    l₁  l₂
      
     λ (g :  a  get l₁ a  get l₂ a) 
     λ (s :  a b  set l₁ a b  set l₂ a b) 
      Erased
        ((∀ a b 
            trans (sym (trans (cong (get l₁) (s a b))
                          (g (set l₂ a b))))
              (get-set l₁ a b) 
            get-set l₂ a b) ×
         (∀ a 
            trans (sym (trans (s a (get l₁ a))
                          (cong (set l₂ a) (g a))))
              (set-get l₁ a) 
            set-get l₂ a) ×
         (∀ a b₁ b₂ 
            trans (set-set l₁ a b₁ b₂) (s a b₂) 
            trans (cong  set  set (set a b₁) b₂) (⟨ext⟩ (⟨ext⟩  s)))
              (set-set l₂ a b₁ b₂)))

  equality-characterisation₄ {l₁ = l₁} {l₂ = l₂} =
    l₁  l₂                                                              ↝⟨ equality-characterisation₃ 

    ( λ (g : get l₁  get l₂) 
      λ (s : set l₁  set l₂) 
     Erased
       ((∀ a b  trans (sym (cong₂  set get  get (set a b)) s g))
                   (get-set l₁ a b) 
                 get-set l₂ a b) ×
        (∀ a  trans (sym (cong₂  set get  set a (get a)) s g))
                 (set-get l₁ a) 
               set-get l₂ a) ×
        (∀ a b₁ b₂ 
           trans (set-set l₁ a b₁ b₂) (cong  set  set a b₂) s) 
           trans (cong  set  set (set a b₁) b₂) s)
             (set-set l₂ a b₁ b₂))))                                     ↝⟨ (Σ-cong (inverse $ Eq.extensionality-isomorphism ext) λ g 
                                                                             Σ-cong (inverse $
                                                                                     Eq.extensionality-isomorphism ext F.∘
                                                                                     ∀-cong ext λ _  Eq.extensionality-isomorphism ext) λ s 
                                                                             Erased-cong (
                                                                             (∀-cong ext λ a  ∀-cong ext λ b 
                                                                              ≡⇒↝ _ $ cong  eq  trans (sym eq) (get-set l₁ a b)  _) (
        cong₂  set get  get (set a b)) s g                                   ≡⟨⟩

        trans (cong  set  get l₁ (set a b)) s)
          (cong  get  get (set l₂ a b)) g)                                   ≡⟨ cong  eq  trans eq (ext⁻¹ g (set l₂ a b))) $ sym $
                                                                                   cong-∘ _ _ s 
        trans (cong (get l₁  (_$ b)) (ext⁻¹ s a))
          (ext⁻¹ g (set l₂ a b))                                                ≡⟨ cong  eq  trans eq (ext⁻¹ g (set l₂ a b))) $ sym $
                                                                                   cong-∘ _ _ (ext⁻¹ s a) ⟩∎
        trans (cong (get l₁) (ext⁻¹ (ext⁻¹ s a) b))
          (ext⁻¹ g (set l₂ a b))                                                ))
                                                                               ×-cong
                                                                             (∀-cong ext λ a 
                                                                              ≡⇒↝ _ $ cong  eq  trans (sym eq) (set-get l₁ a)  _) (
        cong₂  set get  set a (get a)) s g                                   ≡⟨⟩

        trans (cong  set  set a (get l₁ a)) s)
          (cong  get  set l₂ a (get a)) g)                                   ≡⟨ sym $ cong₂ trans (cong-∘ _ _ s) (cong-∘ _ _ g) 

        trans (ext⁻¹ (ext⁻¹ s a) (get l₁ a))
          (cong (set l₂ a) (ext⁻¹ g a))                                         ))
                                                                               ×-cong
                                                                             ∀-cong ext λ a  ∀-cong ext λ b₁  ∀-cong ext λ b₂ 
                                                                              ≡⇒↝ _ $
                                                                              cong₂  p q  trans _ p 
                                                                                             trans (cong  set  set (set a b₁) b₂) q)
                                                                                               (set-set l₂ a b₁ b₂)) (
        cong  set  set a b₂) s                                               ≡⟨ sym $ cong-∘ _ _ s ⟩∎

        ext⁻¹ (ext⁻¹ s a) b₂                                                    )
                                                                                (
        s                                                                       ≡⟨ sym $ _≃_.right-inverse-of
                                                                                           (Eq.extensionality-isomorphism ext) _ 
        ⟨ext⟩ (ext⁻¹ s)                                                         ≡⟨ (cong ⟨ext⟩ $ ⟨ext⟩ λ _  sym $
                                                                                    _≃_.right-inverse-of
                                                                                      (Eq.extensionality-isomorphism ext) _) ⟩∎
        ⟨ext⟩ (⟨ext⟩  ext⁻¹  ext⁻¹ s)                                         ))) ⟩□

    ( λ (g :  a  get l₁ a  get l₂ a) 
      λ (s :  a b  set l₁ a b  set l₂ a b) 
     Erased
       ((∀ a b 
           trans (sym (trans (cong (get l₁) (s a b))
                         (g (set l₂ a b))))
             (get-set l₁ a b) 
           get-set l₂ a b) ×
        (∀ a 
           trans (sym (trans (s a (get l₁ a))
                         (cong (set l₂ a) (g a))))
             (set-get l₁ a) 
           set-get l₂ a) ×
        (∀ a b₁ b₂ 
           trans (set-set l₁ a b₁ b₂) (s a b₂) 
           trans (cong  set  set (set a b₁) b₂) (⟨ext⟩ (⟨ext⟩  s)))
             (set-set l₂ a b₁ b₂))))                                     
    where
    open Lens

  -- A lemma that can be used to prove that two lenses with
  -- definitionally equal getters and setters are equal.

  equal-laws→≡ :
    {get : A  B} {set : A  B  A}
    {l₁′ l₂′ : Erased ((∀ a b  get (set a b)  b) ×
                       (∀ a  set a (get a)  a) ×
                       (∀ a b₁ b₂  set (set a b₁) b₂  set a b₂))} 

    let l₁ = _↔_.from Lens-as-Σ (get , set , l₁′)
        l₂ = _↔_.from Lens-as-Σ (get , set , l₂′)
        open Lens
    in

    @0 (∀ a b  get-set l₁ a b  get-set l₂ a b) 
    @0 (∀ a  set-get l₁ a  set-get l₂ a) 
    @0 (∀ a b₁ b₂  set-set l₁ a b₁ b₂  set-set l₂ a b₁ b₂) 
    l₁  l₂
  equal-laws→≡ {l₁′ = l₁′} {l₂′ = l₂′} hyp₁ hyp₂ hyp₃ =
    let l₁″ = _↔_.from Lens-as-Σ (_ , _ , l₁′)
        l₂″ = _↔_.from Lens-as-Σ (_ , _ , l₂′)
    in
    _↔_.from equality-characterisation₂
      ( refl _
      , refl _
      , [  a b 
             trans (sym (cong₂  set get  get (set a b))
                           (refl _) (refl _)))
               (get-set l₁″ a b)                            ≡⟨ cong  eq  trans (sym eq) _) $ cong₂-refl _ 

             trans (sym (refl _)) (get-set l₁″ a b)         ≡⟨ cong (flip trans _) sym-refl 

             trans (refl _) (get-set l₁″ a b)               ≡⟨ trans-reflˡ _ 

             get-set l₁″ a b                                ≡⟨ hyp₁ _ _ ⟩∎

             get-set l₂″ a b                                )
        ,  a 
             trans (sym (cong₂  set get  set a (get a))
                           (refl _) (refl _)))
               (set-get l₁″ a)                              ≡⟨ cong  eq  trans (sym eq) _) $ cong₂-refl _ 

             trans (sym (refl _)) (set-get l₁″ a)           ≡⟨ cong (flip trans _) sym-refl 

             trans (refl _) (set-get l₁″ a)                 ≡⟨ trans-reflˡ _ 

             set-get l₁″ a                                  ≡⟨ hyp₂ _ ⟩∎

             set-get l₂″ a                                  )
        ,  a b₁ b₂ 
             subst  set  set (set a b₁) b₂  set a b₂) (refl _)
               (set-set l₁″ a b₁ b₂)                                ≡⟨ subst-refl _ _ 

             set-set l₁″ a b₁ b₂                                    ≡⟨ hyp₃ _ _ _ ⟩∎

             set-set l₂″ a b₁ b₂                                    )
        ]
      )
    where
    open Lens

-- An equality characterisation lemma for lenses from sets.

@0 equality-characterisation-for-sets :
  let open Lens in

  {l₁ l₂ : Lens A B} 

  Is-set A 

  l₁  l₂
    
  set l₁  set l₂
equality-characterisation-for-sets
  {A = A} {B = B} {l₁ = l₁} {l₂ = l₂} A-set =

  l₁  l₂            ↔⟨ inverse $ Eq.≃-≡ Lens≃Traditional-lens 
  trad l₁  trad l₂  ↝⟨ T.equality-characterisation-for-sets A-set ⟩□
  set l₁  set l₂    
  where
  open Lens

------------------------------------------------------------------------
-- More isomorphisms/equivalences related to lenses

-- Lens ⊤ B is equivalent (with erased proofs) to Contractibleᴱ B.

lens-from-⊤≃codomain-contractible :
  Lens  B ≃ᴱ Contractibleᴱ B
lens-from-⊤≃codomain-contractible = EEq.⇔→≃ᴱ
  (lens-preserves-h-level-of-domain 0 (mono₁ 0 ⊤-contractible))
  (ECP.Contractibleᴱ-propositional ext)
   l  Contractibleᴱ→Contractibleᴱ l
           (ECP.Contractible→Contractibleᴱ ⊤-contractible))
   (b , irrB)  record
     { get     = λ _  b
     ; get-set = λ _  erased irrB
     ; set-get = refl
     ; set-set = λ _ _ _  refl _
     })

-- Lens ⊥ B is equivalent to the unit type.

lens-from-⊥≃⊤ : Lens ( { = a}) B  
lens-from-⊥≃⊤ =
  Eq.↔⇒≃ $ _⇔_.to contractible⇔↔⊤ $
    record
      { get = ⊥-elim
      ; set = ⊥-elim
      ; get-set = λ a  ⊥-elim a
      ; set-get = λ a  ⊥-elim a
      ; set-set = λ a  ⊥-elim a
      } ,
    λ l  _↔_.from equality-characterisation₁
            ( ⟨ext⟩  a  ⊥-elim a)
            , ⟨ext⟩  a  ⊥-elim a)
            , [  a  ⊥-elim a)
              ,  a  ⊥-elim a)
              ,  a  ⊥-elim a)
              ]
            )

-- If A is a set and there is a lens from A to B, then A is equivalent
-- (with erased proofs) to the cartesian product of some type (that
-- can be expressed using the setter of l) and B.
--
-- This result is based on Theorem 2.3.9 from "Lenses and View Update
-- Translation" by Pierce and Schmitt.

≃ᴱΣ∥set⁻¹ᴱ∥ᴱ× :
  @0 Is-set A 
  (l : Lens A B) 
  A ≃ᴱ (( λ (f : B  A)   Lens.set l ⁻¹ᴱ f ∥ᴱ) × B)
≃ᴱΣ∥set⁻¹ᴱ∥ᴱ× {A = A} {B = B} A-set l = EEq.↔→≃ᴱ
   a  (set a ,  a , [ refl _ ] ) , get a)
   ((f , _) , b)  f b)
  to-from
   a 
     set a (get a)  ≡⟨ set-get a ⟩∎
     a              )
  where
  open Lens l

  @0 B-set : A  Is-set B
  B-set a =
    h-level-respects-lens-from-inhabited 2 l a A-set

  @0 to-from :  _  _
  to-from ((f , p) , b) = flip TE.rec p λ @0 where
    .TE.truncation-is-propositionʳ 
      ×-closure 2
        (Σ-closure 2
           (Π-closure ext 2 λ _  A-set) λ _ 
           mono₁ 1 TE.truncation-is-proposition)
        (B-set (f b))
    .TE.∣∣ʳ (a , [ q ]) 
      let
        lemma₁ =
          set (f b)      ≡⟨ cong  f  set (f b)) $ sym q 
          set (set a b)  ≡⟨ ⟨ext⟩ $ set-set a b 
          set a          ≡⟨ q ⟩∎
          f              

        lemma₂ =
          get (f b)      ≡⟨ cong  f  get (f b)) $ sym q 
          get (set a b)  ≡⟨ get-set _ _ ⟩∎
          b              
      in
      (set (f b) ,  f b , [ refl _ ] ) , get (f b)  ≡⟨ cong₂ _,_ (Σ-≡,≡→≡ lemma₁ (TE.truncation-is-proposition _ _)) lemma₂ ⟩∎
      (f         , p)                    , b          

-- If B is an inhabited set and there is a lens from A to B, then A is
-- equivalent (with erased proofs) to the cartesian product of some
-- type (that can be expressed using the getter of l) and B.
--
-- This result is based on Corollary 13 from "Algebras and Update
-- Strategies" by Johnson, Rosebrugh and Wood.

≃ᴱget⁻¹ᴱ× :
  @0 Is-set B 
  (b : B)
  (l : Lens A B) 
  A ≃ᴱ (Lens.get l ⁻¹ᴱ b × B)
≃ᴱget⁻¹ᴱ× {B = B} {A = A} B-set b₀ l = EEq.↔→≃ᴱ
   a  (set a b₀ , [ get-set a b₀ ]) , get a)
   ((a , _) , b)  set a b)
   ((a , [ h ]) , b) 
     let
       lemma =
         set (set a b) b₀  ≡⟨ set-set a b b₀ 
         set a b₀          ≡⟨ cong (set a) (sym h) 
         set a (get a)     ≡⟨ set-get a ⟩∎
         a                 
     in
     (set (set a b) b₀ , [ get-set (set a b) b₀ ]) , get (set a b)  ≡⟨ cong₂ _,_ (Σ-≡,≡→≡ lemma ([]-cong [ B-set _ _ ])) (get-set a b) ⟩∎
     (a                , [ h                    ]) , b              )
   a 
     set (set a b₀) (get a)  ≡⟨ set-set a b₀ (get a) 
     set a (get a)           ≡⟨ set-get a ⟩∎
     a                       )
  where
  open Lens l

-- For somewhat coherent lenses the previous result can be proved
-- without the assumption that the codomain is a set.

≃ᴱget⁻¹ᴱ×-coherent :
  (b : B)
  (l : Coherent-lens A B) 
  A ≃ᴱ (Coherent-lens.get l ⁻¹ᴱ b × B)
≃ᴱget⁻¹ᴱ×-coherent {B = B} {A = A} b₀ l = EEq.↔→≃ᴱ
   a  (set a b₀ , [ get-set a b₀ ]) , get a)
   ((a , _) , b)  set a b)
   ((a , [ h ]) , b) 
     let
       lemma₁ =
         set (set a b) b₀  ≡⟨ set-set a b b₀ 
         set a b₀          ≡⟨ cong (set a) (sym h) 
         set a (get a)     ≡⟨ set-get a ⟩∎
         a                 

       lemma₂₁ =
         cong get (trans (set-set a b b₀)
                     (trans (cong (set a) (sym h))
                        (set-get a)))               ≡⟨ trans (cong-trans _ _ _) $
                                                       cong (trans _) $
                                                       trans (cong-trans _ _ _) $
                                                       cong (flip trans _) $
                                                       cong-∘ _ _ _ 
         trans (cong get (set-set a b b₀))
           (trans (cong (get  set a) (sym h))
              (cong get (set-get a)))               ≡⟨ cong₂  p q  trans p (trans (cong (get  set a) (sym h)) q))
                                                         (get-set-set _ _ _)
                                                         (get-set-get _) ⟩∎
         trans (trans (get-set (set a b) b₀)
                  (sym (get-set a b₀)))
           (trans (cong (get  set a) (sym h))
              (get-set a (get a)))                  

       lemma₂₂ =
         sym (trans (trans (get-set (set a b) b₀)
                       (sym (get-set a b₀)))
                (trans (cong (get  set a) (sym h))
                   (get-set a (get a))))               ≡⟨ trans (sym-trans _ _) $
                                                          cong₂ trans
                                                            (sym-trans _ _)
                                                            (sym-trans _ _) 
         trans (trans (sym (get-set a (get a)))
                  (sym (cong (get  set a) (sym h))))
           (trans (sym (sym (get-set a b₀)))
              (sym (get-set (set a b) b₀)))            ≡⟨ cong₂  p q  trans (trans (sym (get-set a (get a))) p)
                                                                           (trans q (sym (get-set (set a b) b₀))))
                                                            (trans (cong sym $ cong-sym _ _) $
                                                             sym-sym _)
                                                            (sym-sym _) 
         trans (trans (sym (get-set a (get a)))
                  (cong (get  set a) h))
           (trans (get-set a b₀)
              (sym (get-set (set a b) b₀)))            ≡⟨ trans (sym $ trans-assoc _ _ _) $
                                                          cong (flip trans _) $ trans-assoc _ _ _ ⟩∎
         trans (trans (sym (get-set a (get a)))
                  (trans (cong (get  set a) h)
                     (get-set a b₀)))
           (sym (get-set (set a b) b₀))                

       lemma₂′ =
         subst  a  get a  b₀)
           (trans (set-set a b b₀)
              (trans (cong (set a) (sym h)) (set-get a)))
           (get-set (set a b) b₀)                            ≡⟨ subst-∘ _ _ _ 

         subst (_≡ b₀)
           (cong get (trans (set-set a b b₀)
                        (trans (cong (set a) (sym h))
                           (set-get a))))
           (get-set (set a b) b₀)                            ≡⟨ subst-trans-sym 

         trans
           (sym (cong get (trans (set-set a b b₀)
                             (trans (cong (set a) (sym h))
                                (set-get a)))))
           (get-set (set a b) b₀)                            ≡⟨ cong (flip (trans  sym) _) lemma₂₁ 

         trans
           (sym (trans (trans (get-set (set a b) b₀)
                          (sym (get-set a b₀)))
                   (trans (cong (get  set a) (sym h))
                      (get-set a (get a)))))
           (get-set (set a b) b₀)                            ≡⟨ cong (flip trans _) lemma₂₂ 

         trans
           (trans (trans (sym (get-set a (get a)))
                     (trans (cong (get  set a) h)
                        (get-set a b₀)))
              (sym (get-set (set a b) b₀)))
           (get-set (set a b) b₀)                            ≡⟨ trans-[trans-sym]- _ _ 

         trans (sym (get-set a (get a)))
           (trans (cong (get  set a) h)
              (get-set a b₀))                                ≡⟨ cong  f  trans (sym (f (get a))) (trans (cong (get  set a) h) (f b₀))) $ sym $
                                                                _≃_.left-inverse-of (Eq.extensionality-isomorphism ext) (get-set a) 
         trans (sym (ext⁻¹ (⟨ext⟩ (get-set a)) (get a)))
           (trans (cong (get  set a) h)
              (ext⁻¹ (⟨ext⟩ (get-set a)) b₀))                ≡⟨ elim₁
                                                                   {f} eq 
                                                                     trans (sym (ext⁻¹ eq (get a)))
                                                                       (trans (cong f h) (ext⁻¹ eq b₀)) 
                                                                       h)
                                                                  (
             trans (sym (ext⁻¹ (refl P.id) (get a)))
               (trans (cong P.id h) (ext⁻¹ (refl P.id) b₀))        ≡⟨ cong₂  p q  trans p (trans (cong P.id h) q))
                                                                        (trans (cong sym (ext⁻¹-refl _)) sym-refl)
                                                                        (ext⁻¹-refl _) 

             trans (refl _) (trans (cong P.id h) (refl _))         ≡⟨ trans-reflˡ _ 

             trans (cong P.id h) (refl _)                          ≡⟨ trans-reflʳ _ 

             cong P.id h                                           ≡⟨ sym $ cong-id _ ⟩∎

             h                                                     )
                                                                  _ ⟩∎
         h                                                   

       lemma₂ =
         subst  a  Erased (get a  b₀))
           (trans (set-set a b b₀)
              (trans (cong (set a) (sym h)) (set-get a)))
           [ get-set (set a b) b₀ ]                          ≡⟨ push-subst-[] 

         [ subst  a  get a  b₀)
             (trans (set-set a b b₀)
                (trans (cong (set a) (sym h)) (set-get a)))
             (get-set (set a b) b₀)
         ]                                                   ≡⟨ []-cong [ lemma₂′ ] ⟩∎

         [ h ]                                               
     in
     ((set (set a b) b₀ , [ get-set (set a b) b₀ ]) , get (set a b))  ≡⟨ cong₂ _,_ (Σ-≡,≡→≡ lemma₁ lemma₂) (get-set a b) ⟩∎
     ((a                , [ h                    ]) , b            )  )
   a 
     set (set a b₀) (get a)  ≡⟨ set-set a b₀ (get a) 
     set a (get a)           ≡⟨ set-get a ⟩∎
     a                       )
  where
  open Coherent-lens l

------------------------------------------------------------------------
-- A conversion function

-- If A is a set, then Lens A B is equivalent to Coherent-lens A B.

≃coherent : @0 Is-set A  Lens A B  Coherent-lens A B
≃coherent {A = A} {B = B} A-set = Eq.↔→≃
  to
  Coherent-lens.lens
   l  let l′ = Coherent-lens.lens l in
                          $⟨ H-level-Erased 1
                               (×-closure 1
                                  (Π-closure ext 1 λ a 
                                   mono₁ 2 (B-set l′ a))
                                  (Π-closure ext 1 λ a 
                                   Π-closure ext 1 λ _ 
                                   Π-closure ext 1 λ _ 
                                   mono₁ 2 (B-set l′ a))) 
     Is-proposition _     ↝⟨  p  cong (l′ ,_) (p _ _))  (_  _) 
     (l′ , _)  (l′ , _)  ↔⟨ Eq.≃-≡ Coherent-lens-as-Σ ⟩□
     to l′  l            )
  refl
  where
  @0 B-set : Lens A B  A  Is-set B
  B-set l a =
    h-level-respects-lens-from-inhabited 2 l a A-set

  to : Lens A B  Coherent-lens A B
  to l = record
    { lens        = l
    ; get-set-get = λ a  B-set l a _ _
    ; get-set-set = λ a _ _  B-set l a _ _
    }

-- The conversion preserves getters and setters.

≃coherent-preserves-getters-and-setters :
  {A : Type a}
  (@0 s : Is-set A) 
  Preserves-getters-and-setters-⇔ A B
    (_≃_.logical-equivalence (≃coherent s))
≃coherent-preserves-getters-and-setters _ =
     _  refl _ , refl _)
  ,  _  refl _ , refl _)

------------------------------------------------------------------------
-- Lens combinators

module Lens-combinators where

  -- If two types are isomorphic, then there is a lens between them.

  ↔→lens : A  B  Lens A B
  ↔→lens A↔B = record
    { get     = to
    ; set     = const from
    ; get-set = const right-inverse-of
    ; set-get = left-inverse-of
    ; set-set = λ _ _ _  refl _
    }
    where
    open _↔_ A↔B

  -- If there is an equivalence with erased proofs between two types,
  -- then there is a lens between them.

  ≃ᴱ→lens : A ≃ᴱ B  Lens A B
  ≃ᴱ→lens A≃B = record
    { get     = to
    ; set     = const from
    ; get-set = const right-inverse-of
    ; set-get = left-inverse-of
    ; set-set = λ _ _ _  refl _
    }
    where
    open _≃ᴱ_ A≃B

  -- Identity lens.

  id : Lens A A
  id = ≃ᴱ→lens F.id

  -- The identity lens is equal to the one obtained from the
  -- traditional identity lens without erased proofs.

  Traditional-lens-id≡id :
    Traditional-lens→Lens TC.id  id {A = A}
  Traditional-lens-id≡id = refl _

  -- Composition of lenses.

  infixr 9 _∘_

  _∘_ : Lens B C  Lens A B  Lens A C
  l₁  l₂ = record
    { get     = λ a  get l₁ (get l₂ a)
    ; set     = λ a c 
                let b = set l₁ (get l₂ a) c in
                set l₂ a b
    ; get-set = T.Lens.get-set l₁∘l₂
    ; set-get = T.Lens.set-get l₁∘l₂
    ; set-set = T.Lens.set-set l₁∘l₂
    }
    where
    open Lens

    @0 l₁∘l₂ : _
    l₁∘l₂ = trad l₁ TC.∘ trad l₂

  -- Traditional-lens→Lens commutes with composition.

  @0 Traditional-lens-∘≡∘ :
    {l₁ : T.Lens B C} {l₂ : T.Lens A B} 
    Traditional-lens→Lens (l₁ TC.∘ l₂) 
    Traditional-lens→Lens l₁  Traditional-lens→Lens l₂
  Traditional-lens-∘≡∘ = refl _

  -- Note that composition can be defined in several different ways.
  -- Here are two alternative implementations.

  infixr 9 _∘′_ _∘″_

  _∘′_ : Lens B C  Lens A B  Lens A C
  l₁ ∘′ l₂ = record (l₁  l₂)
    { set-set = T.Lens.set-set l₁∘′l₂
    }
    where
    @0 l₁∘′l₂ : _
    l₁∘′l₂ = trad l₁ TC.∘′ trad l₂

  _∘″_ : Lens B C  Lens A B  Lens A C
  l₁ ∘″ l₂ = record (l₁  l₂)
    { set-set = T.Lens.set-set l₁∘″l₂
    }
    where
    @0 l₁∘″l₂ : _
    l₁∘″l₂ = trad l₁ TC.∘″ trad l₂

  -- These two implementations are pointwise equal to the other one.
  -- However, I don't know if there is some other definition that is
  -- distinct from these two (if we require that the definitions are
  -- polymorphic, that get and set are implemented in the same way as
  -- for _∘_, and that the three composition laws below hold).

  ∘≡∘′ : l₁  l₂  l₁ ∘′ l₂
  ∘≡∘′ {l₁ = l₁} {l₂ = l₂} = equal-laws→≡
     _ _  refl _)
     _  refl _)
     a c₁ c₂ 
       let b₁ = set l₁ (get l₂ a) c₁
           b₂ = set l₁ b₁ c₂
           a′ = set l₂ a b₁
           b′ = set l₁ (get l₂ a′) c₂
       in
       set-set (l₁  l₂) a c₁ c₂                                          ≡⟨⟩

       trans (set-set l₂ a b₁ b′)
         (trans (cong  b  set l₂ a (set l₁ b c₂)) (get-set l₂ a b₁))
            (cong (set l₂ a) (set-set l₁ (get l₂ a) c₁ c₂)))              ≡⟨ sym $ trans-assoc _ _ _ 

       trans (trans (set-set l₂ a b₁ b′)
                (cong  b  set l₂ a (set l₁ b c₂)) (get-set l₂ a b₁)))
         (cong (set l₂ a) (set-set l₁ (get l₂ a) c₁ c₂))                  ≡⟨ cong (flip trans _) $
                                                                             elim₁
                                                                                eq 
                                                                                  trans (set-set l₂ _ b₁ _)
                                                                                    (cong  b  set l₂ a (set l₁ b c₂)) eq) 
                                                                                  trans (cong  b  set l₂ _ (set l₁ b _)) eq)
                                                                                    (set-set l₂ _ _ _))
                                                                               (
           trans (set-set l₂ a b₁ b₂)
             (cong  b  set l₂ a (set l₁ b c₂)) (refl _))                     ≡⟨ trans (cong (trans _) $ cong-refl _) $
                                                                                   trans-reflʳ _ 

           set-set l₂ a b₁ b₂                                                   ≡⟨ sym $
                                                                                   trans (cong (flip trans _) $ cong-refl _) $
                                                                                   trans-reflˡ _ ⟩∎
           trans (cong  b  set l₂ a′ (set l₁ b c₂)) (refl _))
             (set-set l₂ a b₁ b₂)                                               )
                                                                               (get-set l₂ a b₁) 
       trans (trans (cong  b  set l₂ a′ (set l₁ b c₂))
                       (get-set l₂ a b₁))
                (set-set l₂ a b₁ b₂))
         (cong (set l₂ a) (set-set l₁ (get l₂ a) c₁ c₂))                  ≡⟨ trans-assoc _ _ _ 

       trans (cong  b  set l₂ a′ (set l₁ b c₂)) (get-set l₂ a b₁))
         (trans (set-set l₂ a b₁ b₂)
            (cong (set l₂ a) (set-set l₁ (get l₂ a) c₁ c₂)))              ≡⟨⟩

       set-set (l₁ ∘′ l₂) a c₁ c₂                                         )
    where
    open Lens

  ∘≡∘″ : l₁  l₂  l₁ ∘″ l₂
  ∘≡∘″ {l₁ = l₁} {l₂ = l₂} = equal-laws→≡
     _ _  refl _)
     _  refl _)
     a c₁ c₂ 
       let b₁ = set l₁ (get l₂ a) c₁
           b₂ = set l₁ (get l₂ a) c₂
           a′ = set l₂ a b₁
           b′ = set l₁ (get l₂ a′) c₂

           eq : b′  b₂
           eq = trans (cong  b  set l₁ b c₂) (get-set l₂ a b₁))
                  (set-set l₁ (get l₂ a) c₁ c₂)
       in
       set-set (l₁  l₂) a c₁ c₂                                         ≡⟨⟩

       trans (set-set l₂ a b₁ b′)
         (trans (cong  b  set l₂ a (set l₁ b c₂)) (get-set l₂ a b₁))
            (cong (set l₂ a) (set-set l₁ (get l₂ a) c₁ c₂)))             ≡⟨ cong (trans (set-set l₂ a b₁ b′)) $
                                                                            trans (cong (flip trans _) $ sym $ cong-∘ _ _ _) $
                                                                            sym $ cong-trans _ _ _ 

       trans (set-set l₂ a b₁ b′) (cong (set l₂ a) eq)                   ≡⟨ elim¹
                                                                               {b₂} eq  trans (set-set l₂ a b₁ b′) (cong (set l₂ a) eq) 
                                                                                           trans (cong (set l₂ a′) eq) (set-set l₂ a b₁ b₂))
                                                                              (
           trans (set-set l₂ a b₁ b′) (cong (set l₂ a) (refl _))               ≡⟨ cong (trans _) $ cong-refl _ 
           trans (set-set l₂ a b₁ b′) (refl _)                                 ≡⟨ trans-reflʳ _ 
           set-set l₂ a b₁ b′                                                  ≡⟨ sym $ trans-reflˡ _ 
           trans (refl _) (set-set l₂ a b₁ b′)                                 ≡⟨ cong (flip trans _) $ sym $ cong-refl _ ⟩∎
           trans (cong (set l₂ a′) (refl _)) (set-set l₂ a b₁ b′)              )
                                                                              eq 

       trans (cong (set l₂ a′) eq) (set-set l₂ a b₁ b₂)                  ≡⟨ trans (cong (flip trans _) $
                                                                                   trans (cong-trans _ _ _) $
                                                                                   cong (flip trans _) $ cong-∘ _ _ _) $
                                                                            trans-assoc _ _ _ 
       trans (cong  b  set l₂ a′ (set l₁ b c₂)) (get-set l₂ a b₁))
         (trans (cong (set l₂ a′) (set-set l₁ (get l₂ a) c₁ c₂))
            (set-set l₂ a b₁ b₂))                                        ≡⟨⟩

       set-set (l₁ ∘″ l₂) a c₁ c₂                                        )
    where
    open Lens

  -- id is a left identity of _∘_.

  left-identity : (l : Lens A B)  id  l  l
  left-identity l = equal-laws→≡
     a b 
       trans (cong P.id (get-set a b)) (refl _)  ≡⟨ trans-reflʳ _ 
       cong P.id (get-set a b)                   ≡⟨ sym $ cong-id _ ⟩∎
       get-set a b                               )
     a 
       trans (cong (set a) (refl _)) (set-get a)  ≡⟨ cong (flip trans _) $ cong-refl _ 
       trans (refl _) (set-get a)                 ≡⟨ trans-reflˡ _ ⟩∎
       set-get a                                  )
     a b₁ b₂ 
       trans (set-set a b₁ b₂)
         (trans (cong  _  set a b₂) (get-set a b₁))
            (cong (set a) (refl _)))                      ≡⟨ cong₂  p q  trans _ (trans p q))
                                                               (cong-const _)
                                                               (cong-refl _) 

       trans (set-set a b₁ b₂) (trans (refl _) (refl _))  ≡⟨ trans (cong (trans _) trans-refl-refl) $
                                                             trans-reflʳ _ ⟩∎
       set-set a b₁ b₂                                    )
    where
    open Lens l

  -- id is a right identity of _∘_.

  right-identity : (l : Lens A B)  l  id  l
  right-identity l = equal-laws→≡
     a b 
       trans (cong get (refl _)) (get-set a b)  ≡⟨ cong (flip trans _) $ cong-refl _ 
       trans (refl _) (get-set a b)             ≡⟨ trans-reflˡ _ ⟩∎
       get-set a b                              )
     a 
       trans (cong P.id (set-get a)) (refl _)  ≡⟨ trans-reflʳ _ 
       cong P.id (set-get a)                   ≡⟨ sym $ cong-id _ ⟩∎
       set-get a                               )
     a b₁ b₂ 
       trans (refl _)
         (trans (cong  b  set b b₂) (refl _))
            (cong P.id (set-set a b₁ b₂)))        ≡⟨ trans-reflˡ _ 

       trans (cong  b  set b b₂) (refl _))
         (cong P.id (set-set a b₁ b₂))            ≡⟨ cong₂ trans (cong-refl _) (sym $ cong-id _) 

       trans (refl _) (set-set a b₁ b₂)           ≡⟨ trans-reflˡ _ ⟩∎

       set-set a b₁ b₂                            )
    where
    open Lens l

  -- _∘_ is associative.

  associativity :
    (l₁ : Lens C D) (l₂ : Lens B C) (l₃ : Lens A B) 
    l₁  (l₂  l₃)  (l₁  l₂)  l₃
  associativity l₁ l₂ l₃ = equal-laws→≡ lemma₁ lemma₂ lemma₃
    where
    open Lens

    @0 lemma₁ : _
    lemma₁ = λ a d 
      let
        f  = get l₁
        g  = get l₂
        b  = get l₃ a
        c  = g b
        c′ = set l₁ c d
        x  = get-set l₃ a (set l₂ b c′)
        y  = get-set l₂ b c′
        z  = get-set l₁ c d
      in
      trans (cong f $ trans (cong g x) y) z           ≡⟨ cong  x  trans x z) (cong-trans f _ y) 
      trans (trans (cong f $ cong g x) (cong f y)) z  ≡⟨ trans-assoc _ _ z 
      trans (cong f $ cong g x) (trans (cong f y) z)  ≡⟨ cong  x  trans x (trans (cong f y) z)) (cong-∘ f g x) ⟩∎
      trans