text:
------------------------------------------------------------------------
-- Equivalence between omniscience principles
------------------------------------------------------------------------

-- http://math.fau.edu/lubarsky/Separating%20LLPO.pdf
-- https://pdfs.semanticscholar.org/deb5/23b6078032c845d8041ee6a5383fec41191c.pdf
-- http://www.math.lmu.de/~schwicht/pc16transparencies/ishihara/lecture1.pdf
-- https://ncatlab.org/nlab/show/weak+excluded+middle

------------------------------------------------------------------------
-- ->  : implication
-- <=> : equivalence
-- ∧   : conjunction

{-
                EM <=> DNE <=> Peirce <=> MI <=> DEM₁ <=> DEM₂-----┐
                 |      |        |                         |       v
                 |      |        v                         v     EM⁻¹ <=> DNE⁻¹
                 |      |       DGP          ¬ ¬ EM  <=>  DNS
                 |      |        |
                 |      |        v
                 |      |       WEM <=> DEM₃ <=> DN-distrib-⊎
                 v      v        |
                LPO     KS-------------┐
                /  \             |     \
               /    \            |      \
              v      v           v       v
Σ-Call/CC <=> MP    WLPO <=> Σ-Π-DGP -> PFP -> WPFP
              |\     |
              | \    v
              |  \  LLPO <=> Σ-DGP <=> Π-DGP
              |   \  |
              v    v v
             WMP   MP∨
-}

-- WLPO ∧ MP -> LPO
-- WLPO ∧ WMP -> LPO

-- WMP ∧ MP∨ -> MP

-- WPFP ∧ MP -> LPO

-- WPFP ∧ MP∨ -> WLPO
-- WPFP ∧ LLPO -> WLPO

-- Inhabited ∧ LPO <=> Searchable

-- MR <=> Σ-Σ-Peirce

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

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

module Constructive.Axiom.Properties.Base where

-- agda-stdlib
open import Axiom.Extensionality.Propositional
open import Level renaming (suc to lsuc; zero to lzero)
open import Data.Bool using (Bool; true; false; not)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt)
open import Data.Sum as Sum
open import Data.Product as Prod
open import Data.Nat as ℕ using (ℕ; zero; suc; _≤_; s≤s; z≤n; _≤?_; _+_; _*_)
import Data.Nat.Properties as ℕₚ
import Data.Nat.Induction as ℕInd
open import Data.Fin using (Fin)
import Data.Fin.Properties as Finₚ
open import Function.Base
import Function.Equality as Eq
import Function.Equivalence as Eqv
import Function.LeftInverse as LInv -- TODO use new packages
import Induction.WellFounded as Ind
open import Relation.Binary
  using (tri≈; tri<; tri>; Rel; Trichotomous)
open import Relation.Binary.PropositionalEquality hiding (Extensionality) -- TODO remove
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Decidable using (⌊_⌋)

-- agda-misc
open import Constructive.Axiom
import Constructive.Axiom.Properties.Base.Lemma as Lemma
open import Constructive.Combinators
open import Constructive.Common
open import TypeTheory.HoTT.Data.Sum.Properties using (isProp-⊎)
open import TypeTheory.HoTT.Relation.Nullary.Negation.Properties
  using (isProp-¬)

-- Properties
aclt : ∀ {a b p} {A : Set a} {B : Set b} → ACLT A B p
aclt f = (λ x → proj₁ (f x)) , (λ x → proj₂ (f x))

lower-dne : ∀ a b → DNE (a ⊔ b) → DNE a
lower-dne a b dne = lower ∘′ dne ∘′ DN-map (lift {ℓ = b})

lower-wem : ∀ a b → WEM (a ⊔ b) → WEM a
lower-wem a b wem with wem
... | inj₁ ¬Lx  = inj₁ λ x → ¬Lx (lift {ℓ = b} x)
... | inj₂ ¬¬Lx = inj₂ λ ¬A → ¬¬Lx λ LA → ¬A (lower LA)

-- LPO for finite set
lpo-Fin : ∀ {n p} → LPO (Fin n) p
lpo-Fin = dec⇒dec⊎ ∘ Finₚ.any? ∘ DecU⇒decidable

dec-dns-i : ∀ {a p} {A : Set a} {P : A → Set p} → DecU P → DNS-i P
dec-dns-i P? ∀¬¬P = DN-intro (P?⇒∀¬¬P→∀P P? ∀¬¬P)

-- TODO
-- dns-Fin : ∀ {n p} → DNS (Fin n) p

------------------------------------------------------------------------
-- Equivalence between classical proposition
------------------------------------------------------------------------

-- DNE <=> EM
dne⇒em : ∀ {a} → DNE a → EM a
dne⇒em dne = dne DN-Dec⊎

em⇒dne : ∀ {a} → EM a → DNE a
em⇒dne em = A⊎B→¬B→A em

-- Peirce => DNE, EM => Peirce
peirce⇒dne : ∀ {a b} → Peirce a b → DNE a
peirce⇒dne peirce ¬¬A =
  peirce {B = Lift _ ⊥} λ A→B → ⊥-elim (¬¬A λ x → lower $ A→B x)

em⇒peirce : ∀ {a b} → EM a → Peirce a b
em⇒peirce em f = Sum.[ id , [[A→B]→A]→¬A→A f ] em

-- DEM₁ => EM, DNE => DEM₁
dem₁⇒em : ∀ {a} → DEM₁ a a → EM a
dem₁⇒em dem₁ = dem₁ (uncurry (flip _$_))

dne⇒dem₁ : ∀ {a b} → DNE (a ⊔ b) → DEM₁ a b
dne⇒dem₁ dne g = dne (g ∘ ¬[A⊎B]→¬A×¬B)

-- DNE <=> DEM₂
dne⇒dem₂ : ∀ {a} → DNE a → DEM₂ a a
dne⇒dem₂ dne f = Prod.map dne dne $ ¬[A⊎B]→¬A×¬B f

dem₂⇒dne : ∀ {a} → DEM₂ a lzero → DNE a
dem₂⇒dne dem₂ ¬¬A = uncurry id (dem₂ Sum.[ (λ f → ¬¬A (f ∘′ const)) , _$ tt ])

-- DNE => DEM₃
dne⇒dem₃ : ∀ {a b} → DNE (a ⊔ b) → DEM₃ a b
dne⇒dem₃ dne ¬[A×B] = dne (¬[A×B]→¬¬[¬A⊎¬B] ¬[A×B])

-- Converse of contraposition
dne⇒contraposition-converse : ∀ {a b} → DNE a →
                              {A : Set a} {B : Set b} → (¬ A → ¬ B) → B → A
dne⇒contraposition-converse dne ¬A→¬B b = dne $ contraposition ¬A→¬B (DN-intro b)

contraposition-converse⇒dne : ∀ {a} → ({A B : Set a} → (¬ A → ¬ B) → B → A) →
                              DNE a
contraposition-converse⇒dne f = f DN-intro

-- MI <=> EM
mi⇒em : ∀ {a} → MI a a → EM a
mi⇒em f = Sum.swap $ f id

em⇒mi : ∀ {a b} → EM a → MI a b
em⇒mi em f = Sum.swap $ Sum.map₁ f em

-- EM <=> [¬A→B]→A⊎B
em⇒[¬A→B]→A⊎B : ∀ {a b} → EM a → {A : Set a} {B : Set b} → (¬ A → B) → A ⊎ B
em⇒[¬A→B]→A⊎B em f = Sum.map₂ f em

[¬A→B]→A⊎B⇒em : ∀ {a} → ({A B : Set a} → (¬ A → B) → A ⊎ B) → EM a
[¬A→B]→A⊎B⇒em f = f id

-- Properties of WEM
em⇒wem : ∀ {a} → EM a → WEM a
em⇒wem em {A = A} = em {A = ¬ A}

-- WEM <=> DEM₃
wem⇒dem₃ : ∀ {a} → WEM a → DEM₃ a a
wem⇒dem₃ wem ¬[A×B] with wem | wem
... | inj₁ ¬A  | _        = inj₁ ¬A
... | inj₂ ¬¬A | inj₁ ¬B  = inj₂ ¬B
... | inj₂ ¬¬A | inj₂ ¬¬B = ⊥-elim $ DN-undistrib-× (¬¬A , ¬¬B) ¬[A×B]

dem₃⇒wem : ∀ {a} → DEM₃ a a → WEM a
dem₃⇒wem dem₃ = dem₃ ¬[A×¬A]

dgp-i⇒DN-distrib-⊎-i : ∀ {a b} {A : Set a} {B : Set b} →
                       DGP-i A B → ¬ ¬ (A ⊎ B) → ¬ ¬ A ⊎ ¬ ¬ B
dgp-i⇒DN-distrib-⊎-i dgp-i ¬¬[A⊎B] =
  Sum.map (λ B→A ¬A → ¬¬[A⊎B] Sum.[ ¬A , contraposition B→A ¬A ])
          (λ A→B ¬B → ¬¬[A⊎B] Sum.[ contraposition A→B ¬B , ¬B ])
          (Sum.swap dgp-i)

-- WEM <=> DN-distrib-⊎
wem⇒DN-distrib-⊎ : ∀ {a b} → WEM (a ⊔ b) →
                   {A : Set a} {B : Set b} → ¬ ¬ (A ⊎ B) → ¬ ¬ A ⊎ ¬ ¬ B
wem⇒DN-distrib-⊎ {a} {b} wem ¬¬[A⊎B] with lower-wem a b wem | lower-wem b a wem
... | inj₁ ¬A  | inj₁ ¬B  = ⊥-elim $ ¬¬[A⊎B] (¬A×¬B→¬[A⊎B] (¬A , ¬B))
... | inj₁ ¬A  | inj₂ ¬¬B = inj₂ ¬¬B
... | inj₂ ¬¬A | _        = inj₁ ¬¬A

DN-distrib-⊎⇒wem : ∀ {a} → ({A B : Set a} → ¬ ¬ (A ⊎ B) → ¬ ¬ A ⊎ ¬ ¬ B) → WEM a
DN-distrib-⊎⇒wem DN-distrib-⊎ = Sum.swap $ Sum.map₂ TN-to-N $ DN-distrib-⊎ DN-Dec⊎

-- WEM-i ∧ Stable => Dec⊎
wem-i∧stable⇒dec⊎ : ∀ {a} {A : Set a} → WEM-i A → Stable A → Dec⊎ A
wem-i∧stable⇒dec⊎ (inj₁ x) stable = inj₂ x
wem-i∧stable⇒dec⊎ (inj₂ y) stable = inj₁ (stable y)

-- EM => DGP => WEM
em⇒dgp : ∀ {a b} → EM (a ⊔ b) → DGP a b
em⇒dgp em = em⇒[¬A→B]→A⊎B em ¬[A→B]→B→A

dgp-i⇒dem₃-i : ∀ {a b} {A : Set a} {B : Set b} → DGP-i A B → DEM₃-i A B
dgp-i⇒dem₃-i dgp-i ¬[A×B] =
  Sum.map (λ A→B → contraposition (λ x → x , A→B x) ¬[A×B])
          (λ B→A → contraposition (λ y → B→A y , y) ¬[A×B])
          dgp-i

dgp⇒dem₃ : ∀ {a b} → DGP a b → DEM₃ a b
dgp⇒dem₃ dgp ¬[A×B] = dgp-i⇒dem₃-i dgp ¬[A×B]

dgp⇒wem : ∀ {a} → DGP a a → WEM a
dgp⇒wem dgp = dem₃⇒wem $ dgp⇒dem₃ dgp

-- Properties of DNS
-- DNE => DNS
dne⇒dns : ∀ {a p} {A : Set a} → DNE (a ⊔ p) → DNS A (a ⊔ p)
dne⇒dns dne f = λ x → x λ y → dne (f y)

-- DNS <=> ¬ ¬ EM
dns⇒¬¬em : ∀ {a} → ({A : Set (lsuc a)} → DNS A a) → ¬ ¬ EM a
dns⇒¬¬em dns = DN-map (λ x {A} → x A) $ dns (λ _ → DN-Dec⊎)

¬¬em⇒dns : ∀ {a} → ¬ ¬ EM a → ({A : Set a} → DNS A a)
¬¬em⇒dns ¬¬em =
  λ ∀x→¬¬Px ¬[∀x→Px] → ¬¬em λ em → ¬[∀x→Px] (λ x → em⇒dne em (∀x→¬¬Px x))

-- call/cc is classical
call/cc⇒dne : ∀ {a} → Call/CC a → DNE a
call/cc⇒dne call/cc ¬¬A = call/cc λ ¬A → ⊥-elim (¬¬A ¬A)

em⇒call/cc : ∀ {a} → EM a → Call/CC a
em⇒call/cc em ¬A→A = Sum.[ id , ¬A→A ] em

-- DNE <=> ¬[A×¬B]→A→B
dne⇒¬[A×¬B]→A→B : ∀ {a b} → DNE (a ⊔ b) →
                  {A : Set a} {B : Set b} → ¬ (A × ¬ B) → A → B
dne⇒¬[A×¬B]→A→B dne = dne λ x → x λ y z → ⊥-elim (y (z , (λ w → x λ u v → w)))

¬[A×¬B]→A→B⇒dne : ∀ {a} → ({A B : Set a} → ¬ (A × ¬ B) → A → B) → DNE a
¬[A×¬B]→A→B⇒dne f ¬¬A = f (uncurry id) ¬¬A

-- EM <=> [A→B]→¬A⊎B
em⇒[A→B]→¬A⊎B : ∀ {a b} → EM b → {A : Set a} {B : Set b} → (A → B) → ¬ A ⊎ B
em⇒[A→B]→¬A⊎B em f = Sum.swap (Sum.map₂ (contraposition f) em)

[A→B]→¬A⊎B⇒em : ∀ {a} → ({A B : Set a} → (A → B) → ¬ A ⊎ B) → EM a
[A→B]→¬A⊎B⇒em f = Sum.swap (f id)

dne⇒¬[A→¬B]→A×B : ∀ {a b} → DNE (a ⊔ b) →
                  {A : Set a} {B : Set b} → ¬ (A → ¬ B) → A × B
dne⇒¬[A→¬B]→A×B dne f = dne λ ¬[A×B] → f λ x y → ¬[A×B] (x , y)

-- the counterexample principle
dne⇒¬[A→B]→A×¬B : ∀ {a b} → DNE (a ⊔ b) →
                  {A B : Set a} {B : Set b} → ¬ (A → B) → A × ¬ B
dne⇒¬[A→B]→A×¬B dne f =
  dne λ ¬[A×¬B] → f λ x → ⊥-elim (¬[A×¬B] (x , (λ y → f (const y))))

¬[A→B]→A×¬B⇒dne : ∀ {a} → ({A B : Set a} → ¬ (A → B) → A × ¬ B) → DNE a
¬[A→B]→A×¬B⇒dne {a} f ¬¬A with f {B = Lift a ⊥} λ A→L⊥ → ¬¬A λ x → lower $ A→L⊥ x
... | x , _ = x

dne⇒ip : ∀ {a b c} → DNE (a ⊔ b ⊔ c) → IP a b c
dne⇒ip dne q f = dne (DN-ip q f)

-- Properties of DNE⁻¹ and EM⁻¹
em⇒em⁻¹ : ∀ {a} → EM a → EM⁻¹ a
em⇒em⁻¹ em _ = em

-- DNE⁻¹ <=> EM⁻¹
dne⁻¹⇒em⁻¹ : ∀ {a} → Extensionality a lzero → DNE⁻¹ a → EM⁻¹ a
dne⁻¹⇒em⁻¹ ext dne⁻¹ isP = dne⁻¹ isP′ DN-Dec⊎
  where
  isP′ : ∀ x y → x ≡ y
  isP′ = isProp-⊎ ¬[A×¬A] isP (isProp-¬ ext)

em⁻¹⇒dne⁻¹ : ∀ {a} → EM⁻¹ a → DNE⁻¹ a
em⁻¹⇒dne⁻¹ em⁻¹ isP = dec⊎⇒stable (em⁻¹ isP)

-----------------------------------------------------------------------
-- Properties of LPO, LLPO, WLPO, MP, MP⊎, WMP, KS, PFP, WPFP, Σ-DGP,
--   Π-DGP, Σ-Π-DGP, Σ-Call/CC
-----------------------------------------------------------------------

-----------------------------------------------------------------------
-- Convert between alternative forms

-- MP <=> MR
mp⇒mr : ∀ {a p} {A : Set a} → MP A p → MR A p
mp⇒mr mp P? ¬¬∃P = P?⇒∃¬¬P→∃P P? $ mp (¬-DecU P?) (¬¬∃P→¬∀¬P ¬¬∃P)

mr⇒mp : ∀ {a p} {A : Set a} → MR A p → MP A p
mr⇒mp mr P? ¬∀P = mr (¬-DecU P?) (P?⇒¬∀P→¬¬∃¬P P? ¬∀P)

-- WLPO <=> WLPO-Alt
wlpo⇒wlpo-Alt : ∀ {a p} {A : Set a} → WLPO A p → WLPO-Alt A p
wlpo⇒wlpo-Alt wlpo P? = Sum.map ∀¬P→¬∃P ¬∀¬P→¬¬∃P (wlpo (¬-DecU P?))

wlpo-Alt⇒wlpo : ∀ {a p} {A : Set a} → WLPO-Alt A p → WLPO A p
wlpo-Alt⇒wlpo wlpo-Alt P? =
  Sum.map (P?⇒¬∃¬P→∀P P?) ¬¬∃¬P→¬∀P (wlpo-Alt (¬-DecU P?))

-- MP⊎ <=> MP⊎-Alt
mp⊎⇒mp⊎-Alt : ∀ {a p} {A : Set a} → MP⊎ A p → MP⊎-Alt A p
mp⊎⇒mp⊎-Alt mp⊎ P? Q? =
  Sum.map (contraposition ∀P→¬∃¬P) (contraposition ∀P→¬∃¬P) ∘′
  mp⊎ (¬-DecU P?) (¬-DecU Q?) ∘′
  contraposition (Prod.map (P?⇒¬∃¬P→∀P P?) (P?⇒¬∃¬P→∀P Q?))

mp⊎-Alt⇒mp⊎ : ∀ {a p} {A : Set a} → MP⊎-Alt A p → MP⊎ A p
mp⊎-Alt⇒mp⊎ mp⊎-Alt P? Q? =
  Sum.map (contraposition ¬∃P→∀¬P) (contraposition ¬∃P→∀¬P) ∘′
  mp⊎-Alt (¬-DecU P?) (¬-DecU Q?) ∘′
  contraposition (Prod.map ∀¬P→¬∃P ∀¬P→¬∃P)

-- MP⊎ <=> MP∨
mp⊎⇒mp∨ : ∀ {a p} {A : Set a} → MP⊎ A p → MP∨ A p
mp⊎⇒mp∨ mp⊎ P? Q? ¬¬∃x→Px⊎Qx = mp⊎ P? Q? ([¬¬∃x→Px⊎Qx]→¬[¬∃P×¬∃Q] ¬¬∃x→Px⊎Qx)

mp∨⇒mp⊎ : ∀ {a p} {A : Set a} → MP∨ A p → MP⊎ A p
mp∨⇒mp⊎ mp∨ P? Q? ¬[¬∃P×¬∃Q] = mp∨ P? Q? (¬[¬∃P×¬∃Q]→¬¬∃x→Px⊎Qx ¬[¬∃P×¬∃Q])

-- LLPO <=> LLPO-Alt
llpo⇒llpo-Alt : ∀ {a p} {A : Set a} → LLPO A p → LLPO-Alt A p
llpo⇒llpo-Alt llpo P? Q? =
  Sum.map (P?⇒¬∃¬P→∀P P?) (P?⇒¬∃¬P→∀P Q?) ∘′
  llpo (¬-DecU P?) (¬-DecU Q?) ∘′
  contraposition (¬A×¬B→¬[A⊎B] ∘ Prod.map ∃¬P→¬∀P ∃¬P→¬∀P)

llpo-Alt⇒llpo : ∀ {a p} {A : Set a} → LLPO-Alt A p → LLPO A p
llpo-Alt⇒llpo llpo-Alt P? Q? =
  Sum.map ∀¬P→¬∃P ∀¬P→¬∃P ∘′
  llpo-Alt (¬-DecU P?) (¬-DecU Q?) ∘′
  DN-map (Sum.map ¬∃P→∀¬P ¬∃P→∀¬P) ∘′ ¬[A×B]→¬¬[¬A⊎¬B]

-- LLPO <=> LLPO-ℕ
llpo⇒llpo-ℕ : ∀ {p} → LLPO ℕ p → LLPO-ℕ p
llpo⇒llpo-ℕ llpo P? ∀mn→m≢n→Pm⊎Pn with
  llpo (λ n → ¬-DecU P? (2 * n)) (λ n → ¬-DecU P? (1 + 2 * n))
       (uncurry (Lemma.lemma₁ ∀mn→m≢n→Pm⊎Pn))
... | inj₁ ¬∃n→¬P2n   = inj₁ (P?⇒¬∃¬P→∀P (λ n → P? (2 * n)) ¬∃n→¬P2n)
... | inj₂ ¬∃n→¬P1+2n = inj₂ (P?⇒¬∃¬P→∀P (λ n → P? (suc (2 * n))) ¬∃n→¬P1+2n)

private
  module _ {p} {P Q : ℕ → Set p} (P? : DecU P) (Q? : DecU Q) where
    combine : DecU (λ n → Sum.[ P , Q ] (Lemma.parity n))
    combine n with Lemma.parity n
    ... | inj₁ m = P? m
    ... | inj₂ m = Q? m

{-
    lemma : ¬ (∃ P × ∃ Q) → ∀ m n → m ≢ n →
            Sum.[ (λ o → ¬ P o) , (λ o → ¬ Q o) ] (Lemma.parity m) ⊎
            Sum.[ (λ o → ¬ P o) , (λ o → ¬ Q o) ] (Lemma.parity n)
    lemma _ m n m≢n with
      Lemma.parity n | inspect Lemma.parity n | Lemma.parity m | inspect Lemma.parity m
    ... | inj₁ o | [ eq₁ ] | inj₁ p | [ eq₂ ] = {!   !}
    ... | inj₁ o | [ eq₁ ] | inj₂ p | [ eq₂ ] = {!   !}
    ... | inj₂ o | [ eq₁ ] | inj₁ p | [ eq₂ ] = {!   !}
    ... | inj₂ o | [ eq₁ ] | inj₂ p | [ eq₂ ] = {!   !}

llpo-ℕ⇒llpo-Alt : ∀ {p} → LLPO-ℕ p → LLPO-Alt ℕ p
llpo-ℕ⇒llpo-Alt llpo-ℕ P? Q? ¬¬[∀P⊎∀Q] with llpo-ℕ (combine P? Q?) {!   !}
... | inj₁ ∀n→[P,Q]parity[2*n]   =
  inj₁ λ n → subst Sum.[ _ , _ ] (Lemma.parity-even n) (∀n→[P,Q]parity[2*n] n)
... | inj₂ ∀n→[P,Q]parity[1+2*n] =
  inj₂ λ n → subst Sum.[ _ , _ ] (Lemma.parity-odd n) (∀n→[P,Q]parity[1+2*n] n)
-}

-----------------------------------------------------------------------
-- Implications

-- EM => LPO
em⇒lpo : ∀ {a p} {A : Set a} → EM (a ⊔ p) → LPO A p
em⇒lpo em _ = em

-- LPO => LLPO
lpo⇒llpo : ∀ {a p} {A : Set a} → LPO A p → LLPO A p
lpo⇒llpo lpo P? Q? ¬[∃P×∃Q] with lpo P? | lpo Q?
... | inj₁ ∃P  | inj₁ ∃Q  = contradiction (∃P , ∃Q) ¬[∃P×∃Q]
... | inj₁ ∃P  | inj₂ ¬∃Q = inj₂ ¬∃Q
... | inj₂ ¬∃P | _        = inj₁ ¬∃P

-- LPO <=> WLPO-Alt ∧ MR
lpo⇒wlpo-Alt : ∀ {a p} {A : Set a} → LPO A p → WLPO-Alt A p
lpo⇒wlpo-Alt lpo P? = ¬-dec⊎ (lpo P?)

lpo⇒mr : ∀ {a p} {A : Set a} → LPO A p → MR A p
lpo⇒mr lpo P? = dec⊎⇒stable (lpo P?)

wlpo-Alt∧mr⇒lpo : ∀ {a p} {A : Set a} → WLPO-Alt A p → MR A p → LPO A p
wlpo-Alt∧mr⇒lpo wlpo-Alt mr P? = wem-i∧stable⇒dec⊎ (wlpo-Alt P?) (mr P?)

-- WLPO => LLPO-Alt
wlpo⇒llpo-Alt : ∀ {a p} {A : Set a} → WLPO A p → LLPO-Alt A p
wlpo⇒llpo-Alt wlpo P? Q? ¬¬[∀P⊎∀Q] with wlpo P? | wlpo Q?
... | inj₁ ∀P  | _        = inj₁ ∀P
... | inj₂ ¬∀P | inj₁ ∀Q  = inj₂ ∀Q
... | inj₂ ¬∀P | inj₂ ¬∀Q = contradiction (¬A×¬B→¬[A⊎B] (¬∀P , ¬∀Q)) ¬¬[∀P⊎∀Q]

-- WEM => WLPO-Alt
wem⇒wlpo-Alt : ∀ {a p} {A : Set a} → WEM (a ⊔ p) → WLPO-Alt A p
wem⇒wlpo-Alt wem P? = wem

-- (WMP ∧ MP∨) <=> MR
mr⇒wmp : ∀ {a p} {A : Set a} → MR A p → WMP A p
mr⇒wmp mr {P = P} P? pp =
  mr P? $ Sum.[ id , (λ ¬¬∃x→Px×¬Px _ → f ¬¬∃x→Px×¬Px) ] (pp P?)
  where
  f : ¬ ¬ ∃ (λ x → P x × ¬ P x) → ⊥
  f ¬¬∃x→Px×¬Px = ⊥-stable $ DN-map (¬[A×¬A] ∘ proj₂) ¬¬∃x→Px×¬Px

-- MR => MP∨
mr⇒mp∨ : ∀ {a p} {A : Set a} → MR A p → MP∨ A p
mr⇒mp∨ mr {P = P} {Q = Q} P? Q? ¬¬∃x→Px⊎Qx =
  Sum.map DN-intro DN-intro $ ∃-distrib-⊎ $
  mr {P = λ x → P x ⊎ Q x} (DecU-⊎ P? Q?) ¬¬∃x→Px⊎Qx

-- WMP ∧ MP∨ => MR
-- α = P, β = Q, γ = R in [2]
wmp∧mp∨⇒mr : ∀ {a p} {A : Set a} → WMP A p → MP∨ A p → MR A p
wmp∧mp∨⇒mr {a} {p} {A} wmp mp∨ {P = P} P? ¬¬∃P = wmp P? Lem.¬¬∃Q⊎¬¬∃R
  where
  module Lem {Q : A → Set p} (Q? : DecU Q) where
    R : A → Set p
    R x = P x × ¬ Q x

    ¬¬∃x→Qx⊎Rx : ¬ ¬ ∃ λ x → Q x ⊎ R x
    ¬¬∃x→Qx⊎Rx = DN-map f ¬¬∃P
      where
      f : ∃ P → ∃ (λ x → Q x ⊎ (P x × ¬ Q x))
      f (x , Px) = x , Sum.map₂ (Px ,_) (Q? x)

    R? : DecU R
    R? = DecU-× P? (¬-DecU Q?)

    ¬¬∃Q⊎¬¬∃R : ¬ ¬ ∃ Q ⊎ ¬ ¬ ∃ R
    ¬¬∃Q⊎¬¬∃R = mp∨ Q? R? ¬¬∃x→Qx⊎Rx

-- Properties that required to prove `llpo⇒Σ-dgp`
record HasProperties
  {a} r p (A : Set a) : Set (a ⊔ lsuc r ⊔ lsuc p)
  where
  field
    _<_       : Rel A r
    <-cmp     : Trichotomous _≡_ _<_
    <-any-dec : {P : A → Set p} → DecU P → DecU (λ n → ∃ λ m → (m < n) × P m)
    <-wf      : Ind.WellFounded _<_

  private
    ¬∃¬→∀ : ∀ {P : A → Set p} {x} →
            DecU P → ¬ (∃ λ y → y < x × ¬ P y) → ∀ y → y < x → P y
    ¬∃¬→∀ {x} P? ¬∃y→y<x×¬Py y y<x =
      DecU⇒stable P? y λ ¬Py → ¬∃y→y<x×¬Py (y , (y<x , ¬Py))

  <-all-dec : {P : A → Set p} → DecU P → DecU (λ n → ∀ i → i < n → P i)
  <-all-dec P? n with <-any-dec (¬-DecU P?) n
  ... | inj₁ (m , m<n , ¬Pm) = inj₂ λ ∀i→i<n→Pi → ¬Pm (∀i→i<n→Pi m m<n)
  ... | inj₂ ¬∃m→m<n×¬Pm     = inj₁ (¬∃¬→∀ P? ¬∃m→m<n×¬Pm)

  First : (A → Set p) → A → Set (a ⊔ p ⊔ r)
  First P x = (∀ y → y < x → ¬ P y) × P x

  First? : {P : A → Set p} → DecU P → DecU (First P)
  First? P? = DecU-× (<-all-dec (¬-DecU P?)) P?

  None : (A → Set p) → A → Set (a ⊔ p ⊔ r)
  None P x = (∀ y → y < x → ¬ P y) × ¬ P x

  None? : {P : A → Set p} → DecU P → DecU (None P)
  None? P? = DecU-× (<-all-dec (¬-DecU P?)) (¬-DecU P?)

  ∃⊎None : {P : A → Set p} → DecU P → ∀ x → ∃ P ⊎ None P x
  ∃⊎None P? x with P? x | <-any-dec P? x
  ... | inj₁ Px  | _                 = inj₁ (x , Px)
  ... | inj₂ ¬Px | inj₁ (y , _ , Py) = inj₁ (y , Py)
  ... | inj₂ ¬Px | inj₂ ¬∃           =
    inj₂ ((λ y y<x Py → ¬∃ (y , (y<x , Py))) , ¬Px)

  findFirst : {P : A → Set p} → DecU P →
              ∃ P → ∃ (First P)
  findFirst {P} P? (x , Px) = go x (<-wf x) Px
    where
    go : ∀ x → Ind.Acc _<_ x → P x → ∃ λ y → (∀ i → i < y → ¬ P i) × P y
    go x (Ind.acc rs) Px with <-any-dec P? x
    ... | inj₁ (y , y<x , Py) = go y (rs y y<x) Py
    ... | inj₂ ¬∃y→y<x×Py     =
      x , (λ i i<x Pi → ¬∃y→y<x×Py (i , (i<x , Pi))) , Px

  First-unique : ∀ {P : A → Set p} {x y} → First P x → First P y → x ≡ y
  First-unique {P} {x} {y} (∀i→i<x→¬Pi , Px) (∀i→i<y→¬Pi , Py) with <-cmp x y
  ... | tri< x<y _ _ = contradiction Px (∀i→i<y→¬Pi x x<y)
  ... | tri≈ _ x≡y _ = x≡y
  ... | tri> _ _ x>y = contradiction Py (∀i→i<x→¬Pi y x>y)

  module HasPropertiesLemma
    {P Q : A → Set p} (P? : DecU P) (Q? : DecU Q)
    where

    R S : A → Set (r ⊔ p ⊔ a)
    R x = First P x × None Q x
    S x = First Q x × None P x

    R? : DecU R
    R? = DecU-× (First? P?) (None? Q?)

    S? : DecU S
    S? = DecU-× (First? Q?) (None? P?)

    ¬[∃R×∃S] : ¬ (∃ R × ∃ S)
    ¬[∃R×∃S] ((x , (∀i→i<x→¬Pi , Px) , ∀i→i<x→¬Qi , ¬Qx) ,
              (y , (∀i→i<y→¬Qi , Qy) , ∀i→i<y→¬Pi , ¬Py )) with <-cmp x y
    ... | tri< x<y _ _ = ∀i→i<y→¬Pi x x<y Px
    ... | tri≈ _ x≡y _ = ¬Py (subst P x≡y Px)
    ... | tri> _ _ y<x = ∀i→i<x→¬Qi y y<x Qy

    ¬∃R→∃P→∃Q : ¬ ∃ R → ∃ P → ∃ Q
    ¬∃R→∃P→∃Q ¬∃R ∃P with findFirst P? ∃P
    ¬∃R→∃P→∃Q ¬∃R ∃P | x , firstP with ∃⊎None Q? x
    ¬∃R→∃P→∃Q ¬∃R ∃P | x , firstP | inj₁ ∃Q    = ∃Q
    ¬∃R→∃P→∃Q ¬∃R ∃P | x , firstP | inj₂ noneQ =
      contradiction (x , firstP , noneQ) ¬∃R

    ¬∃S→∃Q→∃P : ¬ ∃ S → ∃ Q → ∃ P
    ¬∃S→∃Q→∃P ¬∃S ∃Q with findFirst Q? ∃Q
    ¬∃S→∃Q→∃P ¬∃S ∃Q | x , firstQ with ∃⊎None P? x
    ¬∃S→∃Q→∃P ¬∃S ∃Q | x , firstQ | inj₁ ∃P    = ∃P
    ¬∃S→∃Q→∃P ¬∃S ∃Q | x , firstQ | inj₂ noneP =
      contradiction (x , firstQ , noneP) ¬∃S

-- Proposition 8.6.1. [1]
-- Σ-DGP <=> LLPO
llpo⇒Σ-dgp : ∀ {r p a} {A : Set a} → HasProperties r p A →
             LLPO A (p ⊔ a ⊔ r) → Σ-DGP A p
llpo⇒Σ-dgp has llpo {P = P} {Q} P? Q? =
  Sum.map ¬∃R→∃P→∃Q ¬∃S→∃Q→∃P ¬∃R⊎¬∃S
  where
  open HasProperties has
  open HasPropertiesLemma P? Q?

  ¬∃R⊎¬∃S : ¬ ∃ R ⊎ ¬ ∃ S
  ¬∃R⊎¬∃S = llpo R? S? ¬[∃R×∃S]

Σ-dgp⇒llpo : ∀ {a p} {A : Set a} → Σ-DGP A p → LLPO A p
Σ-dgp⇒llpo Σ-dgp P? Q? ¬[∃P×∃Q] = dgp-i⇒dem₃-i (Σ-dgp P? Q?) ¬[∃P×∃Q]

-- Σ-DGP => MP∨
Σ-dgp⇒mp∨ : ∀ {p a} {A : Set a} → Σ-DGP A p → MP∨ A p
Σ-dgp⇒mp∨ Σ-dgp {P = P} {Q} P? Q? ¬¬[∃x→Px⊎Qx] = ¬¬∃P⊎¬¬∃Q
  where
  ¬¬[∃P⊎∃Q] : ¬ ¬ (∃ P ⊎ ∃ Q)
  ¬¬[∃P⊎∃Q] = DN-map ∃-distrib-⊎ ¬¬[∃x→Px⊎Qx]

  ¬¬∃P⊎¬¬∃Q : ¬ ¬ ∃ P ⊎ ¬ ¬ ∃ Q
  ¬¬∃P⊎¬¬∃Q = dgp-i⇒DN-distrib-⊎-i (Σ-dgp P? Q?) ¬¬[∃P⊎∃Q]

-- Σ-DGP => Π-DGP
Σ-dgp⇒Π-dgp : ∀ {p a} {A : Set a} → Σ-DGP A p → Π-DGP A p
Σ-dgp⇒Π-dgp Σ-dgp P? Q? =
  Sum.map (P?⇒[∃¬P→∃¬Q]→∀Q→∀P Q?) (P?⇒[∃¬P→∃¬Q]→∀Q→∀P P?)
          (Σ-dgp (¬-DecU Q?) (¬-DecU P?))

-- Π-DGP => LLPO-Alt
Π-dgp⇒llpo-Alt : ∀ {a p} {A : Set a} → Π-DGP A p → LLPO-Alt A p
Π-dgp⇒llpo-Alt Π-dgp P? Q? = Sum.map (P?⇒¬¬∀P→∀P P?) (P?⇒¬¬∀P→∀P Q?) ∘′
                             dgp-i⇒DN-distrib-⊎-i (Π-dgp P? Q?)

-- LLPO => MP∨
llpo⇒mp∨ : ∀ {r p a} {A : Set a} →
           HasProperties r p A → LLPO A (p ⊔ a ⊔ r) → MP∨ A p
llpo⇒mp∨ has llpo = Σ-dgp⇒mp∨ (llpo⇒Σ-dgp has llpo)

ℕ-hasProperties : ∀ p → HasProperties lzero p ℕ
ℕ-hasProperties _ = record
  { _<_       = ℕ._<_
  ; <-cmp     = ℕₚ.<-cmp
  ; <-any-dec = Lemma.ℕ<-any-dec
  ; <-wf      = ℕInd.<-wellFounded
  }

ℕ-llpo⇒mp∨ : ∀ {p} → LLPO ℕ p → MP∨ ℕ p
ℕ-llpo⇒mp∨ = llpo⇒mp∨ (ℕ-hasProperties _)

ℕ-llpo⇒Σ-dgp : ∀ {p} → LLPO ℕ p → Σ-DGP ℕ p
ℕ-llpo⇒Σ-dgp = llpo⇒Σ-dgp (ℕ-hasProperties _)

-- Proposition 8.6.1. [1]
-- WLPO <=> Σ-Π-DGP
wlpo⇒Σ-Π-dgp : ∀ {a p} {A : Set a} → WLPO A p → Σ-Π-DGP A p
wlpo⇒Σ-Π-dgp wlpo P? Q? with wlpo Q?
... | inj₁  ∀Q = inj₁ λ _ → ∀Q
... | inj₂ ¬∀Q = inj₂ λ ∀Q → ⊥-elim $ ¬∀Q ∀Q

Σ-Π-dgp⇒wlpo : ∀ {a p} {A : Set a} → Σ-Π-DGP A p → WLPO A p
Σ-Π-dgp⇒wlpo Σ-Π-dgp P? with Σ-Π-dgp (¬-DecU P?) P?
... | inj₁ ∃¬P→∀P = inj₁ (P?⇒[∃¬P→∀P]→∀P P? ∃¬P→∀P)
... | inj₂ ∀P→∃¬P = inj₂ λ ∀P → ∃¬P→¬∀P (∀P→∃¬P ∀P) ∀P

-- Question 15 [1]
-- MR <=> Σ-Call/CC
mr⇒Σ-call/cc : ∀ {a p} {A : Set a} → MR A p → Σ-Call/CC A p
mr⇒Σ-call/cc mr P? = mr P? ∘′ [¬A→A]→¬¬A

Σ-call/cc⇒mr : ∀ {a p} {A : Set a} → Σ-Call/CC A p → MR A p
Σ-call/cc⇒mr Σ-call/cc P? ¬¬∃P = Σ-call/cc P? λ ¬∃P → ⊥-elim $ ¬¬∃P ¬∃P

-- Question 15 [1]
-- MR <=> Σ-Σ-Peirce
mr⇒Σ-Σ-peirce : ∀ {a p} {A : Set a} → MR A p → Σ-Σ-Peirce A p
mr⇒Σ-Σ-peirce mr P? Q? [∃P→∃Q]→∃P = mr P? ([[A→B]→A]→¬¬A [∃P→∃Q]→∃P)

Σ-Σ-peirce⇒mr : ∀ {a p} {A : Set a} → Σ-Σ-Peirce A p → MR A p
Σ-Σ-peirce⇒mr {A = A} Σ-Σ-peirce P? =
  [[[A→B]→A]→A]→¬B→¬¬A→A (Σ-Σ-peirce {Q = λ _ → Lift _ ⊥} P? (λ _ → inj₂ lower))
                         f
  where
  f : Σ A (λ _ → Lift _ ⊥) → ⊥
  f (_ , ())

-- MR => Σ-Π-Peirce
mr⇒Σ-Π-peirce : ∀ {a p} {A : Set a} → MR A p → Σ-Π-Peirce A p
mr⇒Σ-Π-peirce mr P? Q? [∃P→∀Q]→∃P = mr P? ([[A→B]→A]→¬¬A [∃P→∀Q]→∃P)

-- Inhabited ∧ Σ-Π-peirce => MR
inhabited∧Σ-Π-peirce⇒mr : ∀ {a p} {A : Set a} →
                          Inhabited A → Σ-Π-Peirce A p → MR A p
inhabited∧Σ-Π-peirce⇒mr {p = p} {A} inhabited Σ-Π-peirce P? =
  [[[A→B]→A]→A]→¬B→¬¬A→A (Σ-Π-peirce {Q = λ _ → Lift _ ⊥} P? (λ _ → inj₂ lower))
                         f
  where
  f : ¬ ((x : A) → Lift p ⊥)
  f ∀x→L⊥ = lower (∀x→L⊥ inhabited)

-- Proposition 6.4.1. [1]
-- WMP ∧ WLPO-Alt => LPO
wmp∧wlpo-Alt⇒lpo : ∀ {a p} {A : Set a} → WMP A p → WLPO-Alt A p → LPO A p
wmp∧wlpo-Alt⇒lpo {a} {p} {A} wmp wlpo-Alt {P = P} P? with wlpo-Alt P?
... | inj₁ ¬∃P  = inj₂ ¬∃P
... | inj₂ ¬¬∃P = inj₁ (wmp P? Lem.res)
  where
  module Lem {Q : A → Set p} (Q? : DecU Q) where
    R : A → Set p
    R x = P x × ¬ Q x

    R? : DecU R
    R? = DecU-× P? (¬-DecU Q?)

    ¬∃R⊎¬¬∃R : ¬ ∃ R ⊎ ¬ ¬ ∃ R
    ¬∃R⊎¬¬∃R = wlpo-Alt R?

    res : ¬ ¬ ∃ Q ⊎ (¬ ¬ ∃ λ x → P x × ¬ Q x)
    res = Sum.map₁ (λ ¬∃R ¬∃Q → ¬¬∃P (f ¬∃R ¬∃Q)) ¬∃R⊎¬¬∃R
      where
      f : ¬ ∃ R → ¬ ∃ Q → ¬ ∃ P
      f ¬∃R ¬∃Q (x , Px) = ¬∃R (x , (Px , ¬∃P→∀¬P ¬∃Q x))

-- direct proof of WLPO => MP⊎
wlpo-Alt⇒mp⊎ : ∀ {a p} {A : Set a} → WLPO-Alt A p → MP⊎ A p
wlpo-Alt⇒mp⊎ wlpo-Alt P? Q? ¬[¬∃P×¬∃Q] with wlpo-Alt P? | wlpo-Alt Q?
... | inj₁ ¬∃P  | inj₁ ¬∃Q  = ⊥-elim $ ¬[¬∃P×¬∃Q] (¬∃P , ¬∃Q)
... | inj₁ ¬∃P  | inj₂ ¬¬∃Q = inj₂ ¬¬∃Q
... | inj₂ ¬¬∃P | _         = inj₁ ¬¬∃P

-- EM => KS
em⇒ks : ∀ {a p} q {A : Set a} (x : A) → EM p → KS A p q
em⇒ks q x em P with em {A = P}
em⇒ks q x em P | inj₁ xP =
  (λ _ → Lift q ⊤) , (λ _ → inj₁ (lift tt)) , ((λ _ → x , lift tt) , (λ _ → xP))
em⇒ks q x em P | inj₂ ¬P =
  (λ _ → Lift q ⊥) , (λ _ → inj₂ lower) ,
  ((λ xP → ⊥-elim $ ¬P xP) , (λ A×L⊥ → ⊥-elim $ lower $ proj₂ A×L⊥))

-- KS => PFP
ks⇒pfp : ∀ {a p q} {A : Set a} → KS A (a ⊔ p) q → PFP A p q
ks⇒pfp ks {P = P} P? = ks (∀ x → P x)

-- PFP => WPFP
pfp⇒wpfp : ∀ {a p q} {A : Set a} → PFP A p q → WPFP A p q
pfp⇒wpfp pfp {P = P} P? with pfp P?
... | Q , Q? , ∀P→∃Q , ∃Q→∀P = (λ x → ¬ Q x) , (¬-DecU Q? , (f , g))
  where
  f : (∀ x → P x) → ¬ (∀ x → ¬ Q x)
  f ∀P = ∃P→¬∀¬P (∀P→∃Q ∀P)
  g : (¬ (∀ x → ¬ Q x)) → ∀ x → P x
  g = P?⇒[∃Q→∀P]→¬∀¬Q→∀P P? ∃Q→∀P

-- WLPO => PFP
wlpo⇒pfp : ∀ {a p} q {A : Set a} → Inhabited A → WLPO A p → PFP A p q
wlpo⇒pfp {p = p} q xA wlpo {P = P} P? with wlpo P?
... | inj₁ ∀P  = (λ _ → Lift q ⊤) , (λ _ → inj₁ (lift tt)) , (f , g)
  where
  f : (∀ x → P x) → ∃ λ x → Lift q ⊤
  f _ = xA , lift tt
  g : (∃ λ x → Lift q ⊤) → (∀ x → P x)
  g _ = ∀P
... | inj₂ ¬∀P = (λ _ → Lift q ⊥) , (λ _ → inj₂ lower) , f , g
  where
  f : (∀ x → P x) → ∃ (λ x → Lift q ⊥)
  f ∀P = ⊥-elim $ ¬∀P ∀P
  g : ∃ (λ x → Lift q ⊥) → ∀ x → P x
  g (x , L⊥) = ⊥-elim $ lower L⊥

-- WLPO => WPFP
wlpo⇒wpfp : ∀ {a p} q {A : Set a} → Inhabited A → WLPO A p → WPFP A p q
wlpo⇒wpfp q xA wlpo = pfp⇒wpfp (wlpo⇒pfp q xA wlpo)

-- Proposition 6.2.3 [1]
-- WPFP ∧ MP⊎-Alt => WLPO
wpfp∧mp⊎-Alt⇒wlpo : ∀ {a p} {A : Set a} → WPFP A p p → MP⊎-Alt A p → WLPO A p
wpfp∧mp⊎-Alt⇒wlpo wpfp mp⊎-Alt {P = P} P? with wpfp P?
... | Q , Q? , ∀P→¬∀Q , ¬∀Q→∀P = Sum.map₁ ¬∀Q→∀P (Sum.swap ¬∀P⊎¬∀Q)
  where
  ¬[∀P×∀Q] : ¬ ((∀ x → P x) × (∀ x → Q x))
  ¬[∀P×∀Q] (∀P , ∀Q) = ∀P→¬∀Q ∀P ∀Q
  ¬∀P⊎¬∀Q : ¬ (∀ x → P x) ⊎ ¬ (∀ x → Q x)
  ¬∀P⊎¬∀Q = mp⊎-Alt P? Q? ¬[∀P×∀Q]

-- WPFP ∧ LLPO-Alt => WLPO
wpfp∧llpo-Alt⇒wlpo : ∀ {a p} {A : Set a} → WPFP A p p → LLPO-Alt A p → WLPO A p
wpfp∧llpo-Alt⇒wlpo wpfp llpo-Alt {P = P} P? with wpfp P?
... | Q , Q? , ∀P→¬∀Q , ¬∀Q→∀P = Sum.map₂ (λ ∀Q ∀P → ∀P→¬∀Q ∀P ∀Q) ∀P⊎∀Q
  where
  ∀P⊎∀Q : (∀ x → P x) ⊎ (∀ x → Q x)
  ∀P⊎∀Q = llpo-Alt P? Q? (DN-map (Sum.swap ∘′ Sum.map₂ ¬∀Q→∀P) DN-Dec⊎)

-- WPFP ∧ MR <=> LPO
wpfp∧mr⇒lpo : ∀ {a p} {A : Set a} → WPFP A p p → MR A p → LPO A p
wpfp∧mr⇒lpo wpfp mr =
  wlpo-Alt∧mr⇒lpo (wlpo⇒wlpo-Alt (wpfp∧mp⊎-Alt⇒wlpo wpfp (mp⊎⇒mp⊎-Alt
                    (mp∨⇒mp⊎ (mr⇒mp∨ mr)))))
                  mr

-- Proposition 1.2.1.2 in [1]
{-
lpo⇒P1212 : ∀ {p} → LPO ℕ p →
            {P : ℕ → Set p} → DecU P →
            (∃ λ N → ∀ n → N ≤ n → ¬ P n) ⊎ (Σ (ℕ → ℕ) λ k → ∀ n → P (k n))
lpo⇒P1212 {p} lpo {P} P? = {!   !}
  where
  R : ℕ → Set p
  R k = ∀ n → k ≤ n → ¬ P n

  -- use lpo
  R? : DecU R
  R? k = ?
-}

-- Searchable set
-- Searchable <=> Inhabited ∧ LPO
searchable⇒lpo : ∀ {a p} {A : Set a} → Searchable A p → LPO A p
searchable⇒lpo searchable P? with searchable (¬-DecU P?)
... | x₀ , ¬Px₀→∀¬P = Sum.[ (λ Px₀  → inj₁ (x₀ , Px₀)) ,
                            (λ ¬Px₀ → inj₂ (∀¬P→¬∃P (¬Px₀→∀¬P ¬Px₀))) ]′
                          (P? x₀)

searchable⇒inhabited : ∀ {a p} {A : Set a} →
                       Searchable A p → Inhabited A
searchable⇒inhabited {p = p} searchable =
  proj₁ (searchable {P = λ _ → Lift p ⊤} λ _ → inj₁ (lift tt))

inhabited∧lpo⇒searchable : ∀ {a p} {A : Set a} →
                           Inhabited A → LPO A p → Searchable A p
inhabited∧lpo⇒searchable inhabited lpo P? with lpo (¬-DecU P?)
... | inj₁ (x , ¬Px) = x , (λ Px → contradiction Px ¬Px)
... | inj₂ ¬∃¬P      = inhabited , (λ _ → P?⇒¬∃¬P→∀P P? ¬∃¬P)

-- [1] Hannes Diener "Constructive Reverse Mathematics"
-- [2] Hajime lshihara "Markov’s principle, Church’s thesis and LindeUf’s theorem"


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}

{-

This file shows that the property of the natural numbers being a homotopy-initial algebra of
the functor (1 + _) is equivalent to fulfilling a closely related inductive elimination principle.

Proofing the latter is trivial, since the typechecker does the work for us.

For details see the paper [Homotopy-initial algebras in type theory](https://arxiv.org/abs/1504.05531)
by Steve Awodey, Nicola Gambino and Kristina Sojakova.

-}

module Cubical.Data.Nat.Algebra where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Path
open import Cubical.Foundations.Isomorphism
  hiding (section)
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Reflection.StrictEquiv

open import Cubical.Data.Nat.Base

private
  variable
    ℓ ℓ' : Level

record NatAlgebra ℓ : Type (ℓ-suc ℓ) where
  field
    Carrier  : Type ℓ
    alg-zero : Carrier
    alg-suc  : Carrier → Carrier

record NatMorphism (A : NatAlgebra ℓ) (B : NatAlgebra ℓ') : Type (ℓ-max ℓ ℓ') where
  open NatAlgebra
  field
    morph     : A .Carrier → B .Carrier
    comm-zero : morph (A .alg-zero) ≡ B .alg-zero
    comm-suc  : morph ∘ A .alg-suc ≡ B .alg-suc ∘ morph

record NatFiber (N : NatAlgebra ℓ') ℓ : Type (ℓ-max ℓ' (ℓ-suc ℓ)) where
  open NatAlgebra N
  field
    Fiber    : Carrier → Type ℓ
    fib-zero : Fiber alg-zero
    fib-suc  : ∀ {n} → Fiber n → Fiber (alg-suc n)

record NatSection {N : NatAlgebra ℓ'} (F : NatFiber N ℓ) : Type (ℓ-max ℓ' ℓ) where
  open NatAlgebra N
  open NatFiber F
  field
    section       : ∀ n → Fiber n
    sec-comm-zero : section alg-zero ≡ fib-zero
    sec-comm-suc  : ∀ n → section (alg-suc n) ≡ fib-suc (section n)

isNatHInitial  : NatAlgebra ℓ' → (ℓ : Level) → Type (ℓ-max ℓ' (ℓ-suc ℓ))
isNatHInitial N ℓ = (M : NatAlgebra ℓ) → isContr (NatMorphism N M)

isNatInductive : NatAlgebra ℓ' → (ℓ : Level) → Type (ℓ-max ℓ' (ℓ-suc ℓ))
isNatInductive N ℓ = (S : NatFiber N ℓ) → NatSection S

module AlgebraPropositionality {N : NatAlgebra ℓ'} where
  open NatAlgebra N
  isPropIsNatHInitial : isProp (isNatHInitial N ℓ)
  isPropIsNatHInitial = isPropΠ (λ _ → isPropIsContr)

  -- under the assumption that some shape is nat-inductive, the type of sections over any fiber
  -- is propositional
  module SectionProp (ind : isNatInductive N ℓ) {F : NatFiber N ℓ} (S T : NatSection F) where
    open NatFiber
    open NatSection

    ConnectingFiber : NatFiber N ℓ
    Fiber ConnectingFiber n = S .section n ≡ T .section n
    fib-zero ConnectingFiber = S .sec-comm-zero ∙∙ refl ∙∙ sym (T .sec-comm-zero)
    fib-suc ConnectingFiber {n} sntn = S .sec-comm-suc n ∙∙ (λ i → F .fib-suc (sntn i)) ∙∙ sym (T .sec-comm-suc n)

    open NatSection (ind ConnectingFiber)
      renaming (section to α ; sec-comm-zero to ζ ; sec-comm-suc to σ)

    squeezeSquare : ∀{a}{A : Type a}{w x y z : A} (p : w ≡ x) {q : x ≡ y} (r : z ≡ y)
                  → (P : w ≡ z) → (sq : P ≡ p ∙∙ q ∙∙ sym r) → I → I → A
    squeezeSquare p {q} r P sq i j = transport (sym (PathP≡doubleCompPathʳ p P q r)) sq i j

    S≡T : S ≡ T
    section (S≡T i) n = α n i
    sec-comm-zero (S≡T i) j  = squeezeSquare (S .sec-comm-zero)  (T .sec-comm-zero)  (α alg-zero)    ζ     j i
    sec-comm-suc (S≡T i) n j = squeezeSquare (S .sec-comm-suc n) (T .sec-comm-suc n) (α (alg-suc n)) (σ n) j i

  isPropIsNatInductive : isProp (isNatInductive N ℓ)
  isPropIsNatInductive a b i F = SectionProp.S≡T a (a F) (b F) i

module AlgebraHInd→HInit {N : NatAlgebra ℓ'} (ind : isNatInductive N ℓ) (M : NatAlgebra ℓ) where
  open NatAlgebra
  open NatFiber

  ConstFiberM : NatFiber N ℓ
  Fiber ConstFiberM _ = M .Carrier
  fib-zero ConstFiberM = M .alg-zero
  fib-suc ConstFiberM = M .alg-suc

  morph→section : NatMorphism N M → NatSection ConstFiberM
  morph→section x = record { section = morph ; sec-comm-zero = comm-zero ; sec-comm-suc = λ i n → comm-suc n i }
    where open NatMorphism x
  section→morph : NatSection ConstFiberM → NatMorphism N M
  section→morph x = record { morph = section ; comm-zero = sec-comm-zero ; comm-suc = λ n i → sec-comm-suc i n }
    where open NatSection x

  Morph≡Section : NatSection ConstFiberM ≡ NatMorphism N M
  Morph≡Section = ua e
    where
    unquoteDecl e = declStrictEquiv e section→morph morph→section

  isContrMorph : isContr (NatMorphism N M)
  isContrMorph = subst isContr Morph≡Section (inhProp→isContr (ind ConstFiberM) (AlgebraPropositionality.SectionProp.S≡T ind))

open NatAlgebra
open NatFiber
open NatSection
open NatMorphism

module AlgebraHInit→Ind (N : NatAlgebra ℓ') ℓ (hinit : isNatHInitial N (ℓ-max ℓ' ℓ)) (F : NatFiber N (ℓ-max ℓ' ℓ)) where

  ΣAlgebra : NatAlgebra (ℓ-max ℓ' ℓ)
  Carrier ΣAlgebra = Σ (N .Carrier) (F .Fiber)
  alg-zero ΣAlgebra = N .alg-zero , F .fib-zero
  alg-suc ΣAlgebra (n , fn) = N .alg-suc n , F .fib-suc fn

  -- the fact that we have to lift the Carrier obstructs readability a bit
  -- this is the same algebra as N, but lifted into the correct universe
  LiftN : NatAlgebra (ℓ-max ℓ' ℓ)
  Carrier LiftN = Lift {_} {ℓ} (N .Carrier)
  alg-zero LiftN = lift (N .alg-zero)
  alg-suc LiftN = lift ∘ N .alg-suc ∘ lower

  _!_ : ∀ {x y} → x ≡ y → F .Fiber x → F .Fiber y
  _!_ = subst (F .Fiber)

  -- from homotopy initiality of N we get
  -- 1) an algebra morphism μ from N → Σ N F together with proofs of commutativity with the algebras
  -- 2) projecting out the first component after μ, called α, will turn out to be the identity function
  -- 3) witnesses that μ respects the definitions given in ΣAlgebra
  --   a) at zero the witnesses are ζ and ζ-h
  --   b) at suc the witnesses are σ and σ-h
  open NatMorphism (hinit ΣAlgebra .fst) renaming (morph to μ ; comm-zero to μ-zc ; comm-suc to μ-sc)
  module _ n where open Σ (μ n) public renaming (fst to α ; snd to α-h)
  -- module _ i where open Σ (μ-zc i) public renaming (fst to ζ ; snd to ζ-h)
  ζ   : α (N .alg-zero) ≡ N .alg-zero
  ζ i = μ-zc i .fst
  ζ-h : PathP (λ i → F .Fiber (ζ i)) (α-h (N .alg-zero)) (F .fib-zero)
  ζ-h i = μ-zc i .snd
  -- module _ n i where open Σ (μ-sc i n) public renaming (fst to σ ; snd to σ-h)
  σ   : ∀ n → α (N .alg-suc n) ≡ N .alg-suc (α n)
  σ n i = μ-sc i n .fst
  σ-h : ∀ n → PathP (λ i → F .Fiber (σ n i)) (α-h (N .alg-suc n)) (F .fib-suc (α-h n))
  σ-h n i = μ-sc i n .snd

  -- liftMorph would be the identity morphism if it weren't for size issues
  liftMorph : NatMorphism N LiftN
  liftMorph = record { morph = lift ; comm-zero = refl ; comm-suc = refl }
  -- instead of abstractly defining morphism composition and a projection algebra morphism
  -- from Σ N F → N, define the composite directly. comm-zero and comm-suc thus are
  -- defined without path composition
  fst∘μ : NatMorphism N LiftN
  morph fst∘μ = lift ∘ α
  comm-zero fst∘μ i = lift (ζ i)
  comm-suc fst∘μ i n = lift (σ n i)

  fst∘μ≡id : fst∘μ ≡ liftMorph
  fst∘μ≡id = isContr→isProp (hinit LiftN) _ _

  -- we get a proof that the index is preserved uniformly
  P : ∀ n → α n ≡ n
  P n i = lower (fst∘μ≡id i .morph n)

  -- we also have proofs that α cancels after the algebra of N
  Q-zero : α (N .alg-zero) ≡ N .alg-zero
  Q-zero = ζ
  Q-suc : ∀ n → α (N .alg-suc n) ≡ N .alg-suc n
  Q-suc n = σ n ∙ cong (N .alg-suc) (P n)

  -- but P and Q are the same up to homotopy
  P-zero : P (N .alg-zero) ≡ Q-zero
  P-zero i j = hcomp (λ k → λ where
      (i = i0) → lower (fst∘μ≡id j .comm-zero (~ k))
      (i = i1) → ζ (j ∨ ~ k)
      (j = i0) → ζ (~ k)
      (j = i1) → N .alg-zero
    ) (N .alg-zero)
  P-suc : ∀ n → P (N .alg-suc n) ≡ Q-suc n
  P-suc n i j = hcomp (λ k → λ where
      (i = i0) → lower (fst∘μ≡id j .comm-suc (~ k) n)
      (i = i1) → compPath-filler' (σ n) (cong (N .alg-suc) (P n)) k j
      (j = i0) → σ n (~ k)
      (j = i1) → N .alg-suc n
    ) (N .alg-suc (P n j))

  Fsection : NatSection F
  section Fsection n = P n ! α-h n
  sec-comm-zero Fsection =
    P (N .alg-zero) ! α-h (N .alg-zero)
      ≡[ i ]⟨ P-zero i ! α-h _ ⟩
    Q-zero ! α-h (N .alg-zero)
      ≡⟨ fromPathP ζ-h ⟩
    F .fib-zero
      ∎
  sec-comm-suc Fsection n =
    P (N .alg-suc n) ! α-h (N .alg-suc n)
      ≡[ i ]⟨ P-suc n i ! α-h _ ⟩
    Q-suc n ! α-h (N .alg-suc n)
      ≡⟨ substComposite (F .Fiber) (σ n) (cong (N .alg-suc) (P n)) _ ⟩
    cong (N .alg-suc) (P n) ! (σ n ! α-h (N .alg-suc n))
      ≡[ i ]⟨ cong (N .alg-suc) (P n) ! fromPathP (σ-h n) i ⟩
    cong (N .alg-suc) (P n) ! (F .fib-suc (α-h n))
      ≡⟨ substCommSlice (F .Fiber) (F .Fiber ∘ N .alg-suc) (λ _ → F .fib-suc) (P n) (α-h n) ⟩
    F .fib-suc (P n ! α-h n)
      ∎

isNatInductive≡isNatHInitial : {N : NatAlgebra ℓ'} (ℓ : Level)
                             → isNatInductive N (ℓ-max ℓ' ℓ) ≡ isNatHInitial N (ℓ-max ℓ' ℓ)
isNatInductive≡isNatHInitial {_} {N} ℓ = hPropExt isPropIsNatInductive isPropIsNatHInitial ind→init init→ind where
  open AlgebraPropositionality
  open AlgebraHInit→Ind N ℓ renaming (Fsection to init→ind)
  open AlgebraHInd→HInit renaming (isContrMorph to ind→init)

-- given two homotopy initial algebras there is a path between the algebras
-- this implies moreover that the carrier types are isomorphic
-- according to 5.16 in the paper this could be strengthened to isContr (N ≡ M)
isNatHInitial→algebraPath : {N M : NatAlgebra ℓ}
                          → (hinitN : isNatHInitial N ℓ) (hinitM : isNatHInitial M ℓ)
                          → N ≡ M
isNatHInitial→algebraPath {N = N} {M} hinitN hinitM = N≡M where
  open Σ (hinitN M) renaming (fst to N→M)
  open Σ (hinitM N) renaming (fst to M→N)
  idN : NatMorphism N N
  idN = record { morph = λ x → x ; comm-zero = refl ; comm-suc = refl }
  idM : NatMorphism M M
  idM = record { morph = λ x → x ; comm-zero = refl ; comm-suc = refl }
  N→M→N : NatMorphism N N
  morph N→M→N = morph M→N ∘ morph N→M
  comm-zero N→M→N = (λ i → morph M→N (comm-zero N→M i)) ∙ comm-zero M→N
  comm-suc N→M→N = (λ i → morph M→N ∘ comm-suc N→M i) ∙ (λ i → comm-suc M→N i ∘ morph N→M)
  nmn≡idn : N→M→N ≡ idN
  nmn≡idn = isContr→isProp (hinitN N) _ _

  M→N→M : NatMorphism M M
  morph M→N→M = morph N→M ∘ morph M→N
  comm-zero M→N→M = (λ i → morph N→M (comm-zero M→N i)) ∙ comm-zero N→M
  comm-suc M→N→M = (λ i → morph N→M ∘ comm-suc M→N i) ∙ (λ i → comm-suc N→M i ∘ morph M→N)
  mnm≡idm : M→N→M ≡ idM
  mnm≡idm = isContr→isProp (hinitM M) _ _

  carrier≡ : N .Carrier ≡ M .Carrier
  carrier≡ = isoToPath (iso (N→M .morph) (M→N .morph) (λ x i → mnm≡idm i .morph x) (λ x i → nmn≡idn i .morph x))
  zero≡ : PathP (λ i → carrier≡ i) (N .alg-zero) (M .alg-zero)
  zero≡ = toPathP λ i → transportRefl (N→M .comm-zero i) i
  suc≡ : PathP (λ i → carrier≡ i → carrier≡ i) (N .alg-suc) (M .alg-suc)
  suc≡ = toPathP (
        transport refl ∘ N→M .morph ∘ N .alg-suc ∘ M→N .morph ∘ transport refl
          ≡[ i ]⟨ transportReflF i ∘ N→M .morph ∘ N .alg-suc ∘ M→N .morph ∘ transportReflF i ⟩
        N→M .morph ∘ N .alg-suc ∘ M→N .morph
          ≡[ i ]⟨ N→M .comm-suc i ∘ M→N .morph ⟩
        M .alg-suc ∘ N→M .morph ∘ M→N .morph
          ≡[ i ]⟨ M .alg-suc ∘ mnm≡idm i .morph ⟩
        M .alg-suc
          ∎) where
     transportReflF : transport refl ≡ (λ x → x)
     transportReflF = funExt transportRefl

  N≡M : N ≡ M
  Carrier (N≡M i) = carrier≡ i
  alg-zero (N≡M i) = zero≡ i
  alg-suc (N≡M i) = suc≡ i

-- the payoff, it is straight forward to define the algebra and show inductiveness of ℕ
NatAlgebraℕ : NatAlgebra ℓ-zero
Carrier NatAlgebraℕ = ℕ
alg-zero NatAlgebraℕ = zero
alg-suc NatAlgebraℕ = suc

isNatInductiveℕ : isNatInductive NatAlgebraℕ ℓ
section (isNatInductiveℕ F) = nat-sec where
  nat-sec : ∀ n → F .Fiber n
  nat-sec zero = F .fib-zero
  nat-sec (suc n) = F .fib-suc (nat-sec n)
sec-comm-zero (isNatInductiveℕ F) = refl
sec-comm-suc (isNatInductiveℕ F) n = refl

isNatHInitialℕ : isNatHInitial NatAlgebraℕ ℓ
isNatHInitialℕ = transport (isNatInductive≡isNatHInitial _) isNatInductiveℕ

ext: agda

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
------------------------------------------------------------------------
-- A variant of Paolo Capriotti's variant of higher lenses
------------------------------------------------------------------------

{-# OPTIONS --cubical #-}

import Equality.Path as P

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

open P.Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude as P hiding (id)

open import Bijection equality-with-J as B using (_↔_)
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as T using (∥_∥; ∣_∣)
open import Preimage equality-with-J as Preimage
open import Univalence-axiom equality-with-J

open import Lens.Non-dependent eq
import Lens.Non-dependent.Higher eq as Higher

private
  variable
    a b p : Level
    A B   : Type a
    P Q   : A → Type p

------------------------------------------------------------------------
-- Coherently-constant

-- Coherently constant type-valued functions.
--
-- This definition is based on Paolo Capriotti's definition of higher
-- lenses, but uses a family of equivalences instead of an equality.

Coherently-constant :
  {A : Type a} → (A → Type p) → Type (a ⊔ lsuc p)
Coherently-constant {p = p} {A = A} P =
  ∃ λ (Q : ∥ A ∥ → Type p) → ∀ x → P x ≃ Q ∣ x ∣

-- A preservation lemma for Coherently-constant.
--
-- Note that P and Q must target the same universe.

Coherently-constant-map :
  {P : A → Type p} {Q : B → Type p}
  (f : B → A) →
  (∀ x → P (f x) ≃ Q x) →
  Coherently-constant P → Coherently-constant Q
Coherently-constant-map {P = P} {Q = Q} f P≃Q (R , P≃R) =
    R ∘ T.∥∥-map f
  , λ x →
      Q x        ↝⟨ inverse $ P≃Q x ⟩
      P (f x)    ↝⟨ P≃R (f x) ⟩□
      R ∣ f x ∣  □

-- Coherently-constant is, in a certain sense, closed under Σ.
--
-- This lemma is due to Paolo Capriotti.

Coherently-constant-Σ :
  Coherently-constant P →
  Coherently-constant Q →
  Coherently-constant (λ x → ∃ λ (y : P x) → Q (x , y))
Coherently-constant-Σ {P = P} {Q = Q} (P′ , p) (Q′ , q) =
    (λ x → ∃ λ (y : P′ x) →
               Q′ (T.elim
                     (λ x → P′ x → ∥ ∃ P ∥)
                     (λ _ → Π-closure ext 1 λ _ →
                            T.truncation-is-proposition)
                     (λ x y → ∣ x , _≃_.from (p x) y ∣)
                     x y))
  , (λ x →

       (∃ λ (y : P x) → Q (x , y))                         ↝⟨ (Σ-cong (p x) λ y →

          Q (x , y)                                              ↝⟨ q (x , y) ⟩
          Q′ ∣ x , y ∣                                           ↝⟨ ≡⇒≃ $ cong Q′ $ T.truncation-is-proposition _ _ ⟩□
          Q′ ∣ x , _≃_.from (p x) (_≃_.to (p x) y) ∣             □) ⟩□

       (∃ λ (y : P′ ∣ x ∣) → Q′ ∣ x , _≃_.from (p x) y ∣)  □)

------------------------------------------------------------------------
-- The lens type family

-- Paolo Capriotti's variant of higher lenses, but with a family of
-- equivalences instead of an equality.

Lens : Type a → Type b → Type (lsuc (a ⊔ b))
Lens A B = ∃ λ (get : A → B) → Coherently-constant (get ⁻¹_)

-- Some derived definitions (based on Capriotti's).

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

  -- A getter.

  get : A → B
  get = proj₁ l

  -- A predicate.

  H : Pow a ∥ B ∥
  H = proj₁ (proj₂ l)

  -- An equivalence.

  get⁻¹-≃ : ∀ b → get ⁻¹ b ≃ H ∣ b ∣
  get⁻¹-≃ = proj₂ (proj₂ l)

  -- All the getter's "preimages" are equivalent.

  get⁻¹-constant : (b₁ b₂ : B) → get ⁻¹ b₁ ≃ get ⁻¹ b₂
  get⁻¹-constant b₁ b₂ =
    get ⁻¹ b₁  ↝⟨ get⁻¹-≃ b₁ ⟩
    H ∣ b₁ ∣   ↝⟨ ≡⇒≃ $ cong H $ T.truncation-is-proposition _ _ ⟩
    H ∣ b₂ ∣   ↝⟨ inverse $ get⁻¹-≃ b₂ ⟩□
    get ⁻¹ b₂  □

  -- The two directions of get⁻¹-constant.

  get⁻¹-const : (b₁ b₂ : B) → get ⁻¹ b₁ → get ⁻¹ b₂
  get⁻¹-const b₁ b₂ = _≃_.to (get⁻¹-constant b₁ b₂)

  get⁻¹-const⁻¹ : (b₁ b₂ : B) → get ⁻¹ b₂ → get ⁻¹ b₁
  get⁻¹-const⁻¹ b₁ b₂ = _≃_.from (get⁻¹-constant b₁ b₂)

  -- Some coherence properties.

  get⁻¹-const-∘ :
    (b₁ b₂ b₃ : B) (p : get ⁻¹ b₁) →
    get⁻¹-const b₂ b₃ (get⁻¹-const b₁ b₂ p) ≡ get⁻¹-const b₁ b₃ p
  get⁻¹-const-∘ b₁ b₂ b₃ p =
    _≃_.from (get⁻¹-≃ b₃)
      (≡⇒→ (cong H $ T.truncation-is-proposition _ _)
         (_≃_.to (get⁻¹-≃ b₂)
            (_≃_.from (get⁻¹-≃ b₂)
               (≡⇒→ (cong H $ T.truncation-is-proposition _ _)
                  (_≃_.to (get⁻¹-≃ b₁) p)))))                   ≡⟨ cong (_≃_.from (get⁻¹-≃ _) ∘ ≡⇒→ _) $
                                                                   _≃_.right-inverse-of (get⁻¹-≃ _) _ ⟩
    _≃_.from (get⁻¹-≃ b₃)
      (≡⇒→ (cong H $ T.truncation-is-proposition _ _)
         (≡⇒→ (cong H $ T.truncation-is-proposition _ _)
            (_≃_.to (get⁻¹-≃ b₁) p)))                           ≡⟨ cong (λ eq → _≃_.from (get⁻¹-≃ _) (_≃_.to eq (_≃_.to (get⁻¹-≃ _) _))) $ sym $
                                                                   ≡⇒≃-trans ext _ _ ⟩
    _≃_.from (get⁻¹-≃ b₃)
      (≡⇒→ (trans (cong H $ T.truncation-is-proposition _ _)
              (cong H $ T.truncation-is-proposition _ _))
            (_≃_.to (get⁻¹-≃ b₁) p))                            ≡⟨ cong (λ eq → _≃_.from (get⁻¹-≃ b₃) (≡⇒→ eq _)) $
                                                                   trans (sym $ cong-trans _ _ _) $
                                                                   cong (cong H) $ mono₁ 1 T.truncation-is-proposition _ _ ⟩∎
    _≃_.from (get⁻¹-≃ b₃)
      (≡⇒→ (cong H $ T.truncation-is-proposition _ _)
         (_≃_.to (get⁻¹-≃ b₁) p))                               ∎

  get⁻¹-const-id :
    (b : B) (p : get ⁻¹ b) → get⁻¹-const b b p ≡ p
  get⁻¹-const-id b p =
    get⁻¹-const b b p                                        ≡⟨ sym $ _≃_.left-inverse-of (get⁻¹-constant _ _) _ ⟩
    get⁻¹-const⁻¹ b b (get⁻¹-const b b (get⁻¹-const b b p))  ≡⟨ cong (get⁻¹-const⁻¹ b b) $ get⁻¹-const-∘ _ _ _ _ ⟩
    get⁻¹-const⁻¹ b b (get⁻¹-const b b p)                    ≡⟨ _≃_.left-inverse-of (get⁻¹-constant _ _) _ ⟩∎
    p                                                        ∎

  get⁻¹-const-inverse :
    (b₁ b₂ : B) (p : get ⁻¹ b₁) →
    get⁻¹-const b₁ b₂ p ≡ get⁻¹-const⁻¹ b₂ b₁ p
  get⁻¹-const-inverse b₁ b₂ p =
    sym $ _≃_.to-from (get⁻¹-constant _ _) (
      get⁻¹-const b₂ b₁ (get⁻¹-const b₁ b₂ p)  ≡⟨ get⁻¹-const-∘ _ _ _ _ ⟩
      get⁻¹-const b₁ b₁ p                      ≡⟨ get⁻¹-const-id _ _ ⟩∎
      p                                        ∎)

  -- A setter.

  set : A → B → A
  set a b =                    $⟨ get⁻¹-const _ _ ⟩
    (get ⁻¹ get a → get ⁻¹ b)  ↝⟨ _$ (a , refl _) ⟩
    get ⁻¹ b                   ↝⟨ proj₁ ⟩□
    A                          □

  -- Lens laws.

  get-set : ∀ a b → get (set a b) ≡ b
  get-set a b =
    get (proj₁ (get⁻¹-const (get a) b (a , refl _)))  ≡⟨ proj₂ (get⁻¹-const (get a) b (a , refl _)) ⟩∎
    b                                                 ∎

  set-get : ∀ a → set a (get a) ≡ a
  set-get a =
    proj₁ (get⁻¹-const (get a) (get a) (a , refl _))  ≡⟨ cong proj₁ $ get⁻¹-const-id _ _ ⟩∎
    a                                                 ∎

  set-set : ∀ a b₁ b₂ → set (set a b₁) b₂ ≡ set a b₂
  set-set a b₁ b₂ =
    proj₁ (get⁻¹-const (get (set a b₁)) b₂ (set a b₁ , refl _))  ≡⟨ elim¹
                                                                      (λ {b} eq →
                                                                         proj₁ (get⁻¹-const (get (set a b₁)) b₂ (set a b₁ , refl _)) ≡
                                                                         proj₁ (get⁻¹-const b b₂ (set a b₁ , eq)))
                                                                      (refl _)
                                                                      (get-set a b₁) ⟩
    proj₁ (get⁻¹-const b₁ b₂ (set a b₁ , get-set a b₁))          ≡⟨⟩

    proj₁ (get⁻¹-const b₁ b₂
             (get⁻¹-const (get a) b₁ (a , refl _)))              ≡⟨ cong proj₁ $ get⁻¹-const-∘ _ _ _ _ ⟩∎

    proj₁ (get⁻¹-const (get a) b₂ (a , refl _))                  ∎

  -- TODO: Can get-set-get and get-set-set be proved for the lens laws
  -- given above?

instance

  -- The lenses defined above have getters and setters.

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

------------------------------------------------------------------------
-- Equality characterisation lemmas

-- An equality characterisation lemma.

equality-characterisation₁ :
  {A : Type a} {B : Type b} {l₁ l₂ : Lens A B} →
  Block "equality-characterisation" →
  let open Lens in

  (l₁ ≡ l₂)
    ≃
  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     ∀ b p →
     subst (_$ ∣ b ∣) h
       (_≃_.to (get⁻¹-≃ l₁ b) (subst (_⁻¹ b) (sym g) p)) ≡
     _≃_.to (get⁻¹-≃ l₂ b) p)
equality-characterisation₁ {a = a} {l₁ = l₁} {l₂ = l₂} ⊠ =
  l₁ ≡ l₂                                                          ↝⟨ inverse $ Eq.≃-≡ $ Eq.↔⇒≃ Σ-assoc ⟩

  ((get l₁ , H l₁) , get⁻¹-≃ l₁) ≡ ((get l₂ , H l₂) , get⁻¹-≃ l₂)  ↔⟨ inverse B.Σ-≡,≡↔≡ ⟩

  (∃ λ (eq : (get l₁ , H l₁) ≡ (get l₂ , H l₂)) →
     subst (λ (g , H) → ∀ b → g ⁻¹ b ≃ H ∣ b ∣) eq (get⁻¹-≃ l₁) ≡
     get⁻¹-≃ l₂)                                                   ↝⟨ (Σ-cong-contra ≡×≡↔≡ λ _ → F.id) ⟩

  (∃ λ ((g , h) : get l₁ ≡ get l₂ × H l₁ ≡ H l₂) →
     subst (λ (g , H) → ∀ b → g ⁻¹ b ≃ H ∣ b ∣)
       (cong₂ _,_ g h) (get⁻¹-≃ l₁) ≡
     get⁻¹-≃ l₂)                                                   ↔⟨ inverse Σ-assoc ⟩

  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     subst (λ (g , H) → ∀ b → g ⁻¹ b ≃ H ∣ b ∣)
       (cong₂ _,_ g h) (get⁻¹-≃ l₁) ≡
     get⁻¹-≃ l₂)                                                   ↝⟨ (∃-cong λ _ → ∃-cong λ _ → inverse $
                                                                       Eq.extensionality-isomorphism ext) ⟩
  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     ∀ b → subst (λ (g , H) → ∀ b → g ⁻¹ b ≃ H ∣ b ∣)
             (cong₂ _,_ g h) (get⁻¹-≃ l₁) b ≡
           get⁻¹-≃ l₂ b)                                           ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ → ≡⇒↝ _ $ cong (_≡ _) $ sym $
                                                                       push-subst-application _ _) ⟩
  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     ∀ b → subst (λ (g , H) → g ⁻¹ b ≃ H ∣ b ∣)
             (cong₂ _,_ g h) (get⁻¹-≃ l₁ b) ≡
           get⁻¹-≃ l₂ b)                                           ↔⟨ (∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ → inverse $
                                                                       ≃-to-≡↔≡ ext) ⟩
  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     ∀ b p →
     _≃_.to (subst (λ (g , H) → g ⁻¹ b ≃ H ∣ b ∣)
               (cong₂ _,_ g h) (get⁻¹-≃ l₁ b)) p ≡
     _≃_.to (get⁻¹-≃ l₂ b) p)                                      ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                       ≡⇒↝ _ $ cong (_≡ _) $ lemma _ _ _ _) ⟩□
  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     ∀ b p →
     subst (_$ ∣ b ∣) h
       (_≃_.to (get⁻¹-≃ l₁ b) (subst (_⁻¹ b) (sym g) p)) ≡
     _≃_.to (get⁻¹-≃ l₂ b) p)                                      □
  where
  open Lens

  lemma : ∀ _ _ _ _ → _ ≡ _
  lemma g h b p =
    _≃_.to (subst (λ (g , H) → g ⁻¹ b ≃ H ∣ b ∣)
              (cong₂ _,_ g h) (get⁻¹-≃ l₁ b)) p                 ≡⟨ cong (_$ p) Eq.to-subst ⟩

    subst (λ (g , H) → g ⁻¹ b → H ∣ b ∣)
      (cong₂ _,_ g h) (_≃_.to (get⁻¹-≃ l₁ b)) p                 ≡⟨ subst-→ ⟩

    subst (λ (g , H) → H ∣ b ∣) (cong₂ _,_ g h)
      (_≃_.to (get⁻¹-≃ l₁ b)
         (subst (λ (g , H) → g ⁻¹ b) (sym $ cong₂ _,_ g h) p))  ≡⟨ subst-∘ _ _ _ ⟩

    subst (_$ ∣ b ∣) (cong proj₂ $ cong₂ _,_ g h)
      (_≃_.to (get⁻¹-≃ l₁ b)
         (subst (λ (g , H) → g ⁻¹ b) (sym $ cong₂ _,_ g h) p))  ≡⟨ cong₂ (λ p q → subst (λ (H : Pow a _) → H ∣ b ∣)
                                                                                p (_≃_.to (get⁻¹-≃ l₁ b) q))
                                                                     (cong-proj₂-cong₂-, _ _)
                                                                     (subst-∘ _ _ _) ⟩
    subst (_$ ∣ b ∣) h
      (_≃_.to (get⁻¹-≃ l₁ b)
         (subst (_⁻¹ b) (cong proj₁ $ sym $ cong₂ _,_ g h) p))  ≡⟨ cong (λ eq → subst (_$ ∣ b ∣) h
                                                                                (_≃_.to (get⁻¹-≃ l₁ b) (subst (_⁻¹ b) eq p))) $
                                                                   trans (cong-sym _ _) $
                                                                   cong sym $ cong-proj₁-cong₂-, _ _ ⟩∎
    subst (_$ ∣ b ∣) h
      (_≃_.to (get⁻¹-≃ l₁ b) (subst (_⁻¹ b) (sym g) p))         ∎

-- Another equality characterisation lemma.

equality-characterisation₂ :
  {l₁ l₂ : Lens A B} →
  Block "equality-characterisation" →
  let open Lens in

  (l₁ ≡ l₂)
    ≃
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     ∀ b p →
     subst P.id (h ∣ b ∣)
       (_≃_.to (get⁻¹-≃ l₁ b) (subst (_⁻¹ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃_.to (get⁻¹-≃ l₂ b) p)
equality-characterisation₂ {l₁ = l₁} {l₂ = l₂} ⊠ =
  l₁ ≡ l₂                                                           ↝⟨ equality-characterisation₁ ⊠ ⟩

  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     ∀ b p →
     subst (_$ ∣ b ∣) h
       (_≃_.to (get⁻¹-≃ l₁ b) (subst (_⁻¹ b) (sym g) p)) ≡
     _≃_.to (get⁻¹-≃ l₂ b) p)                                       ↝⟨ (Σ-cong-contra (Eq.extensionality-isomorphism bad-ext) λ _ →
                                                                        Σ-cong-contra (Eq.extensionality-isomorphism bad-ext) λ _ →
                                                                        F.id) ⟩
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     ∀ b p →
     subst (_$ ∣ b ∣) (⟨ext⟩ h)
       (_≃_.to (get⁻¹-≃ l₁ b) (subst (_⁻¹ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃_.to (get⁻¹-≃ l₂ b) p)                                       ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                        ≡⇒↝ _ $ cong (_≡ _) $
                                                                        subst-ext _ _) ⟩□
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     ∀ b p →
     subst P.id (h ∣ b ∣)
       (_≃_.to (get⁻¹-≃ l₁ b) (subst (_⁻¹ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃_.to (get⁻¹-≃ l₂ b) p)                                       □
  where
  open Lens

-- Yet another equality characterisation lemma.

equality-characterisation₃ :
  {A : Type a} {B : Type b}
  {l₁ l₂ : Lens A B} →
  Block "equality-characterisation" →
  Univalence (a ⊔ b) →
  let open Lens in

  (l₁ ≡ l₂)
    ≃
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≃ H l₂ b) →
     ∀ b p →
     _≃_.to (h ∣ b ∣)
       (_≃_.to (get⁻¹-≃ l₁ b) (subst (_⁻¹ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃_.to (get⁻¹-≃ l₂ b) p)
equality-characterisation₃ {l₁ = l₁} {l₂ = l₂} ⊠ univ =
  l₁ ≡ l₂                                                           ↝⟨ equality-characterisation₂ ⊠ ⟩

  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     ∀ b p →
     subst P.id (h ∣ b ∣)
       (_≃_.to (get⁻¹-≃ l₁ b) (subst (_⁻¹ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃_.to (get⁻¹-≃ l₂ b) p)                                       ↝⟨ (∃-cong λ _ →
                                                                        Σ-cong-contra (∀-cong ext λ _ → inverse $ ≡≃≃ univ) λ _ → F.id) ⟩
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≃ H l₂ b) →
     ∀ b p →
     subst P.id (≃⇒≡ univ (h ∣ b ∣))
       (_≃_.to (get⁻¹-≃ l₁ b) (subst (_⁻¹ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃_.to (get⁻¹-≃ l₂ b) p)                                       ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                        ≡⇒↝ _ $ cong (_≡ _) $
                                                                        trans (subst-id-in-terms-of-≡⇒↝ equivalence) $
                                                                        cong (λ eq → _≃_.to eq _) $
                                                                        _≃_.right-inverse-of (≡≃≃ univ) _) ⟩□
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≃ H l₂ b) →
     ∀ b p →
     _≃_.to (h ∣ b ∣)
       (_≃_.to (get⁻¹-≃ l₁ b) (subst (_⁻¹ b) (sym (⟨ext⟩ g)) p)) ≡
     _≃_.to (get⁻¹-≃ l₂ b) p)                                       □
  where
  open Lens

------------------------------------------------------------------------
-- Conversion functions

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

Lens⇔Higher-lens : Lens A B ⇔ Higher.Lens A B
Lens⇔Higher-lens {A = A} {B = B} = record
  { to = λ (g , H , eq) → record
           { R = Σ ∥ B ∥ H

           ; equiv =
               A                                      ↔⟨ (inverse $ drop-⊤-right λ _ → _⇔_.to contractible⇔↔⊤ $
                                                          other-singleton-contractible _) ⟩
               (∃ λ (a : A) → ∃ λ (b : B) → g a ≡ b)  ↔⟨ ∃-comm ⟩
               (∃ λ (b : B) → g ⁻¹ b)                 ↝⟨ ∃-cong eq ⟩
               (∃ λ (b : B) → H ∣ b ∣)                ↝⟨ (Σ-cong (inverse T.∥∥×≃) λ _ → ≡⇒↝ _ $ cong H $ T.truncation-is-proposition _ _) ⟩
               (∃ λ ((b , _) : ∥ B ∥ × B) → H b)      ↔⟨ Σ-assoc F.∘
                                                         (∃-cong λ _ → ×-comm) F.∘
                                                         inverse Σ-assoc ⟩□
               Σ ∥ B ∥ H × B                          □

           ; inhabited = proj₁
           }
  ; from = λ l →
               Higher.Lens.get l
             , (λ _ → Higher.Lens.R l)
             , (λ b → inverse (Higher.remainder≃get⁻¹ l b))
  }

-- The conversion preserves getters and setters.

Lens⇔Higher-lens-preserves-getters-and-setters :
  Preserves-getters-and-setters-⇔ A B Lens⇔Higher-lens
Lens⇔Higher-lens-preserves-getters-and-setters =
    (λ l@(g , H , eq) →
         refl _
       , ⟨ext⟩ λ a → ⟨ext⟩ λ b →
         let h₁ = _≃_.to (eq (g a)) (a , refl _)

             h₂ =
               _≃_.from (≡⇒≃ (cong H _))
                 (subst (H ∘ proj₁) (sym (_≃_.left-inverse-of T.∥∥×≃ _))
                    (≡⇒→ (cong H _) h₁))

             h₃ = ≡⇒→ (cong H _) h₁

             lemma =
               h₂                                                         ≡⟨ sym $ subst-in-terms-of-inverse∘≡⇒↝ equivalence _ _ _ ⟩

               subst H _
                 (subst (H ∘ proj₁) (sym (_≃_.left-inverse-of T.∥∥×≃ _))
                    (≡⇒→ (cong H _) h₁))                                  ≡⟨ cong (λ x → subst H (sym $ T.truncation-is-proposition _ _)
                                                                                (subst (H ∘ proj₁)
                                                                                (sym (_≃_.left-inverse-of T.∥∥×≃ (∣ g a ∣ , b)))
                                                                                x)) $ sym $
                                                                             subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩
               subst H _
                 (subst (H ∘ proj₁) (sym (_≃_.left-inverse-of T.∥∥×≃ _))
                    (subst H _ h₁))                                       ≡⟨ cong (λ x → subst H (sym $ T.truncation-is-proposition _ _) x) $
                                                                             subst-∘ _ _ _ ⟩

               subst H _ (subst H _ (subst H _ h₁))                       ≡⟨ cong (λ x → subst H (sym $ T.truncation-is-proposition _ _) x) $
                                                                             subst-subst _ _ _ _ ⟩

               subst H _ (subst H _ h₁)                                   ≡⟨ subst-subst _ _ _ _ ⟩

               subst H _ h₁                                               ≡⟨ cong (λ eq → subst H eq h₁) $
                                                                             mono₁ 1 T.truncation-is-proposition _ _ ⟩

               subst H _ h₁                                               ≡⟨ subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩∎

               ≡⇒→ (cong H _) h₁                                          ∎
         in
         Higher.Lens.set (_⇔_.to Lens⇔Higher-lens l) a b  ≡⟨⟩
         proj₁ (_≃_.from (eq b) h₂)                       ≡⟨ cong (λ h → proj₁ (_≃_.from (eq b) h)) lemma ⟩
         proj₁ (_≃_.from (eq b) h₃)                       ≡⟨⟩
         Lens.set l a b                                   ∎)
  , (λ l →
         refl _
       , ⟨ext⟩ λ a → ⟨ext⟩ λ b →
         Lens.set (_⇔_.from Lens⇔Higher-lens l) a b        ≡⟨⟩

         _≃_.from (Higher.Lens.equiv l)
           ( ≡⇒→ (cong (λ _ → Higher.Lens.R l) _)
               (Higher.Lens.remainder l a)
           , b
           )                                               ≡⟨ cong (λ eq → _≃_.from (Higher.Lens.equiv l) (≡⇒→ eq _ , b)) $
                                                              cong-const _ ⟩
         _≃_.from (Higher.Lens.equiv l)
           (≡⇒→ (refl _) (Higher.Lens.remainder l a) , b)  ≡⟨ cong (λ f → _≃_.from (Higher.Lens.equiv l) (f _ , b)) $
                                                              ≡⇒→-refl ⟩
         _≃_.from (Higher.Lens.equiv l)
           (Higher.Lens.remainder l a , b)                 ≡⟨⟩

         Higher.Lens.set l a b                             ∎)

-- Lens A B is equivalent to Higher.Lens A B (assuming univalence).

Lens≃Higher-lens :
  {A : Type a} {B : Type b} →
  Block "conversion" →
  Univalence (a ⊔ b) →
  Lens A B ≃ Higher.Lens A B
Lens≃Higher-lens {A = A} {B = B} ⊠ univ =
  Eq.↔→≃ to from to∘from from∘to
  where
  to = _⇔_.to Lens⇔Higher-lens

  from = _⇔_.from Lens⇔Higher-lens

  to∘from : ∀ l → to (from l) ≡ l
  to∘from l = _↔_.from (Higher.equality-characterisation₂ ⊠ univ)
    ( (∥ B ∥ × R  ↔⟨ (drop-⊤-left-× λ r → _⇔_.to contractible⇔↔⊤ $
                      propositional⇒inhabited⇒contractible
                        T.truncation-is-proposition
                        (inhabited r)) ⟩□
       R          □)
    , (λ a →
         ≡⇒→ (cong (λ _ → R) (T.truncation-is-proposition _ _))
           (remainder a)                                         ≡⟨ cong (λ eq → ≡⇒→ eq _) $ cong-const _ ⟩

         ≡⇒→ (refl _) (remainder a)                              ≡⟨ cong (_$ _) ≡⇒→-refl ⟩∎

         remainder a                                             ∎)
    , (λ _ → refl _)
    )
    where
    open Higher.Lens l

  from∘to : ∀ l → from (to l) ≡ l
  from∘to l = _≃_.from (equality-characterisation₃ ⊠ univ)
    ( (λ _ → refl _)
    , Σ∥B∥H≃H
    , (λ b p@(a , get-a≡b) →
         _≃_.to (Σ∥B∥H≃H ∣ b ∣)
           (_≃_.from (Higher.remainder≃get⁻¹ (to l) b)
              (subst (_⁻¹ b) (sym (⟨ext⟩ λ _ → refl _)) p))             ≡⟨ cong (_≃_.to (Σ∥B∥H≃H ∣ b ∣) ∘
                                                                                _≃_.from (Higher.remainder≃get⁻¹ (to l) b)) $
                                                                           trans (cong (flip (subst (_⁻¹ b)) p) $
                                                                                trans (cong sym ext-refl) $
                                                                                sym-refl) $
                                                                           subst-refl _ _ ⟩
         _≃_.to (Σ∥B∥H≃H ∣ b ∣)
           (_≃_.from (Higher.remainder≃get⁻¹ (to l) b) p)               ≡⟨⟩

         _≃_.to (Σ∥B∥H≃H ∣ b ∣) (Higher.Lens.remainder (to l) a)        ≡⟨⟩

         subst H _
           (≡⇒→ (cong H _) (_≃_.to (get⁻¹-≃ (get a)) (a , refl _)))     ≡⟨ cong (subst H _) $ sym $
                                                                           subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩

         subst H _ (subst H _ (_≃_.to (get⁻¹-≃ (get a)) (a , refl _)))  ≡⟨ subst-subst _ _ _ _ ⟩

         subst H _ (_≃_.to (get⁻¹-≃ (get a)) (a , refl _))              ≡⟨ cong (λ eq → subst H eq (_≃_.to (get⁻¹-≃ (get a)) (a , refl _))) $
                                                                           mono₁ 1 T.truncation-is-proposition _ _ ⟩
         subst H (cong ∣_∣ get-a≡b)
           (_≃_.to (get⁻¹-≃ (get a)) (a , refl _))                      ≡⟨ elim¹
                                                                             (λ {b} eq →
                                                                                subst H (cong ∣_∣ eq)
                                                                                (_≃_.to (get⁻¹-≃ (get a)) (a , refl _)) ≡
                                                                                _≃_.to (get⁻¹-≃ b) (a , eq))
                                                                             (
           subst H (cong ∣_∣ (refl _))
             (_≃_.to (get⁻¹-≃ (get a)) (a , refl _))                          ≡⟨ trans (cong (flip (subst H) _) $ cong-refl _) $
                                                                                subst-refl _ _ ⟩
           _≃_.to (get⁻¹-≃ (get a)) (a , refl _)                              ∎)
                                                                             _ ⟩∎
         _≃_.to (get⁻¹-≃ b) p                                           ∎)
    )
    where
    open Lens l

    Σ∥B∥H≃H = λ b →
      Σ ∥ B ∥ H  ↔⟨ (drop-⊤-left-Σ $ _⇔_.to contractible⇔↔⊤ $
                     propositional⇒inhabited⇒contractible
                       T.truncation-is-proposition b) ⟩□
      H b        □

-- The equivalence preserves getters and setters.

Lens≃Higher-lens-preserves-getters-and-setters :
  {A : Type a} {B : Type b}
  (bl : Block "conversion")
  (univ : Univalence (a ⊔ b)) →
  Preserves-getters-and-setters-⇔ A B
    (_≃_.logical-equivalence (Lens≃Higher-lens bl univ))
Lens≃Higher-lens-preserves-getters-and-setters ⊠ _ =
  Lens⇔Higher-lens-preserves-getters-and-setters

------------------------------------------------------------------------
-- Identity

-- An identity lens.

id : {A : Type a} → Lens A A
id =
    P.id
  , (λ _ → ↑ _ ⊤)
  , (λ a →
       P.id ⁻¹ a  ↔⟨ _⇔_.to contractible⇔↔⊤ $ Preimage.id⁻¹-contractible _ ⟩
       ⊤          ↔⟨ inverse B.↑↔ ⟩□
       ↑ _ ⊤      □)

------------------------------------------------------------------------
-- Some results related to fibres of Lens.set

-- When proving that Lens.set ⁻¹ s is a proposition, for
-- s : A → B → A, one can assume that B is inhabited.
--
-- This result is due to Andrea Vezzosi.

[codomain-inhabited→proposition]→proposition :
  {s : A → B → A} →
  (B → Is-proposition (Lens.set ⁻¹ s)) ≃
  Is-proposition (Lens.set ⁻¹ s)
[codomain-inhabited→proposition]→proposition {B = B} {s = s} =
  block λ b →

  (B → Is-proposition (Lens.set ⁻¹ s))      ↝⟨ inverse $ T.universal-property (H-level-propositional ext 1) ⟩
  (∥ B ∥ → Is-proposition (Lens.set ⁻¹ s))  ↔⟨⟩
  (∥ B ∥ → (p q : Lens.set ⁻¹ s) → p ≡ q)   ↔⟨ (∀-cong ext λ _ → Π-comm) F.∘ Π-comm ⟩
  ((p q : Lens.set ⁻¹ s) → ∥ B ∥ → p ≡ q)   ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → lemma b _ _) ⟩
  ((p q : Lens.set ⁻¹ s) → p ≡ q)           ↔⟨⟩
  Is-proposition (Lens.set ⁻¹ s)            □
  where
  open Lens

  lemma :
    (b : Block "equality-characterisation") →
    (p₁ p₂ : Lens.set ⁻¹ s) →
    (∥ B ∥ → p₁ ≡ p₂) ≃ (p₁ ≡ p₂)
  lemma b p₁@(l₁ , eq₁) p₂@(l₂ , eq₂) =
    (∥ B ∥ → p₁ ≡ p₂)                                           ↝⟨ (∀-cong ext λ _ → ec) ⟩

    (∥ B ∥ →
     ∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
     ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     ∃ λ (f : ∀ b p →
              subst P.id (h ∣ b ∣)
                (_≃_.to (get⁻¹-≃ l₁ b)
                   (subst (_⁻¹ b) (sym (⟨ext⟩ g)) p)) ≡
              _≃_.to (get⁻¹-≃ l₂ b) p) →
       ∀ a → ext⁻¹ (subst (λ l → Lens.set l ≡ s)
                      (_≃_.from (equality-characterisation₂ b)
                         (g , h , f)) eq₁) a ≡
             ext⁻¹ eq₂ a)                                       ↝⟨ T.push-∥∥ (∣_∣ ∘ get l₁) ⟩

    (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
     ∥ B ∥ →
     ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     ∃ λ (f : ∀ b p →
              subst P.id (h ∣ b ∣)
                (_≃_.to (get⁻¹-≃ l₁ b)
                   (subst (_⁻¹ b) (sym (⟨ext⟩ g)) p)) ≡
              _≃_.to (get⁻¹-≃ l₂ b) p) →
       ∀ a → ext⁻¹ (subst (λ l → Lens.set l ≡ s)
                      (_≃_.from (equality-characterisation₂ b)
                         (g , h , f)) eq₁) a ≡
             ext⁻¹ eq₂ a)                                       ↝⟨ (∃-cong λ _ → T.push-∥∥ P.id) ⟩

    (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
     ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     ∥ B ∥ →
     ∃ λ (f : ∀ b p →
              subst P.id (h ∣ b ∣)
                (_≃_.to (get⁻¹-≃ l₁ b)
                   (subst (_⁻¹ b) (sym (⟨ext⟩ g)) p)) ≡
              _≃_.to (get⁻¹-≃ l₂ b) p) →
       ∀ a → ext⁻¹ (subst (λ l → Lens.set l ≡ s)
                      (_≃_.from (equality-characterisation₂ b)
                         (g , h , f)) eq₁) a ≡
             ext⁻¹ eq₂ a)                                       ↝⟨ (∃-cong λ _ → ∃-cong λ _ → T.push-∥∥ ∣_∣) ⟩

    (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
     ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     ∃ λ (f : ∀ b p →
              subst P.id (h ∣ b ∣)
                (_≃_.to (get⁻¹-≃ l₁ b)
                   (subst (_⁻¹ b) (sym (⟨ext⟩ g)) p)) ≡
              _≃_.to (get⁻¹-≃ l₂ b) p) →
       ∥ B ∥ →
       ∀ a → ext⁻¹ (subst (λ l → Lens.set l ≡ s)
                      (_≃_.from (equality-characterisation₂ b)
                         (g , h , f)) eq₁) a ≡
             ext⁻¹ eq₂ a)                                       ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → T.drop-∥∥ (∣_∣ ∘ get l₁)) ⟩

    (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
     ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     ∃ λ (f : ∀ b p →
              subst P.id (h ∣ b ∣)
                (_≃_.to (get⁻¹-≃ l₁ b)
                   (subst (_⁻¹ b) (sym (⟨ext⟩ g)) p)) ≡
              _≃_.to (get⁻¹-≃ l₂ b) p) →
       ∀ a → ext⁻¹ (subst (λ l → Lens.set l ≡ s)
                      (_≃_.from (equality-characterisation₂ b)
                         (g , h , f)) eq₁) a ≡
             ext⁻¹ eq₂ a)                                       ↝⟨ inverse ec ⟩□

    p₁ ≡ p₂                                                     □
    where
    ec =
      p₁ ≡ p₂                                                     ↔⟨ inverse B.Σ-≡,≡↔≡ ⟩

      (∃ λ (l : l₁ ≡ l₂) →
         subst (λ l → Lens.set l ≡ s) l eq₁ ≡ eq₂)                ↝⟨ (∃-cong λ _ → inverse $
                                                                      Eq.≃-≡ $ inverse $ Eq.extensionality-isomorphism ext) ⟩
      (∃ λ (l : l₁ ≡ l₂) →
         ext⁻¹ (subst (λ l → Lens.set l ≡ s) l eq₁) ≡ ext⁻¹ eq₂)  ↝⟨ (∃-cong λ _ → inverse $
                                                                      Eq.extensionality-isomorphism ext) ⟩
      (∃ λ (l : l₁ ≡ l₂) →
         ∀ a → ext⁻¹ (subst (λ l → Lens.set l ≡ s) l eq₁) a ≡
               ext⁻¹ eq₂ a)                                       ↝⟨ (Σ-cong-contra (inverse $ equality-characterisation₂ b) λ _ → F.id) ⟩

      (∃ λ (l : ∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
                ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
                  ∀ b p →
                  subst P.id (h ∣ b ∣)
                    (_≃_.to (get⁻¹-≃ l₁ b)
                       (subst (_⁻¹ b) (sym (⟨ext⟩ g)) p)) ≡
                  _≃_.to (get⁻¹-≃ l₂ b) p) →
         ∀ a → ext⁻¹ (subst (λ l → Lens.set l ≡ s)
                        (_≃_.from (equality-characterisation₂ b)
                           l) eq₁) a ≡
               ext⁻¹ eq₂ a)                                       ↔⟨ (∃-cong λ _ → inverse Σ-assoc) F.∘ inverse Σ-assoc ⟩□

      (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
       ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
       ∃ λ (f : ∀ b p →
                subst P.id (h ∣ b ∣)
                  (_≃_.to (get⁻¹-≃ l₁ b)
                     (subst (_⁻¹ b) (sym (⟨ext⟩ g)) p)) ≡
                _≃_.to (get⁻¹-≃ l₂ b) p) →
         ∀ a → ext⁻¹ (subst (λ l → Lens.set l ≡ s)
                        (_≃_.from (equality-characterisation₂ b)
                           (g , h , f)) eq₁) a ≡
               ext⁻¹ eq₂ a)                                       □

-- The previous result holds also for the lenses in Higher (assuming
-- univalence).

[codomain-inhabited→proposition]→proposition-for-higher :
  {A : Type a} {B : Type b} {s : A → B → A} →
  Univalence (a ⊔ b) →
  (B → Is-proposition (Higher.Lens.set ⁻¹ s)) ≃
  Is-proposition (Higher.Lens.set ⁻¹ s)
[codomain-inhabited→proposition]→proposition-for-higher
  {A = A} {B = B} {s = s} univ =

  (B → Is-proposition (Higher.Lens.set ⁻¹ s))  ↝⟨ (∀-cong ext λ _ → H-level-cong ext 1 lemma) ⟩
  (B → Is-proposition (Lens.set ⁻¹ s))         ↝⟨ [codomain-inhabited→proposition]→proposition ⟩
  Is-proposition (Lens.set ⁻¹ s)               ↝⟨ inverse $ H-level-cong ext 1 lemma ⟩□
  Is-proposition (Higher.Lens.set ⁻¹ s)        □
  where
  lemma : Higher.Lens.set ⁻¹ s ≃ Lens.set ⁻¹ s
  lemma = block λ b →
    (∃ λ (l : Higher.Lens A B) → Higher.Lens.set l ≡ s)  ↝⟨ (Σ-cong (inverse $ Lens≃Higher-lens b univ) λ l →
                                                             ≡⇒↝ _ $ cong (_≡ s) $ sym $ proj₂ $
                                                             proj₂ (Lens≃Higher-lens-preserves-getters-and-setters b univ) l) ⟩□
    (∃ λ (l : Lens A B) → Lens.set l ≡ s)                □

-- If a certain variant of Higher.lenses-equal-if-setters-equal can be
-- proved, then Higher.Lens.set ⁻¹ s is a proposition (assuming
-- univalence).

lenses-equal-if-setters-equal→set⁻¹-proposition :
  {A : Type a} {B : Type b}
  (univ : Univalence (a ⊔ b)) →
  ((l₁ l₂ : Higher.Lens A B) →
   B →
   (s : Higher.Lens.set l₁ ≡ Higher.Lens.set l₂) →
   ∃ λ (l : l₁ ≡ l₂) → cong Higher.Lens.set l ≡ s) →
  (s : A → B → A) →
  Is-proposition (Higher.Lens.set ⁻¹ s)
lenses-equal-if-setters-equal→set⁻¹-proposition
  {B = B} univ lenses-equal-if-setters-equal s =
                                               $⟨ lemma ⟩
  (B → Is-proposition (Higher.Lens.set ⁻¹ s))  ↝⟨ [codomain-inhabited→proposition]→proposition-for-higher univ ⟩□
  Is-proposition (Higher.Lens.set ⁻¹ s)        □
  where
  lemma : B → Is-proposition (Higher.Lens.set ⁻¹ s)
  lemma b (l₁ , set-l₁≡s) (l₂ , set-l₂≡s) = Σ-≡,≡→≡
    lemma₁
    (subst (λ l → set l ≡ s) lemma₁ set-l₁≡s                     ≡⟨ subst-∘ _ _ _ ⟩
     subst (_≡ s) (cong set lemma₁) set-l₁≡s                     ≡⟨ subst-trans-sym ⟩
     trans (sym (cong set lemma₁)) set-l₁≡s                      ≡⟨ cong (λ eq → trans (sym eq) set-l₁≡s) lemma₂ ⟩
     trans (sym (trans set-l₁≡s (sym set-l₂≡s))) set-l₁≡s        ≡⟨ cong (λ eq → trans eq set-l₁≡s) $ sym-trans _ _ ⟩
     trans (trans (sym (sym set-l₂≡s)) (sym set-l₁≡s)) set-l₁≡s  ≡⟨ trans-[trans-sym]- _ _ ⟩
     sym (sym set-l₂≡s)                                          ≡⟨ sym-sym _ ⟩∎
     set-l₂≡s                                                    ∎)
    where
    open Higher.Lens

    lemma′ =
      lenses-equal-if-setters-equal l₁ l₂ b
        (set l₁  ≡⟨ set-l₁≡s ⟩
         s       ≡⟨ sym set-l₂≡s ⟩∎
         set l₂  ∎)

    lemma₁ = proj₁ lemma′
    lemma₂ = proj₂ lemma′

-- If a certain variant of Higher.lenses-equal-if-setters-equal can be
-- proved, then lenses with equal setters are equal (assuming
-- univalence).

lenses-equal-if-setters-equal→lenses-equal-if-setters-equal :
  {A : Type a} {B : Type b} →
  Univalence (a ⊔ b) →
  ((l₁ l₂ : Higher.Lens A B) →
   B →
   (s : Higher.Lens.set l₁ ≡ Higher.Lens.set l₂) →
   ∃ λ (l : l₁ ≡ l₂) → cong Higher.Lens.set l ≡ s) →
  (l₁ l₂ : Higher.Lens A B) →
  Higher.Lens.set l₁ ≡ Higher.Lens.set l₂ →
  l₁ ≡ l₂
lenses-equal-if-setters-equal→lenses-equal-if-setters-equal
  univ lenses-equal-if-setters-equal l₁ l₂ s =
  cong proj₁ (
    (l₁ , s)       ≡⟨ lenses-equal-if-setters-equal→set⁻¹-proposition
                        univ lenses-equal-if-setters-equal (Higher.Lens.set l₂) _ _ ⟩∎
    (l₂ , refl _)  ∎)

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


text:
module README where

------------------------------------------------------------------------
-- The Agda standard library, version 1.3
--
-- Authors: Nils Anders Danielsson, Matthew Daggitt, Guillaume Allais
-- with contributions from Andreas Abel, Stevan Andjelkovic,
-- Jean-Philippe Bernardy, Peter Berry, Bradley Hardy Joachim Breitner,
-- Samuel Bronson, Daniel Brown, Jacques Carette, James Chapman,
-- Liang-Ting Chen, Dominique Devriese, Dan Doel, Érdi Gergő,
-- Zack Grannan, Helmut Grohne, Simon Foster, Liyang Hu, Jason Hu,
-- Patrik Jansson, Alan Jeffrey, Wen Kokke, Evgeny Kotelnikov,
-- Sergei Meshveliani, Eric Mertens, Darin Morrison, Guilhem Moulin,
-- Shin-Cheng Mu, Ulf Norell, Noriyuki Ohkawa, Nicolas Pouillard,
-- Andrés Sicard-Ramírez, Lex van der Stoep, Sandro Stucki, Milo Turner,
-- Noam Zeilberger and other anonymous contributors.
------------------------------------------------------------------------

-- This version of the library has been tested using Agda 2.6.1.

-- The library comes with a .agda-lib file, for use with the library
-- management system.

-- Currently the library does not support the JavaScript compiler
-- backend.

------------------------------------------------------------------------
-- Module hierarchy
------------------------------------------------------------------------

-- The top-level module names of the library are currently allocated
-- as follows:
--
-- • Algebra
--     Abstract algebra (monoids, groups, rings etc.), along with
--     properties needed to specify these structures (associativity,
--     commutativity, etc.), and operations on and proofs about the
--     structures.

-- • Axiom
--     Types and consequences of various additional axioms not
--     necessarily included in Agda, e.g. uniqueness of identity
--     proofs, function extensionality and excluded middle.

import README.Axiom

-- • Category
--     Category theory-inspired idioms used to structure functional
--     programs (functors and monads, for instance).

-- • Codata
--     Coinductive data types and properties. There are two different
--     approaches taken. The `Codata` folder contains the new more
--     standard approach using sized types. The `Codata.Musical`
--     folder contains modules using the old musical notation.

-- • Data
--     Data types and properties.

import README.Data

-- • Function
--     Combinators and properties related to functions.

-- • Foreign
--     Related to the foreign function interface.

-- • Induction
--     A general framework for induction (includes lexicographic and
--     well-founded induction).

-- • IO
--     Input/output-related functions.

-- • Level
--     Universe levels.

-- • Reflection
--     Support for reflection.

-- • Relation
--     Properties of and proofs about relations.

-- • Size
--     Sizes used by the sized types mechanism.

-- • Strict
--     Provides access to the builtins relating to strictness.

-- • Tactic
--     Tactics for automatic proof generation

------------------------------------------------------------------------
-- A selection of useful library modules
------------------------------------------------------------------------

-- Note that module names in source code are often hyperlinked to the
-- corresponding module. In the Emacs mode you can follow these
-- hyperlinks by typing M-. or clicking with the middle mouse button.

-- • Some data types

import Data.Bool     -- Booleans.
import Data.Char     -- Characters.
import Data.Empty    -- The empty type.
import Data.Fin      -- Finite sets.
import Data.List     -- Lists.
import Data.Maybe    -- The maybe type.
import Data.Nat      -- Natural numbers.
import Data.Product  -- Products.
import Data.String   -- Strings.
import Data.Sum      -- Disjoint sums.
import Data.Unit     -- The unit type.
import Data.Vec      -- Fixed-length vectors.

-- • Some co-inductive data types

import Codata.Stream -- Streams.
import Codata.Colist -- Colists.

-- • Some types used to structure computations

import Category.Functor      -- Functors.
import Category.Applicative  -- Applicative functors.
import Category.Monad        -- Monads.

-- • Equality

-- Propositional equality:
import Relation.Binary.PropositionalEquality

-- Convenient syntax for "equational reasoning" using a preorder:
import Relation.Binary.Reasoning.Preorder

-- Solver for commutative ring or semiring equalities:
import Algebra.Solver.Ring

-- • Properties of functions, sets and relations

-- Monoids, rings and similar algebraic structures:
import Algebra

-- Negation, decidability, and similar operations on sets:
import Relation.Nullary

-- Properties of homogeneous binary relations:
import Relation.Binary

-- • Induction

-- An abstraction of various forms of recursion/induction:
import Induction

-- Well-founded induction:
import Induction.WellFounded

-- Various forms of induction for natural numbers:
import Data.Nat.Induction

-- • Support for coinduction

import Codata.Musical.Notation
import Codata.Thunk

-- • IO

import IO

------------------------------------------------------------------------
-- Record hierarchies
------------------------------------------------------------------------

-- When an abstract hierarchy of some sort (for instance semigroup →
-- monoid → group) is included in the library the basic approach is to
-- specify the properties of every concept in terms of a record
-- containing just properties, parameterised on the underlying
-- operations, sets etc.:
--
--   record IsSemigroup {A} (≈ : Rel A) (∙ : Op₂ A) : Set where
--     open FunctionProperties ≈
--     field
--       isEquivalence : IsEquivalence ≈
--       assoc         : Associative ∙
--       ∙-cong        : ∙ Preserves₂ ≈ ⟶ ≈ ⟶ ≈
--
-- More specific concepts are then specified in terms of the simpler
-- ones:
--
--     record IsMonoid {A} (≈ : Rel A) (∙ : Op₂ A) (ε : A) : Set where
--       open FunctionProperties ≈
--       field
--         isSemigroup : IsSemigroup ≈ ∙
--         identity    : Identity ε ∙
--
--     open IsSemigroup isSemigroup public
--
-- Note here that `open IsSemigroup isSemigroup public` ensures that the
-- fields of the isSemigroup record can be accessed directly; this
-- technique enables the user of an IsMonoid record to use underlying
-- records without having to manually open an entire record hierarchy.
-- This is not always possible, though. Consider the following definition
-- of preorders:
--
--   record IsPreorder {A : Set}
--                     (_≈_ : Rel A) -- The underlying equality.
--                     (_∼_ : Rel A) -- The relation.
--                     : Set where
--     field
--       isEquivalence : IsEquivalence _≈_
--       -- Reflexivity is expressed in terms of an underlying equality:
--       reflexive     : _≈_ ⇒ _∼_
--       trans         : Transitive _∼_
--
--     module Eq = IsEquivalence isEquivalence
--
--     ...
--
-- The Eq module in IsPreorder is not opened publicly, because it
-- contains some fields which clash with fields or other definitions
-- in IsPreorder.

-- Records packing up properties with the corresponding operations,
-- sets, etc. are also defined:
--
--   record Semigroup : Set₁ where
--     infixl 7 _∙_
--     infix  4 _≈_
--     field
--       Carrier     : Set
--       _≈_         : Rel Carrier
--       _∙_         : Op₂ Carrier
--       isSemigroup : IsSemigroup _≈_ _∙_
--
--     open IsSemigroup isSemigroup public
--
--     setoid : Setoid
--     setoid = record { isEquivalence = isEquivalence }
--
--   record Monoid : Set₁ where
--     infixl 7 _∙_
--     infix  4 _≈_
--     field
--       Carrier  : Set
--       _≈_      : Rel Carrier
--       _∙_      : Op₂ Carrier
--       ε        : Carrier
--       isMonoid : IsMonoid _≈_ _∙_ ε
--
--     open IsMonoid isMonoid public
--
--     semigroup : Semigroup
--     semigroup = record { isSemigroup = isSemigroup }
--
--     open Semigroup semigroup public using (setoid)
--
-- Note that the Monoid record does not include a Semigroup field.
-- Instead the Monoid /module/ includes a "repackaging function"
-- semigroup which converts a Monoid to a Semigroup.

-- The above setup may seem a bit complicated, but we think it makes the
-- library quite easy to work with, while also providing enough
-- flexibility.

------------------------------------------------------------------------
-- More documentation
------------------------------------------------------------------------

-- Examples of how decidability is handled in the library.

import README.Decidability

-- Some examples showing how the case expression can be used.

import README.Case

-- Some examples showing how combinators can be used to emulate
-- "functional reasoning"

import README.Function.Reasoning

-- An example showing how to use the debug tracing mechanism to inspect
-- the behaviour of compiled Agda programs.

import README.Debug.Trace

-- An exploration of the generic programs acting on n-ary functions and
-- n-ary heterogeneous products

import README.Nary

-- Explaining the inspect idiom: use case, equivalent handwritten
-- auxiliary definitions, and implementation details.

import README.Inspect

-- Explaining string formats and the behaviour of printf

import README.Text.Printf

-- Showcasing the pretty printing module

import README.Text.Pretty

-- Explaining how to display tables of strings:

import README.Text.Tabular

-- Explaining how to display a tree:

import README.Text.Tree

-- Explaining how to use the automatic solvers

import README.Tactic.MonoidSolver
import README.Tactic.RingSolver

-- Explaining how the Haskell FFI works

import README.Foreign.Haskell

------------------------------------------------------------------------
-- Core modules
------------------------------------------------------------------------

-- Some modules have names ending in ".Core". These modules are
-- internal, and have (mostly) been created to avoid mutual recursion
-- between modules. They should not be imported directly; their
-- contents are reexported by other modules.

------------------------------------------------------------------------
-- All library modules
------------------------------------------------------------------------

-- For short descriptions of every library module, see Everything;
-- to exclude unsafe modules, see EverythingSafe:

import Everything
import EverythingSafe

-- Note that the Everything* modules are generated automatically. If
-- you have downloaded the library from its Git repository and want
-- to type check README then you can (try to) construct Everything by
-- running "cabal install && GenerateEverything".

-- Note that all library sources are located under src or ffi. The
-- modules README, README.* and Everything are not really part of the
-- library, so these modules are located in the top-level directory
-- instead.


text:
-- Note: out of order true and false. Confuses the
-- values if we mess up and compile it to a fresh
-- datatype instead of Haskell Bool.
data Two : Set where tt ff : Two

{-# BUILTIN BOOL Two #-}
{-# BUILTIN FALSE ff #-}
{-# BUILTIN TRUE  tt #-}

-- Note: out of order nil and cons. Causes segfault
-- if we mess up and compile it to a fresh datatype
-- instead of Haskell lists.
data List {a} (A : Set a) : Set a where
  _∷_ : A → List A → List A
  []  : List A

{-# BUILTIN LIST List #-}

postulate
  String : Set
  Char : Set

{-# BUILTIN STRING String #-}
{-# BUILTIN CHAR   Char #-}

primitive
  primStringToList   : String → List Char
  primStringFromList : List Char → String
  primStringEquality : String → String → Two

drop1 : {A : Set} → List A → List A
drop1 (x ∷ xs) = xs
drop1 [] = []

postulate
  drop1' : List Char → List Char
{-# COMPILE GHC drop1' = drop 1 #-}

onList : (List Char → List Char) → String → String
onList f s = primStringFromList (f (primStringToList s))

postulate
  _==_ : String → String → Two
{-# COMPILE GHC _==_ = (==) #-}

show : Two → String
show tt = onList drop1  "TRUE"
show ff = onList drop1' "FALSE"

record One : Set where
{-# COMPILE GHC One = data () (()) #-}

postulate IO : Set → Set
{-# BUILTIN IO IO #-}
{-# COMPILE GHC IO = type IO #-}

{-# FOREIGN GHC import qualified Data.Text.IO #-}

postulate putStrLn : String → IO One
{-# COMPILE GHC putStrLn = Data.Text.IO.putStrLn #-}

postulate _>>_ : IO One → IO One → IO One
{-# COMPILE GHC _>>_ = (>>) #-}

main : IO One
main = do
  putStrLn (show ("foo" == "bar"))
  putStrLn (show ("foo" == "foo"))

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module ch1 where

data 𝔹 : Set where
 tt : 𝔹
 ff : 𝔹

_||_ : 𝔹 -> 𝔹 -> 𝔹
tt || _ = tt
ff || b = b

data day : Set where
  monday : day
  tuesday : day
  wednesday : day
  thursday : day
  friday : day
  saturday : day
  sunday : day

nextday : day -> day
nextday monday = tuesday
nextday tuesday = wednesday
nextday wednesday = thursday
nextday thursday = friday
nextday friday = saturday
nextday saturday = sunday
nextday sunday = monday

data suit : Set where
  hearts : suit
  spades : suit
  diamonds : suit
  clubs : suit

is-red : suit -> 𝔹
is-red hearts = tt
is-red spades = ff
is-red diamonds = tt
is-red clubs = ff


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic products of binary relations
------------------------------------------------------------------------

-- The definition of lexicographic product used here is suitable if
-- the left-hand relation is a (non-strict) partial order.

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

module Data.Product.Relation.Binary.Lex.NonStrict where

open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Sum using (inj₁; inj₂)
open import Relation.Binary
open import Relation.Binary.Consequences
import Relation.Binary.Construct.NonStrictToStrict as Conv
open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
  using (Pointwise)
import Data.Product.Relation.Binary.Lex.Strict as Strict

module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} where

------------------------------------------------------------------------
-- A lexicographic ordering over products

  ×-Lex : (_≈₁_ _≤₁_ : Rel A₁ ℓ₁) (_≤₂_ : Rel A₂ ℓ₂) → Rel (A₁ × A₂) _
  ×-Lex _≈₁_ _≤₁_ _≤₂_ = Strict.×-Lex _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_

------------------------------------------------------------------------
-- Some properties which are preserved by ×-Lex (under certain
-- assumptions).

  ×-reflexive : ∀ _≈₁_ _≤₁_ {_≈₂_} _≤₂_ →
                _≈₂_ ⇒ _≤₂_ →
                (Pointwise _≈₁_ _≈₂_) ⇒ (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-reflexive _≈₁_ _≤₁_ _≤₂_ refl₂ =
    Strict.×-reflexive _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_ refl₂

  ×-transitive : ∀ {_≈₁_ _≤₁_} → IsPartialOrder _≈₁_ _≤₁_ →
                 ∀ {_≤₂_} → Transitive _≤₂_ →
                 Transitive (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-transitive {_≈₁_} {_≤₁_} po₁ {_≤₂_} trans₂ =
    Strict.×-transitive
      {_<₁_ = Conv._<_ _≈₁_ _≤₁_}
      isEquivalence (Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
      (Conv.<-trans _ _ po₁)
      {_≤₂_} trans₂
    where open IsPartialOrder po₁

  ×-antisymmetric :
    ∀ {_≈₁_ _≤₁_} → IsPartialOrder _≈₁_ _≤₁_ →
    ∀ {_≈₂_ _≤₂_} → Antisymmetric _≈₂_ _≤₂_ →
    Antisymmetric (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-antisymmetric {_≈₁_} {_≤₁_}
                  po₁ {_≤₂_ = _≤₂_} antisym₂ =
    Strict.×-antisymmetric {_<₁_ = Conv._<_ _≈₁_ _≤₁_}
                           ≈-sym₁ irrefl₁ asym₁
                           {_≤₂_ = _≤₂_} antisym₂
    where
    open IsPartialOrder po₁
    open Eq renaming (refl to ≈-refl₁; sym to ≈-sym₁)

    irrefl₁ : Irreflexive _≈₁_ (Conv._<_ _≈₁_ _≤₁_)
    irrefl₁ = Conv.<-irrefl _≈₁_ _≤₁_

    asym₁ : Asymmetric (Conv._<_ _≈₁_ _≤₁_)
    asym₁ = trans∧irr⟶asym {_≈_ = _≈₁_}
                           ≈-refl₁ (Conv.<-trans _ _ po₁) irrefl₁

  ×-respects₂ :
    ∀ {_≈₁_ _≤₁_} → IsEquivalence _≈₁_ → _≤₁_ Respects₂ _≈₁_ →
    ∀ {_≈₂_ _≤₂_ : Rel A₂ ℓ₂} → _≤₂_ Respects₂ _≈₂_ →
    (×-Lex _≈₁_ _≤₁_ _≤₂_) Respects₂ (Pointwise _≈₁_ _≈₂_)
  ×-respects₂ eq₁ resp₁ resp₂ =
    Strict.×-respects₂ eq₁ (Conv.<-resp-≈ _ _ eq₁ resp₁) resp₂

  ×-decidable : ∀ {_≈₁_ _≤₁_} → Decidable _≈₁_ → Decidable _≤₁_ →
                ∀ {_≤₂_} → Decidable _≤₂_ →
                Decidable (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-decidable dec-≈₁ dec-≤₁ dec-≤₂ =
    Strict.×-decidable dec-≈₁ (Conv.<-decidable _ _ dec-≈₁ dec-≤₁)
                       dec-≤₂

  ×-total : ∀ {_≈₁_ _≤₁_} → Symmetric _≈₁_ → Decidable _≈₁_ →
                            Antisymmetric _≈₁_ _≤₁_ → Total _≤₁_ →
            ∀ {_≤₂_} → Total _≤₂_ →
            Total (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-total {_≈₁_} {_≤₁_} sym₁ dec₁ antisym₁ total₁ {_≤₂_} total₂ =
    total
    where
    tri₁ : Trichotomous _≈₁_ (Conv._<_ _≈₁_ _≤₁_)
    tri₁ = Conv.<-trichotomous _ _ sym₁ dec₁ antisym₁ total₁

    total : Total (×-Lex _≈₁_ _≤₁_ _≤₂_)
    total x y with tri₁ (proj₁ x) (proj₁ y)
    ... | tri< x₁<y₁ x₁≉y₁ x₁≯y₁ = inj₁ (inj₁ x₁<y₁)
    ... | tri> x₁≮y₁ x₁≉y₁ x₁>y₁ = inj₂ (inj₁ x₁>y₁)
    ... | tri≈ x₁≮y₁ x₁≈y₁ x₁≯y₁ with total₂ (proj₂ x) (proj₂ y)
    ...   | inj₁ x₂≤y₂ = inj₁ (inj₂ (x₁≈y₁ , x₂≤y₂))
    ...   | inj₂ x₂≥y₂ = inj₂ (inj₂ (sym₁ x₁≈y₁ , x₂≥y₂))

  -- Some collections of properties which are preserved by ×-Lex
  -- (under certain assumptions).

  ×-isPartialOrder :
    ∀ {_≈₁_ _≤₁_} → IsPartialOrder _≈₁_ _≤₁_ →
    ∀ {_≈₂_ _≤₂_} → IsPartialOrder _≈₂_ _≤₂_ →
    IsPartialOrder (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-isPartialOrder {_≈₁_} {_≤₁_} po₁
                     {_≤₂_ = _≤₂_} po₂ = record
    { isPreorder = record
        { isEquivalence = Pointwise.×-isEquivalence
                            (isEquivalence po₁)
                            (isEquivalence po₂)
        ; reflexive     = ×-reflexive _≈₁_ _≤₁_ _≤₂_ (reflexive po₂)
        ; trans         = ×-transitive po₁ {_≤₂_ = _≤₂_} (trans po₂)
        }
    ; antisym = ×-antisymmetric {_≤₁_ = _≤₁_} po₁
                                {_≤₂_ = _≤₂_} (antisym po₂)
    }
    where open IsPartialOrder

  ×-isTotalOrder :
    ∀ {_≈₁_ _≤₁_} → Decidable _≈₁_ → IsTotalOrder _≈₁_ _≤₁_ →
    ∀ {_≈₂_ _≤₂_} → IsTotalOrder _≈₂_ _≤₂_ →
    IsTotalOrder (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-isTotalOrder {_≤₁_ = _≤₁_} ≈₁-dec to₁ {_≤₂_ = _≤₂_} to₂ = record
    { isPartialOrder = ×-isPartialOrder
                         (isPartialOrder to₁) (isPartialOrder to₂)
    ; total          = ×-total {_≤₁_ = _≤₁_} (Eq.sym to₁) ≈₁-dec
                                             (antisym to₁) (total to₁)
                               {_≤₂_ = _≤₂_} (total to₂)
    }
    where open IsTotalOrder

  ×-isDecTotalOrder :
    ∀ {_≈₁_ _≤₁_} → IsDecTotalOrder _≈₁_ _≤₁_ →
    ∀ {_≈₂_ _≤₂_} → IsDecTotalOrder _≈₂_ _≤₂_ →
    IsDecTotalOrder (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
  ×-isDecTotalOrder {_≤₁_ = _≤₁_} to₁ {_≤₂_ = _≤₂_} to₂ = record
    { isTotalOrder = ×-isTotalOrder (_≟_ to₁)
                                    (isTotalOrder to₁)
                                    (isTotalOrder to₂)
    ; _≟_          = Pointwise.×-decidable (_≟_ to₁) (_≟_ to₂)
    ; _≤?_         = ×-decidable (_≟_ to₁) (_≤?_ to₁) (_≤?_ to₂)
    }
    where open IsDecTotalOrder

------------------------------------------------------------------------
-- "Packages" can also be combined.

module _ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} where

  ×-poset : Poset ℓ₁ ℓ₂ _ → Poset ℓ₃ ℓ₄ _ → Poset _ _ _
  ×-poset p₁ p₂ = record
    { isPartialOrder = ×-isPartialOrder
                         (isPartialOrder p₁) (isPartialOrder p₂)
    } where open Poset

  ×-totalOrder : DecTotalOrder ℓ₁ ℓ₂ _ → TotalOrder ℓ₃ ℓ₄ _ →
                 TotalOrder _ _ _
  ×-totalOrder t₁ t₂ = record
    { isTotalOrder = ×-isTotalOrder T₁._≟_ T₁.isTotalOrder T₂.isTotalOrder
    }
    where
    module T₁ = DecTotalOrder t₁
    module T₂ =    TotalOrder t₂

  ×-decTotalOrder : DecTotalOrder ℓ₁ ℓ₂ _ → DecTotalOrder ℓ₃ ℓ₄ _ →
                    DecTotalOrder _ _ _
  ×-decTotalOrder t₁ t₂ = record
    { isDecTotalOrder = ×-isDecTotalOrder
        (isDecTotalOrder t₁) (isDecTotalOrder t₂)
    } where open DecTotalOrder

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.15

_×-isPartialOrder_  = ×-isPartialOrder
{-# WARNING_ON_USAGE _×-isPartialOrder_
"Warning: _×-isPartialOrder_ was deprecated in v0.15.
Please use ×-isPartialOrder instead."
#-}
_×-isDecTotalOrder_ = ×-isDecTotalOrder
{-# WARNING_ON_USAGE _×-isDecTotalOrder_
"Warning: _×-isDecTotalOrder_ was deprecated in v0.15.
Please use ×-isDecTotalOrder instead."
#-}
_×-poset_           = ×-poset
{-# WARNING_ON_USAGE _×-poset_
"Warning: _×-poset_ was deprecated in v0.15.
Please use ×-poset instead."
#-}
_×-totalOrder_      = ×-totalOrder
{-# WARNING_ON_USAGE _×-totalOrder_
"Warning: _×-totalOrder_ was deprecated in v0.15.
Please use ×-totalOrder instead."
#-}
_×-decTotalOrder_   = ×-decTotalOrder
{-# WARNING_ON_USAGE _×-decTotalOrder_
"Warning: _×-decTotalOrder_ was deprecated in v0.15.
Please use ×-decTotalOrder instead."
#-}
×-≈-respects₂       = ×-respects₂
{-# WARNING_ON_USAGE ×-≈-respects₂
"Warning: ×-≈-respects₂ was deprecated in v0.15.
Please use ×-respects₂ instead."
#-}


text:
-- Andreas, 2013-03-22
-- {-# OPTIONS -v tc.lhs:40 #-}
module Issue279-3 where

module M (X : Set) where

  data R : Set where
    r : X → R

postulate
  P Q : Set

open M P

shouldn't-check : M.R Q → Q
shouldn't-check (r q) = q

-- Agda uses the type of the original constructor
--
--   M.r {X : Set} : X → R X
--
-- instead of the type of the copied constructor
--
--   r : P → R
--
-- If one changes the domain to _, it will be resolved to
-- R, which is M.R P, and q gets assigned type P, leading
-- to expected failure.

-- Fixed this issue by comparing the parameter reconstructed
-- from the domain, Q, to the parameter of the unambiguous
-- constructor r, which is P.