------------------------------------------------------------------------
-- Dependent lenses
------------------------------------------------------------------------

-- Some code below depends on UIP for Type ℓ (for some ℓ). This kind
-- of assumption is inconsistent in Cubical Agda. However, Andrea
-- Vezzosi and I have discussed whether UIP, the propositional
-- truncation, and extensionality are mutually consistent, and it
-- seems plausible that some form of extensional type theory with
-- squash types would provide a model for these things.
--
-- Note that the code that depends on UIP does not make use of
-- univalence, or at least it did not use to do this, things may have
-- changed after this code was written. This module uses types to
-- track uses of univalence, but imported code might contain "hidden"
-- uses of univalence.

module Lens.Dependent where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (module _⇔_)
open import Prelude as P hiding (id; swap; Unit) renaming (_∘_ to _⊚_)

open import Bijection equality-with-J as Bij using (_↔_; module _↔_)
open import Bool equality-with-J
open import Equality.Decidable-UIP equality-with-J using (Constant)
open import Equality.Decision-procedures equality-with-J
import Equality.Groupoid equality-with-J as EG
open import Equality.Tactic equality-with-J as Tactic hiding (module Eq)
open import Equivalence equality-with-J as Eq using (_≃_; module _≃_)
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import Groupoid equality-with-J
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional equality-with-paths
  as Trunc
open import Surjection equality-with-J using (module _↠_)
open import Univalence-axiom equality-with-J

import Lens.Non-dependent.Higher equality-with-paths as ND
import Lens.Non-dependent.Higher.Combinators equality-with-paths as NDC

private
  variable
    a b b₁ b₂ b₃ c r r₁ r₂ r₃ : Level
    A                         : Type a

------------------------------------------------------------------------
-- Dependent lenses with "remainder types" visible in the type

-- If Lens₃ A R B is inhabited, then a value of type A can be split up
-- into a "remainder" r of type R and a value of type B r.

Lens₃ : Type a → (R : Type r) → (R → Type b) → Type _
Lens₃ A R B = A ≃ Σ R B

module Lens₃ {R : Type r} {B : R → Type b} (lens : Lens₃ A R B) where

  open _≃_

  -- The remainder.

  remainder : A → R
  remainder a = proj₁ (to lens a)

  -- Getter.

  get : (a : A) → B (remainder a)
  get a = proj₂ (to lens a)

  -- Setter.

  set : (a : A) → B (remainder a) → A
  set a b = from lens (remainder a , b)

  -- Modifier.

  modify : (a : A) → (B (remainder a) → B (remainder a)) → A
  modify a f = set a (f (get a))

  -- Setting leaves the remainder unchanged.

  remainder-set : ∀ a b → remainder (set a b) ≡ remainder a
  remainder-set a b =
    proj₁ (to lens (from lens (remainder a , b)))  ≡⟨ cong proj₁ (right-inverse-of lens _) ⟩∎
    remainder a                                    ∎

  -- A related isomorphism.

  codomain-set-≃ : ∀ {a b} → B (remainder (set a b)) ≃ B (remainder a)
  codomain-set-≃ = ≡⇒≃ (cong B (remainder-set _ _))

  -- Some lens laws.

  set-get : ∀ a → set a (get a) ≡ a
  set-get a =
    from lens (proj₁ (to lens a) , proj₂ (to lens a))  ≡⟨⟩
    from lens (to lens a)                              ≡⟨ left-inverse-of lens _ ⟩∎
    a                                                  ∎

  get-set₁ : ∀ a b → get (set a b) ≡ subst B (sym (remainder-set a b)) b
  get-set₁ a b =
    proj₂ (to lens (from lens (remainder a , b)))  ≡⟨ sym $ dcong proj₂ (sym lemma) ⟩

    subst (B ⊚ proj₁) (sym lemma)
          (proj₂ {B = B} (remainder a , b))        ≡⟨⟩

    subst (B ⊚ proj₁) (sym lemma) b                ≡⟨ subst-∘ _ _ (sym lemma) ⟩

    subst B (cong proj₁ (sym lemma)) b             ≡⟨ cong (λ x → subst B x b) (cong-sym _ lemma) ⟩∎

    subst B (sym (cong proj₁ lemma)) b             ∎
    where
    lemma = right-inverse-of lens _

  get-set₂ : ∀ a b → get (set a b) ≡ from codomain-set-≃ b
  get-set₂ a b =
    proj₂ (to lens (from lens (remainder a , b)))  ≡⟨ get-set₁ _ _ ⟩
    subst B (sym (cong proj₁ lemma)) b             ≡⟨ subst-in-terms-of-inverse∘≡⇒↝ equivalence (cong proj₁ lemma) _ _ ⟩∎
    ≡⇒← (cong B (cong proj₁ lemma)) b              ∎
    where
    lemma = right-inverse-of lens _

  set-set₁ : ∀ a b₁ b₂ →
             set (set a b₁) b₂ ≡ set a (subst B (remainder-set a b₁) b₂)
  set-set₁ a b₁ b₂ =
    from lens (remainder (set a b₁) , b₂)    ≡⟨ cong (from lens) (Σ-≡,≡→≡ eq refl) ⟩∎
    from lens (remainder a , subst B eq b₂)  ∎
    where
    eq = remainder-set a b₁

  set-set₂ : ∀ a b₁ b₂ →
             set (set a b₁) b₂ ≡ set a (to codomain-set-≃ b₂)
  set-set₂ a b₁ b₂ =
    set (set a b₁) b₂           ≡⟨ set-set₁ _ _ _ ⟩
    set a (subst B eq b₂)       ≡⟨ cong (set a) (subst-in-terms-of-≡⇒↝ equivalence eq _ _) ⟩∎
    set a (≡⇒→ (cong B eq) b₂)  ∎
    where
    eq = remainder-set a b₁

------------------------------------------------------------------------
-- Lens₃ combinators

-- Identity lens.

id₃ : Lens₃ A ⊤ (λ _ → A)
id₃ {A = A} =
  A      ↔⟨ inverse ×-left-identity ⟩□
  ⊤ × A  □

-- Composition of lenses.

infixr  _₃∘₃_

_₃∘₃_ : {R₁ : Type r₁} {B₁ : R₁ → Type b₁}
        {R₂ : R₁ → Type r₂} {B₂ : (r : R₁) → R₂ r → Type b₂} →
        (∀ {r} → Lens₃ (B₁ r) (R₂ r) (B₂ r)) → Lens₃ A R₁ B₁ →
        Lens₃ A (Σ R₁ R₂) (uncurry B₂)
_₃∘₃_ {A = A} {R₁ = R₁} {B₁ = B₁} {R₂ = R₂} {B₂ = B₂} l₁ l₂ =
  A                             ↔⟨ l₂ ⟩
  Σ R₁ B₁                       ↔⟨ ∃-cong (λ _ → l₁) ⟩
  Σ R₁ (λ r → Σ (R₂ r) (B₂ r))  ↔⟨ Σ-assoc ⟩□
  Σ (Σ R₁ R₂) (uncurry B₂)      □

------------------------------------------------------------------------
-- Some Lens₃ properties

-- id₃ and _₃∘₃_ form a kind of precategory.

left-identity₃ :
  {R : Type r} {B : R → Type b} →
  (l : Lens₃ A R B) →
  id₃ ₃∘₃ l
    ≡
  (A                      ↝⟨ l ⟩
   Σ R B                  ↝⟨ Σ-cong (inverse ×-right-identity) (λ _ → F.id) ⟩□
   Σ (R × ⊤) (B ⊚ proj₁)  □)
left-identity₃ _ = Eq.lift-equality ext refl

right-identity₃ :
  {R : Type r} {B : R → Type b} →
  (l : Lens₃ A R B) →
  l ₃∘₃ id₃
    ≡
  (A                      ↝⟨ l ⟩
   Σ R B                  ↝⟨ Σ-cong (inverse ×-left-identity) (λ _ → F.id) ⟩□
   Σ (⊤ × R) (B ⊚ proj₂)  □)
right-identity₃ _ = Eq.lift-equality ext refl

associativity₃ :
  {R₁ : Type r₁} {B₁ : R₁ → Type b₁}
  {R₂ : R₁ → Type r₂} {B₂ : (r₁ : R₁) → R₂ r₁ → Type b₂}
  {R₃ : (r₁ : R₁) → R₂ r₁ → Type r₃}
  {B₃ : (r₁ : R₁) (r₂ : R₂ r₁) → R₃ r₁ r₂ → Type b₃} →
  (l₁ : ∀ {r₁ r₂} → Lens₃ (B₂ r₁ r₂) (R₃ r₁ r₂) (B₃ r₁ r₂))
  (l₂ : ∀ {r} → Lens₃ (B₁ r) (R₂ r) (B₂ r))
  (l₃ : Lens₃ A R₁ B₁) →
  l₁ ₃∘₃ (l₂ ₃∘₃ l₃)
    ≡
  (A                                                             ↝⟨ (l₁ ₃∘₃ l₂) ₃∘₃ l₃ ⟩
   Σ (Σ R₁ (λ r₁ → Σ (R₂ r₁) (R₃ r₁))) (uncurry (uncurry ⊚ B₃))  ↝⟨ Σ-cong Σ-assoc (λ _ → F.id) ⟩□
   Σ (Σ (Σ R₁ R₂) (uncurry R₃)) (uncurry (uncurry B₃))           □)
associativity₃ _ _ _ = Eq.lift-equality ext refl

------------------------------------------------------------------------
-- Dependent lenses without "remainder types" visible in the type

-- One definition.

Lens : (A : Type a) → (A → Type b) → Type (lsuc (a ⊔ b))
Lens {a = a} {b = b} A B =
  ∃ λ (R : Type (a ⊔ b)) →
  ∃ λ (B′ : R → Type b) →
  ∃ λ (lens : Lens₃ A R B′) →
  ((r : R) → ∥ B′ r ∥)
    ×
  (∀ a → B′ (Lens₃.remainder lens a) ≡ B a)

-- An alternative definition. This definition is pointwise isomorphic
-- to the previous one, see Lens↔Lens′ below.

Lens′ : (A : Type a) → (A → Type b) → Type (lsuc (a ⊔ b))
Lens′ {a = a} {b = b} A B =
  ∃ λ (get : (a : A) → B a) →
  ∃ λ (R : Type (a ⊔ b)) →
  ∃ λ (remainder : A → R) →
  Surjective remainder
    ×
  ∃ λ (B′ : R → Type b) →
  ∃ λ (variant : ∀ {a} → B a ≡ B′ (remainder a)) →
  Eq.Is-equivalence {B = ∃ B′}
                    (λ a → remainder a , subst P.id variant (get a))

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

  -- The remainder type: what remains of A when B is removed
  -- (roughly).

  R : Type (a ⊔ b)
  R = proj₁ l

  -- A variant of B, indexed by Rs instead of As.

  B′ : R → Type b
  B′ = proj₁ (proj₂ l)

  -- The main lens isomorphism.

  lens : Lens₃ A R B′
  lens = proj₁ (proj₂ (proj₂ l))

  -- If the remainder type is inhabited, then the corresponding view
  -- should also be (merely) inhabited.

  inhabited : (r : R) → ∥ B′ r ∥
  inhabited = proj₁ (proj₂ (proj₂ (proj₂ l)))

  private module L = Lens₃ lens
  open _≃_

  -- The "non-B" part of the A value.

  remainder : A → R
  remainder = L.remainder

  -- An equality that specifies in what sense B′ is a variant of B.
  --
  -- (This used to be a bijection, but it was turned into an
  -- equality in order to make it obvious that, if the K rule is
  -- enabled, then variant cannot do anything strange.)

  variant : ∀ a → B′ (remainder a) ≡ B a
  variant = proj₂ (proj₂ (proj₂ (proj₂ l)))

  -- A corresponding isomorphism.

  variant≃ : ∀ {a} → B′ (remainder a) ≃ B a
  variant≃ = ≡⇒≃ (variant _)

  -- A variant of variant.

  other-variant : ∀ r (b′ : B′ r) → B′ r ≡ B (from lens (r , b′))
  other-variant r b′ =
    B′ r                                       ≡⟨⟩
    B′ (proj₁ {B = B′} (r , b′))               ≡⟨ cong (B′ ⊚ proj₁) (sym $ right-inverse-of lens (r , b′)) ⟩
    B′ (proj₁ (to lens (from lens (r , b′))))  ≡⟨⟩
    B′ (remainder (from lens (r , b′)))        ≡⟨ variant (_≃_.from lens (r , b′)) ⟩∎
    B (from lens (r , b′))                     ∎

  -- Note that B ⊚ _≃_.from lens only depends on the "R part" of the
  -- argument.

  independent-of-B′ : (r : R) → Constant (B ⊚ _≃_.from lens ⊚ (r ,_))
  independent-of-B′ r b₁ b₂ =
    B (_≃_.from lens (r , b₁))  ≡⟨ sym $ other-variant _ _ ⟩
    B′ r                        ≡⟨ other-variant _ _ ⟩∎
    B (_≃_.from lens (r , b₂))  ∎

  -- Thus we can, assuming that Type b is a set, define a variant of B
  -- that only depends on R.

  module First-variant-of-B (uip : Is-set (Type b)) where

    private

      B̲′ : (r : R) → ∥ B′ r ∥ → Type b
      B̲′ r =
        to (constant-function≃∥inhabited∥⇒inhabited uip)
           (B ⊚ _≃_.from lens ⊚ (r ,_) , independent-of-B′ r)

    B̲ : R → Type b
    B̲ r = B̲′ r (inhabited r)

    -- This type family is pointwise equal to B′ (given the same
    -- assumptions).

    B′≡B̲ : ∀ r → B′ r ≡ B̲ r
    B′≡B̲ r = Trunc.elim
      (λ ∥b′∥ → B′ r ≡ B̲′ r ∥b′∥)
      (λ _ → uip)
      (other-variant r)
      (inhabited r)

  -- We can also use other assumptions:
  --
  -- * Univalence.
  -- * B should be a family of sets.

  module Second-variant-of-B
           (univ  : Univalence b)
           (B-set : ∀ a → Is-set (B a))
           where

    private opaque

      B̲-triple : (r : R) → ∃ λ (X : Set b) → B′ r ≡ proj₁ X
      B̲-triple r =
        to (coherently-constant-function≃∥inhabited∥⇒inhabited
              (Σ-closure 
                 (∃-H-level-H-level-1+ ext univ )
                 (λ { (_ , X-set) → mono₁  $
                      H-level-H-level-≡ʳ ext univ  X-set })))
           ( (λ b′ →   (B (_≃_.from lens (r , b′)) , B-set _)
                     , other-variant r b′)
           , (λ b′₁ b′₂ → Σ-≡,≡→≡
                (Σ-≡,≡→≡ (independent-of-B′ r b′₁ b′₂)
                         (Is-set-is-propositional _ _))
                (subst (λ X → B′ r ≡ proj₁ X)
                       (Σ-≡,≡→≡ (independent-of-B′ r b′₁ b′₂) _)
                       (other-variant r b′₁)                        ≡⟨ subst-∘ (B′ r ≡_) proj₁
                                                                               (Σ-≡,≡→≡ (independent-of-B′ r b′₁ b′₂) _) ⟩
                 subst (B′ r ≡_)
                       (cong proj₁ $
                          Σ-≡,≡→≡ (independent-of-B′ r b′₁ b′₂) _)
                       (other-variant r b′₁)                        ≡⟨⟩

                 trans (other-variant r b′₁)
                       (cong proj₁ $
                          Σ-≡,≡→≡ (independent-of-B′ r b′₁ b′₂) _)  ≡⟨ cong (trans (other-variant r b′₁)) $
                                                                         proj₁-Σ-≡,≡→≡ (independent-of-B′ r b′₁ b′₂) _ ⟩
                 trans (other-variant r b′₁)
                       (independent-of-B′ r b′₁ b′₂)                ≡⟨⟩

                 trans (other-variant r b′₁)
                       (trans (sym $ other-variant r b′₁)
                              (other-variant r b′₂))                ≡⟨ sym $ trans-assoc _ _ (other-variant r b′₂) ⟩

                 trans (trans (other-variant r b′₁)
                              (sym $ other-variant r b′₁))
                       (other-variant r b′₂)                        ≡⟨ cong (flip trans (other-variant r b′₂)) $
                                                                         trans-symʳ (other-variant r b′₁) ⟩
                 trans refl (other-variant r b′₂)                   ≡⟨ trans-reflˡ _ ⟩∎

                 other-variant r b′₂                                ∎))
           , (λ b′₁ b′₂ b′₃ →
                let lemma =
                      trans (independent-of-B′ r b′₁ b′₂)
                            (independent-of-B′ r b′₂ b′₃)              ≡⟨⟩

                      trans (trans (sym $ other-variant r b′₁)
                                   (other-variant r b′₂))
                            (trans (sym $ other-variant r b′₂)
                                   (other-variant r b′₃))              ≡⟨ sym $ trans-assoc (independent-of-B′ r b′₁ b′₂)
                                                                                            (sym $ other-variant r b′₂)
                                                                                            (other-variant r b′₃) ⟩
                      trans (trans (trans (sym $ other-variant r b′₁)
                                          (other-variant r b′₂))
                                   (sym $ other-variant r b′₂))
                            (other-variant r b′₃)                      ≡⟨ cong (flip trans (other-variant r b′₃)) $
                                                                            trans-[trans]-sym (sym $ other-variant r b′₁)
                                                                                              (other-variant r b′₂) ⟩
                      trans (sym $ other-variant r b′₁)
                            (other-variant r b′₃)                      ≡⟨ refl ⟩∎

                      independent-of-B′ r b′₁ b′₃                      ∎
                in
                trans
                  (Σ-≡,≡→≡ (Σ-≡,≡→≡ (independent-of-B′ r b′₁ b′₂) _) _)
                  (Σ-≡,≡→≡ (Σ-≡,≡→≡ (independent-of-B′ r b′₂ b′₃) _) _)  ≡⟨ trans-Σ-≡,≡→≡ (Σ-≡,≡→≡ (independent-of-B′ r b′₁ b′₂) _)
                                                                                          (Σ-≡,≡→≡ (independent-of-B′ r b′₂ b′₃) _)
                                                                                          _ _ ⟩
                Σ-≡,≡→≡
                  (trans (Σ-≡,≡→≡ (independent-of-B′ r b′₁ b′₂) _)
                         (Σ-≡,≡→≡ (independent-of-B′ r b′₂ b′₃) _))
                  _                                                      ≡⟨ Σ-≡,≡→≡-cong (trans-Σ-≡,≡→≡ (independent-of-B′ r b′₁ b′₂)
                                                                                                        (independent-of-B′ r b′₂ b′₃)
                                                                                                        _ _)
                                                                                         refl ⟩
                Σ-≡,≡→≡
                  (Σ-≡,≡→≡ (trans (independent-of-B′ r b′₁ b′₂)
                                  (independent-of-B′ r b′₂ b′₃))
                           _)
                  _                                                      ≡⟨ Σ-≡,≡→≡-cong
                                                                              (Σ-≡,≡→≡-cong lemma
                                                                                            (mono₁  (+⇒≡ Is-set-is-propositional) _ _))
                                                                              (H-level-H-level-≡ʳ ext univ  (B-set _) _ _) ⟩∎
                Σ-≡,≡→≡ (Σ-≡,≡→≡ (independent-of-B′ r b′₁ b′₃) _) _      ∎))
          (inhabited r)
        where
        Is-set-is-propositional :
          {B : Type b} → Is-proposition (Is-set B)
        Is-set-is-propositional =
          H-level-propositional ext 

    B̲ : R → Type b
    B̲ r = proj₁ (proj₁ (B̲-triple r))

    B̲-set : ∀ r → Is-set (B̲ r)
    B̲-set r = proj₂ (proj₁ (B̲-triple r))

    B′≡B̲ : ∀ r → B′ r ≡ B̲ r
    B′≡B̲ r = proj₂ (B̲-triple r)

  -- Getter.

  get : (a : A) → B a
  get a = to variant≃ (L.get a)

  -- Setter.

  set : (a : A) → B a → A
  set a b = L.set a (from variant≃ b)

  -- Modifier.

  modify : (a : A) → (B a → B a) → A
  modify a f = set a (f (get a))

  -- Setting leaves the remainder unchanged.

  remainder-set : ∀ a b → remainder (set a b) ≡ remainder a
  remainder-set a b = L.remainder-set a (from variant≃ b)

  -- Hence the type of the gettable part stays unchanged after a set.

  codomain-set : ∀ {a b} → B (set a b) ≡ B a
  codomain-set {a} {b} =
    B (set a b)               ≡⟨ sym (variant _) ⟩
    B′ (remainder (set a b))  ≡⟨ cong B′ (remainder-set a b) ⟩
    B′ (remainder a)          ≡⟨ variant _ ⟩∎
    B a                       ∎

  -- A corresponding isomorphism.

  codomain-set-≃ : ∀ {a b} → B (set a b) ≃ B a
  codomain-set-≃ = ≡⇒≃ codomain-set

  -- Unfolding lemmas for codomain-set-≃.

  to-codomain-set-≃ :
    ∀ {a b} →
    to (codomain-set-≃ {a = a} {b = b}) ≡
    to variant≃ ⊚ to L.codomain-set-≃ ⊚ from variant≃
  to-codomain-set-≃ =
    ≡⇒→ (trans (sym (variant _)) (trans eq (variant _)))  ≡⟨ ≡⇒↝-trans equivalence {B≡C = trans eq (variant _)} ⟩
    ≡⇒→ (trans eq (variant _)) ⊚ ≡⇒→ (sym (variant _))    ≡⟨ cong (≡⇒→ (trans eq (variant _)) ⊚_)
                                                                  (≡⇒↝-sym equivalence {eq = variant _}) ⟩
    ≡⇒→ (trans eq (variant _)) ⊚ from variant≃            ≡⟨ cong (_⊚ from variant≃) (≡⇒↝-trans equivalence {B≡C = variant _}) ⟩∎
    to variant≃ ⊚ ≡⇒→ eq ⊚ from variant≃                  ∎
    where
    eq = cong B′ (remainder-set _ _)

  from-codomain-set-≃ :
    ∀ {a b} →
    from (codomain-set-≃ {a = a} {b = b}) ≡
    to variant≃ ⊚ from L.codomain-set-≃ ⊚ from variant≃
  from-codomain-set-≃ =
    ≡⇒← (trans (sym (variant _)) (trans eq (variant _)))        ≡⟨ sym $ ≡⇒↝-sym equivalence {eq = trans (sym (variant _))
                                                                                                         (trans eq (variant _))} ⟩
    ≡⇒→ (sym (trans (sym (variant _)) (trans eq (variant _))))  ≡⟨ cong ≡⇒→
                                                                        (Tactic.prove (Sym (Trans (Sym (Lift (variant _)))
                                                                                                  (Trans (Lift eq) (Lift (variant _)))))
                                                                                      (Trans (Trans (Sym (Lift (variant _)))
                                                                                                    (Sym (Lift eq)))
                                                                                             (Lift (variant _)))
                                                                                      refl) ⟩
    ≡⇒→ (trans (trans (sym (variant _)) (sym eq)) (variant _))  ≡⟨ ≡⇒↝-trans equivalence {B≡C = variant _} ⟩
    to variant≃ ⊚ ≡⇒→ (trans (sym (variant _)) (sym eq))        ≡⟨ cong (to variant≃ ⊚_) (≡⇒↝-trans equivalence {B≡C = sym eq}) ⟩
    to variant≃ ⊚ ≡⇒→ (sym eq) ⊚ ≡⇒→ (sym (variant _))          ≡⟨ cong₂ (λ f g → to variant≃ ⊚ f ⊚ g)
                                                                         (≡⇒↝-sym equivalence {eq = eq})
                                                                         (≡⇒↝-sym equivalence {eq = variant _}) ⟩∎
    to variant≃ ⊚ ≡⇒← eq ⊚ from variant≃                        ∎
    where
    eq = cong B′ (remainder-set _ _)

  -- Some lens laws.

  set-get : ∀ a → set a (get a) ≡ a
  set-get a =
    L.set a (from variant≃ (to variant≃ (L.get a)))  ≡⟨ cong (L.set a) (left-inverse-of variant≃ _) ⟩
    L.set a (L.get a)                                ≡⟨ L.set-get a ⟩∎
    a                                                ∎

  get-set : ∀ a b → get (set a b) ≡ from codomain-set-≃ b
  get-set a b =
    to variant≃ (L.get (L.set a (from variant≃ b)))  ≡⟨ cong (to variant≃) $ L.get-set₂ _ _ ⟩
    to variant≃ (≡⇒← eq (from variant≃ b))           ≡⟨ cong (_$ b) (sym from-codomain-set-≃) ⟩∎
    from codomain-set-≃ b                            ∎
    where
    eq = cong B′ (remainder-set a b)

  set-set : ∀ a b₁ b₂ → set (set a b₁) b₂ ≡ set a (to codomain-set-≃ b₂)
  set-set a b₁ b₂ =
    L.set (L.set a (from variant≃ b₁)) (from variant≃ b₂)  ≡⟨ L.set-set₂ a (from variant≃ b₁) (from variant≃ b₂) ⟩
    L.set a (to L.codomain-set-≃ (from variant≃ b₂))       ≡⟨ cong (L.set a) lemma ⟩∎
    L.set a (from variant≃ (to codomain-set-≃ b₂))         ∎
    where
    lemma =
      to L.codomain-set-≃ (from variant≃ b₂)                    ≡⟨ sym $ left-inverse-of variant≃ _ ⟩

      from variant≃
        (to variant≃ (to L.codomain-set-≃ (from variant≃ b₂)))  ≡⟨ cong (from variant≃ ⊚ (_$ b₂)) $ sym to-codomain-set-≃ ⟩∎

      from variant≃ (to codomain-set-≃ b₂)                      ∎

-- For a non-dependent dependent lens, for which UIP holds for the
-- codomain's universe, codomain-set-≃ is equal to the identity.

codomain-set-≃≡id :
  {B : Type b} →
  Is-set (Type b) →
  (l : Lens A (λ _ → B)) →
  ∀ {a b} → Lens.codomain-set-≃ l {a = a} {b = b} ≡ Eq.id
codomain-set-≃≡id uip l =
  codomain-set-≃    ≡⟨⟩
  ≡⇒≃ codomain-set  ≡⟨ cong ≡⇒≃ (uip codomain-set refl) ⟩
  ≡⇒≃ refl          ≡⟨ refl ⟩∎
  Eq.id             ∎
  where
  open Lens l

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

-- Lens preserves level-preserving equivalences (assuming univalence).

Lens-cong :
  {A₁ A₂ : Type a} {B₁ : A₁ → Type b} {B₂ : A₂ → Type b} →
  Univalence b →
  (A₁≃A₂ : A₁ ≃ A₂) →
  (∀ a → B₁ a ≃ B₂ (_≃_.to A₁≃A₂ a)) →
  Lens A₁ B₁ ≃ Lens A₂ B₂
Lens-cong {A₁ = A₁} {A₂} {B₁} {B₂} univ A₁≃A₂ B₁≃B₂ =
  (∃ λ (R : Type _) →
   ∃ λ (B′ : R → Type _) →
   ∃ λ (lens : Lens₃ A₁ R B′) →
   ((r : R) → ∥ B′ r ∥)
     ×
   (∀ a → B′ (remainder lens a) ≡ B₁ a))              ↝⟨ (∃-cong λ R → ∃-cong λ B′ →
                                                          Σ-cong (Eq.≃-preserves ext A₁≃A₂ F.id) λ lens →
                                                          ∃-cong λ _ →
                                                          Π-cong ext A₁≃A₂ λ a →
                                                          ≡-preserves-≃ ext univ univ
                                                            (≡⇒≃ (
      B′ (proj₁ (to lens a))                                      ≡⟨ cong (λ a → B′ (proj₁ (to lens a))) $ sym $ left-inverse-of A₁≃A₂ _ ⟩∎
      B′ (proj₁ (to lens (from A₁≃A₂ (to A₁≃A₂ a))))              ∎))
                                                            (B₁≃B₂ a)) ⟩□
  (∃ λ (R : Type _) →
   ∃ λ (B′ : R → Type _) →
   ∃ λ (lens : Lens₃ A₂ R B′) →
   ((r : R) → ∥ B′ r ∥)
     ×
   (∀ a → B′ (remainder lens a) ≡ B₂ a))              □
  where
  open Lens₃
  open _≃_

-- If B x is a proposition for all x, then Lens A B is isomorphic to
-- (x : A) → B x (assuming univalence).

lens-to-proposition↔get :
  {A : Type a} {B : A → Type b} →
  Univalence (a ⊔ b) →
  Univalence b →
  (∀ x → Is-proposition (B x)) →
  Lens A B ↔ ((x : A) → B x)
lens-to-proposition↔get {b = b} {A = A} {B = B} univ₁ univ₂ B-prop =
  (∃ λ (R : Type _) →
   ∃ λ (B′ : R → Type _) →
   ∃ λ (lens : A ≃ Σ R B′) →
   ((r : R) → ∥ B′ r ∥)
     ×
   (∀ a → B′ (Lens₃.remainder lens a) ≡ B a))                ↝⟨ (∃-cong λ _ → ∃-cong λ B′ → ∃-cong λ l → ∃-cong λ _ →
                                                                 Π-cong ext l λ _ →
                                                                 ≡⇒↝ _ $ cong (λ x → B′ _ ≡ B x) $ sym $ _≃_.left-inverse-of l _) ⟩
  (∃ λ (R : Type _) →
   ∃ λ (B′ : R → Type _) →
   ∃ λ (lens : A ≃ Σ R B′) →
   ((r : R) → ∥ B′ r ∥)
     ×
   (∀ p → B′ (proj₁ p) ≡ B (_≃_.from lens p)))               ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → currying) ⟩

  (∃ λ (R : Type _) →
   ∃ λ (B′ : R → Type _) →
   ∃ λ (lens : A ≃ Σ R B′) →
   ((r : R) → ∥ B′ r ∥)
     ×
   ((r : R) (b : B′ r) → B′ r ≡ B (_≃_.from lens (r , b))))  ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → inverse ΠΣ-comm) ⟩

  (∃ λ (R : Type _) →
   ∃ λ (B′ : R → Type _) →
   ∃ λ (lens : A ≃ Σ R B′) →
   ((r : R) →
      ∥ B′ r ∥
        ×
      ((b : B′ r) → B′ r ≡ B (_≃_.from lens (r , b)))))      ↔⟨ (∃-cong λ _ → ∃-cong λ B′ → ∃-cong λ lens → ∀-cong ext $
                                                                 lemma₁ B′ lens) ⟩
  (∃ λ (R : Type _) →
   ∃ λ (B′ : R → Type _) →
   ∃ λ (lens : A ≃ Σ R B′) →
   ((r : R) → ∃ λ (⊤≃B′ : ⊤ ≃ B′ r) →
                B (_≃_.from lens (r , _≃_.to ⊤≃B′ _))))      ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ΠΣ-comm) ⟩

  (∃ λ (R : Type _) →
   ∃ λ (B′ : R → Type _) →
   ∃ λ (lens : A ≃ Σ R B′) →
   ∃ λ (⊤≃B′ : ∀ r → ⊤ ≃ B′ r) →
   ∀ r → B (_≃_.from lens (r , _≃_.to (⊤≃B′ r) _)))          ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-comm) ⟩

  (∃ λ (R : Type _) →
   ∃ λ (B′ : R → Type _) →
   ∃ λ (⊤≃B′ : ∀ r → ⊤ ≃ B′ r) →
   ∃ λ (lens : A ≃ Σ R B′) →
   ∀ r → B (_≃_.from lens (r , _≃_.to (⊤≃B′ r) _)))          ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ ⊤≃B′ →
                                                                 Σ-cong (Eq.≃-preserves ext F.id
                                                                           (drop-⊤-right (λ r → inverse (⊤≃B′ r)))) λ _ →
                                                                 F.id) ⟩
  (∃ λ (R : Type _) →
   ∃ λ (B′ : R → Type _) →
   (∀ r → ⊤ ≃ B′ r)
     ×
   ∃ λ (lens : A ≃ R) →
   ∀ r → B (_≃_.from lens r))                                ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-comm) ⟩

  (∃ λ (R : Type _) →
   ∃ λ (B′ : R → Type _) →
   ∃ λ (lens : A ≃ R) →
   (∀ r → ⊤ ≃ B′ r)
     ×
   ∀ r → B (_≃_.from lens r))                                ↝⟨ (∃-cong λ _ → ∃-comm) ⟩

  (∃ λ (R : Type _) →
   ∃ λ (lens : A ≃ R) →
   ∃ λ (B′ : R → Type _) →
   (∀ r → ⊤ ≃ B′ r)
     ×
   ∀ r → B (_≃_.from lens r))                                ↝⟨ Σ-assoc ⟩

  (Σ (∃ λ (R : Type _) → A ≃ R) λ { (R , lens) →
   ∃ λ (B′ : R → Type _) →
   (∀ r → ⊤ ≃ B′ r)
     ×
   ∀ r → B (_≃_.from lens r) })                              ↝⟨ drop-⊤-left-Σ (other-singleton-with-≃-↔-⊤ {b = b} ext univ₁) ⟩

  (∃ λ (B′ : ↑ _ A → Type _) →
   (∀ a → ⊤ ≃ B′ a)
     ×
   (∀ a → B (lower a)))                                      ↝⟨ Σ-assoc ⟩

  (∃ λ (B′ : ↑ _ A → Type _) → ∀ a → ⊤ ≃ B′ a)
    ×
  (∀ a → B (lower a))                                        ↔⟨ ((∃-cong λ _ → ∀-cong ext λ _ →
                                                                  Eq.≃-preserves ext (inverse $ Eq.↔⇒≃ Bij.↑↔) F.id)
                                                                   ×-cong
                                                                 Π-cong ext (Eq.↔⇒≃ Bij.↑↔) (λ _ → F.id)) ⟩
  (∃ λ (B′ : ↑ _ A → Type _) → ∀ a → ↑ _ ⊤ ≃ B′ a)
    ×
  (∀ a → B a)                                                ↔⟨ (∃-cong λ B′ → ∀-cong ext λ _ →
                                                                 inverse $ ≡≃≃ univ₂)
                                                                  ×-cong
                                                                F.id ⟩
  (∃ λ (B′ : ↑ _ A → Type _) → ∀ a → ↑ _ ⊤ ≡ B′ a)
    ×
  (∀ a → B a)                                                ↔⟨ (∃-cong λ _ →
                                                                 Eq.extensionality-isomorphism ext)
                                                                  ×-cong
                                                                F.id ⟩
  (∃ λ (B′ : ↑ _ A → Type _) → const (↑ _ ⊤) ≡ B′)
    ×
  (∀ a → B a)                                                ↝⟨ drop-⊤-left-× (λ _ →
                                                                _⇔_.to contractible⇔↔⊤ (other-singleton-contractible _)) ⟩□
  (∀ a → B a)                                                □
  where
  lemma₂ : {R : Type _} (B′ : R → Type _) (r : R) → _
  lemma₂ B′ r =
    (∥ B′ r ∥ × Is-proposition (B′ r))  ↝⟨ ×-comm ⟩

    (Is-proposition (B′ r) × ∥ B′ r ∥)  ↝⟨ (∃-cong λ B′-prop → ∥∥↔ B′-prop) ⟩

    (Is-proposition (B′ r) × B′ r)      ↔⟨ _↠_.from (Eq.≃↠⇔ (Σ-closure  (H-level-propositional ext ) λ B′-prop →
                                                             B′-prop)
                                                            (H-level-propositional ext ))
                                                    (record { to   = uncurry propositional⇒inhabited⇒contractible
                                                            ; from = λ B′-contr → mono₁  B′-contr , proj₁ B′-contr
                                                            }) ⟩
    Contractible (B′ r)                 ↝⟨ contractible↔≃⊤ ext ⟩

    B′ r ≃ ⊤                            ↝⟨ Eq.inverse-isomorphism ext ⟩□

    ⊤ ≃ B′ r                            □

  lemma₁ :
    {R : Type _}
    (B′ : R → Type _) (lens : A ≃ Σ R B′) (r : R) → _
  lemma₁ B′ lens r =
    ∥ B′ r ∥
      ×
    ((b′ : B′ r) → B′ r ≡ B (_≃_.from lens (r , b′)))  ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ →
                                                           ≡≃≃ univ₂) ⟩
    ∥ B′ r ∥
      ×
    ((b′ : B′ r) → B′ r ≃ B (_≃_.from lens (r , b′)))  ↝⟨ (∃-cong λ _ → ∀-cong ext λ b′ →
                                                           _↠_.from (Eq.≃↠⇔ (Eq.right-closure ext  (B-prop _))
                                                                            (×-closure 
                                                                                       (H-level-propositional ext )
                                                                                       (B-prop _)))
                                                                    (record
                                                                       { to   = λ eq →   H-level.respects-surjection
                                                                                           (_≃_.surjection (inverse eq))
                                                                                           
                                                                                           (B-prop _)
                                                                                       , _≃_.to eq b′
                                                                       ; from = λ { (B′-prop , b) → _↠_.from (Eq.≃↠⇔ B′-prop (B-prop _))
                                                                                                             (record { to   = const b
                                                                                                                     ; from = const b′
                                                                                                                     }) }
                                                                       })) ⟩
    ∥ B′ r ∥
      ×
    ((b′ : B′ r) → Is-proposition (B′ r)
                     ×
                   B (_≃_.from lens (r , b′)))         ↔⟨ (∃-cong λ _ → ΠΣ-comm) ⟩

    ∥ B′ r ∥
      ×
    (B′ r → Is-proposition (B′ r))
      ×
    ((b′ : B′ r) → B (_≃_.from lens (r , b′)))         ↝⟨ (∃-cong λ _ →
                                                           _↠_.from (Eq.≃↠⇔ (Π-closure ext  λ _ →
                                                                             H-level-propositional ext )
                                                                            (H-level-propositional ext ))
                                                                    (record { to   = λ B′-prop → [inhabited⇒+]⇒+  B′-prop
                                                                            ; from = λ B′-prop _ → B′-prop
                                                                            })
                                                             ×-cong
                                                           F.id) ⟩
    ∥ B′ r ∥
      ×
    Is-proposition (B′ r)
      ×
    ((b′ : B′ r) → B (_≃_.from lens (r , b′)))         ↔⟨ ×-assoc ⟩

    (∥ B′ r ∥
      ×
     Is-proposition (B′ r))
      ×
    ((b′ : B′ r) → B (_≃_.from lens (r , b′)))         ↔⟨ lemma₂ B′ r ×-cong F.id ⟩

    (⊤ ≃ B′ r)
      ×
    ((b′ : B′ r) → B (_≃_.from lens (r , b′)))         ↝⟨ (∃-cong λ ⊤≃B′ → drop-⊤-left-Π ext (_≃_.bijection $ inverse ⊤≃B′)) ⟩□

    (∃ λ (⊤≃B′ : ⊤ ≃ B′ r) →
     B (_≃_.from lens (r , _≃_.to ⊤≃B′ _)))            □

-- If B x is contractible for all x, then Lens A B is isomorphic to ⊤
-- (assuming univalence).

lens-to-contractible↔⊤ :
  {A : Type a} {B : A → Type b} →
  Univalence (a ⊔ b) →
  Univalence b →
  (∀ x → Contractible (B x)) →
  Lens A B ↔ ⊤
lens-to-contractible↔⊤ {A = A} {B} univ₁ univ₂ cB =
  Lens A B         ↝⟨ lens-to-proposition↔get univ₁ univ₂ (mono₁  ⊚ cB) ⟩
  ((x : A) → B x)  ↝⟨ (∀-cong ext λ _ →
                       _⇔_.to contractible⇔↔⊤ (cB _)) ⟩
  (A → ⊤)          ↝⟨ →-right-zero ⟩□
  ⊤                □

-- Lens A (const ⊥) is isomorphic to ¬ A (assuming univalence).

lens-to-⊥↔¬ :
  {A : Type a} →
  Univalence (a ⊔ b) →
  Univalence b →
  Lens A (const (⊥ {ℓ = b})) ↔ ¬ A
lens-to-⊥↔¬ {A = A} univ₁ univ₂ =
  Lens A (const ⊥)  ↝⟨ lens-to-proposition↔get univ₁ univ₂ (λ _ → ⊥-propositional) ⟩
  (A → ⊥)           ↝⟨ inverse $ ¬↔→⊥ ext ⟩□
  ¬ A               □

------------------------------------------------------------------------
-- Results relating different kinds of lenses

-- If we assume that equality with the codomain type is propositional,
-- then non-dependent dependent lenses are isomorphic to non-dependent
-- lenses.
--
-- TODO: Can this be proved without assuming that equality with the
-- codomain type is propositional? If not, can the definition of Lens
-- be changed so that it can be proved?

non-dependent-lenses-isomorphic :
  {B : Type b} →
  (∀ {B′} → Is-proposition (B′ ≡ B)) →
  ∃ λ (iso : Lens A (const B) ↔ ND.Lens A B) →
    ∀ {l a} → Lens.get l a ≡ ND.Lens.get (_↔_.to iso l) a
non-dependent-lenses-isomorphic {A = A} {B = B} ≡B-prop =
  (Lens A (const B)  ↝⟨ inverse (from-equivalence ND.Lens-as-Σ) F.∘ ∃-cong lemma ⟩□
   ND.Lens A B       □)
  , λ {l a} →
    let p = variant l a
        q = Trunc.rec
              ≡B-prop
              (λ b → subst (λ { (r , _) → B′ l r ≡ B })
                           (_≃_.right-inverse-of (lens l)
                              (remainder l a , b))
                           (variant l (Lens₃.set (lens l) a b)))
              (inhabited l (remainder l a))
    in
    ≡⇒→ p (proj₂ (_≃_.to (lens l) a))  ≡⟨ cong (λ eq → ≡⇒→ eq (proj₂ (_≃_.to (lens l) a)))
                                               (≡B-prop p q) ⟩∎
    ≡⇒→ q (proj₂ (_≃_.to (lens l) a))  ∎
  where
  open Lens

  lemma = λ R →
    (∃ λ (B′ : R → Type _) →
     ∃ λ (lens : A ≃ Σ R B′) →
     ((r : R) → ∥ B′ r ∥)
       ×
     (∀ a → B′ (Lens₃.remainder lens a) ≡ B))     ↝⟨ (∃-cong λ _ → ∃-cong λ l → ∃-cong λ _ →
                                                      Π-cong ext l (λ _ → F.id)) ⟩
    (∃ λ (B′ : R → Type _) →
     (A ≃ Σ R B′)
       ×
     ((r : R) → ∥ B′ r ∥)
       ×
     (∀ p → B′ (proj₁ p) ≡ B))                    ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → currying) ⟩

    (∃ λ (B′ : R → Type _) →
     (A ≃ Σ R B′)
       ×
     ((r : R) → ∥ B′ r ∥)
       ×
     ((r : R) → B′ r → B′ r ≡ B))                 ↔⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ inh →
                                                      ∀-cong ext λ r →
                                                      _↠_.from (Eq.≃↠⇔ (Π-closure ext  λ _ →
                                                                        ≡B-prop)
                                                                       ≡B-prop)
                                                        (record { from = λ B′r≡B     → const B′r≡B
                                                                ; to   = λ B′r→B′r≡B → Trunc.rec ≡B-prop B′r→B′r≡B (inh r)
                                                                })) ⟩
    (∃ λ (B′ : R → Type _) →
     (A ≃ Σ R B′)
       ×
     ((r : R) → ∥ B′ r ∥)
       ×
     ((r : R) → B′ r ≡ B))                        ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ×-comm) ⟩

    (∃ λ (B′ : R → Type _) →
     (A ≃ Σ R B′)
       ×
     ((r : R) → B′ r ≡ B)
       ×
     ((r : R) → ∥ B′ r ∥))                        ↝⟨ (∃-cong λ _ → ∃-comm) ⟩

    (∃ λ (B′ : R → Type _) →
     ((r : R) → B′ r ≡ B)
       ×
     (A ≃ Σ R B′)
       ×
     ((r : R) → ∥ B′ r ∥))                        ↔⟨ (∃-cong λ _ →
                                                      Σ-cong (Eq.extensionality-isomorphism ext) λ B′≡B →
                                                      Eq.≃-preserves ext F.id (∃-cong λ _ → ≡⇒↝ _ (B′≡B _))
                                                        ×-cong
                                                      ∀-cong ext (λ _ → Eq.↔⇒≃ $ ∥∥-cong (≡⇒↝ _ (B′≡B _)))) ⟩
    (∃ λ (B′ : R → Type _) →
     B′ ≡ const B
       ×
     (A ≃ (R × B))
       ×
     (R → ∥ B ∥))                                 ↝⟨ Σ-assoc ⟩

    ((∃ λ (B′ : R → Type _) → B′ ≡ const B)
       ×
     (A ≃ (R × B))
       ×
     (R → ∥ B ∥))                                 ↝⟨ drop-⊤-left-× (λ _ →
                                                     _⇔_.to contractible⇔↔⊤ (singleton-contractible _)) ⟩□
    ((A ≃ (R × B))
       ×
     (R → ∥ B ∥))                                 □

-- The type of non-dependent dependent lenses from A to B is
-- isomorphic to the type of non-dependent lenses from A to B if UIP
-- holds for B.

non-dependent-lenses-isomorphic-UIP :
  {B : Type b} →
  Is-set (Type b) →
  ∃ λ (iso : Lens A (const B) ↔ ND.Lens A B) →
    ∀ {l a} → Lens.get l a ≡ ND.Lens.get (_↔_.to iso l) a
non-dependent-lenses-isomorphic-UIP uip =
  non-dependent-lenses-isomorphic uip

-- Lens and Lens′ are pointwise isomorphic.

Lens↔Lens′ : {A : Type a} {B : A → Type b} →
             Lens A B ↔ Lens′ A B
Lens↔Lens′ {a = a} {b = b} {A = A} {B = B} =
  (∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (B′ : R → Type b) →
   ∃ λ (lens : Lens₃ A R B′) →
   ((r : R) → ∥ B′ r ∥)
     ×
   (∀ a → B′ (Lens₃.remainder lens a) ≡ B a))                           ↝⟨ (∃-cong λ _ → ∃-cong λ _ →
                                                                            Σ-cong (Eq.≃-as-Σ) λ _ → F.id) ⟩
  (∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (B′ : R → Type b) →
   ∃ λ (lens : ∃ λ (rg : A → Σ R B′) → Eq.Is-equivalence rg) →
   ((r : R) → ∥ B′ r ∥)
     ×
   (∀ a → B′ (proj₁ (proj₁ lens a)) ≡ B a))                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ →
                                                                            inverse Σ-assoc) ⟩
  (∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (B′ : R → Type b) →
   ∃ λ (rg : A → Σ R B′) →
   Eq.Is-equivalence rg
     ×
   ((r : R) → ∥ B′ r ∥)
     ×
   (∀ a → B′ (proj₁ (rg a)) ≡ B a))                                     ↝⟨ (∃-cong λ _ → ∃-cong λ _ →
                                                                            Σ-cong ΠΣ-comm λ _ → F.id) ⟩
  (∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (B′ : R → Type b) →
   ∃ λ (rg : ∃ λ (remainder : A → R) →
             (a : A) → B′ (remainder a)) →
   Eq.Is-equivalence {B = ∃ B′} (λ a → proj₁ rg a , proj₂ rg a)
     ×
   ((r : R) → ∥ B′ r ∥)
     ×
   (∀ a → B′ (proj₁ rg a) ≡ B a))                                       ↝⟨ (∃-cong λ _ → ∃-cong λ _ →
                                                                            inverse Σ-assoc) ⟩
  (∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (B′ : R → Type b) →
   ∃ λ (remainder : A → R) →
   ∃ λ (get′ : (a : A) → B′ (remainder a)) →
   Eq.Is-equivalence {B = ∃ B′} (λ a → remainder a , get′ a)
     ×
   ((r : R) → ∥ B′ r ∥)
     ×
   (∀ a → B′ (remainder a) ≡ B a))                                      ↝⟨ (∃-cong λ R → ∃-cong λ B′ → ∃-cong λ rem → ∃-cong λ get′ → ∃-cong λ eq →
                                                                            ∀-cong ext (λ r → ∥∥-cong (lemma R B′ rem get′ eq r))
                                                                              ×-cong
                                                                            F.id) ⟩
  (∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (B′ : R → Type b) →
   ∃ λ (remainder : A → R) →
   ∃ λ (get′ : (a : A) → B′ (remainder a)) →
   Eq.Is-equivalence {B = ∃ B′} (λ a → remainder a , get′ a)
     ×
   Surjective remainder
     ×
   (∀ a → B′ (remainder a) ≡ B a))                                      ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                            ×-comm) ⟩
  (∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (B′ : R → Type b) →
   ∃ λ (remainder : A → R) →
   ∃ λ (get′ : (a : A) → B′ (remainder a)) →
   Eq.Is-equivalence {B = ∃ B′} (λ a → remainder a , get′ a)
     ×
   (∀ a → B′ (remainder a) ≡ B a)
     ×
   Surjective remainder)                                                ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                            ∃-comm) ⟩
  (∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (B′ : R → Type b) →
   ∃ λ (remainder : A → R) →
   ∃ λ (get′ : (a : A) → B′ (remainder a)) →
   (∀ a → B′ (remainder a) ≡ B a)
     ×
   Eq.Is-equivalence {B = ∃ B′} (λ a → remainder a , get′ a)
     ×
   Surjective remainder)                                                ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                            ∃-comm) ⟩
  (∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (B′ : R → Type b) →
   ∃ λ (remainder : A → R) →
   (∀ a → B′ (remainder a) ≡ B a)
     ×
   ∃ λ (get′ : (a : A) → B′ (remainder a)) →
   Eq.Is-equivalence {B = ∃ B′} (λ a → remainder a , get′ a)
     ×
   Surjective remainder)                                                ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ×-cong₁ λ _ →
                                                                            ∀-cong ext λ _ →
                                                                            Groupoid.⁻¹-bijection (EG.groupoid _)) ⟩
  (∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (B′ : R → Type b) →
   ∃ λ (remainder : A → R) →
   (∀ a → B a ≡ B′ (remainder a))
     ×
   ∃ λ (get′ : (a : A) → B′ (remainder a)) →
   Eq.Is-equivalence {B = ∃ B′} (λ a → remainder a , get′ a)
     ×
   Surjective remainder)                                                ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ×-cong₁ λ _ →
                                                                            inverse Bij.implicit-Π↔Π) ⟩
  (∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (B′ : R → Type b) →
   ∃ λ (remainder : A → R) →
   (∀ {a} → B a ≡ B′ (remainder a))
     ×
   ∃ λ (get′ : (a : A) → B′ (remainder a)) →
   Eq.Is-equivalence {B = ∃ B′} (λ a → remainder a , get′ a)
     ×
   Surjective remainder)                                                ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ variant → inverse $
                                                                            Σ-cong (∀-cong ext λ _ →
                                                                                    Eq.subst-as-equivalence P.id (variant {_})) λ _ →
                                                                            F.id) ⟩
  (∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (B′ : R → Type b) →
   ∃ λ (remainder : A → R) →
   ∃ λ (variant : ∀ {a} → B a ≡ B′ (remainder a)) →
   ∃ λ (get : (a : A) → B a) →
   Eq.Is-equivalence {B = ∃ B′}
                     (λ a → remainder a , subst P.id variant (get a))
     ×
   Surjective remainder)                                                ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                            ∃-comm) ⟩
  (∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (B′ : R → Type b) →
   ∃ λ (remainder : A → R) →
   ∃ λ (get : (a : A) → B a) →
   ∃ λ (variant : ∀ {a} → B a ≡ B′ (remainder a)) →
   Eq.Is-equivalence {B = ∃ B′}
                     (λ a → remainder a , subst P.id variant (get a))
     ×
   Surjective remainder)                                                ↝⟨ (∃-cong λ _ → ∃-cong λ _ →
                                                                            ∃-comm) ⟩
  (∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (B′ : R → Type b) →
   ∃ λ (get : (a : A) → B a) →
   ∃ λ (remainder : A → R) →
   ∃ λ (variant : ∀ {a} → B a ≡ B′ (remainder a)) →
   Eq.Is-equivalence {B = ∃ B′}
                     (λ a → remainder a , subst P.id variant (get a))
     ×
   Surjective remainder)                                                ↝⟨ (∃-cong λ _ →
                                                                            ∃-comm) ⟩
  (∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (get : (a : A) → B a) →
   ∃ λ (B′ : R → Type b) →
   ∃ λ (remainder : A → R) →
   ∃ λ (variant : ∀ {a} → B a ≡ B′ (remainder a)) →
   Eq.Is-equivalence {B = ∃ B′}
                     (λ a → remainder a , subst P.id variant (get a))
     ×
   Surjective remainder)                                                ↝⟨ ∃-comm ⟩

  (∃ λ (get : (a : A) → B a) →
   ∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (B′ : R → Type b) →
   ∃ λ (remainder : A → R) →
   ∃ λ (variant : ∀ {a} → B a ≡ B′ (remainder a)) →
   Eq.Is-equivalence {B = ∃ B′}
                     (λ a → remainder a , subst P.id variant (get a))
     ×
   Surjective remainder)                                                ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                            ×-comm) ⟩
  (∃ λ (get : (a : A) → B a) →
   ∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (B′ : R → Type b) →
   ∃ λ (remainder : A → R) →
   ∃ λ (variant : ∀ {a} → B a ≡ B′ (remainder a)) →
   Surjective remainder
     ×
   Eq.Is-equivalence {B = ∃ B′}
                     (λ a → remainder a , subst P.id variant (get a)))  ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                            ∃-comm) ⟩
  (∃ λ (get : (a : A) → B a) →
   ∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (B′ : R → Type b) →
   ∃ λ (remainder : A → R) →
   Surjective remainder
     ×
   ∃ λ (variant : ∀ {a} → B a ≡ B′ (remainder a)) →
   Eq.Is-equivalence {B = ∃ B′}
                     (λ a → remainder a , subst P.id variant (get a)))  ↝⟨ (∃-cong λ _ → ∃-cong λ _ →
                                                                            ∃-comm) ⟩
  (∃ λ (get : (a : A) → B a) →
   ∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (remainder : A → R) →
   ∃ λ (B′ : R → Type b) →
   Surjective remainder
     ×
   ∃ λ (variant : ∀ {a} → B a ≡ B′ (remainder a)) →
   Eq.Is-equivalence {B = ∃ B′}
                     (λ a → remainder a , subst P.id variant (get a)))  ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                            ∃-comm) ⟩□
  (∃ λ (get : (a : A) → B a) →
   ∃ λ (R : Type (a ⊔ b)) →
   ∃ λ (remainder : A → R) →
   Surjective remainder
     ×
   ∃ λ (B′ : R → Type b) →
   ∃ λ (variant : ∀ {a} → B a ≡ B′ (remainder a)) →
   Eq.Is-equivalence {B = ∃ B′}
                     (λ a → remainder a , subst P.id variant (get a)))  □
  where
  lemma : ∀ _ _ _ _ _ _ → _
  lemma = λ _ B′ remainder _ eq r →
    B′ r                            ↝⟨ (inverse $ drop-⊤-right λ _ →
                                        _⇔_.to contractible⇔↔⊤ $
                                        singleton-contractible _) ⟩
    B′ r × Singleton r              ↝⟨ ∃-comm ⟩
    (∃ λ r′ → B′ r × r′ ≡ r)        ↝⟨ ∃-cong (λ _ → ×-cong₁ λ r′≡r → ≡⇒↝ _ (cong B′ (sym r′≡r))) ⟩
    (∃ λ r′ → B′ r′ × r′ ≡ r)       ↝⟨ Σ-assoc ⟩
    (∃ λ (p : ∃ B′) → proj₁ p ≡ r)  ↝⟨ inverse $ Σ-cong Eq.⟨ _ , eq ⟩ (λ _ → F.id) ⟩□
    (∃ λ a → remainder a ≡ r)       □

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

-- Conversion from Lens₃ to Lens.

Lens₃-to-Lens :
  {A : Type a} {R : Type (a ⊔ b)} {B : R → Type b} →
  (l : Lens₃ A R B) →
  Lens A (B ⊚ Lens₃.remainder l)
Lens₃-to-Lens {A = A} {R} {B} l =
  _ ,
  _ ,
  (A                                              ↝⟨ l ⟩
   Σ R B                                          ↔⟨ ∃-cong (λ _ → inverse ∥∥×↔) ⟩
   Σ R (λ r → ∥ B r ∥ × B r)                      ↔⟨ Σ-assoc ⟩□
   Σ (Σ R (λ r → ∥ B r ∥)) (λ { (r , _) → B r })  □) ,
  proj₂ ,
  λ _ → refl

-- A variant of Lens₃-to-Lens.

Lens₃-to-Lens′ :
  {A : Type (a ⊔ r)} {R : Type r} {B : R → Type b} →
  (l : Lens₃ A R B) →
  Lens A (B ⊚ Lens₃.remainder l)
Lens₃-to-Lens′ {a = a} {b = b} {A = A} {R = R} {B = B} l =
  Lens₃-to-Lens
    (A                                       ↝⟨ l ⟩
     Σ R B                                   ↝⟨ Σ-cong (inverse Bij.↑↔) (λ _ → F.id) ⟩□
     Σ (↑ (a ⊔ b) R) (λ { (lift r) → B r })  □)

-- Identity lens.

id : Lens A (λ _ → A)
id {A = A} = Lens₃-to-Lens′
  (A      ↔⟨ inverse ×-left-identity ⟩□
   ⊤ × A  □)

-- Composition of lenses.
--
-- Note that this function combines a family of Lenses and a Lens₃.

infixr  _∘₃_

_∘₃_ :
  {A : Type (a ⊔ b ⊔ c)} {R : Type (a ⊔ b ⊔ c)}
  {B : R → Type (b ⊔ c)} {C : {r : R} → B r → Type c} →
  (∀ {r} → Lens (B r) C) → (l₂ : Lens₃ A R B) →
  Lens A (C ⊚ Lens₃.get l₂)
_∘₃_ {R = R} l₁ l₂ =
  (∃ λ (r : R) → Lens.R (l₁ {r = r})) ,
  (λ { (r₁ , r₂) → Lens.B′ (l₁ {r = r₁}) r₂ }) ,
  Lens.lens l₁ ₃∘₃ l₂ ,
  Lens.inhabited l₁ ⊚ proj₂ ,
  Lens.variant l₁ ⊚ Lens₃.get l₂

-- /Forward/ composition of lenses.
--
-- This function combines /Lens/es, but has a type which is arguably
-- more complicated. The type is also somewhat restricted: C is only
-- indexed by As, not Bs.

infixr  _⨾_

_⨾_ : {A : Type (a ⊔ b ⊔ c)} {B : A → Type (b ⊔ c)} {C : A → Type c} →
      (l₁ : Lens A B) →
      let open Lens l₁; open _≃_ lens in
      (∀ {r} → Lens (B′ r) (λ b′ → C (from (r , b′)))) →
      Lens A C
_⨾_ {C = C} l₁ l₂ =
  (∃ λ (r₁ : R l₁) → Lens.R (l₂ {r = r₁})) ,
  (λ { (r₁ , r₂) → B′ (l₂ {r = r₁}) r₂ }) ,
  lens l₂ ₃∘₃ lens l₁ ,
  (λ { (_ , r₂) → inhabited l₂ r₂ }) ,
  λ a →
    B′ l₂ (remainder l₂ (Lens₃.get (lens l₁) a))  ≡⟨ variant l₂ _ ⟩
    C (from (lens l₁) (to (lens l₁) a))           ≡⟨ cong C (left-inverse-of (lens l₁) a) ⟩∎
    C a                                           ∎
  where
  open _≃_
  open Lens

-- Can the composition operation be generalised?

-- The argument below does not depend on the details of the
-- implementation of Lens.

module No-fully-general-composition-operator
  (Lens′ : (A : Type) → (A → Type) → Type₁)
  (get′  : ∀ {A B} → Lens′ A B → (a : A) → B a)
  where

  -- The following type signature—and partial specification—might seem
  -- like a reasonable goal (if we restrict attention to Type₀).

  Type-of-composition : Type₁
  Type-of-composition =
    {A : Type} {B : A → Type} {C : (a : A) → B a → Type}
    (l₁ : Lens′ A B)
    (l₂ : ∀ a → Lens′ (B a) (C a)) →
    ∃ λ (l₃ : Lens′ A (λ a → C a (get′ l₁ a))) →
      ∀ a → get′ l₃ a ≡ get′ (l₂ a) (get′ l₁ a)

  -- However, this specification is unsatisfiable in the non-dependent
  -- case (for ND.Lens).

  no-corresponding-non-dependent-composition-operator :
    let open ND.Lens in
    ¬ ({A B C : Type}
       (l₁ : ND.Lens A B)
       (l₂ : A → ND.Lens B C) →
       ∃ λ (l₃ : ND.Lens A C) →
         ∀ a → get l₃ a ≡ get (l₂ a) (get l₁ a))
  no-corresponding-non-dependent-composition-operator comp =
    contradiction
    where
    open ND.Lens
    open _≃_

    idL : ND.Lens Bool Bool
    idL = NDC.id

    swapL : ND.Lens Bool Bool
    swapL = ND.isomorphism-to-lens
      (Bool      ↔⟨ swap ⟩
       Bool      ↔⟨ inverse ×-left-identity ⟩□
       ⊤ × Bool  □)

    l₁ : ND.Lens Bool Bool
    l₁ = idL

    l₂ : Bool → ND.Lens Bool Bool
    l₂ = if_then idL else swapL

    l₃ : ND.Lens Bool Bool
    l₃ = proj₁ (comp l₁ l₂)

    opaque
      unfolding NDC.id

      get-constant : ∀ b → get l₃ b ≡ true
      get-constant true  = proj₂ (comp l₁ l₂) _
      get-constant false = proj₂ (comp l₁ l₂) _

    contradiction : ⊥
    contradiction = Bool.true≢false (
      true                        ≡⟨ sym $ get-constant (set l₃ true false) ⟩
      get l₃ (set l₃ true false)  ≡⟨ get-set l₃ true false ⟩∎
      false                       ∎)

  -- Thus it is also unsatisfiable if non-dependent dependent lenses
  -- are isomorphic (in a certain sense) to the corresponding
  -- non-dependent lenses.

  no-composition-operator :
    ({A B : Type} →
     ∃ λ (iso : Lens′ A (λ _ → B) ↔ ND.Lens A B) →
       ∀ {l a} → get′ l a ≡ ND.Lens.get (_↔_.to iso l) a) →
    ¬ Type-of-composition
  no-composition-operator Lens↔Lens comp =
    no-corresponding-non-dependent-composition-operator
      (λ l₁ l₂ →
         let l₃ , get-l₃ = comp (from l₁) (λ a → from (l₂ a))
         in
         to l₃ , λ a →
           get (to l₃) a                                  ≡⟨ sym $ proj₂ Lens↔Lens ⟩
           get′ l₃ a                                      ≡⟨ get-l₃ a ⟩
           get′ (from (l₂ a)) (get′ (from l₁) a)          ≡⟨ cong (get′ (from (l₂ a))) (proj₂ Lens↔Lens) ⟩
           get′ (from (l₂ a)) (get (to (from l₁)) a)      ≡⟨ proj₂ Lens↔Lens ⟩
           get (to (from (l₂ a))) (get (to (from l₁)) a)  ≡⟨ cong₂ (λ l₁ l₂ → get l₁ (get l₂ a))
                                                                   (right-inverse-of _)
                                                                   (right-inverse-of _) ⟩∎
           get (l₂ a) (get l₁ a)                          ∎)
    where
    open ND.Lens
    open module Lens↔Lens {A B : Type} =
      _↔_ (proj₁ (Lens↔Lens {A = A} {B = B}))

-- In the presence of UIP for Type it is impossible to define a fully
-- general composition operator.

no-fully-general-composition-operator-UIP :
  let open Lens in
  Is-set Type →
  ¬ ({A : Type} {B : A → Type} {C : (a : A) → B a → Type}
     (l₁ : Lens A B)
     (l₂ : ∀ a → Lens (B a) (C a)) →
     ∃ λ (l₃ : Lens A (λ a → C a (Lens.get l₁ a))) →
       ∀ a → get l₃ a ≡ get (l₂ a) (get l₁ a))
no-fully-general-composition-operator-UIP uip =
  No-fully-general-composition-operator.no-composition-operator
    Lens Lens.get
    (non-dependent-lenses-isomorphic-UIP uip)

------------------------------------------------------------------------
-- An observation

-- Lens₃ lenses cannot (easily) be used to replace ordinary
-- projections: one cannot, in general, define lenses with the type of
-- the first projection from a Σ-type. For Lens lenses the situation
-- is unclear.

module Observation where

  -- A Σ-type which is isomorphic to the unit type.

  Unit = Σ Bool λ b → b ≡ true

  -- All its inhabitants are equal.

  equal : (u₁ u₂ : Unit) → u₁ ≡ u₂
  equal (.true , refl) (.true , refl) = refl

  -- Its only inhabitant.

  u : Unit
  u = (true , refl)

  -- The first projection Lens₃ cannot be defined for Unit.

  not-proj₁₃ : ∀ {r} {R : Type r} → ¬ Lens₃ Unit R (λ _ → Bool)
  not-proj₁₃ l = Bool.true≢false (
    true                                                    ≡⟨ sym $ subst-const (sym $ remainder-set u true) ⟩
    subst (λ _ → Bool) (sym $ remainder-set u true) true    ≡⟨ sym $ get-set₁ u true ⟩
    get (set u true)                                        ≡⟨ cong get (equal (set u true) (set u false)) ⟩
    get (set u false)                                       ≡⟨ get-set₁ u false ⟩
    subst (λ _ → Bool) (sym $ remainder-set u false) false  ≡⟨ subst-const (sym $ remainder-set u false) ⟩∎
    false                                                   ∎)
    where
    open Lens₃ l

  -- The first projection Lens cannot be defined for Unit /if/ we
  -- assume that UIP holds for Type.

  not-proj₁ : Is-set Type → ¬ Lens Unit (λ _ → Bool)
  not-proj₁ uip l = Bool.true≢false (
    true                       ≡⟨ sym $ cong (λ eq → from eq true) $ codomain-set-≃≡id uip l ⟩
    from codomain-set-≃ true   ≡⟨ sym $ get-set u true ⟩
    get (set u true)           ≡⟨ cong get (equal (set u true) (set u false)) ⟩
    get (set u false)          ≡⟨ get-set u false ⟩
    from codomain-set-≃ false  ≡⟨ cong (λ eq → from eq false) $ codomain-set-≃≡id uip l ⟩∎
    false                      ∎)
    where
    open _≃_
    open Lens l

  -- TODO: What is the situation in the presence of univalence?