text:
------------------------------------------------------------------------
-- Traditional non-dependent lenses
------------------------------------------------------------------------

{-# OPTIONS --cubical #-}

import Equality.Path as P

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

open P.Derived-definitions-and-properties eq

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

open import Bijection equality-with-J as Bij using (_↔_)
open import Circle eq as Circle using (𝕊¹)
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq
  using (_≃_; Is-equivalence)
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 Trunc
  using (∥_∥; ∣_∣)
open import Preimage equality-with-J using (_⁻¹_)
open import Surjection equality-with-J using (_↠_)
open import Univalence-axiom equality-with-J

open import Lens.Non-dependent eq as Non-dependent
  hiding (no-first-projection-lens; no-singleton-projection-lens)

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

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

-- Lenses.

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.
    get-set : ∀ a b → get (set a b) ≡ b
    set-get : ∀ a → set a (get a) ≡ a
    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 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) →
  (∀ 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

private
  variable
    l₁ l₂ : Lens A B

-- An example: A lens corresponding to the value of a function for a
-- certain input.

function-at : Decidable-equality A → A → Lens (A → B) B
function-at _≟_ a = record
  { get     = λ f → f a
  ; set     = λ f b a′ → if a ≟ a′ then b else f a′
  ; get-set = λ f b → lemma₁ (a ≟ a)
  ; set-get = λ f → ⟨ext⟩ λ a′ → lemma₂ f (a ≟ a′)
  ; set-set = λ f b₁ b₂ → ⟨ext⟩ λ a′ → lemma₃ (a ≟ a′)
  }
  where
  lemma₁ :
    ∀ {b₁ b₂} (d : Dec (a ≡ a)) →
    if d then b₁ else b₂ ≡ b₁
  lemma₁ (yes _)  = refl _
  lemma₁ (no a≢a) = ⊥-elim $ a≢a (refl _)

  lemma₂ :
    ∀ f {a′} (d : Dec (a ≡ a′)) →
    if d then f a else f a′ ≡ f a′
  lemma₂ f (yes a≡a′) = cong f a≡a′
  lemma₂ _ (no _)     = refl _

  lemma₃ :
    ∀ {a′ b₁ b₂ b₃} (d : Dec (a ≡ a′)) →
    if d then b₂ else (if d then b₁ else b₃) ≡
    if d then b₂ else b₃
  lemma₃ (yes _) = refl _
  lemma₃ (no _)  = refl _

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

-- Traditional lenses that satisfy some extra coherence properties.

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

  open Lens lens public

  field
    get-set-get : ∀ a → cong get (set-get a) ≡ get-set a (get a)
    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
    (∀ 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

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

-- If two lenses have equal setters, then they also have equal
-- getters.

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₂ setters-equal = ⟨ext⟩ λ a →
  get l₁ a                      ≡⟨ cong (get l₁) $ sym $ set-get l₂ _ ⟩
  get l₁ (set l₂ a (get l₂ a))  ≡⟨ cong (λ f → get l₁ (f _ _)) $ sym setters-equal ⟩
  get l₁ (set l₁ a (get l₂ a))  ≡⟨ get-set l₁ _ _ ⟩∎
  get l₂ a                      ∎
  where
  open Lens

-- If the forward direction of an equivalence is Lens.get l, then the
-- setter of l can be expressed using the other direction of the
-- equivalence.

from≡set :
  ∀ (l : Lens A B) is-equiv →
  let open Lens
      A≃B = Eq.⟨ get l , is-equiv ⟩
  in
  ∀ a b → _≃_.from A≃B b ≡ set l a b
from≡set l is-equiv a b =
  _≃_.to-from Eq.⟨ get , is-equiv ⟩ (
    get (set a b)  ≡⟨ get-set _ _ ⟩∎
    b              ∎)
  where
  open Lens l

------------------------------------------------------------------------
-- 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₁) →
   (∀ 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 →
                                                           (Π-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₂) →
   (∀ 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, then Lens A B is isomorphic to
-- (A → B) × ((a : A) → a ≡ a).

lens-to-proposition↔ :
  Is-proposition B →
  Lens A B ↔ (A → B) × ((a : A) → a ≡ a)
lens-to-proposition↔ {B = B} {A = A} B-prop =
  Lens A B                                                               ↝⟨ Lens-as-Σ ⟩

  (∃ λ (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₂))                         ↝⟨ (∃-cong λ _ → ∃-cong λ _ →
                                                                             drop-⊤-left-× λ _ →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                             Π-closure ext 0 λ _ →
                                                                             Π-closure ext 0 λ _ →
                                                                             +⇒≡ B-prop) ⟩
  (∃ λ (get : A → B) →
   ∃ λ (set : A → B → A) →
     (∀ a → set a (get a) ≡ a) ×
     (∀ a b₁ b₂ → set (set a b₁) b₂ ≡ set a b₂))                         ↝⟨ (∃-cong λ get → ∃-cong λ set → ∃-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 _ _) ⟩
       (set (set a (get a))                    b₂ ≡ set a b₂)                    ≡⟨ cong (λ b → set (set a (get a)) b ≡ _) (B-prop _ _) ⟩
       (set (set a (get a)) (get (set a (get a))) ≡ set a b₂)                    ≡⟨ cong (λ b → _ ≡ set a b) (B-prop _ _) ⟩∎
       (set (set a (get a)) (get (set a (get a))) ≡ set a (get a))               ∎)) ⟩

  (∃ λ (get : A → B) →
   ∃ λ (set : A → B → A) →
     (∀ 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 → Σ-cong (A→B→A↔A→A get) λ _ → F.id) ⟩

  ((A → B) ×
   ∃ λ (f : A → A) →
     (∀ a → f a ≡ a) ×
     (∀ a → B → B → f (f a) ≡ f a))                                      ↝⟨ (∃-cong λ get → ∃-cong λ _ → ∃-cong λ _ →
                                                                             ∀-cong ext λ a →
                                                                             drop-⊤-left-Π ext (B↔⊤ (get a)) F.∘
                                                                             drop-⊤-left-Π ext (B↔⊤ (get a))) ⟩

  ((A → B) × ∃ λ (f : A → A) → (∀ a → f a ≡ a) × (∀ a → f (f a) ≡ f a))  ↝⟨ (∃-cong λ _ → ∃-cong λ f → ∃-cong λ f≡id →
                                                                             ∀-cong ext λ a →
                                                                             ≡⇒↝ _ (cong₂ _≡_ (trans (f≡id (f a)) (f≡id a)) (f≡id a))) ⟩

  ((A → B) × ∃ λ (f : A → A) → (∀ a → f a ≡ a) × (∀ a → a ≡ a))          ↝⟨ (∃-cong λ _ →
                                                                             Σ-assoc F.∘
                                                                             (∃-cong λ _ →
                                                                              Σ-cong (Eq.extensionality-isomorphism ext) λ _ → F.id)) ⟩

  (A → B) × (∃ λ (f : A → A) → f ≡ id) × (∀ a → a ≡ a)                   ↝⟨ (∃-cong λ _ → drop-⊤-left-× λ _ →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                             singleton-contractible _) ⟩□
  (A → B) × (∀ a → a ≡ a)                                                □
  where
  B↔⊤ : B → B ↔ ⊤
  B↔⊤ b =
    _⇔_.to contractible⇔↔⊤ $
      propositional⇒inhabited⇒contractible B-prop b

  A→B→A↔A→A : (A → B) → (A → B → A) ↔ (A → A)
  A→B→A↔A→A get =
    (A → B → A)  ↝⟨ ∀-cong ext (λ a → drop-⊤-left-Π ext $ B↔⊤ (get a)) ⟩□
    (A → A)      □

-- Lens A ⊤ is isomorphic to (a : A) → a ≡ a.

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

-- Lens A ⊥ is isomorphic to ¬ A.

lens-to-⊥↔ : Lens A (⊥ {ℓ = b}) ↔ ¬ A
lens-to-⊥↔ {A = A} =
  Lens A ⊥                     ↝⟨ lens-to-proposition↔ ⊥-propositional ⟩
  (A → ⊥) × ((a : A) → a ≡ a)  ↝⟨ →-cong ext F.id (Bij.⊥↔uninhabited ⊥-elim)
                                    ×-cong
                                  F.id ⟩
  ¬ A × ((a : A) → a ≡ a)      ↝⟨ drop-⊤-right lemma ⟩□
  ¬ A                          □
  where
  lemma : ¬ A → ((a : A) → a ≡ a) ↔ ⊤
  lemma ¬a = record
    { surjection = record
      { logical-equivalence = record
        { to   = _
        ; from = λ _ _ → refl _
        }
      ; right-inverse-of = λ _ → refl _
      }
    ; left-inverse-of = λ eq → ⟨ext⟩ λ a →
        ⊥-elim (¬a 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.

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 {A = A} {B = B} n l a =
  H-level n A  ↝⟨ H-level.respects-surjection surj n ⟩□
  H-level n B  □
  where
  open Lens l

  surj : A ↠ B
  surj = record
    { logical-equivalence = record
      { to   = get
      ; from = set a
      }
    ; right-inverse-of = λ b →
        get (set a b)  ≡⟨ get-set a b ⟩∎
        b              ∎
    }

-- Lenses with contractible domains have contractible codomains.

contractible-to-contractible :
  Lens A B → Contractible A → Contractible B
contractible-to-contractible l c =
  h-level-respects-lens-from-inhabited _ l (proj₁ c) 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) λ _ →
  ×-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.

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 n hA =
  [inhabited⇒+]⇒+ n λ l →
    lens-preserves-h-level (1 + n) (λ _ → hA) λ a →
      h-level-respects-lens-from-inhabited _ l a hA

-- Lens 𝕊¹ ⊤ is not propositional (assuming univalence).
--
-- (The lemma does not actually use the univalence argument, but
-- univalence is used by Circle.¬-type-of-refl-propositional.)

¬-lens-to-⊤-propositional :
  Univalence (# 0) →
  ¬ Is-proposition (Lens 𝕊¹ ⊤)
¬-lens-to-⊤-propositional _ =
  Is-proposition (Lens 𝕊¹ ⊤)                 ↝⟨ H-level.respects-surjection (_↔_.surjection lens-to-⊤↔) 1 ⟩
  Is-proposition ((x : 𝕊¹) → x ≡ x)          ↝⟨ H-level-cong _ 1 (Π-cong ext (inverse Bij.↑↔) λ _ → Eq.≃-≡ $ Eq.↔⇒≃ Bij.↑↔) ⟩
  Is-proposition ((x : ↑ lzero 𝕊¹) → x ≡ x)  ↝⟨ proj₂ $ Circle.¬-type-of-refl-propositional ⟩□
  ⊥                                          □

------------------------------------------------------------------------
-- 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₂) →
      (∀ 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) →
                (∀ 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) →
                                                                                (∀ 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) →
                (∀ 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) →
                (∀ 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 (λ x → x ≡ proj₂ (proj₂ l₂′))
                                                                                (push-subst-, {y≡z = _↔_.to ≡×≡↔≡ (g , s)} _ _)) ⟩
    (∃ λ (g : get l₁ ≡ get l₂) →
     ∃ λ (s : set l₁ ≡ set l₂) →
     ( 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₂ (proj₂ (proj₂ l₁′)))
     ) ≡
     proj₂ (proj₂ l₂′))                                                ↝⟨ (∃-cong λ _ → ∃-cong λ _ → inverse ≡×≡↔≡) ⟩

    (∃ λ (g : get l₁ ≡ get l₂) →
     ∃ λ (s : set l₁ ≡ set l₂) →
     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₂ (proj₂ (proj₂ l₁′))) ≡
     proj₂ (proj₂ (proj₂ l₂′)))                                        ↝⟨ (∃-cong λ g → ∃-cong λ s → ∃-cong λ _ → ≡⇒↝ _ $
                                                                           cong (λ x → x ≡ proj₂ (proj₂ (proj₂ l₂′)))
                                                                                (push-subst-, {y≡z = _↔_.to ≡×≡↔≡ (g , s)} _ _)) ⟩
    (∃ λ (g : get l₁ ≡ get l₂) →
     ∃ λ (s : set l₁ ≡ set l₂) →
     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₂ (proj₂ (proj₂ l₂′)))                                        ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → inverse ≡×≡↔≡) ⟩

    (∃ λ (g : get l₁ ≡ get l₂) →
     ∃ λ (s : set l₁ ≡ set l₂) →
     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 →
                                                                           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₂) →
     (∀ 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 →
                                                                           (∀-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₂) →
     (∀ 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 → ∃-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₂) →
     (∀ 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 →
                                                                           (∀-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₂) →
     (∀ 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 λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                           ∀-cong ext λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                           ≡⇒↝ _ $ cong (λ x → x ≡ _) $ subst-const g) ⟩□
    (∃ λ (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)) ≡
              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₂) →
      (∀ 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₂) →
       (∀ 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 →
                                                                         (∀-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₂) →
       (∀ 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

    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 {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 _ 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)                                         ∎

    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 _ 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₂) →
      (∀ 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₂) →
       (∀ 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 → ∃-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₂) →
       (∀ 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

    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) →
      (∀ 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₂) →
       (∀ 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 →
                                                                            (∀-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 bad-ext) _ ⟩
        ⟨ext⟩ (ext⁻¹ s)                                                        ≡⟨ (cong ⟨ext⟩ $ ⟨ext⟩ λ _ → sym $
                                                                                _≃_.right-inverse-of
                                                                                (Eq.extensionality-isomorphism bad-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) →
       (∀ 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₂′ : (∀ 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

    (∀ a b → get-set l₁ a b ≡ get-set l₂ a b) →
    (∀ a → set-get l₁ a ≡ set-get l₂ a) →
    (∀ 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.

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₂                                                         ↝⟨ equality-characterisation₁ ⟩

  (∃ λ (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))
                ≡
              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 λ _ → ∃-cong λ _ → drop-⊤-left-Σ $ _⇔_.to contractible⇔↔⊤ $
                                                                      Π-closure ext 0 λ a →
                                                                      Π-closure ext 0 λ _ →
                                                                      +⇒≡ (B-set a)) ⟩
  (∃ λ (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))
              ≡
            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 λ _ → ∃-cong λ _ → drop-⊤-left-Σ $ _⇔_.to contractible⇔↔⊤ $
                                                                      Π-closure ext 0 λ _ →
                                                                      +⇒≡ A-set) ⟩
  (∃ λ (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₂))                            ↝⟨ (∃-cong λ _ → drop-⊤-right λ _ → _⇔_.to contractible⇔↔⊤ $
                                                                      Π-closure ext 0 λ _ →
                                                                      Π-closure ext 0 λ _ →
                                                                      Π-closure ext 0 λ _ →
                                                                      +⇒≡ A-set) ⟩

  get l₁ ≡ get l₂ × set l₁ ≡ set l₂                               ↝⟨ (drop-⊤-left-× λ setters-equal → _⇔_.to contractible⇔↔⊤ $
                                                                      propositional⇒inhabited⇒contractible
                                                                        (Π-closure ext 2 λ a →
                                                                         B-set a)
                                                                        (getters-equal-if-setters-equal l₁ l₂ setters-equal)) ⟩□
  set l₁ ≡ set l₂                                                 □
  where
  open Lens

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

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

-- Lens ⊤ B is equivalent to Contractible B.

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

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

lens-from-⊥≃⊤ : Lens (⊥ {ℓ = a}) B ≃ ⊤
lens-from-⊥≃⊤ = Eq.⇔→≃
  (lens-preserves-h-level-of-domain 0 ⊥-propositional)
  (mono₁ 0 ⊤-contractible)
  _
  (λ _ → record
     { get = ⊥-elim
     ; set = ⊥-elim
     ; get-set = λ a → ⊥-elim a
     ; set-get = λ a → ⊥-elim a
     ; set-set = λ a → ⊥-elim a
     })

-- If A is a set and there is a lens from A to B, then A is equivalent
-- 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.
--
-- See also Lens.Non-dependent.Traditional.Combinators.≄Σ∥set⁻¹∥×.

≃Σ∥set⁻¹∥× :
  Is-set A →
  (l : Lens A B) →
  A ≃ ((∃ λ (f : B → A) → ∥ Lens.set l ⁻¹ f ∥) × B)
≃Σ∥set⁻¹∥× {A = A} {B = B} A-set l = Eq.↔→≃
  (λ a → (set a , ∣ a , refl _ ∣) , get a)
  (λ ((f , _) , b) → f b)
  (λ ((f , p) , b) →
     flip (Trunc.rec (×-closure 2
                        (Σ-closure 2
                           (Π-closure ext 2 λ _ → A-set) λ _ →
                           mono₁ 1 Trunc.truncation-is-proposition)
                        (B-set (f b))))
       p λ (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₁ (Trunc.truncation-is-proposition _ _)) lemma₂ ⟩∎
     (f         , p               ) , b          ∎)
  (λ a →
     set a (get a)  ≡⟨ set-get a ⟩∎
     a              ∎)
  where
  open Lens l

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

-- If B is an inhabited set and there is a lens from A to B, then A is
-- equivalent 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⁻¹× :
  Is-set B →
  (b : B)
  (l : Lens A B) →
  A ≃ (Lens.get l ⁻¹ b × B)
≃get⁻¹× {B = B} {A = A} B-set b₀ l = Eq.↔→≃
  (λ 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 (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 = Eq.↔→≃
  (λ 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 bad-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 id) (get a)))
               (trans (cong id h) (ext⁻¹ (refl id) b₀))            ≡⟨ cong₂ (λ p q → trans p (trans (cong id h) q))
                                                                        (trans (cong sym (ext⁻¹-refl _)) sym-refl)
                                                                        (ext⁻¹-refl _) ⟩

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

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

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

             h                                                     ∎)
                                                                  _ ⟩∎
         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 : 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
                          $⟨ ×-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
  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}
  (s : Is-set A) →
  Preserves-getters-and-setters-⇔ A B
    (_≃_.logical-equivalence (≃coherent s))
≃coherent-preserves-getters-and-setters _ =
    (λ _ → refl _ , refl _)
  , (λ _ → refl _ , refl _)

------------------------------------------------------------------------
-- Some existence results

-- There is, in general, no lens for the first projection from a
-- Σ-type.

no-first-projection-lens :
  ¬ Lens (∃ λ (b : Bool) → b ≡ true) Bool
no-first-projection-lens =
  Non-dependent.no-first-projection-lens
    Lens contractible-to-contractible

-- A variant of the previous result: If A is merely inhabited, and one
-- can "project" out a boolean from a value of type A, but this
-- boolean is necessarily true, then there is no lens corresponding to
-- this projection.

no-singleton-projection-lens :
  ∥ A ∥ →
  (bool : A → Bool) →
  (∀ x → bool x ≡ true) →
  ¬ ∃ λ (l : Lens A Bool) →
      ∀ x → Lens.get l x ≡ bool x
no-singleton-projection-lens =
  Non-dependent.no-singleton-projection-lens _ _ Lens.get-set

-- There are two lenses with equal setters that are not equal
-- (assuming univalence).
--
-- (The lemma does not actually use the univalence argument, but
-- univalence is used by Circle.not-refl≢refl.)

equal-setters-but-not-equal :
  Univalence lzero →
  ∃ λ (A : Type) →
  ∃ λ (B : Type) →
  ∃ λ (l₁ : Lens A B) →
  ∃ λ (l₂ : Lens A B) →
    Lens.set l₁ ≡ Lens.set l₂ ×
    l₁ ≢ l₂
equal-setters-but-not-equal _ =
  𝕊¹ , ⊤ , l₁′ , l₂′ , refl _ , l₁′≢l₂′
  where
  open Lens

  lemma : Lens 𝕊¹ ⊤ ≃ ((x : 𝕊¹) → x ≡ x)
  lemma =
    Lens 𝕊¹ ⊤                      ↔⟨ lens-to-proposition↔ (mono₁ 0 ⊤-contractible) ⟩
    (𝕊¹ → ⊤) × ((x : 𝕊¹) → x ≡ x)  ↔⟨ (drop-⊤-left-× λ _ → →-right-zero) ⟩□
    ((x : 𝕊¹) → x ≡ x)             □

  l₁′ : Lens 𝕊¹ ⊤
  l₁′ = _≃_.from lemma Circle.not-refl

  l₂′ : Lens 𝕊¹ ⊤
  l₂′ = _≃_.from lemma refl

  set-l₁′≡set-l₂′ : set l₁′ ≡ set l₂′
  set-l₁′≡set-l₂′ = refl _

  l₁′≢l₂′ : l₁′ ≢ l₂′
  l₁′≢l₂′ =
    l₁′ ≡ l₂′               ↔⟨ Eq.≃-≡ (inverse lemma) {x = Circle.not-refl} {y = refl} ⟩
    Circle.not-refl ≡ refl  ↝⟨ Circle.not-refl≢refl ⟩□
    ⊥                       □

-- A lens which is used in some counterexamples below.

bad : (a : Level) → Lens (↑ a 𝕊¹) (↑ a 𝕊¹)
bad a = record
  { get     = id
  ; set     = const id
  ; get-set = λ _ → cong lift ∘ Circle.not-refl ∘ lower
  ; set-get = refl
  ; set-set = λ _ _ → cong lift ∘ Circle.not-refl ∘ lower
  }

-- The lens bad a has a getter which is an equivalence, but it does
-- not satisfy either of the coherence laws that Coherent-lens lenses
-- must satisfy (assuming univalence).
--
-- (The lemma does not actually use the univalence argument, but
-- univalence is used by Circle.not-refl≢refl.)

getter-equivalence-but-not-coherent :
  Univalence lzero →
  let open Lens (bad a) in
  Is-equivalence get ×
  ¬ (∀ a → cong get (set-get a) ≡ get-set a (get a)) ×
  ¬ (∀ a₁ a₂ a₃ →
     cong get (set-set a₁ a₂ a₃) ≡
     trans (get-set (set a₁ a₂) a₃) (sym (get-set a₁ a₃)))
getter-equivalence-but-not-coherent {a = a} _ =
    _≃_.is-equivalence F.id
  , (((x : ↑ a 𝕊¹) → cong get (set-get x) ≡ get-set x (get x))        ↔⟨⟩

     ((x : ↑ a 𝕊¹) →
      cong id (refl _) ≡ cong lift (Circle.not-refl (lower x)))       ↔⟨ (Π-cong ext Bij.↑↔ λ _ → Eq.id) ⟩

     ((x : 𝕊¹) → cong id (refl _) ≡ cong lift (Circle.not-refl x))    ↝⟨ trans (trans (cong-refl _) (cong-id _)) ∘_ ⟩

     ((x : 𝕊¹) → cong lift (refl x) ≡ cong lift (Circle.not-refl x))  ↔⟨ (∀-cong ext λ _ →
                                                                          Eq.≃-≡ $ inverse $ Eq.≃-≡ $ Eq.↔⇒≃ $ inverse Bij.↑↔) ⟩

     ((x : 𝕊¹) → refl x ≡ Circle.not-refl x)                          ↔⟨ Eq.extensionality-isomorphism ext ⟩

     refl ≡ Circle.not-refl                                           ↝⟨ Circle.not-refl≢refl ∘ sym ⟩□

     ⊥                                                                □)
  , (((x y z : ↑ a 𝕊¹) →
      cong get (set-set x y z) ≡
      trans (get-set (set x y) z) (sym (get-set x z)))     ↔⟨⟩

     ((x y z : ↑ a 𝕊¹) →
      cong id (cong lift (Circle.not-refl (lower z))) ≡
      trans (cong lift (Circle.not-refl (lower z)))
        (sym (cong lift (Circle.not-refl (lower z)))))     ↔⟨ (Π-cong ext Bij.↑↔ λ _ →
                                                               Π-cong ext Bij.↑↔ λ _ →
                                                               Π-cong ext Bij.↑↔ λ _ →
                                                               Eq.id) ⟩
     ((x y z : 𝕊¹) →
      cong id (cong lift (Circle.not-refl z)) ≡
      trans (cong lift (Circle.not-refl z))
        (sym (cong lift (Circle.not-refl z))))             ↝⟨ (λ hyp → hyp Circle.base Circle.base) ⟩

     ((x : 𝕊¹) →
      cong id (cong lift (Circle.not-refl x)) ≡
      trans (cong lift (Circle.not-refl x))
        (sym (cong lift (Circle.not-refl x))))             ↔⟨ (∀-cong ext λ _ → ≡⇒≃ $ cong₂ _≡_
                                                                 (sym $ cong-id _)
                                                                 (trans (trans-symʳ _) $
                                                                  sym $ cong-refl _)) ⟩
     ((x : 𝕊¹) →
      cong lift (Circle.not-refl x) ≡ cong lift (refl x))  ↔⟨ (∀-cong ext λ _ →
                                                               Eq.≃-≡ $ inverse $ Eq.≃-≡ $ Eq.↔⇒≃ $ inverse Bij.↑↔) ⟩

     ((x : 𝕊¹) → Circle.not-refl x ≡ refl x)               ↔⟨ Eq.extensionality-isomorphism ext ⟩

     Circle.not-refl ≡ refl                                ↝⟨ Circle.not-refl≢refl ⟩□

     ⊥                                                     □)
  where
  open Lens (bad a)

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


text:
{-# OPTIONS --without-K --safe #-}

-- The category of Cats is Monoidal

module Categories.Category.Monoidal.Instance.Cats where

open import Level

open import Categories.Category.BinaryProducts using (BinaryProducts)
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
open import Categories.Category.Instance.Cats using (Cats)
open import Categories.Category.Instance.One using (One-⊤)
open import Categories.Category.Monoidal using (Monoidal)
open import Categories.Category.Product using (Product; πˡ; πʳ; _※_)
open import Categories.Category.Product.Properties using (project₁; project₂; unique)

-- Cats is a Monoidal Category with Product as Bifunctor
module Product {o ℓ e : Level} where
  private
    C = Cats o ℓ e

  Cats-has-all : BinaryProducts C
  Cats-has-all = record { product = λ {A} {B} → record
    { A×B = Product A B
    ; π₁ = πˡ
    ; π₂ = πʳ
    ; ⟨_,_⟩ = _※_
    ; project₁ = λ {_} {h} {i} → project₁ {i = h} {j = i}
    ; project₂ = λ {_} {h} {i} → project₂ {i = h} {j = i}
    ; unique = unique
    } }

  Cats-is : Cartesian C
  Cats-is = record { terminal = One-⊤ ; products = Cats-has-all }

  Cats-Monoidal : Monoidal C
  Cats-Monoidal = CartesianMonoidal.monoidal Cats-is

ext: agda

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --warning=error --safe --without-K #-}

open import LogicalFormulae
open import Numbers.Naturals.Definition
open import Numbers.Naturals.Addition
open import Numbers.Naturals.Multiplication
open import Semirings.Definition
open import Monoids.Definition

module Numbers.Naturals.Semiring where

open Numbers.Naturals.Definition using (ℕ ; zero ; succ ; succInjective ; naughtE) public
open Numbers.Naturals.Addition using (_+N_ ; canSubtractFromEqualityRight ; canSubtractFromEqualityLeft) public
open Numbers.Naturals.Multiplication using (_*N_ ; multiplicationNIsCommutative) public

ℕSemiring : Semiring 0 1 _+N_ _*N_
Monoid.associative (Semiring.monoid ℕSemiring) a b c = equalityCommutative (additionNIsAssociative a b c)
Monoid.idLeft (Semiring.monoid ℕSemiring) _ = refl
Monoid.idRight (Semiring.monoid ℕSemiring) a = additionNIsCommutative a 0
Semiring.commutative ℕSemiring = additionNIsCommutative
Monoid.associative (Semiring.multMonoid ℕSemiring) = multiplicationNIsAssociative
Monoid.idLeft (Semiring.multMonoid ℕSemiring) a = additionNIsCommutative a 0
Monoid.idRight (Semiring.multMonoid ℕSemiring) a = transitivity (multiplicationNIsCommutative a 1) (additionNIsCommutative a 0)
Semiring.productZeroLeft ℕSemiring _ = refl
Semiring.productZeroRight ℕSemiring a = multiplicationNIsCommutative a 0
Semiring.+DistributesOver* ℕSemiring = productDistributes
Semiring.+DistributesOver*' ℕSemiring a b c rewrite multiplicationNIsCommutative (a +N b) c | multiplicationNIsCommutative a c | multiplicationNIsCommutative b c = productDistributes c a b

succExtracts : (x y : ℕ) → (x +N succ y) ≡ (succ (x +N y))
succExtracts x y = transitivity (Semiring.commutative ℕSemiring x (succ y)) (applyEquality succ (Semiring.commutative ℕSemiring y x))

productZeroImpliesOperandZero : {a b : ℕ} → a *N b ≡ 0 → (a ≡ 0) || (b ≡ 0)
productZeroImpliesOperandZero {zero} {b} pr = inl refl
productZeroImpliesOperandZero {succ a} {zero} pr = inr refl
productZeroImpliesOperandZero {succ a} {succ b} ()

*NWellDefined : {a b c d : ℕ} → (a ≡ c) → (b ≡ d) → a *N b ≡ c *N d
*NWellDefined refl refl = refl

+NWellDefined : {a b c d : ℕ} → (a ≡ c) → (b ≡ d) → a +N b ≡ c +N d
+NWellDefined refl refl = refl


text:
-- Type-checker for the simply-typed lambda calculus
--
-- Where we make sure that failing to typecheck a term is justified by
-- an "ill-typing judgment", which erases to the original term.

open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.List hiding ([_])
open import Data.Nat hiding (_*_ ; _+_ ; _≟_)
open import Data.Product

open import Relation.Nullary
open import Relation.Binary hiding (_⇒_)
open import Relation.Binary.PropositionalEquality hiding ([_])

infix 5 _⊢?_∋_
infix 5 _⊢?_∈
infix 19 _↪_
infixr 30 _+_
infixr 35 _*_
infixr 40 _⇒_
infix 50 _∈_
infix 50 _∈
infix 50 _∋_
infixl 150 _▹_

-- * Types

data type : Set where
  unit nat : type
  _*_ _+_ _⇒_ : (A B : type) → type

bool : type
bool = unit + unit

-- TODO: automate this definition using reflection of Agda in Agda
-- see https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Deriving/Eq.agda
_≟_ : Decidable {A = type} _≡_
unit      ≟ unit          = yes refl
nat       ≟ nat           = yes refl
(A₁ + B₁) ≟ (A₂ + B₂)
  with A₁ ≟ A₂ | B₁ ≟ B₂
... | yes refl | yes refl = yes refl
... | yes refl | no ¬p    = no (λ { refl → ¬p refl })
... | no ¬p | _           = no (λ { refl → ¬p refl })
(A₁ ⇒ B₁) ≟ (A₂ ⇒ B₂)
  with A₁ ≟ A₂ | B₁ ≟ B₂
... | yes refl | yes refl = yes refl
... | yes _    | no ¬p    = no λ { refl → ¬p refl }
... | no ¬p    | _        = no λ { refl → ¬p refl }
(A₁ * B₁) ≟ (A₂ * B₂)
  with A₁ ≟ A₂ | B₁ ≟ B₂
... | yes refl | yes refl = yes refl
... | yes _    | no ¬p    = no λ { refl → ¬p refl }
... | no ¬p    | q₂       = no λ { refl → ¬p refl }
unit      ≟ (_ ⇒ _)       = no λ {()}
unit      ≟ (_ * _)       = no λ {()}
unit      ≟ nat           = no λ {()}
unit      ≟ (_ + _)       = no λ {()}
nat       ≟ (_ ⇒ _)       = no λ {()}
nat       ≟ (_ * _)       = no λ {()}
nat       ≟ unit          = no λ {()}
nat       ≟ (_ + _)       = no λ {()}
(_ + _)   ≟ (_ ⇒ _)       = no λ {()}
(_ + _)   ≟ (_ * _)       = no λ {()}
(_ + _)   ≟ nat           = no λ {()}
(_ + _)   ≟ unit          = no λ {()}
(_ ⇒ _)   ≟ unit          = no λ {()}
(_ ⇒ _)   ≟ nat           = no λ {()}
(_ ⇒ _)   ≟ (_ * _)       = no λ {()}
(_ ⇒ _)   ≟ (_ + _)       = no λ {()}
(_ * _)   ≟ unit          = no λ {()}
(_ * _)   ≟ nat           = no λ {()}
(_ * _)   ≟ (_ ⇒ _)       = no λ {()}
(_ * _)   ≟ (_ + _)       = no λ {()}

-- * Syntax of terms

data dir : Set where
  ⇑ ⇓ : dir

data can (T : Set) : Set where
  tt        :               can T
  pair      : (t₁ t₂ : T) → can T
  lam       : (b : T)     → can T
  ze        :               can T
  su        : (t : T)     → can T
  inj₁ inj₂ : (t : T)     → can T

data elim (T : Set) : dir → Set where
  apply   : (s : T)     → elim T ⇑
  fst snd :               elim T ⇑
  split   : (c₁ c₂ : T) → elim T ⇓

data term : dir → Set  where
  C       : (c : can (term ⇓))                           → term ⇓
  inv     : (t : term ⇑)                                 → term ⇓
  var     : (k : ℕ)                                      → term ⇑
  _#_     : ∀ {d} → (n : term ⇑)(args : elim (term ⇓) d) → term d
  [_:∋:_] : (T : type)(t : term ⇓)                       → term ⇑

pattern Ctt       = C tt
pattern Cze       = C ze
pattern Csu x     = C (su x)
pattern Cpair x y = C (pair x y)
pattern Clam b    = C (lam b)
pattern Cinj₁ x   = C (inj₁ x)
pattern Cinj₂ x   = C (inj₂ x)

-- ** Tests

true : term ⇓
true = Cinj₁ Ctt

false : term ⇓
false = Cinj₂ Ctt

t1 : term ⇓
t1 = inv ([ nat ⇒ nat :∋: Clam {- x -} (inv (var {- x -} 0)) ] # apply (Csu (Csu Cze)))

t2 : term ⇓
t2 = Clam {-x-} (var {- x -} 0 # split true false)

-- * Type system

context = List type

pattern _▹_ Γ T = T ∷ Γ
pattern ε       = []

data _∈_ (T : type) : context → Set where
  here : ∀ {Γ} →

      ---------
      T ∈ Γ ▹ T

  there : ∀ {Γ T'} →

      T ∈ Γ
    → ----------
      T ∈ Γ ▹ T'

mutual

  data _C⊢[_]_ : context → dir → type → Set where
    lam : ∀ {Γ A B} →

        Γ ▹ A ⊢[ ⇓ ] B
      → ---------------
        Γ C⊢[ ⇓ ] A ⇒ B

    tt : ∀ {Γ} →

        --------------
        Γ C⊢[ ⇓ ] unit

    ze : ∀ {Γ} →

        -------------
        Γ C⊢[ ⇓ ] nat

    su : ∀ {Γ} →

        Γ ⊢[ ⇓ ] nat
      → -------------
        Γ C⊢[ ⇓ ] nat

    inj₁ : ∀ {Γ A B} →

        Γ ⊢[ ⇓ ] A
      → ---------------
        Γ C⊢[ ⇓ ] A + B

    inj₂ : ∀ {Γ A B} →

        Γ ⊢[ ⇓ ] B
      → ---------------
        Γ C⊢[ ⇓ ] A + B

    pair : ∀ {Γ A B} →

        Γ ⊢[ ⇓ ] A →
        Γ ⊢[ ⇓ ] B
      → ---------------
        Γ C⊢[ ⇓ ] A * B

  data _E⊢[_]_↝_ : context → dir → type → type → Set where
    apply : ∀ {Γ A B} →

        Γ ⊢[ ⇓ ] A
      → -------------------
        Γ E⊢[ ⇑ ] A ⇒ B ↝ B

    fst : ∀ {Γ A B} →

        -------------------
        Γ E⊢[ ⇑ ] A * B ↝ A

    snd : ∀ {Γ A B} →

        -------------------
        Γ E⊢[ ⇑ ] A * B ↝ B

    iter : ∀ {Γ A} →

        Γ ▹ A ⊢[ ⇓ ] A →
        Γ ⊢[ ⇓ ] A
      → -----------------
        Γ E⊢[ ⇓ ] nat ↝ A

    case : ∀ {Γ A B C} →

        Γ ▹ A ⊢[ ⇓ ] C →
        Γ ▹ B ⊢[ ⇓ ] C
      → -------------------
        Γ E⊢[ ⇓ ] A + B ↝ C

  data _⊢[_]_ : context → dir → type → Set where

    C : ∀ {Γ d T} →

        Γ C⊢[ d ] T
      → -----------
        Γ ⊢[ d ] T

    inv : ∀ {Γ T} →

        Γ ⊢[ ⇑ ] T
      → ----------
        Γ ⊢[ ⇓ ] T

    var : ∀ {Γ T} →

        T ∈ Γ
      → ----------
        Γ ⊢[ ⇑ ] T

    _#_ : ∀ {Γ d I O} →

        Γ ⊢[ ⇑ ] I →
        Γ E⊢[ d ] I ↝ O
      → ---------------
        Γ ⊢[ d ] O

    [_:∋:_by_] : ∀ {Γ A} →

        (B : type) → Γ ⊢[ ⇓ ] B → A ≡ B
      → -------------------------------
        Γ ⊢[ ⇑ ] A

-- ** Tests

⊢true : [] ⊢[ ⇓ ] bool
⊢true = C (inj₁ (C tt))

⊢false : [] ⊢[ ⇓ ] bool
⊢false = C (inj₂ (C tt))

⊢t1 : [] ⊢[ ⇓ ] nat
⊢t1 = inv ([ (nat ⇒ nat) :∋: (C (lam (inv (var here)))) by refl ]
          # (apply (C (su (C (su (C ze)))))))

-- * Relating typing and terms

record _↪_ (S T : Set) : Set where
  field
    ⌊_⌋ : S → T

open _↪_ {{...}} public

instance
  VarRaw : ∀ {T Γ} → T ∈ Γ ↪ ℕ
  ⌊_⌋ {{ VarRaw }} here      = zero
  ⌊_⌋ {{ VarRaw }} (there x) = suc ⌊ x ⌋

  OTermRaw : ∀ {Γ T d} → Γ ⊢[ d ] T ↪ term d
  ⌊_⌋ {{OTermRaw}} (C (lam b))         = C (lam ⌊ b ⌋)
  ⌊_⌋ {{OTermRaw}} (C tt)              = C tt
  ⌊_⌋ {{OTermRaw}} (C ze)              = C ze
  ⌊_⌋ {{OTermRaw}} (C (su t))          = C (su ⌊ t ⌋)
  ⌊_⌋ {{OTermRaw}} (C (inj₁ t))        = C (inj₁ ⌊ t ⌋)
  ⌊_⌋ {{OTermRaw}} (C (inj₂ t))        = C (inj₂ ⌊ t ⌋)
  ⌊_⌋ {{OTermRaw}} (C (pair t₁ t₂))    = C (pair ⌊ t₁ ⌋ ⌊ t₂ ⌋)
  ⌊_⌋ {{OTermRaw}} (inv t)             = inv ⌊ t ⌋
  ⌊_⌋ {{OTermRaw}} (var x)             = var ⌊ x ⌋
  ⌊_⌋ {{OTermRaw}} (f # (apply s))     = ⌊ f ⌋ # apply ⌊ s ⌋
  ⌊_⌋ {{OTermRaw}} (p # fst)           = ⌊ p ⌋ # fst
  ⌊_⌋ {{OTermRaw}} (p # snd)           = ⌊ p ⌋ # snd
  ⌊_⌋ {{OTermRaw}} (t # case x y)      = ⌊ t ⌋ # split ⌊ x ⌋ ⌊ y ⌋
  ⌊_⌋ {{OTermRaw}} (t # iter fs fz)    = ⌊ t ⌋ # split ⌊ fs ⌋ ⌊ fz ⌋
  ⌊_⌋ {{OTermRaw}} [ T :∋: t by refl ] = [ T :∋: ⌊ t ⌋ ]

data _⊢_∋_ (Γ : context)(T : type){d} : term d → Set where
  well-typed : (Δ : Γ ⊢[ d ] T ) → Γ ⊢ T ∋ ⌊ Δ ⌋

-- TODO: one could prove that `Γ ⊢ T ∋ t` is H-prop when `t : term ⇓`, ie. we have
--     lemma-proof-irr : ∀ {Γ T}{t : term ⇓} → ∀ (pf₁ pf₂ : Γ ⊢ T ∋ t) → → pf₁ ≅ pf₂
-- but this requires proving that `⌊_⌋` is injective.

-- TODO: conversely, one should be able to prove that `Γ ⊢ T ∋ t` is
-- equivalent to `type` when `t : term ⇑` but I haven't tried.

-- ** Tests

bool∋true : [] ⊢ bool ∋ true
bool∋true = well-typed ⊢true

bool∋false : [] ⊢ bool ∋ false
bool∋false = well-typed ⊢false

nat∋t1 : [] ⊢ nat ∋ t1
nat∋t1 = well-typed ⊢t1

-- * Ill-type system

data Canonical {X} : type → can X → Set where
  can-unit-tt   :               Canonical unit tt
  can-nat-ze    :               Canonical nat ze
  can-nat-su    : ∀ {a}       → Canonical nat (su a)
  can-sum-inj₁  : ∀ {A B a}   → Canonical (A + B) (inj₁ a)
  can-sum-inj₂  : ∀ {A B b}   → Canonical (A + B) (inj₂ b)
  can-prod-pair : ∀ {A B a b} → Canonical (A * B) (pair a b)

data IsProduct : type → Set where
  is-product : ∀ {A B} → IsProduct (A * B)

data IsArrow : type → Set where
  is-arrow : ∀ {A B} → IsArrow (A ⇒ B)

data IsSplit : type → Set where
  is-split-nat :           IsSplit nat
  is-split-sum : ∀ {A B} → IsSplit (A + B)

mtype : dir → Set
mtype ⇑ = ⊤
mtype ⇓ = type

data _B⊬[_]_ (Γ : context) : (d : dir) → mtype d → Set where
  not-canonical : ∀ {c : can (term ⇓)}{T} →

      ¬ Canonical T c
    → ---------------
      Γ B⊬[ ⇓ ] T

  unsafe-inv : ∀ {A B} →

      Γ ⊢[ ⇑ ] A → A ≢ B
    → -------------------
      Γ B⊬[ ⇓ ] B

  bad-split : ∀ {A B}{c₁ c₂ : term ⇓} →

      Γ ⊢[ ⇑ ] A  → ¬ IsSplit A
    → -------------------------
      Γ B⊬[ ⇓ ] B

  out-of-scope : ∀ {x : ℕ} →

      x ≥ length Γ
    → ------------
      Γ B⊬[ ⇑ ] _

  bad-function : ∀ {T}{s : term ⇓} →

      Γ ⊢[ ⇑ ] T → ¬ IsArrow T
    → ------------------------
      Γ B⊬[ ⇑ ] _

  bad-fst : ∀ {T} →

      Γ ⊢[ ⇑ ] T → ¬ IsProduct T
    → --------------------------
      Γ B⊬[ ⇑ ] _

  bad-snd : ∀ {T} →

      Γ ⊢[ ⇑ ] T → ¬ IsProduct T
    → --------------------------
      Γ B⊬[ ⇑ ] _

-- TODO: automate this "trisection & free monad" construction by meta-programming
-- see: "The gentle art of levitation", Chapman et al. for the free monad
-- see: "Clowns to the left of me, jokers to the right", McBride for the dissection
mutual
  data _C⊬[_]_ : context → (d : dir) → mtype d → Set where
    lam   : ∀ {Γ A B} → Γ ▹ A ⊬[ ⇓ ] B           → Γ C⊬[ ⇓ ] A ⇒ B
    su    : ∀ {Γ} → Γ ⊬[ ⇓ ] nat                 → Γ C⊬[ ⇓ ] nat
    inj₁  : ∀ {Γ A B} → Γ ⊬[ ⇓ ] A               → Γ C⊬[ ⇓ ] A + B
    inj₂  : ∀ {Γ A B} → Γ ⊬[ ⇓ ] B               → Γ C⊬[ ⇓ ] A + B
    pair₁ : ∀ {Γ A B} → Γ ⊬[ ⇓ ] A → term ⇓      → Γ C⊬[ ⇓ ] A * B
    pair₂ : ∀ {Γ A B} → Γ ⊢[ ⇓ ] A → Γ ⊬[ ⇓ ] B  → Γ C⊬[ ⇓ ] A * B

  data _E⊬[_]_↝_ : context → (d : dir) → type → mtype d → Set where
    apply : ∀ {Γ A B} → Γ ⊬[ ⇓ ] A                        → Γ E⊬[ ⇑ ] A ⇒ B ↝ _
    iter₁ : ∀ {Γ T} → Γ ▹ T ⊬[ ⇓ ] T → term ⇓             → Γ E⊬[ ⇓ ] nat ↝ T
    iter₂ : ∀ {Γ T} → Γ ▹ T ⊢[ ⇓ ] T → Γ ⊬[ ⇓ ] T         → Γ E⊬[ ⇓ ] nat ↝ T
    case₁ : ∀ {Γ A B C} → Γ ▹ A ⊬[ ⇓ ] C → term ⇓         → Γ E⊬[ ⇓ ] A + B ↝ C
    case₂ : ∀ {Γ A B C} → Γ ▹ A ⊢[ ⇓ ] C → Γ ▹ B ⊬[ ⇓ ] C → Γ E⊬[ ⇓ ] A + B ↝ C

  data _⊬[_]_ : context → (d : dir) → mtype d → Set where
    because  : ∀ {Γ d T} → Γ B⊬[ d ] T                    → Γ ⊬[ d ] T
    C        : ∀ {Γ d T} → Γ C⊬[ d ] T                    → Γ ⊬[ d ] T
    inv      : ∀ {Γ T} → Γ ⊬[ ⇑ ] _                       → Γ ⊬[ ⇓ ] T
    _#₁_     : ∀ {Γ d T} → Γ ⊬[ ⇑ ] _ → elim (term ⇓) d   → Γ ⊬[ d ] T
    _#₂_     : ∀ {Γ d I O} → Γ ⊢[ ⇑ ] I → Γ E⊬[ d ] I ↝ O → Γ ⊬[ d ] O
    [_:∋:_]  : ∀ {Γ} → (T : type) → Γ ⊬[ ⇓ ] T            → Γ ⊬[ ⇑ ] _

instance
  BTermRaw : ∀ {Γ d T} → Γ B⊬[ d ] T ↪ term d
  ⌊_⌋ {{BTermRaw}} (not-canonical {c} x) = C c
  ⌊_⌋ {{BTermRaw}} (unsafe-inv q _)      = inv ⌊ q ⌋
  ⌊_⌋ {{BTermRaw}} (bad-split {c₁        = c₁} {c₂} t _) = ⌊ t ⌋ # split c₁ c₂
  ⌊_⌋ {{BTermRaw}} (out-of-scope {x} _)  = var x
  ⌊_⌋ {{BTermRaw}} (bad-function {s      = s} f _) = ⌊ f ⌋ # apply s
  ⌊_⌋ {{BTermRaw}} (bad-fst p _)         = ⌊ p ⌋ # fst
  ⌊_⌋ {{BTermRaw}} (bad-snd p _)         = ⌊ p ⌋ # snd

  ETermRaw : ∀ {Γ d T} → Γ ⊬[ d ] T ↪ term d
  ⌊_⌋ {{ETermRaw}} (because e)        = ⌊ e ⌋
  ⌊_⌋ {{ETermRaw}} (C (lam b))        = C (lam ⌊ b ⌋)
  ⌊_⌋ {{ETermRaw}} (C (su t))         = C (su ⌊ t ⌋)
  ⌊_⌋ {{ETermRaw}} (C (inj₁ t))       = C (inj₁ ⌊ t ⌋)
  ⌊_⌋ {{ETermRaw}} (C (inj₂ t))       = C (inj₂ ⌊ t ⌋)
  ⌊_⌋ {{ETermRaw}} (C (pair₁ t₁ t₂))  = C (pair ⌊ t₁ ⌋ t₂)
  ⌊_⌋ {{ETermRaw}} (C (pair₂ t₁ t₂))  = C (pair ⌊ t₁ ⌋ ⌊ t₂ ⌋)
  ⌊_⌋ {{ETermRaw}} (inv t)            = inv ⌊ t ⌋
  ⌊_⌋ {{ETermRaw}} [ T :∋: t ]        = [ T :∋: ⌊ t ⌋ ]
  ⌊_⌋ {{ETermRaw}} (t #₁ e)           = ⌊ t ⌋ # e
  ⌊_⌋ {{ETermRaw}} (t #₂ apply x)     = ⌊ t ⌋ # apply ⌊ x ⌋
  ⌊_⌋ {{ETermRaw}} (t #₂ iter₁ fs fz) = ⌊ t ⌋ # split ⌊ fs ⌋ fz
  ⌊_⌋ {{ETermRaw}} (t #₂ iter₂ fs fz) = ⌊ t ⌋ # split ⌊ fs ⌋ ⌊ fz ⌋
  ⌊_⌋ {{ETermRaw}} (t #₂ case₁ cX cY) = ⌊ t ⌋ # split ⌊ cX ⌋ cY
  ⌊_⌋ {{ETermRaw}} (t #₂ case₂ cX cY) = ⌊ t ⌋ # split ⌊ cX ⌋ ⌊ cY ⌋

-- * Type-checking

-- ** View on variable lookup

data _∈-view_ : ℕ → context → Set where
  yes : ∀ {T Γ} → (x : T ∈ Γ)  → ⌊ x ⌋ ∈-view Γ
  no  : ∀ {Γ n} → n ≥ length Γ → n ∈-view Γ

_∈?_ : ∀ n Γ → n ∈-view Γ
_     ∈? ε      = no z≤n
zero  ∈? Γ ▹ T  = yes here
suc n ∈? Γ ▹ T
  with n ∈? Γ
... | yes t     = yes (there t)
... | no q      = no (s≤s q)

-- ** View on typing

data Dir : dir → Set where
  _∈  : term ⇑        → Dir ⇑
  _∋_ : type → term ⇓ → Dir ⇓

instance
  DirRaw : ∀ {Γ d T} → Γ ⊢[ d ] T ↪ Dir d
  ⌊_⌋ {{DirRaw {d = ⇑}}} e    = ⌊ e ⌋ ∈
  ⌊_⌋ {{DirRaw {d = ⇓}{T}}} e = T ∋ ⌊ e ⌋

  EDirRaw : ∀ {Γ d T} → Γ ⊬[ d ] T ↪ Dir d
  ⌊_⌋ {{EDirRaw {d = ⇑}}} e    = ⌊ e ⌋ ∈
  ⌊_⌋ {{EDirRaw {d = ⇓}{T}}} e = T ∋ ⌊ e ⌋

data _⊢[_]-view_ (Γ : context)(d : dir) : Dir d → Set where
  yes : ∀ {T} (Δ : Γ ⊢[ d ] T)   → Γ ⊢[ d ]-view ⌊ Δ ⌋
  no  : ∀ {T} (¬Δ : Γ ⊬[ d ] T)  → Γ ⊢[ d ]-view ⌊ ¬Δ ⌋

isYes : ∀ {Γ T t} → Γ ⊢[ ⇓ ]-view T ∋ t → Set
isYes (yes Δ) = ⊤
isYes (no ¬Δ) = ⊥

lemma : ∀ {Γ T t} → (pf : Γ ⊢[ ⇓ ]-view T ∋ t) → isYes pf → Γ ⊢ T ∋ t
lemma (yes Δ) tt = well-typed Δ
lemma (no _) ()

-- XXX: Mutually-recursive to please the termination checker
_⊢?_∋_ : (Γ : context)(T : type)(t : term ⇓) → Γ ⊢[ ⇓ ]-view T ∋ t
_⊢?_∈  : (Γ : context)(t : term ⇑) → Γ ⊢[ ⇑ ]-view t ∈

_⊢?_∋C_ : (Γ : context)(T : type)(t : can (term ⇓)) → Γ ⊢[ ⇓ ]-view T ∋ C t

_!_∋_⊢?_∋#_  : (Γ : context)(I : type)(Δt : Γ ⊢[ ⇑ ] I)(T : type)(e : elim (term ⇓) ⇓) → Γ ⊢[ ⇓ ]-view T ∋ (⌊ Δt ⌋ # e)
_!_∋_⊢?_∈#   : (Γ : context)(T : type)(Δt : Γ ⊢[ ⇑ ] T)(e : elim (term ⇓) ⇑) → Γ ⊢[ ⇑ ]-view (⌊ Δt ⌋ # e) ∈

Γ ⊢? T ∋ C t      = Γ ⊢? T ∋C t
Γ ⊢? T ∋ inv t
  with Γ ⊢? t ∈
... | no ¬Δ       = no (inv ¬Δ)
... | yes {T'} Δ
    with T' ≟ T
... | yes refl    = yes (inv Δ)
... | no ¬p       = no (because (unsafe-inv Δ ¬p))
Γ ⊢? A ∋ t # e
  with Γ ⊢? t ∈
... | no ¬Δt      = no (¬Δt #₁ e)
... | yes {T} Δt  = Γ ! T ∋ Δt ⊢? A ∋# e

Γ ⊢? var k ∈
  with k ∈? Γ
... | yes x      = yes (var x)
... | no ¬q      = no (because (out-of-scope ¬q))
Γ ⊢? t # e ∈
  with Γ ⊢? t ∈
... | no ¬Δt     = no (¬Δt #₁ e)
... | yes {T} Δt = Γ ! T ∋ Δt ⊢? e ∈#
Γ ⊢? [ T :∋: t ] ∈
  with Γ ⊢? T ∋ t
... | yes Δt     = yes [ T :∋: Δt by refl ]
... | no ¬Δt     = no [ T :∋: ¬Δt ]

Γ ⊢? unit ∋C tt       = yes (C tt)
Γ ⊢? unit ∋C pair _ _ = no (because (not-canonical (λ {()})))
Γ ⊢? unit ∋C lam _    = no (because (not-canonical (λ {()})))
Γ ⊢? unit ∋C ze       = no (because (not-canonical (λ {()})))
Γ ⊢? unit ∋C su _     = no (because (not-canonical (λ {()})))
Γ ⊢? unit ∋C inj₁ _   = no (because (not-canonical (λ {()})))
Γ ⊢? unit ∋C inj₂ _   = no (because (not-canonical (λ {()})))

Γ ⊢? A * B ∋C pair t₁ t₂
  with Γ ⊢? A ∋ t₁ | Γ ⊢? B ∋ t₂
... | yes Δ₁ | yes Δ₂ = yes (C (pair Δ₁ Δ₂))
... | yes Δ₁ | no ¬Δ₂ = no (C (pair₂ Δ₁ ¬Δ₂))
... | no ¬Δ₁ | _      = no (C (pair₁ ¬Δ₁ t₂))
Γ ⊢? A * B ∋C tt      = no (because (not-canonical (λ {()})))
Γ ⊢? A * B ∋C lam _   = no (because (not-canonical (λ {()})))
Γ ⊢? A * B ∋C ze      = no (because (not-canonical (λ {()})))
Γ ⊢? A * B ∋C su _    = no (because (not-canonical (λ {()})))
Γ ⊢? A * B ∋C inj₁ _  = no (because (not-canonical (λ {()})))
Γ ⊢? A * B ∋C inj₂ _  = no (because (not-canonical (λ {()})))

Γ ⊢? A ⇒ B ∋C lam b
  with Γ ▹ A ⊢? B ∋ b
... | yes Δ            = yes (C (lam Δ))
... | no ¬Δ            = no (C (lam ¬Δ))
Γ ⊢? A ⇒ B ∋C tt       = no (because (not-canonical (λ {()})))
Γ ⊢? A ⇒ B ∋C ze       = no (because (not-canonical (λ {()})))
Γ ⊢? A ⇒ B ∋C su x     = no (because (not-canonical (λ {()})))
Γ ⊢? A ⇒ B ∋C pair _ _ = no (because (not-canonical (λ {()})))
Γ ⊢? A ⇒ B ∋C inj₁ _   = no (because (not-canonical (λ {()})))
Γ ⊢? A ⇒ B ∋C inj₂ _   = no (because (not-canonical (λ {()})))

Γ ⊢? nat ∋C ze       = yes (C ze)
Γ ⊢? nat ∋C su n
  with Γ ⊢? nat ∋ n
... | yes Δ          = yes (C (su Δ))
... | no ¬Δ          = no (C (su ¬Δ))
Γ ⊢? nat ∋C tt       = no (because (not-canonical (λ {()})))
Γ ⊢? nat ∋C pair _ _ = no (because (not-canonical (λ {()})))
Γ ⊢? nat ∋C lam _    = no (because (not-canonical (λ {()})))
Γ ⊢? nat ∋C inj₁ _   = no (because (not-canonical (λ {()})))
Γ ⊢? nat ∋C inj₂ _   = no (because (not-canonical (λ {()})))

Γ ⊢? A + B ∋C inj₁ t
  with Γ ⊢? A ∋ t
... | yes Δ            = yes (C (inj₁ Δ))
... | no ¬Δ            = no (C (inj₁ ¬Δ))
Γ ⊢? A + B ∋C inj₂ t
  with Γ ⊢? B ∋ t
... | yes Δ            = yes (C (inj₂ Δ))
... | no ¬Δ            = no (C (inj₂ ¬Δ))
Γ ⊢? A + B ∋C  tt      = no (because (not-canonical (λ {()})))
Γ ⊢? A + B ∋C pair _ _ = no (because (not-canonical (λ {()})))
Γ ⊢? A + B ∋C lam _    = no (because (not-canonical (λ {()})))
Γ ⊢? A + B ∋C ze       = no (because (not-canonical (λ {()})))
Γ ⊢? A + B ∋C su _     = no (because (not-canonical (λ {()})))

Γ ! nat ∋ Δt ⊢? A ∋# split fs fz
    with Γ ▹ A ⊢? A ∋ fs | Γ ⊢? A ∋ fz
... | yes Δfs | yes Δfz           = yes (Δt # iter Δfs Δfz)
... | yes Δfs | no ¬Δfz           = no (Δt #₂ iter₂ Δfs ¬Δfz)
... | no ¬Δfs | _                 = no (Δt #₂ iter₁ ¬Δfs fz)
Γ ! X + Y ∋ Δt ⊢? A ∋# split cX cY
  with (X ∷ Γ) ⊢? A ∋ cX | (Y ∷ Γ) ⊢? A ∋ cY
... | yes ΔcX | yes ΔcY           = yes (Δt # case ΔcX ΔcY)
... | yes ΔcX | no ¬ΔcY           = no (Δt #₂ case₂ ΔcX ¬ΔcY)
... | no ¬ΔcX | _                 = no (Δt #₂ case₁ ¬ΔcX cY)
Γ ! unit ∋ Δt ⊢? A ∋# split _ _   = no (because (bad-split Δt (λ {()})))
Γ ! _ ⇒ _ ∋ Δt ⊢? A ∋# split _ _  = no (because (bad-split Δt (λ {()})))
Γ ! _ * _ ∋ Δt ⊢? A ∋# split _ _  = no (because (bad-split Δt (λ {()})))

Γ ! A ⇒ B ∋ Δf ⊢? apply s ∈#
    with Γ ⊢? A ∋ s
... | yes Δs                  = yes (Δf # apply Δs)
... | no ¬Δs                  = no (Δf #₂ apply ¬Δs)
Γ ! unit ∋ Δf ⊢? apply _ ∈#   = no (because (bad-function Δf λ {()}))
Γ ! nat ∋ Δf ⊢? apply _ ∈#    = no (because (bad-function Δf λ {()}))
Γ ! _ + _ ∋ Δf ⊢? apply _ ∈#  = no (because (bad-function Δf λ {()}))
Γ ! _ * _ ∋ Δf ⊢? apply _ ∈#  = no (because (bad-function Δf λ {()}))

Γ ! A * B ∋ Δp ⊢? fst ∈#  = yes (Δp # fst)
Γ ! unit ∋ Δp ⊢? fst ∈#   = no (because (bad-fst Δp (λ {()})))
Γ ! nat ∋ Δp ⊢? fst ∈#    = no (because (bad-fst Δp (λ {()})))
Γ ! _ + _ ∋ Δp ⊢? fst ∈#  = no (because (bad-fst Δp (λ {()})))
Γ ! _ ⇒ _ ∋ Δp ⊢? fst ∈#  = no (because (bad-fst Δp (λ {()})))

Γ ! A * B ∋ Δp ⊢? snd ∈#  = yes (Δp # snd)
Γ ! unit ∋ Δp ⊢? snd ∈#   = no (because (bad-snd Δp (λ {()})))
Γ ! nat ∋ Δp ⊢? snd ∈#    = no (because (bad-snd Δp (λ {()})))
Γ ! _ + _ ∋ Δp ⊢? snd ∈#  = no (because (bad-snd Δp (λ {()})))
Γ ! _ ⇒ _ ∋ Δp ⊢? snd ∈#  = no (because (bad-snd Δp (λ {()})))

-- ** Tests

nat∋t1' : [] ⊢ nat ∋ t1
nat∋t1' = lemma ([] ⊢? nat ∋ t1) tt

T1 : type
T1 = nat ⇒ (unit + unit)

T2 : type
T2 = (nat + unit) ⇒ (unit + unit)

T1∋t2 : [] ⊢ T1 ∋ t2
T1∋t2 = lemma ([] ⊢? T1 ∋ t2) tt

T2∋t2 : [] ⊢ T2 ∋ t2
T2∋t2 = lemma ([] ⊢? T2 ∋ t2) tt

max_stars_repo_name: pedagand/typechecker-evolution

max_issues_repo_name: pedagand/typechecker-evolution

max_forks_repo_name: pedagand/typechecker-evolution


text:
-- Andreas 2015-01-07 fixing polarity of projection-like functions

-- {-# OPTIONS -v tc.polarity:20 -v tc.proj.like:10 #-}
-- {-# OPTIONS -v tc.conv.elim:25 --show-implicit #-}

open import Common.Size

-- List covariant covariant
data List (i : Size) (A : Set) : Set where
  [] : List i A
  cons : ∀{j : Size< i} → A → List j A → List i A

-- Id mixed mixed mixed covariant
-- Id is projection-like in argument l
Id : ∀{i A} (l : List i A) → Set → Set
Id [] X = X
Id (cons _ _) X = X

-- should pass
cast : ∀{i A} (l : List i A) → Id l (List i A) → Id l (List ∞ A)
cast l x = x

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda