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

module Definition.Conversion.Soundness where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Conversion
open import Definition.Conversion.Whnf
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.NeTypeEq

open import Tools.Product
import Tools.PropositionalEquality as PE

mutual
  -- Algorithmic equality of neutrals is well-formed.
  soundness~↑! : ∀ {k l A lA Γ} → Γ ⊢ k ~ l ↑! A ^ lA → Γ ⊢ k ≡ l ∷ A ^ [ ! , lA ]
  soundness~↑! (var-refl x x≡y) = PE.subst (λ y → _ ⊢ _ ≡ var y ∷ _ ^ _) x≡y (refl x)
  soundness~↑! (app-cong {rF = !} k~l x₁) = app-cong (soundness~↓! k~l) (soundnessConv↑Term x₁)
  soundness~↑! (app-cong {rF = %} k~l x₁) = app-cong (soundness~↓! k~l) (let _ , _ , y = soundness~↑% x₁ in y)
  soundness~↑! (natrec-cong x₁ x₂ x₃ k~l) =
    natrec-cong (soundnessConv↑ x₁) (soundnessConv↑Term x₂)
                (soundnessConv↑Term x₃) (soundness~↓! k~l)
  soundness~↑! (Emptyrec-cong x₁ k~l) = let ⊢k , ⊢l , _ = soundness~↑% k~l in
    Emptyrec-cong (soundnessConv↑ x₁) ⊢k ⊢l
  soundness~↑! (Id-cong X x x₁) = Id-cong (soundness~↓! X) (soundnessConv↑Term x) (soundnessConv↑Term x₁)
  soundness~↑! (Id-ℕ X x) = Id-cong (refl (ℕⱼ (wfEqTerm (soundness~↓! X)))) (soundness~↓! X) (soundnessConv↑Term x)
  soundness~↑! (Id-ℕ0 X) = let XX = soundness~↓! X in Id-cong (refl (ℕⱼ (wfEqTerm XX))) (refl (zeroⱼ (wfEqTerm XX))) XX
  soundness~↑! (Id-ℕS x X) = let XX = soundness~↓! X in Id-cong (refl (ℕⱼ (wfEqTerm XX))) (suc-cong (soundnessConv↑Term x)) XX
  soundness~↑! (Id-U X x) = Id-cong (refl (univ 0<1 (wfEqTerm (soundness~↓! X)))) (soundness~↓! X) (soundnessConv↑Term x)
  soundness~↑! (Id-Uℕ X) = let XX = soundness~↓! X in Id-cong (refl (univ 0<1 (wfEqTerm XX))) (refl (ℕⱼ (wfEqTerm XX))) XX
  soundness~↑! (Id-UΠ x X) = let XX = soundness~↓! X
                                 xx = soundnessConv↑Term x
                             in Id-cong (refl (univ 0<1 (wfEqTerm XX))) xx XX
  soundness~↑! (cast-cong X x x₁ x₂ x₃) = cast-cong (soundness~↓! X) (soundnessConv↑Term x) (soundnessConv↑Term x₁) x₂ x₃
  soundness~↑! (cast-ℕ X x x₁ x₂) = let XX = soundness~↓! X in cast-cong (refl (ℕⱼ (wfEqTerm XX))) XX (soundnessConv↑Term x) x₁ x₂
  soundness~↑! (cast-ℕℕ X x x₁) = let XX = soundness~↓! X in cast-cong (refl (ℕⱼ (wfEqTerm XX))) (refl (ℕⱼ (wfEqTerm XX))) XX x x₁
  soundness~↑! (cast-Π x X x₁ x₂ x₃) = cast-cong (soundnessConv↑Term x) (soundness~↓! X) (soundnessConv↑Term x₁) x₂ x₃
  soundness~↑! (cast-Πℕ x x₁ x₂ x₃) = let XX = (soundnessConv↑Term x) in cast-cong XX (refl (ℕⱼ (wfEqTerm XX))) (soundnessConv↑Term x₁) x₂ x₃
  soundness~↑! (cast-ℕΠ x x₁ x₂ x₃) = let XX = (soundnessConv↑Term x) in cast-cong (refl (ℕⱼ (wfEqTerm XX))) XX (soundnessConv↑Term x₁) x₂ x₃
  soundness~↑! (cast-ΠΠ%! x x₁ x₂ x₃ x₄) = cast-cong (soundnessConv↑Term x) (soundnessConv↑Term x₁) (soundnessConv↑Term x₂) x₃ x₄
  soundness~↑! (cast-ΠΠ!% x x₁ x₂ x₃ x₄) = cast-cong (soundnessConv↑Term x) (soundnessConv↑Term x₁) (soundnessConv↑Term x₂) x₃ x₄

  soundness~↑% : ∀ {k l A lA Γ} → Γ ⊢ k ~ l ↑% A ^ lA  →  Γ ⊢ k ∷ A ^ [ % , lA ] × Γ ⊢ l ∷ A ^ [ % , lA ] × Γ ⊢ k ≡ l ∷ A ^ [ % , lA ]
  soundness~↑% (%~↑ ⊢k ⊢l) =  ⊢k , ⊢l , proof-irrelevance ⊢k ⊢l

  soundness~↑ : ∀ {k l A rA lA Γ} → Γ ⊢ k ~ l ↑ A ^ [ rA , lA ] → Γ ⊢ k ≡ l ∷ A ^ [ rA , lA ]
  soundness~↑ (~↑! x) = soundness~↑! x
  soundness~↑ (~↑% x) = let _ , _ , y = soundness~↑% x in y

  -- Algorithmic equality of neutrals in WHNF is well-formed.
  soundness~↓! : ∀ {k l A lA Γ} → Γ ⊢ k ~ l ↓! A ^ lA → Γ ⊢ k ≡ l ∷ A ^ [ ! , lA ]
  soundness~↓! ([~] A₁ D whnfA k~l) = conv (soundness~↑! k~l) (subset* D)

  -- Algorithmic equality of types is well-formed.
  soundnessConv↑ : ∀ {A B rA Γ} → Γ ⊢ A [conv↑] B ^ rA → Γ ⊢ A ≡ B ^ rA
  soundnessConv↑ ([↑] A′ B′ D D′ whnfA′ whnfB′ A′<>B′) =
    trans (subset* D) (trans (soundnessConv↓ A′<>B′) (sym (subset* D′)))

  -- Algorithmic equality of types in WHNF is well-formed.
  soundnessConv↓ : ∀ {A B rA Γ} → Γ ⊢ A [conv↓] B ^ rA → Γ ⊢ A ≡ B ^ rA
  soundnessConv↓ (U-refl PE.refl ⊢Γ) = refl (Uⱼ ⊢Γ)
  soundnessConv↓ (univ x₂) = univ (soundnessConv↓Term x₂)

  -- Algorithmic equality of terms is well-formed.
  soundnessConv↑Term : ∀ {a b A lA Γ} → Γ ⊢ a [conv↑] b ∷ A ^ lA → Γ ⊢ a ≡ b ∷ A ^ [ ! , lA ]
  soundnessConv↑Term ([↑]ₜ B t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u) =
    conv (trans (subset*Term d)
                (trans (soundnessConv↓Term t<>u)
                       (sym (subset*Term d′))))
         (sym (subset* D))

  -- Algorithmic equality of terms in WHNF is well-formed.
  soundnessConv↓Term : ∀ {a b A lA Γ} → Γ ⊢ a [conv↓] b ∷ A ^ lA → Γ ⊢ a ≡ b ∷ A ^ [ ! , lA ]
  soundnessConv↓Term (ne x) = soundness~↓! x
  soundnessConv↓Term (ℕ-refl ⊢Γ) = refl (ℕⱼ ⊢Γ)
  soundnessConv↓Term (Empty-refl PE.refl ⊢Γ) = refl (Emptyⱼ ⊢Γ)
  soundnessConv↓Term (Π-cong PE.refl PE.refl PE.refl PE.refl l< l<' F c c₁) =
    Π-cong l< l<' F (soundnessConv↑Term c) (soundnessConv↑Term c₁)
  soundnessConv↓Term (∃-cong PE.refl F c c₁) =
    ∃-cong F (soundnessConv↑Term c) (soundnessConv↑Term c₁)
  soundnessConv↓Term (ℕ-ins x) = soundness~↓! x
  -- soundnessConv↓Term (Empty-ins x) = soundness~↓% x
  soundnessConv↓Term (ne-ins t u x x₁) =
    let whnfM , neA , neB = ne~↓! x₁
        X = soundness~↓! x₁
        _ , t∷M , _ = syntacticEqTerm X
        _ , M≡A' = neTypeEq neA t∷M t -- soundnessConv↑ M≡A
    in conv X M≡A'
  soundnessConv↓Term (zero-refl ⊢Γ) = refl (zeroⱼ ⊢Γ)
  soundnessConv↓Term (suc-cong c) = suc-cong (soundnessConv↑Term c)
  soundnessConv↓Term (η-eq l< l<' F x x₁ y y₁ c) = η-eq l< l<' F x x₁ (soundnessConv↑Term c)
  soundnessConv↓Term (U-refl PE.refl ⊢Γ) = refl (univ 0<1 ⊢Γ)

app-cong′ : ∀ {Γ k l t v F rF lF G lG lΠ}
          → Γ ⊢ k ~ l ↓! Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ ι lΠ
          → Γ ⊢ t [genconv↑] v ∷ F ^ [ rF , ι lF ]
          → Γ ⊢ k ∘ t ^ lΠ ~ l ∘ v ^ lΠ ↑ G [ t ] ^ [ ! , ι lG ]
app-cong′ k~l t=v = ~↑! (app-cong k~l t=v)

natrec-cong′ : ∀ {Γ k l h g a b F lF G}
             → Γ ∙ ℕ ^ [ ! , ι ⁰ ]  ⊢ F [conv↑] G ^ [ ! , ι lF ]
             → Γ ⊢ a [conv↑] b ∷ F [ zero ] ^ ι lF
             → Γ ⊢ h [conv↑] g ∷ Π ℕ ^ ! ° ⁰ ▹ (F ^ ! ° lF ▹▹ F [ suc (var 0) ]↑ ° lF ° lF) ° lF ° lF ^ ι lF
             → Γ ⊢ k ~ l ↓! ℕ ^ ι ⁰
             → Γ ⊢ natrec lF F a h k ~ natrec lF G b g l ↑ F [ k ] ^ [ ! , ι lF ]
natrec-cong′ F=G a=b h=g k~l = ~↑! (natrec-cong F=G a=b h=g k~l)

Emptyrec-cong′ : ∀ {Γ k l F lF lEmpty G}
               → Γ ⊢ F [conv↑] G ^ [ ! , ι lF ]
               → Γ ⊢ k ~ l ↑% Empty lEmpty ^ ι lEmpty
               → Γ ⊢ Emptyrec lF lEmpty F k ~ Emptyrec lF lEmpty G l ↑ F ^ [ ! , ι lF ]
Emptyrec-cong′ F=G k~l = ~↑! (Emptyrec-cong F=G k~l)

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
{-
This second-order term syntax was created from the following second-order syntax description:

syntax Empty | E

type
  𝟘 : 0-ary

term
  abort : 𝟘  ->  α

theory
  (𝟘η) e : 𝟘  c : α |> abort(e) = c
-}

module Empty.Syntax where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive

open import SOAS.Metatheory.Syntax

open import Empty.Signature

private
  variable
    Γ Δ Π : Ctx
    α : ET
    𝔛 : Familyₛ

-- Inductive term declaration
module E:Terms (𝔛 : Familyₛ) where

  data E : Familyₛ where
    var  : ℐ ⇾̣ E
    mvar : 𝔛 α Π → Sub E Π Γ → E α Γ

    abort : E 𝟘 Γ → E α Γ

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  Eᵃ : MetaAlg E
  Eᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (abortₒ ⋮ a) → abort a
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module Eᵃ = MetaAlg Eᵃ

  module _ {𝒜 : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜) where

    open MetaAlg 𝒜ᵃ

    𝕤𝕖𝕞 : E ⇾̣ 𝒜
    𝕊 : Sub E Π Γ → Π ~[ 𝒜 ]↝ Γ
    𝕊 (t ◂ σ) new = 𝕤𝕖𝕞 t
    𝕊 (t ◂ σ) (old v) = 𝕊 σ v
    𝕤𝕖𝕞 (mvar 𝔪 mε) = 𝑚𝑣𝑎𝑟 𝔪 (𝕊 mε)
    𝕤𝕖𝕞 (var v) = 𝑣𝑎𝑟 v

    𝕤𝕖𝕞 (abort a) = 𝑎𝑙𝑔 (abortₒ ⋮ 𝕤𝕖𝕞 a)

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ Eᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ E α Γ) → 𝕤𝕖𝕞 (Eᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      ⟨𝑎𝑙𝑔⟩ (abortₒ ⋮ _) = refl

      𝕊-tab : (mε : Π ~[ E ]↝ Γ)(v : ℐ α Π) → 𝕊 (tabulate mε) v ≡ 𝕤𝕖𝕞 (mε v)
      𝕊-tab mε new = refl
      𝕊-tab mε (old v) = 𝕊-tab (mε ∘ old) v

    module _ (g : E ⇾̣ 𝒜)(gᵃ⇒ : MetaAlg⇒ Eᵃ 𝒜ᵃ g) where

      open MetaAlg⇒ gᵃ⇒

      𝕤𝕖𝕞! : (t : E α Γ) → 𝕤𝕖𝕞 t ≡ g t
      𝕊-ix : (mε : Sub E Π Γ)(v : ℐ α Π) → 𝕊 mε v ≡ g (index mε v)
      𝕊-ix (x ◂ mε) new = 𝕤𝕖𝕞! x
      𝕊-ix (x ◂ mε) (old v) = 𝕊-ix mε v
      𝕤𝕖𝕞! (mvar 𝔪 mε) rewrite cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-ix mε))
        = trans (sym ⟨𝑚𝑣𝑎𝑟⟩) (cong (g ∘ mvar 𝔪) (tab∘ix≈id mε))
      𝕤𝕖𝕞! (var v) = sym ⟨𝑣𝑎𝑟⟩

      𝕤𝕖𝕞! (abort a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩

-- Syntax instance for the signature
E:Syn : Syntax
E:Syn = record
  { ⅀F = ⅀F
  ; ⅀:CS = ⅀:CompatStr
  ; mvarᵢ = E:Terms.mvar
  ; 𝕋:Init = λ 𝔛 → let open E:Terms 𝔛 in record
    { ⊥ = E ⋉ Eᵃ
    ; ⊥-is-initial = record { ! = λ{ {𝒜 ⋉ 𝒜ᵃ} → 𝕤𝕖𝕞 𝒜ᵃ ⋉ 𝕤𝕖𝕞ᵃ⇒ 𝒜ᵃ }
    ; !-unique = λ{ {𝒜 ⋉ 𝒜ᵃ} (f ⋉ fᵃ⇒) {x = t} → 𝕤𝕖𝕞! 𝒜ᵃ f fᵃ⇒ t } } } }

-- Instantiation of the syntax and metatheory
open Syntax E:Syn public
open E:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands Eᵃ public
open import SOAS.Metatheory E:Syn public

ext: agda

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
postulate
  A : Set

f : {{_ : A}} → A
f = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Surjection
open import Oscar.Class.Smap
open import Oscar.Data.Constraint

module Oscar.Class.Surjextensionality where

module Surjextensionality
  {𝔬₁ 𝔯₁ ℓ₁ 𝔬₂ 𝔯₂ ℓ₂} {𝔒₁ : Ø 𝔬₁} {𝔒₂ : Ø 𝔬₂}
  (_∼₁_ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁)
  (_∼̇₁_ : ∀ {x y} → x ∼₁ y → x ∼₁ y → Ø ℓ₁)
  (_∼₂_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂)
  (_∼̇₂_ : ∀ {x y} → x ∼₂ y → x ∼₂ y → Ø ℓ₂)
  (surjection : Surjection.type 𝔒₁ 𝔒₂)
  (smap : Smap.type _∼₁_ _∼₂_ surjection surjection)
  where
  open ℭLASS (_∼₁_ ,, {- FIXME including `(λ {x y} → _∼̇₁_ {x} {y}) ,, ` leads to instance search depth exhausted in Oscar.Data.Surjextenscollation -} _∼₂_ ,, (λ {x y} → _∼̇₂_ {x} {y}) ,, surjection ,, (λ {x y} → smap {x} {y})) (∀ x y (f₁ f₂ : x ∼₁ y) → f₁ ∼̇₁ f₂ → smap f₁ ∼̇₂ smap f₂) public
  TYPE = ∀ {x y} {f₁ f₂ : x ∼₁ y} → f₁ ∼̇₁ f₂ → smap f₁ ∼̇₂ smap f₂

module Surjextensionality!
  {𝔬₁ 𝔯₁ ℓ₁ 𝔬₂ 𝔯₂ ℓ₂} {𝔒₁ : Ø 𝔬₁} {𝔒₂ : Ø 𝔬₂}
  (_∼₁_ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁)
  (_∼̇₁_ : ∀ {x y} → _∼₁_ x y → _∼₁_ x y → Ø ℓ₁)
  (_∼₂_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂)
  (_∼̇₂_ : ∀ {x y} → _∼₂_ x y → _∼₂_ x y → Ø ℓ₂)
  ⦃ _ : Surjection.class 𝔒₁ 𝔒₂ ⦄
  ⦃ _ : Smap.class _∼₁_ _∼₂_ surjection surjection ⦄
  = Surjextensionality (_∼₁_) (λ {x y} → _∼̇₁_ {x} {y}) (_∼₂_) (λ {x y} → _∼̇₂_ {x} {y}) surjection (λ {x y} → smap {x = x} {y})

module _
  {𝔬₁ 𝔯₁ ℓ₁ 𝔬₂ 𝔯₂ ℓ₂} {𝔒₁ : Ø 𝔬₁} {𝔒₂ : Ø 𝔬₂}
  {∼₁ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁}
  {∼̇₁ : ∀ {x y} → ∼₁ x y → ∼₁ x y → Ø ℓ₁}
  {∼₂ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂}
  {∼̇₂ : ∀ {x y} → ∼₂ x y → ∼₂ x y → Ø ℓ₂}
  {surjection : Surjection.type 𝔒₁ 𝔒₂}
  {smap : Smap.type ∼₁ ∼₂ surjection surjection}
  where
  open Surjextensionality
    ∼₁
    (λ {x y} → ∼̇₁ {x} {y})
    ∼₂
    (λ {x y} → ∼̇₂ {x} {y})
    surjection
    (λ {x y} → smap {x = x} {y})
  surjextensionality : ⦃ _ : class ⦄ → TYPE
  surjextensionality = method _ _ _ _

module _
  {𝔬₁ 𝔯₁ ℓ₁ 𝔬₂ 𝔯₂ ℓ₂} {𝔒₁ : Ø 𝔬₁} {𝔒₂ : Ø 𝔬₂}
  {∼₁ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁}
  {∼̇₁ : ∀ {x y} → ∼₁ x y → ∼₁ x y → Ø ℓ₁}
  {∼₂ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂}
  (∼̇₂ : ∀ {x y} → ∼₂ x y → ∼₂ x y → Ø ℓ₂)
  {surjection : Surjection.type 𝔒₁ 𝔒₂}
  {smap : Smap.type ∼₁ ∼₂ surjection surjection}
  where
  open Surjextensionality
    ∼₁
    (λ {x y} → ∼̇₁ {x} {y})
    ∼₂
    (λ {x y} → ∼̇₂ {x} {y})
    surjection
    (λ {x y} → smap {x = x} {y})
  surjextensionality[_] : ⦃ _ : class ⦄ → TYPE
  surjextensionality[_] = surjextensionality
  ⟪⟫-surjextensionality[]-syntax = surjextensionality[_]
  syntax ⟪⟫-surjextensionality[]-syntax t x = ⟪ x ⟫[ t ]


text:
{-# OPTIONS --exact-split #-}
-- {-# OPTIONS -v tc.cover.splittree:10 #-}

open import Common.Prelude
open import Common.Equality

test : {m n : Nat} → m ≡ n → Nat
test {zero}  refl = zero
test {suc m} refl = suc m

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Data.Nat using (ℕ; suc)
open import Data.Fin using (Fin; zero; suc)

infix  9  #_
infixl 7  _·_
infix  6  ƛ_

data Term : ℕ → Set where
  #_  : ∀ {n : ℕ} → Fin n           → Term n
  ƛ_  : ∀ {n : ℕ} → Term (suc n)    → Term n
  _·_ : ∀ {n : ℕ} → Term n → Term n → Term n

Rename : ℕ → ℕ → Set
Rename n m = Fin n → Fin m

Subst : ℕ → ℕ → Set
Subst n m = Fin n → Term m

ext : ∀ {n m} → Rename n m → Rename (suc n) (suc m)
ext ρ zero    = zero
ext ρ (suc x) = suc (ρ x)

rename : ∀ {n m} → Rename n m → (Term n → Term m)
rename ρ (# x)   = # (ρ x)
rename ρ (ƛ M)   = ƛ (rename (ext ρ) M)
rename ρ (M · N) = rename ρ M · rename ρ N

exts : ∀ {n m} → Subst n m → Subst (suc n) (suc m)
exts σ zero    = # zero
exts σ (suc x) = rename suc (σ x)

subst : ∀ {n m} → Subst n m → (Term n → Term m)
subst σ (# x)   = σ x
subst σ (ƛ M)   = ƛ (subst (exts σ) M)
subst σ (M · N) = subst σ M · subst σ N

subst-zero : ∀ {n} → Term n → Subst (suc n) n
subst-zero M zero    = M
subst-zero M (suc x) = # x

infix 8 _[_]

_[_] : ∀ {n} → Term (suc n) → Term n → Term n
M [ N ] = subst (subst-zero N) M

max_stars_repo_name: iwilare/church-rosser

max_issues_repo_name: iwilare/church-rosser

max_forks_repo_name: iwilare/church-rosser


text:
module Formalization.PrimitiveRecursion where

import      Lvl
open import Data
open import Data.ListSized
open import Numeral.Finite
open import Numeral.Natural
open import Syntax.Number
open import Type{Lvl.𝟎}

-- Function(n) is a syntactic representation of primitive recursive functions of type (ℕⁿ → ℕ).
-- The syntax
data Function : ℕ → Type where
  -- Base cases
  Base        : Function(0)
  Successor   : Function(1)
  Projection  : ∀{n : ℕ} → (i : 𝕟(n)) → Function(n)

  -- Inductive cases
  Composition : ∀{m n : ℕ} → Function(n) → List(Function(m))(n) → Function(m)
  Recursion   : ∀{n : ℕ} → Function(n) → Function(𝐒(𝐒(n))) → Function(𝐒(n))

Primitive : Type
Primitive = ℕ

module _ where
  open import Data.ListSized.Functions
  open import Functional

  private variable m n   : ℕ
  private variable i     : 𝕟(n)
  private variable x v   : Primitive
  private variable xs vs : List(Primitive)(n)
  private variable f g   : Function(m)
  private variable fs gs : List(Function(m))(n)

  -- The operational semantics.
  data _$_⟹_ : ∀{m n} → List(Function(m))(n) → List(Primitive)(m) → List(Primitive)(n) → Type
  data _$_⟶_ : ∀{n} → Function(n) → List(Primitive)(n) → ℕ → Type where
    zero : (Base $ ∅ ⟶ 𝟎)
    succ : (Successor $ singleton(n) ⟶ 𝐒(n))
    proj : (Projection{n}(i) $ xs ⟶ index(i)(xs))
    comp : (f $ vs ⟶ v) → (gs $ xs ⟹ vs) → (Composition{m}{n} f gs $ xs ⟶ v)
    rec𝟎 : (f $ xs ⟶ v) → (Recursion f g $ (𝟎 ⊰ xs) ⟶ v)
    rec𝐒 : (Recursion f g $ (n ⊰ xs) ⟶ x) → (g $ (n ⊰ x ⊰ xs) ⟶ v) → (Recursion f g $ (𝐒(n) ⊰ xs) ⟶ v)
  data _$_⟹_ where
    base : (∅ $ xs ⟹ ∅)
    step : (f $ xs ⟶ v) → (fs $ xs ⟹ vs) → ((f ⊰ fs) $ xs ⟹ (v ⊰ vs))

  -- Functionally equivalent to `evaluate f (map(g ↦ evaluate g xs)(gs))`, but the termination checker does not accept that form.
  mapEvaluate : ∀{m n} → List(Function(m))(n) → List(Primitive)(m) → List(Primitive)(n)

  -- The denotational semantics.
  -- This is possible to encode into an Agda function because: Primitive recursive functions ⊆ Agda functions.
  -- `Base` is interpreted as the constant 0.
  -- `Successor` is interpreted as the successor function of ℕ.
  -- `Projection{n}(i)` is interpreted as the projection of the i:th element of ℕⁿ.
  -- `Composition(f)(gs)` is interpreted as generalized composition by using map on the arguments of a function.
  --    Specifically (f ∘ (map gs)).
  -- `Recursion(f)(g)` is interpreted as a "recursion constructor".
  --    This is used to construct a function `r` in which the following holds:
  --    • r(0   ,..xs) = f(..xs)
  --    • r(𝐒(n),..xs) = g(n,r(n,..xs),..xs)
  {-# TERMINATING #-} -- TODO: Terminated before but the termination checker in Agda version 2.6.2-9bed10c denies this (or in some random cases it gives an internal error at src/full/Agda/TypeChecking/Reduce/Fast.hs:1358)
  evaluate : ∀{n} → Function(n) → (List(Primitive)(n) → Primitive)
  evaluate {.𝟎}   (Base)                     ∅             = 𝟎
  evaluate {.𝐒(𝟎)}(Successor)                (singleton x) = 𝐒(x)
  evaluate {_}    (Projection(i))            xs            = index(i)(xs)
  evaluate {m}    (Composition{m}{n}(f)(gs)) xs            = evaluate{n} f (mapEvaluate{m}{n} gs xs)
  evaluate {𝐒(_)} (Recursion(f)(g))          (𝟎    ⊰ xs)   = evaluate f xs
  evaluate {𝐒(m)} (Recursion(f)(g))          (𝐒(n) ⊰ xs)   = evaluate{𝐒(𝐒(m))} g (n ⊰ (evaluate{𝐒 m} (Recursion(f)(g)) (n ⊰ xs) ⊰ xs))

  mapEvaluate          ∅        xs = ∅
  mapEvaluate{m}{𝐒(n)} (g ⊰ gs) xs = (evaluate{m} g xs) ⊰ (mapEvaluate{m}{n} gs xs)

  ------------------------------------------------------
  -- This section proves the equivalence between the operational and the denotational semantics. Or it can be interpreted as the correctness of one of the definitions by the other one.
  -- This equivalence should be obvious from the definitions.
  --

  open import Relator.Equals
  open import Relator.Equals.Proofs
  open import Syntax.Transitivity

  [⟹]-to-eval : (fs $ xs ⟹ vs) → (mapEvaluate fs xs ≡ vs)

  [⟶]-to-eval : (f $ xs ⟶ v) → (evaluate f xs ≡ v)
  [⟶]-to-eval zero = [≡]-intro
  [⟶]-to-eval succ = [≡]-intro
  [⟶]-to-eval {xs = _⊰_ {𝟎}   x xs} (proj {i = 𝟎})   = [≡]-intro
  [⟶]-to-eval {xs = _⊰_ {𝐒 n} x xs} (proj {i = 𝟎})   = [≡]-intro
  [⟶]-to-eval {xs = _⊰_ {𝐒 n} x xs} (proj {i = 𝐒 i}) = [≡]-intro
  [⟶]-to-eval (comp p q) with [⟶]-to-eval p | [⟹]-to-eval q
  ... | [≡]-intro | [≡]-intro = [≡]-intro
  [⟶]-to-eval (rec𝟎 p) with [⟶]-to-eval p
  ... | [≡]-intro = [≡]-intro
  [⟶]-to-eval (rec𝐒 p q) with [⟶]-to-eval p | [⟶]-to-eval q
  ... | [≡]-intro | [≡]-intro = [≡]-intro
  [⟹]-to-eval {fs = ∅}      {vs = ∅}      _           = [≡]-intro
  [⟹]-to-eval {fs = f ⊰ fs} {vs = v ⊰ vs} (step p ps) with [⟶]-to-eval p | [⟹]-to-eval {fs = fs} {vs = vs} ps
  ... | [≡]-intro | [≡]-intro = [≡]-intro

  eval-to-[⟹] : (mapEvaluate fs xs ≡ vs) → (fs $ xs ⟹ vs)

  {-# TERMINATING #-} -- TODO: See TODO above in eval
  eval-to-[⟶] : (evaluate f xs ≡ v) → (f $ xs ⟶ v)
  eval-to-[⟶] {f = Base}             {∅}           [≡]-intro = zero
  eval-to-[⟶] {f = Successor}        {singleton x} [≡]-intro = succ
  eval-to-[⟶] {f = Projection _}                   [≡]-intro = proj
  eval-to-[⟶] {f = Composition f gs} {xs}          p         = comp (eval-to-[⟶] p) (eval-to-[⟹] [≡]-intro)
  eval-to-[⟶] {f = Recursion f g}    {𝟎    ⊰ xs}   p         = rec𝟎(eval-to-[⟶] {f = f}{xs = xs} p)
  eval-to-[⟶] {f = Recursion f g}    {𝐒(n) ⊰ xs}   p         = rec𝐒 (eval-to-[⟶] [≡]-intro) (eval-to-[⟶] p)

  eval-to-[⟹] {fs = ∅}      [≡]-intro = base
  eval-to-[⟹] {fs = f ⊰ fs} [≡]-intro = step (eval-to-[⟶] [≡]-intro) (eval-to-[⟹] [≡]-intro)

  -- TODO: Is it possible to prove that _⟶_ terminates and normalizes by using [⟶]-to-eval (total and deterministic)?

  open import Function.Equals
  open import Logic
  open import Logic.Predicate

  -- When a function on lists of primitives are primitive recursive.
  PrimitiveRecursive : (List(Primitive)(n) → Primitive) → Stmt
  PrimitiveRecursive(f) = ∃(e ↦ evaluate e ⊜ f)

Const : Function(0) → ∀{n} → Function(n)
Const(c) = Composition(c) ∅

-- TODO: Would encoding pairs make this easier to implement (e.g. the Cantor Pairing Function?
--  This is used to construct a function `r` in which the following holds for its evaluation:
--  • r(0      ,..xs) = f(..xs)
--  • r(1      ,..xs) = g(..xs)
--  • r(𝐒(𝐒(n)),..xs) = h(n,r(𝐒(n),..xs),r(n,..xs),..xs)
-- Recursion₂ : ∀{n : ℕ} → Function(n) → Function(n) → Function(𝐒(𝐒(𝐒(n)))) → Function(𝐒(n))
-- Recursion₂{n} (f)(g)(h) = Composition(Projection(0)) (Helper ⊰ ∅) where
--   Recursion
--
--   Helper : Function(2)
--   Helper =
--

module Arithmetic where -- TODO: Prove that these are correct by `evaluate`
  Zero = Base

  Number : ℕ → Function(0)
  Number(𝟎)    = Zero
  Number(𝐒(n)) = Composition(Successor) (Number(n) ⊰ ∅)

  Swap₂ : Function(2) → Function(2)
  Swap₂(f) = Composition(f) (Projection(1) ⊰ Projection(0) ⊰ ∅)

  -- Addition (+) in ℕ.
  -- It describes the following function:
  --   evaluate(Addition)[𝟎   ,b] = 𝟎
  --   evaluate(Addition)[𝐒(a),b] = 𝐒(b)
  Addition : Function(2)
  Addition = Recursion(Projection(0)) (Composition Successor (Projection(1) ⊰ ∅))

  -- Multiplication (⋅) in ℕ.
  -- It describes the following function:
  --   evaluate(Multiplication)[𝟎   ,b] = 𝟎
  --   evaluate(Multiplication)[𝐒(a),b] = evaluate(Multiplication)[a,b] + b
  Multiplication : Function(2)
  Multiplication = Recursion (Const(Zero)) (Composition Addition (Projection(1) ⊰ Projection(2) ⊰ ∅))

  -- Exponentiation (^) in ℕ.
  -- It describes the following function:
  --   evaluate(Exponentiation)[a   ,0   ] = 1
  --   evaluate(Exponentiation)[a   ,𝐒(b)] = evaluate(Exponentiation)[a,b] ⋅ a
  Exponentiation : Function(2)
  Exponentiation = Swap₂(Recursion (Composition Successor (Const Zero ⊰ ∅)) (Composition Multiplication (Projection(1) ⊰ Projection(2) ⊰ ∅)))

  -- Factorial (!) in ℕ.
  -- It describes the following function:
  --   evaluate(Factorial)[𝟎   ] = 1
  --   evaluate(Factorial)[𝐒(a)] = 𝐒(a) ⋅ evaluate(Factorial)[a,b]
  Factorial : Function(1)
  Factorial = Recursion(Number(1)) (Composition Multiplication ((Composition Successor (Projection(0) ⊰ ∅)) ⊰ Projection(1) ⊰ ∅))

  -- Predecessor (𝐏) in ℕ.
  -- It describes the following function:
  --   evaluate(Predecessor)[𝟎   ] = 𝟎
  --   evaluate(Predecessor)[𝐒(a)] = a
  Predecessor : Function(1)
  Predecessor = Recursion(Zero) (Projection(0))

  -- Monus/Cut-off minus (−₀) in ℕ.
  -- It describes the following function:
  --   evaluate(Monus)[b,𝟎   ] = b
  --   evaluate(Monus)[b,𝐒(a)] = 𝐏(evaluate(Monus)[b,a])
  Monus : Function(2)
  Monus = Swap₂(Recursion(Projection(0)) (Composition Predecessor (Projection(1) ⊰ ∅)))

  -- Maximum (max) of ℕ² in ℕ.
  -- It describes the following function:
  --   evaluate(Max)[a,b] = a + (b −₀ a)
  Max : Function(2)
  Max = Composition(Addition) (Projection(0) ⊰ Swap₂(Monus) ⊰ ∅)

  -- Minimum (min) of ℕ² in ℕ.
  -- It describes the following function:
  --   evaluate(Min)[a,b] = (a + b) −₀ max(a,b)
  Min : Function(2)
  Min = Composition(Monus) (Addition ⊰ Max ⊰ ∅)

  -- It describes the following function:
  --   evaluate(Distance)[a,b] = max(x −₀ y , y −₀ x)
  Distance : Function(2)
  Distance = Composition(Addition) (Monus ⊰ Swap₂(Monus) ⊰ ∅)

  -- It describes the following function:
  --   evaluate(IsZero)[𝟎]    = 1
  --   evaluate(IsZero)[𝐒(_)] = 0
  IsZero : Function(1)
  IsZero = Recursion(Number(1)) (Const(Zero))

  -- It describes the following function:
  --   evaluate(IsZero)[𝟎]    = 0
  --   evaluate(IsZero)[𝐒(_)] = 1
  IsNonZero : Function(1)
  IsNonZero = Composition(IsZero) (IsZero ⊰ ∅)

  Eq : Function(2)
  Eq = Composition(IsZero) (Distance ⊰ ∅)

  -- It describes the following function:
  --   evaluate(Fibonacci)[𝟎]    = 0
  --   evaluate(Fibonacci)[𝐒(_)] = 1
  -- Fibonacci : Function(1)
  -- Fibonacci = Composition(Projection(0)) (Fib ⊰ ∅) where
  --   Fib : Function(2)
  --   Fib =

-- TODO: http://www.reluctantm.com/gcruttw/teaching/cpsc513.W2010/A3Solutions.pdf
-- TODO: http://ii.fmph.uniba.sk/cl/courses/1-AIN-625-lpp/0910zs/ln/doc/ch_p_gd.pdf

module Proofs where
  open import Functional
  open import Logic.Propositional
  open import Numeral.Natural.Oper
  open import Numeral.Natural.Oper.Comparisons
  open import Numeral.Natural.Oper.Proofs
  open import Relator.Equals
  open import Relator.Equals.Proofs
  open import Structure.Operator.Properties
  open import Structure.Relator.Properties
  open import Syntax.Transitivity

  addition-correctness : ∀{a b} → (evaluate Arithmetic.Addition (a ⊰ b ⊰ ∅) ≡ a + b)
  addition-correctness {𝟎}   {b} = [≡]-intro
  addition-correctness {𝐒 a} {b} = [≡]-with(𝐒) (addition-correctness {a}{b})

  multiplication-correctness : ∀{a b} → (evaluate Arithmetic.Multiplication (a ⊰ b ⊰ ∅) ≡ a ⋅ b)
  multiplication-correctness {𝟎}   {b} = [≡]-intro
  multiplication-correctness {𝐒 a} {b} =
    addition-correctness {evaluate Arithmetic.Multiplication (a ⊰ b ⊰ ∅)}{b}
    🝖 [≡]-with(_+ b) (multiplication-correctness {a}{b})
    🝖 symmetry(_≡_) ([⋅]-with-[𝐒]ₗ {a}{b})

  exponentiation-correctness : ∀{a b} → (evaluate Arithmetic.Exponentiation (a ⊰ b ⊰ ∅) ≡ a ^ b)
  exponentiation-correctness {a} {𝟎}   = [≡]-intro
  exponentiation-correctness {a} {𝐒 b} =
    multiplication-correctness {evaluate Arithmetic.Exponentiation (a ⊰ b ⊰ ∅)}{a}
    🝖 [≡]-with(_⋅ a) (exponentiation-correctness {a}{b})
    🝖 commutativity(_⋅_) {a ^ b}{a}

  factorial-correctness : ∀{a} → (evaluate Arithmetic.Factorial (a ⊰ ∅) ≡ a !)
  factorial-correctness {𝟎}   = [≡]-intro
  factorial-correctness {𝐒 a} =
    multiplication-correctness {𝐒 a}
    🝖 [≡]-with(𝐒(a) ⋅_) (factorial-correctness {a})

  predecessor-correctness : ∀{a} → (evaluate Arithmetic.Predecessor (a ⊰ ∅) ≡ 𝐏(a))
  predecessor-correctness {𝟎}   = [≡]-intro
  predecessor-correctness {𝐒 a} = [≡]-intro

  monus-correctness : ∀{a b} → (evaluate Arithmetic.Monus (a ⊰ b ⊰ ∅) ≡ a −₀ b)
  monus-correctness {a}   {𝟎}   = [≡]-intro
  monus-correctness {𝟎}   {𝐒 b} = predecessor-correctness{evaluate Arithmetic.Monus (𝟎 ⊰ b ⊰ ∅)} 🝖 [≡]-with(𝐏) (monus-correctness {𝟎}{b})
  monus-correctness {𝐒 a} {𝐒 b} =
    predecessor-correctness{evaluate Arithmetic.Monus (𝐒(a) ⊰ b ⊰ ∅)}
    🝖 [≡]-with(𝐏) (monus-correctness {𝐒 a}{b})
    🝖 symmetry(_≡_) ([−₀]-with-[𝐒]ᵣ {𝐒(a)}{b})

  isnonzero-correctness : ∀{a} → (evaluate Arithmetic.IsNonZero (a ⊰ ∅) ≡ ℕbool(a ≢? 𝟎))
  isnonzero-correctness {𝟎}   = [≡]-intro
  isnonzero-correctness {𝐒 a} = [≡]-intro

  iszero-correctness : ∀{a} → (evaluate Arithmetic.IsZero (a ⊰ ∅) ≡ ℕbool(a ≡? 𝟎))
  iszero-correctness {𝟎}   = [≡]-intro
  iszero-correctness {𝐒 a} = [≡]-intro

  -- TODO: Formalize "Function(1) is countably infinite". Maybe take some inspiration from https://proofwiki.org/wiki/Not_All_URM_Computable_Functions_are_Primitive_Recursive . Then prove that (ℕ → ℕ) is not countably infinite, and therefore not all computable functions are expressible primitive recursively (is this argument constructive?)

  open import Data.Tuple
  open import Function.Inverse
  open import Logic.Predicate
  open import Logic.Propositional
  open import Type.Size.Countable
  open import Structure.Function.Domain.Proofs
  open import Structure.Function using (congruence₁)
  open import Syntax.Function
  open import Syntax.Transitivity

  postulate Function-countablyInfinite : CountablyInfinite(Function(1))
  encodeFunction : Function(1) → ℕ
  encodeFunction = inv _ ⦃ bijective-to-invertible ⦃ bij = [∃]-proof Function-countablyInfinite ⦄ ⦄

  -- TODO: Use a lifted Numeral.Natural.Sequence.pairIndexing as a witness directly (instead of encodePair). Another alternative is (a ↦ b ↦ 2ᵃ⋅3ᵇ) if it is easier to construct f that way.
  postulate Function-value-pair-countablyInfinite : CountablyInfinite(Function(1) ⨯ ℕ)
  encodePair : (Function(1) ⨯ ℕ) → ℕ
  encodePair = inv _ ⦃ bijective-to-invertible ⦃ bij = [∃]-proof Function-value-pair-countablyInfinite ⦄ ⦄

  -- TODO: Is it possible to use Logic.DiagonalMethod for this proof?
  no-self-interpreter : ¬ ∃(interpret ↦ ∀{f}{n} → evaluate interpret (singleton (encodePair(f , n))) ≡ evaluate f (singleton n))
  no-self-interpreter ([∃]-intro interpret ⦃ p ⦄) = 𝐒-not-self(symmetry(_≡_) x) where
    postulate f : Function(1)
    postulate f-correctness : ∀{g} → (evaluate f (singleton(encodeFunction g)) ≡ encodePair(g , encodeFunction g))

    g : Function(1)
    g = Composition Successor (singleton (Composition interpret (singleton f)))

    x : evaluate g (singleton (encodeFunction g)) ≡ 𝐒(evaluate g (singleton (encodeFunction g)))
    x =
      evaluate g (singleton (encodeFunction g))                                   🝖[ _≡_ ]-[]
      𝐒(evaluate interpret (singleton(evaluate f (singleton(encodeFunction g))))) 🝖[ _≡_ ]-[ congruence₁(𝐒) (congruence₁(evaluate interpret) (congruence₁(singleton) f-correctness)) ]
      𝐒(evaluate interpret (singleton(encodePair(g , encodeFunction g))))         🝖[ _≡_ ]-[ congruence₁(𝐒) p ]
      𝐒(evaluate g (singleton(encodeFunction g)))                                 🝖-end

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --type-in-type #-}
-- {-# OPTIONS -v tc.pos:10 -v tc.polarity:10 #-}
-- Andreas, 2012-09-06, message on Agda list "Forget Hurken's paradox..."

module Issue690 where

infix 4 _≡_

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

data ⊥ : Set where

data D : Set where
  abs : ∀ {E : Set} → D ≡ E → (E → ⊥) → D

lam : (D → ⊥) → D
lam f = abs refl f

app : D → D → ⊥
app (abs refl f) d = f d

omega : D
omega = lam (λ x → app x x)

Omega : ⊥
Omega = app omega omega


text:
module Prelude.Empty where

open import Prelude.Erased

data ⊥ : Set where

⊥-elim : ∀ {a} {A : Set a} → ⊥ → A
⊥-elim ()
{-# INLINE ⊥-elim #-}

private postulate erasedBottom : ⊥

{-# DISPLAY erasedBottom = [erased] #-}

erase-⊥ : ⊥ → ⊥
erase-⊥ _ = erasedBottom

infix 4 ¬_
¬_ : ∀ {a} (A : Set a) → Set a
¬ A = A → ⊥

eraseNegation : ∀ {a} {A : Set a} → ¬ A → ¬ A
eraseNegation !a a = erase-⊥ (!a a)

data ⊥′ {a} : Set a where

⊥′-elim : ∀ {a b} {A : Set a} → ⊥′ {b} → A
⊥′-elim ()
{-# INLINE ⊥′-elim #-}

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
------------------------------------------------------------------------
-- Dependent lenses
------------------------------------------------------------------------

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

{-# OPTIONS --cubical --safe #-}

module Lens.Dependent where

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

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

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

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

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

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

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

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

  open _≃_

  -- The remainder.

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

  -- Getter.

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

  -- Setter.

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

  -- Modifier.

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

  -- Setting leaves the remainder unchanged.

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

  -- A related isomorphism.

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

  -- Some lens laws.

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

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

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

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

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

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

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

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

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

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

-- Identity lens.

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

-- Composition of lenses.

infixr 9 _₃∘₃_

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

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

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

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

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

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

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

-- One definition.

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

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

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

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

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

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

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

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

  -- The main lens isomorphism.

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

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

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

  private module L = Lens₃ lens
  open _≃_

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

  remainder : A → R
  remainder = L.remainder

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

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

  -- A corresponding isomorphism.

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

  -- A variant of variant.

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

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

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

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

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

    private

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

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

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

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

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

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

    private
     abstract

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

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

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

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

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

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

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

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

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

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

  -- Getter.

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

  -- Setter.

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

  -- Modifier.

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

  -- Setting leaves the remainder unchanged.

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

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

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

  -- A corresponding isomorphism.

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

  -- Unfolding lemmas for codomain-set-≃.

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

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

  -- Some lens laws.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    ⊤ ≃ B′ r                            □

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- Lens and Lens′ are pointwise isomorphic.

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

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

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

-- Conversion from Lens₃ to Lens.

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

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

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

-- Identity lens.

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

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

infixr 9 _∘₃_

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

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

infixr 9 _⨾_

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

-- Can the composition operation be generalised?

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

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

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

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

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

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

    idL : ND.Lens Bool Bool
    idL = ND.Lens-combinators.id ⊠

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

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

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

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

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

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

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

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

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

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

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

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

module Observation where

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

  Unit = Σ Bool λ b → b ≡ true

  -- All its inhabitants are equal.

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

  -- Its only inhabitant.

  u : Unit
  u = (true , refl)

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

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

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

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

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

max_stars_repo_name: Saizan/dependent-lenses

max_issues_repo_name: Saizan/dependent-lenses

max_forks_repo_name: Saizan/dependent-lenses


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

module Fragment.Extensions.CSemigroup where

open import Fragment.Extensions.CSemigroup.Base using (CSemigroupFrex) public

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


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

module BimonoidalCategory where

open import Level

open import Categories.Category
open import Categories.Monoidal
open import Categories.Monoidal.Braided
open import Categories.NaturalIsomorphism
open import Categories.NaturalTransformation using (id; _∘₁_; _≡_)

------------------------------------------------------------------------------
-- Definition

record SymmetricMonoidalCategory {o ℓ e} {ℂ  : Category o ℓ e} {Mℂ : Monoidal ℂ}
  (BMℂ : Braided Mℂ) : Set (suc (o ⊔ ℓ ⊔ e)) where
  open Braided BMℂ using (braid)
  open NaturalIsomorphism braid using () renaming (F⇒G to x⊗y⇒y⊗x; F⇐G to y⊗x⇒x⊗y)
  field
    symmetry : x⊗y⇒y⊗x ∘₁ y⊗x⇒x⊗y ≡ id

{--

record BimonoidalCategory o ℓ e (C : Category o ℓ e) : Set (suc (o ⊔ ℓ ⊔ e)) where
  infixr 9 _∘_
  infixl 7 _+_ _⊕_
  infixl 6 _*_ _⊗_
  infix  4 _⇒_
  infix  1 _≈_
  field
    -- objects, morphisms, equality on morphisms
    Obj : Set o
    _⇒_ : Rel Obj ℓ
    _≈_ : ∀ {A B} → Rel (A ⇒ B) e
    -- plain category
    id  : ∀ {A} → A ⇒ A
    _∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C)
    -- additive monoid
    0#  : Obj
    _+_ : Op₂ Obj
    _⊕_ : ∀ {A B C D} → (A ⇒ C) → (B ⇒ D) → (A + B ⇒ C + D)
    -- multiplicative monoid
    1#  : Obj
    _*_ : Op₂ Obj
    _⊗_ : ∀ {A B C D} → (A ⇒ C) → (B ⇒ D) → (A * B ⇒ C * D)
    -- axioms
    isBimonoidalCategory : IsBimonoidalCategory _⇒_ _≈_ id _∘_ 0# _+_ _⊕_ 1# _*_ _⊗_

record Iso {o ℓ e} {Obj : Set o}
  (_⇒_ : Rel Obj ℓ)
  (_≈_ : ∀ {A B} → Rel (A ⇒ B) e)
  (id  : ∀ {A} → A ⇒ A)
  (_∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C))
  (A B : Obj)
  :  Set (o ⊔ ℓ ⊔ e) where
  field
    fwd     : A ⇒ B
    bwd     : B ⇒ A
    fwd∘bwd : (_∘_ {B} {A} {B} fwd bwd) ≈ id {B}
    bwd∘fwd : (_∘_ {A} {B} {A} bwd fwd) ≈ id {A}

record IsMonoid {o ℓ e} {Obj : Set o}
  (_⇒_ : Rel Obj ℓ)
  (_≈_ : ∀ {A B} → Rel (A ⇒ B) e)
  (id  : ∀ {A} → A ⇒ A)
  (_∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C))
  (u : Obj)
  (_op_ : Op₂ Obj)
  (_opf_ : ∀ {A B C D} → (A ⇒ C) → (B ⇒ D) → (_⇒_ (A op B) (C op D)))
  : Set (o ⊔ ℓ ⊔ e) where
  field
    assoc : {A B C : Obj} → Iso _⇒_ _≈_ id _∘_ ((A op B) op C) (A op (B op C))
    unite : {A : Obj} → Iso _⇒_ _≈_ id _∘_ (u op A) A
    uniti : {A : Obj} → Iso _⇒_ _≈_ id _∘_ (A op u) A
    funcObj : {A B : Obj} → ((id {A}) opf (id {B})) ≈ id {A op B}
--    funcMor : {A B C D E F G H : Obj} {f : A ⇒ B} {g : C ⇒ D} {k : E ⇒ F} {h : G ⇒ H} →
--              ((k opf h) ∘ (g opf f)) ≈ ((k opf g) ∘ (h opf f))
--    assoc; unite; uniti are natural transformations
--    triangle
--    pentagon

record IsBimonoidalCategory {o ℓ e} {Obj : Set o}
  (_⇒_ : Rel Obj ℓ)
  (_≈_ : ∀ {A B} → Rel (A ⇒ B) e)
  (id  : ∀ {A} → A ⇒ A)
  (_∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C))
  (0#  : Obj)
  (_+_ : Op₂ Obj)
  (_⊕_ : ∀ {A B C D} → (A ⇒ C) → (B ⇒ D) → (_⇒_ (A + B) (C + D)))
  (1#  : Obj)
  (_*_ : Op₂ Obj)
  (_⊗_ : ∀ {A B C D} → (A ⇒ C) → (B ⇒ D) → (_⇒_ (A * B) (C * D)))
  : Set (o ⊔ ℓ ⊔ e) where
  field
    cat        : Category o ℓ e
    +-isMonoid : IsMonoid _⇒_ _≈_ id _∘_ 0# _+_ _⊕_
    *-isMonoid : IsMonoid _⇒_ _≈_ id _∘_ 1# _*_ _⊗_
    -- ⊕ is a bifunctor
    -- units and assoc are natural transformations
    -- pentangon and triangle axioms
    -- multiplicative monoid
    -- distributivity
--}

------------------------------------------------------------------------------

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module Main where

import Automaton.DeterministicFinite
import Automaton.NonDeterministicFinite
import Automaton.Pushdown
import Automaton.TuringMachine
import Cardinal
import Cardinal.Finite.Count
import Cardinal.Proofs
import Data
import Data.Any
import Data.Boolean
import Data.Boolean.Stmt
import Data.Boolean.Operators
import Data.Boolean.Proofs
import Data.Either
import Data.List
import Data.List.Computability
import Data.List.Proofs
import Data.List.Relation.Membership.Proofs
import Data.List.Relation.Sublist.Proofs
import Data.List.Relation
import Data.List.Relation.Membership
import Data.List.Relation.Sublist
import Data.ListNonEmpty
import Data.Option
import Data.Proofs
import Data.Tuple
import Data.Tuple.Function
import Data.Tuple.List
import Data.Tuple.Proofs
import Data.Tuple.Raise
import Data.Tuple.Raiseᵣ
import Data.Tuple.Raiseₗ
import FFI.IO   as FFI
import FormalLanguage
import FormalLanguage.ContextFreeGrammar
import FormalLanguage.Proofs
import FormalLanguage.RegularExpression
import Functional
import Function.DomainRaise
import Function.Domains
import Function.Domains.Proofs
import Function.Equals
import Function.Names
import Function.PrimitiveRecursion
import Function.Proofs
import Function.Iteration
import Function.Iteration.Proofs
-- import Geometry.Test
-- import Geometry.Test2
import Geometry.Test3
import Graph
import Lang.Instance
import Lang.Irrelevance
import Logic.Classical
import Logic.Classical.DoubleNegated
import Logic.Classical.Mere
import Logic.Computability
import Logic.Computability.Binary
import Logic.Convenience
import Logic.DiagonalProof
import Logic.LambdaCalculus
import Logic.Predicate
import Logic.Predicate.Theorems
import Logic.Propositional
import Logic.Propositional.Names
import Logic.Propositional.Theorems
import Lvl
import Metalogic.Classical.Propositional.ProofSystem
import Metalogic.Classical.Propositional.Syntax
import Metalogic.Classical.Propositional.TruthSemanticsModel
import Metalogic.Constructive.NaturalDeduction.TreeModel
-- import Metalogic.Constructive.Provability
import Metalogic.Linear.SequentCalculus
import Metalogic.Linear.Syntax
import Numeral.CoordinateVector
import Numeral.FiniteInclusive
import Numeral.Finite
import Numeral.Finite.Bound
import Numeral.Finite.Functions
import Numeral.Finite.Oper
import Numeral.Finite.Oper.Comparisons
import Numeral.Finite.Proofs
import Numeral.Integer
import Numeral.Integer.Function
import Numeral.Integer.Oper
import Numeral.Integer.Proofs
import Numeral.Integer.Relation
import Numeral.Integer.Sign
import Numeral.Matrix
import Numeral.Natural
import Numeral.Natural.Coprime
import Numeral.Natural.Function
import Numeral.Natural.Function.Proofs
-- import Numeral.Natural.GreatestCommonDivisor
import Numeral.Natural.Induction
import Numeral.Natural.Inductions
import Numeral.Natural.Oper
import Numeral.Natural.Oper.Comparisons
import Numeral.Natural.Oper.Comparisons.Proofs
import Numeral.Natural.Oper.Divisibility
import Numeral.Natural.Oper.Modulo
import Numeral.Natural.Oper.Modulo.Proofs
import Numeral.Natural.Oper.Proofs
import Numeral.Natural.Order
import Numeral.Natural.Prime
import Numeral.Natural.Relation
import Numeral.Natural.Relation.Computability
import Numeral.Natural.Relation.Countable
import Numeral.Natural.Relation.Divisibility
import Numeral.Natural.Relation.Order
import Numeral.Natural.Relation.Order.Computability
import Numeral.Natural.Relation.Order.Existence
import Numeral.Natural.Relation.Order.Existence.Proofs
import Numeral.Natural.Relation.Order.Proofs
import Numeral.Natural.Relation.Properties
import Numeral.Natural.TotalOper
import Numeral.Natural.UnclosedOper
import Numeral.PositiveInteger
import Numeral.PositiveInteger.Oper
import Numeral.Rational.AlterAdd
-- import Numeral.Rational.SternBrocot
import Numeral.Real
import Numeral.Real.Properties
import Numeral.Sign
import Numeral.Sign.Oper
import Numeral.Sign.Oper0
import Operator.Equals
import Relator.Bijection
import Relator.Congruence
import Relator.Congruence.Proofs
import Relator.Countable
import Relator.Equals
import Relator.Equals.Proofs
import Relator.Equals.Proofs.Uniqueness
import Structure.Setoid.Uniqueness
import Relator.Finite
import Sets.BoolSet
import Sets.BoolSet.Proofs
import Sets.ETCS
import Sets.IZF
import Sets.PredicateSet
import Sets.PredicateSet.Filter
import Sets.PredicateSet.Finite
import Sets.PredicateSet.Proofs
import Sets.PredicateSet.Relations
import Structure.Setoid
import Structure.Setoid.Proofs
import Stream
import String
import Structure.Arithmetic
-- import Structure.Category
import Structure.Function.Domain
import Structure.Function.Linear
import Structure.Function.Ordering
import Structure.LinearAlgebra
import Structure.Logic.Classical.PredicateBoundedQuantification
import Structure.Logic.Classical.NaturalDeduction
import Structure.Logic.Classical.NaturalDeduction.Proofs
import Structure.Logic.Classical.SetTheory
import Structure.Logic.Classical.SetTheory.SetBoundedQuantification
import Structure.Logic.Classical.SetTheory.Function
import Structure.Logic.Classical.SetTheory.Relation
import Structure.Logic.Classical.SetTheory.ZFC
import Structure.Logic.Classical.SetTheory.ZFC.BinaryRelatorSet
-- import Structure.Logic.Classical.SetTheory.ZFC.Finite
import Structure.Logic.Classical.SetTheory.ZFC.FunctionSet
import Structure.Logic.Classical.SetTheory.ZFC.Proofs
import Structure.Logic.Constructive.Functions.Properties
import Structure.Logic.Constructive.NaturalDeduction
import Structure.Operator.Field
import Structure.Operator.Functions
import Structure.Operator.Group
import Structure.Operator.Group.Proofs
import Structure.Operator.Monoid
import Structure.Operator.Proofs
import Structure.Operator.Properties
import Structure.Operator.SetAlgebra
import Structure.Operator.Vector
import Structure.Real
import Structure.Relator.Equivalence as Eq
import Structure.Relator.Function
import Structure.Relator.Ordering
import Structure.Relator.Ordering.Subsets
import Structure.Relator.Properties
import Structure.Relator.Properties.Proofs
import Syntax.Function
import Syntax.Method
import Syntax.Number
import Type
import Type.Cardinality
import Type.Cardinality.Proofs
import Type.Dependent
import Type.Properties.Empty
import Type.Properties.Empty.Proofs
import Type.Functions
import Type.Functions.Inverse
import Type.Functions.Inverse.Proofs
import Type.Functions.Proofs
import Type.Singleton
import Type.Singleton.Proofs
import Type.Properties.Singleton
import Type.Properties.Singleton.Proofs
import Type.Univalence

main : FFI.IO Data.Unit
main = FFI.printStrLn("Okay")