text:
open import Data.Product using ( _×_ ; _,_ )
open import Data.Sum using ( inj₁ ; inj₂ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )
open import Relation.Unary using ( _∈_ ; _⊆_ )
open import Web.Semantic.DL.ABox using
  ( ABox ; Assertions ; ⟨ABox⟩ ; ε ; _,_ ; _∼_ ; _∈₁_ ; _∈₂_ )
open import Web.Semantic.DL.ABox.Interp using ( Interp ; _,_ ; ⌊_⌋ ; ind ; _*_ )
open import Web.Semantic.DL.ABox.Interp.Morphism using
  ( _≲_ ; _,_ ; ≲⌊_⌋ ; ≲-resp-ind ; ≡³-impl-≲ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox.Interp using
  ( Δ ; _⊨_≈_ ; ≈-refl ; ≈-sym ; ≈-trans ; con ; rol ; con-≈ ; rol-≈ )
open import Web.Semantic.DL.TBox.Interp.Morphism using
  ( ≲-image ; ≲-resp-≈ ; ≲-resp-con ; ≲-resp-rol ; ≲-refl )
open import Web.Semantic.Util using
  ( True ; tt ; id ; _∘_ ; _⊕_⊕_ ; inode ; bnode ; enode ; →-dist-⊕ )

module Web.Semantic.DL.ABox.Model {Σ : Signature} where

infix 2 _⊨a_ _⊨b_
infixr 5 _,_

_⟦_⟧₀ : ∀ {X} (I : Interp Σ X) → X → (Δ ⌊ I ⌋)
I ⟦ x ⟧₀ = ind I x

_⊨a_ : ∀ {X} → Interp Σ X → ABox Σ X → Set
I ⊨a ε            = True
I ⊨a (A , B)      = (I ⊨a A) × (I ⊨a B)
I ⊨a x ∼ y        = ⌊ I ⌋ ⊨ ind I x ≈ ind I y
I ⊨a x ∈₁ c       = ind I x ∈ con ⌊ I ⌋ c
I ⊨a (x , y) ∈₂ r = (ind I x , ind I y) ∈ rol ⌊ I ⌋ r

Assertions✓ : ∀ {X} (I : Interp Σ X) A {a} →
  (a ∈ Assertions A) → (I ⊨a A) → (I ⊨a a)
Assertions✓ I ε         ()         I⊨A
Assertions✓ I (A , B)   (inj₁ a∈A) (I⊨A , I⊨B) = Assertions✓ I A a∈A I⊨A
Assertions✓ I (A , B)   (inj₂ a∈B) (I⊨A , I⊨B) = Assertions✓ I B a∈B I⊨B
Assertions✓ I (i ∼ j)   refl       I⊨A         = I⊨A
Assertions✓ I (i ∈₁ c)  refl       I⊨A         = I⊨A
Assertions✓ I (ij ∈₂ r) refl       I⊨A         = I⊨A

⊨a-resp-⊇ : ∀ {X} (I : Interp Σ X) A B →
  (Assertions A ⊆ Assertions B) → (I ⊨a B) → (I ⊨a A)
⊨a-resp-⊇ I ε B A⊆B I⊨B = tt
⊨a-resp-⊇ I (A₁ , A₂) B A⊆B I⊨B =
  ( ⊨a-resp-⊇ I A₁ B (A⊆B ∘ inj₁) I⊨B
  , ⊨a-resp-⊇ I A₂ B (A⊆B ∘ inj₂) I⊨B )
⊨a-resp-⊇ I (x ∼ y) B A⊆B I⊨B = Assertions✓ I B (A⊆B refl) I⊨B
⊨a-resp-⊇ I (x ∈₁ c) B A⊆B I⊨B = Assertions✓ I B (A⊆B refl) I⊨B
⊨a-resp-⊇ I (xy ∈₂ r) B A⊆B I⊨B = Assertions✓ I B (A⊆B refl) I⊨B

⊨a-resp-≲ : ∀ {X} {I J : Interp Σ X} → (I ≲ J) → ∀ A → (I ⊨a A) → (J ⊨a A)
⊨a-resp-≲ {X} {I} {J} I≲J ε I⊨A =
  tt
⊨a-resp-≲ {X} {I} {J} I≲J (A , B) (I⊨A , I⊨B) =
  (⊨a-resp-≲ I≲J A I⊨A , ⊨a-resp-≲ I≲J B I⊨B)
⊨a-resp-≲ {X} {I} {J} I≲J (x ∼ y)   I⊨x∼y =
  ≈-trans ⌊ J ⌋ (≈-sym ⌊ J ⌋ (≲-resp-ind I≲J x))
    (≈-trans ⌊ J ⌋ (≲-resp-≈ ≲⌊ I≲J ⌋ I⊨x∼y)
      (≲-resp-ind I≲J y))
⊨a-resp-≲ {X} {I} {J} I≲J (x ∈₁ c)  I⊨x∈c =
  con-≈ ⌊ J ⌋ c (≲-resp-con ≲⌊ I≲J ⌋ I⊨x∈c) (≲-resp-ind I≲J x)
⊨a-resp-≲ {X} {I} {J} I≲J ((x , y) ∈₂ r) I⊨xy∈r =
  rol-≈ ⌊ J ⌋ r (≈-sym ⌊ J ⌋ (≲-resp-ind I≲J x))
    (≲-resp-rol ≲⌊ I≲J ⌋ I⊨xy∈r) (≲-resp-ind I≲J y)

⊨a-resp-≡ : ∀ {X : Set} (I : Interp Σ X) j →
  (ind I ≡ j) → ∀ A → (I ⊨a A) → (⌊ I ⌋ , j ⊨a A)
⊨a-resp-≡ (I , i) .i refl A I⊨A = I⊨A

⊨a-resp-≡³ : ∀ {V X Y : Set} (I : Interp Σ (X ⊕ V ⊕ Y)) j →
  (→-dist-⊕ (ind I) ≡ →-dist-⊕ j) → ∀ A → (I ⊨a A) → (⌊ I ⌋ , j ⊨a A)
⊨a-resp-≡³ I j i≡j = ⊨a-resp-≲ (≡³-impl-≲ I j i≡j)

⟨ABox⟩-Assertions : ∀ {X Y a} (f : X → Y) (A : ABox Σ X) →
  (a ∈ Assertions A) → (⟨ABox⟩ f a ∈ Assertions (⟨ABox⟩ f A))
⟨ABox⟩-Assertions f ε ()
⟨ABox⟩-Assertions f (A , B) (inj₁ a∈A) = inj₁ (⟨ABox⟩-Assertions f A a∈A)
⟨ABox⟩-Assertions f (A , B) (inj₂ a∈B) = inj₂ (⟨ABox⟩-Assertions f B a∈B)
⟨ABox⟩-Assertions f (x ∼ y) refl = refl
⟨ABox⟩-Assertions f (x ∈₁ c) refl = refl
⟨ABox⟩-Assertions f ((x , y) ∈₂ r) refl = refl

⟨ABox⟩-resp-⊨ : ∀ {X Y} {I : Interp Σ X} {j : Y → Δ ⌊ I ⌋}
  (f : X → Y) → (∀ x → ⌊ I ⌋ ⊨ ind I x ≈ j (f x)) →
    ∀ A → (I ⊨a A) → (⌊ I ⌋ , j ⊨a ⟨ABox⟩ f A)
⟨ABox⟩-resp-⊨ {X} {Y} {I} f i≈j∘f ε I⊨ε =
  tt
⟨ABox⟩-resp-⊨ {X} {Y} {I} f i≈j∘f (A , B) (I⊨A , I⊨B) =
  (⟨ABox⟩-resp-⊨ f i≈j∘f A I⊨A , ⟨ABox⟩-resp-⊨ f i≈j∘f B I⊨B)
⟨ABox⟩-resp-⊨ {X} {Y} {I} f i≈j∘f (x ∼ y) x≈y =
  ≈-trans ⌊ I ⌋ (≈-sym ⌊ I ⌋ (i≈j∘f x)) (≈-trans ⌊ I ⌋ x≈y (i≈j∘f y))
⟨ABox⟩-resp-⊨ {X} {Y} {I} f i≈j∘f (x ∈₁ c) x∈⟦c⟧ =
  con-≈ ⌊ I ⌋ c x∈⟦c⟧ (i≈j∘f x)
⟨ABox⟩-resp-⊨ {X} {Y} {I} f i≈j∘f ((x , y) ∈₂ r) xy∈⟦r⟧ =
  rol-≈ ⌊ I ⌋ r (≈-sym ⌊ I ⌋ (i≈j∘f x)) xy∈⟦r⟧ (i≈j∘f y)

*-resp-⟨ABox⟩ : ∀ {X Y} (f : Y → X) I A →
  (I ⊨a ⟨ABox⟩ f A) → (f * I ⊨a A)
*-resp-⟨ABox⟩ f (I , i) ε I⊨ε =
  tt
*-resp-⟨ABox⟩ f (I , i) (A , B) (I⊨A , I⊨B) =
  (*-resp-⟨ABox⟩ f (I , i) A I⊨A , *-resp-⟨ABox⟩ f (I , i) B I⊨B )
*-resp-⟨ABox⟩ f (I , i) (x ∼ y) x≈y =
  x≈y
*-resp-⟨ABox⟩ f (I , i) (x ∈₁ c) x∈⟦c⟧ =
  x∈⟦c⟧
*-resp-⟨ABox⟩ f (I , i) ((x , y) ∈₂ r) xy∈⟦c⟧ =
  xy∈⟦c⟧

-- bnodes I f is the same as I, except that f is used as the interpretation
-- for bnodes.

on-bnode : ∀ {V W X Y Z : Set} → (W → Z) → ((X ⊕ V ⊕ Y) → Z) →
  ((X ⊕ W ⊕ Y) → Z)
on-bnode f g (inode x) = g (inode x)
on-bnode f g (bnode w) = f w
on-bnode f g (enode y) = g (enode y)

bnodes : ∀ {V W X Y} → (I : Interp Σ (X ⊕ V ⊕ Y)) → (W → Δ ⌊ I ⌋) →
  Interp Σ (X ⊕ W ⊕ Y)
bnodes I f = (⌊ I ⌋ , on-bnode f (ind I))

bnodes-resp-≲ : ∀ {V W X Y} (I J : Interp Σ (X ⊕ V ⊕ Y)) →
  (I≲J : I ≲ J) → (f : W → Δ ⌊ I ⌋) →
    (bnodes I f ≲ bnodes J (≲-image ≲⌊ I≲J ⌋ ∘ f))
bnodes-resp-≲ (I , i) (J , j) (I≲J , i≲j) f = (I≲J , lemma) where

  lemma : ∀ x →
    J ⊨ ≲-image I≲J (on-bnode f i x) ≈ on-bnode (≲-image I≲J ∘ f) j x
  lemma (inode x) = i≲j (inode x)
  lemma (bnode v) = ≈-refl J
  lemma (enode y) = i≲j (enode y)

-- I ⊨b A whenever there exists an f such that bnodes I f ⊨a A

data _⊨b_ {V W X Y} (I : Interp Σ (X ⊕ V ⊕ Y))
  (A : ABox Σ (X ⊕ W ⊕ Y)) : Set where
    _,_ : ∀ f → (bnodes I f ⊨a A) → (I ⊨b A)

inb : ∀ {V W X Y} {I : Interp Σ (X ⊕ V ⊕ Y)} {A : ABox Σ (X ⊕ W ⊕ Y)} →
  (I ⊨b A) → W → Δ ⌊ I ⌋
inb (f , I⊨A) = f

⊨b-impl-⊨a : ∀ {V W X Y} {I : Interp Σ (X ⊕ V ⊕ Y)} {A : ABox Σ (X ⊕ W ⊕ Y)} →
  (I⊨A : I ⊨b A) → (bnodes I (inb I⊨A) ⊨a A)
⊨b-impl-⊨a (f , I⊨A) = I⊨A

⊨a-impl-⊨b : ∀ {V X Y} (I : Interp Σ (X ⊕ V ⊕ Y)) A → (I ⊨a A) → (I ⊨b A)
⊨a-impl-⊨b I A I⊨A =
  (ind I ∘ bnode , ⊨a-resp-≲ (≲-refl ⌊ I ⌋ , lemma) A I⊨A) where

  lemma : ∀ x → ⌊ I ⌋ ⊨ ind I x ≈ on-bnode (ind I ∘ bnode) (ind I) x
  lemma (inode x) = ≈-refl ⌊ I ⌋
  lemma (bnode v) = ≈-refl ⌊ I ⌋
  lemma (enode y) = ≈-refl ⌊ I ⌋

⊨b-resp-≲ : ∀ {V W X Y} {I J : Interp Σ (X ⊕ V ⊕ Y)} → (I ≲ J)
  → ∀ (A : ABox Σ (X ⊕ W ⊕ Y)) → (I ⊨b A) → (J ⊨b A)
⊨b-resp-≲ I≲J A (f , I⊨A) =
  ((≲-image ≲⌊ I≲J ⌋ ∘ f) , ⊨a-resp-≲ (bnodes-resp-≲ _ _ I≲J f) A I⊨A)

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


text:
{-# OPTIONS --allow-unsolved-metas --no-termination-check
  #-}
module Bag where

import Prelude
import Equiv
import Datoid
import Eq
import Nat
import List
import Pos

open Prelude
open Equiv
open Datoid
open Eq
open Nat
open List

abstract

----------------------------------------------------------------------
-- Bag type

  private
    -- If this were Coq then the invariant should be a Prop. Similar
    -- remarks apply to some definitions below. Since I have to write
    -- the supporting library myself I can't be bothered to
    -- distinguish Set and Prop right now though.

    data BagType (a : Datoid) : Set where
      bt :  (pairs : List (Pair Pos.Pos (El a)))
         → NoDuplicates a (map snd pairs)
         → BagType a

    list : {a : Datoid} → BagType a → List (Pair Pos.Pos (El a))
    list (bt l _) = l

    contents : {a : Datoid} → BagType a → List (El a)
    contents b = map snd (list b)

    invariant :  {a : Datoid} → (b : BagType a)
              → NoDuplicates a (contents b)
    invariant (bt _ i) = i

  private
    elemDatoid : Datoid → Datoid
    elemDatoid a = pairDatoid Pos.posDatoid a

    BagEq : (a : Datoid) → BagType a → BagType a → Set
    BagEq a b1 b2 = rel' (Permutation (elemDatoid a)) (list b1) (list b2)

    eqRefl : {a : Datoid} → (x : BagType a) → BagEq a x x
    eqRefl {a} x = refl (Permutation (elemDatoid a)) {list x}

    eqSym :  {a : Datoid} → (x y : BagType a)
          → BagEq a x y → BagEq a y x
    eqSym {a} x y = sym (Permutation (elemDatoid a)) {list x} {list y}

    eqTrans :  {a : Datoid} → (x y z : BagType a)
          → BagEq a x y → BagEq a y z → BagEq a x z
    eqTrans {a} x y z = trans (Permutation (elemDatoid a))
                              {list x} {list y} {list z}

    eqDec : {a : Datoid} → (x y : BagType a)
          → Either (BagEq a x y) _
    eqDec {a} x y = decRel (Permutation (elemDatoid a)) (list x) (list y)

    BagEquiv : (a : Datoid) → DecidableEquiv (BagType a)
    BagEquiv a = decEquiv (equiv (BagEq a) eqRefl eqSym eqTrans) (dec eqDec)

  Bag : Datoid → Datoid
  Bag a = datoid (BagType a) (BagEquiv a)

----------------------------------------------------------------------
-- Bag primitives

  empty : {a : Datoid} → El (Bag a)
  empty = bt nil unit

  private
    data LookupResult (a : Datoid) (x : El a) (b : El (Bag a)) : Set where
      lr :  Nat
         → (b' : El (Bag a))
         → Not (member a x (contents b'))
         → ({y : El a} → Not (member a y (contents b))
                        → Not (member a y (contents b')))
         → LookupResult a x b

    lookup1 :  {a : Datoid}
            → (n : Pos.Pos)
            → (y : El a)
            → (b' : El (Bag a))
            → (nyb' : Not (member a y (contents b')))
            → (x : El a)
            → Either (datoidRel a x y) _
            → LookupResult a x b'
            → LookupResult a x (bt (pair n y :: list b')
                                    (pair nyb' (invariant b')))
    lookup1 n y b' nyb' x (left xy) _ =
      lr (Pos.toNat n) b'
         (contrapositive (memberPreservesEq xy (contents b')) nyb')
         (\{y'} ny'b → snd (notDistribIn ny'b))
    lookup1 {a} n y b' nyb' x (right nxy)
            (lr n' (bt b'' ndb'') nxb'' nmPres) =
      lr n' (bt (pair n y :: b'') (pair (nmPres nyb') ndb''))
         (notDistribOut {datoidRel a x y} nxy nxb'')
         (\{y'} ny'b → notDistribOut (fst (notDistribIn ny'b))
                                      (nmPres (snd (notDistribIn ny'b))))

    lookup2
      :  {a : Datoid}
      → (x : El a)
      → (b : El (Bag a))
      → LookupResult a x b
    lookup2 x (bt nil nd) = lr zero (bt nil nd) (not id) (\{_} _ → not id)
    lookup2 {a} x (bt (pair n y :: b) (pair nyb ndb)) =
      lookup1 n y (bt b ndb) nyb x
              (decRel (datoidEq a) x y)
              (lookup2 x (bt b ndb))

    lookup3 :  {a : Datoid} → {x : El a} → {b : El (Bag a)}
            → LookupResult a x b → Pair Nat (El (Bag a))
    lookup3 (lr n b _ _) = pair n b

  lookup : {a : Datoid} → El a → El (Bag a) → Pair Nat (El (Bag a))
  lookup x b = lookup3 (lookup2 x b)

  private
    insert' :  {a : Datoid} → (x : El a) → {b : El (Bag a)}
            → LookupResult a x b → El (Bag a)
    insert' x (lr n (bt b ndb) nxb _) =
      bt (pair (Pos.suc' n) x :: b) (pair nxb ndb)

  insert : {a : Datoid} → El a → El (Bag a) → El (Bag a)
  insert x b = insert' x (lookup2 x b)

  private

    postulate
      insertLemma1
        :  {a : Datoid}
        → (x : El a)
        → (b : El (Bag a))
        → (nxb : Not (member a x (contents b)))
        → datoidRel (Bag a)
                     (insert x b)
                     (bt (pair Pos.one x :: list b) (pair nxb (invariant b)))

      insertLemma2
        :  {a : Datoid}
        → (n : Pos.Pos)
        → (x : El a)
        → (b : El (Bag a))
        → (nxb : Not (member a x (contents b)))
        → datoidRel (Bag a)
                     (insert x (bt (pair n x :: list b)
                                   (pair nxb (invariant b))))
                     (bt (pair (Pos.suc n) x :: list b)
                         (pair nxb (invariant b)))

----------------------------------------------------------------------
-- Bag traversals

data Traverse (a : Datoid) : Set where
  Empty  : Traverse a
  Insert : (x : El a) → (b : El (Bag a)) → Traverse a

run : {a : Datoid} → Traverse a → El (Bag a)
run Empty        = empty
run (Insert x b) = insert x b

abstract

  traverse : {a : Datoid} → El (Bag a) → Traverse a
  traverse     (bt nil _)                          = Empty
  traverse {a} (bt (pair n x :: b) (pair nxb ndb)) = traverse' (Pos.pred n)
    where
    private
      traverse' :  Maybe Pos.Pos → Traverse a
      traverse' Nothing  = Insert x (bt b ndb)
      traverse' (Just n) = Insert x (bt (pair n x :: b) (pair nxb ndb))

  traverseTraverses
    :  {a : Datoid} → (b : El (Bag a))
    → datoidRel (Bag a) (run (traverse b)) b
  traverseTraverses {a} (bt nil unit) = dRefl (Bag a) {empty}
  traverseTraverses {a} (bt (pair n x :: b) (pair nxb ndb)) =
    tT (Pos.pred n) (Pos.predOK n)
    where
    private
      postulate
        subst' :  {a : Datoid} → (P : El a → Set) → (x y : El a)
               → datoidRel a x y → P x → P y

      tT :  (predN : Maybe Pos.Pos)
         → Pos.Pred n predN
         → datoidRel (Bag a)
                      (run (traverse (bt (pair n x :: b) (pair nxb ndb))))
                      (bt (pair n x :: b) (pair nxb ndb))
      tT Nothing  (Pos.ok eq) = {!!}
        -- subst' (\p → datoidRel (Bag a)
        --                 (run (traverse (bt (pair p x :: b) (pair nxb ndb))))
        --                 (bt (pair p x :: b) (pair nxb ndb)))
        --        Pos.one n eq (insertLemma1 x (bt b ndb) nxb)

        -- eq : one == n
        -- data Pred (p : Pos) (mP : Maybe Pos) : Set where
        --   ok : datoidRel posDatoid (sucPred mP) p → Pred p mP
        -- insert x (bt b ndb) == bt (pair n x :: b) (pair nxb ndb)
      tT (Just n) (Pos.ok eq) = {!!} -- insertLemma2 n x (bt b ndb) nxb
        -- insert x (bt (pair n x :: b) (pair nxb btb) ==
        -- bt (pair (suc n) x :: b) (pair nxb btb)

  bagElim
    :  {a : Datoid}
    → (P : El (Bag a) → Set)
    → Respects (Bag a) P
    → P empty
    → ((x : El a) → (b : El (Bag a)) → P b → P (insert x b))
    → (b : El (Bag a))
    → P b
  bagElim {a} P Prespects e i b =
    bagElim' b (traverse b) (traverseTraverses b)
    where
    private
      bagElim'
        :  (b : El (Bag a))
        → (t : Traverse a)
        → datoidRel (Bag a) (run t) b
        → P b
      bagElim' b Empty         eq = subst Prespects empty b eq e
      bagElim' b (Insert x b') eq =
        subst Prespects (insert x b') b eq
              (i x b' (bagElim' b' (traverse b') (traverseTraverses b')))

----------------------------------------------------------------------
-- Respect and equality preservation lemmas

  postulate
    insertPreservesRespect
      :  {a : Datoid}
      → (P : El (Bag a) → Set)
      → (x : El a)
      → Respects (Bag a) P
      → Respects (Bag a) (\b → P (insert x b))

    lookupPreservesRespect
      :  {a : Datoid}
      → (P : El (Bag a) → Set)
      → (x : El a)
      → Respects (Bag a) P
      → Respects (Bag a) (\b → P (snd $ lookup x b))

    -- This doesn't type check without John Major equality or some
    -- ugly substitutions...
    -- bagElimPreservesEquality
    --   :  {a : Datoid}
    --   → (P : El (Bag a) → Set)
    --   → (r : Respects (Bag a) P)
    --   → (e : P empty)
    --   → (i : (x : El a) → (b : El (Bag a)) → P b → P (insert x b))
    --   → (   (x1 x2 : El a) → (b1 b2 : El (Bag a))
    --       → (p1 : P b1) → (p2 : P b2)
    --       → (eqX : datoidRel a x1 x2) → (eqB : datoidRel (Bag a) b1 b2)
    --       → i x1 b1 p1 =^= i x2 b2 p2
    --      )
    --   → (b1 b2 : El (Bag a))
    --   → datoidRel (Bag a) b1 b2
    --   → bagElim P r e i b1 =^= bagElim P r e i b2

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

-- | Operations that ensure a cycle traverses a particular element
-- at most once.
module Dodo.Binary.Cycle where

-- Stdlib import
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; _≢_; refl)
open import Level using (Level; _⊔_)
open import Function using (_∘_)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (yes; no)
open import Relation.Binary using (Rel)
open import Relation.Binary.Construct.Closure.Transitive using (TransClosure; [_]; _∷_; _∷ʳ_; _++_)
-- Local imports
open import Dodo.Unary.Dec
open import Dodo.Binary.Transitive

-- # Definitions

-- | The given relation, with proofs that neither element equals `z`.
ExcludeRel : {a ℓ : Level} {A : Set a} → (R : Rel A ℓ) → (z : A) → Rel A (a ⊔ ℓ)
ExcludeRel R z x y = R x y × x ≢ z × y ≢ z

-- | A cycle of R which passes through `z` /exactly once/.
data PassCycle {a ℓ : Level} {A : Set a} (R : Rel A ℓ) (z : A) : Set (a ⊔ ℓ) where
  cycle₁ : R z z → PassCycle R z
  cycle₂ : {x : A} → x ≢ z → R z x → R x z → PassCycle R z
  cycleₙ : {x y : A} → R z x → TransClosure (ExcludeRel R z) x y → R y z → PassCycle R z

-- # Functions

-- | A cycle of a relation either /does not/ pass through an element `y`, or it
-- can be made to pass through `y` /exactly once/.
--
-- Note that if the original cycle passes `y` /more than once/, then only one
-- cycle of the multi-cycle through `y` may be taken.
divert-cycle : {a ℓ : Level} {A : Set a}
  → {R : Rel A ℓ}
  → {x : A}
  → TransClosure R x x
  → {y : A}
  → DecPred (_≡ y)
  → PassCycle R y ⊎ TransClosure (ExcludeRel R y) x x
divert-cycle {x = x} [ Rxx ] eq-xm with eq-xm x
... | yes refl = inj₁ (cycle₁ Rxx)
... | no  x≢y  = inj₂ [ ( Rxx , x≢y , x≢y ) ]
divert-cycle {A = A} {R = R} {x} ( Rxw ∷ R⁺wx ) {y} eq-dec = lemma Rxw R⁺wx
  where
  -- Chain that starts with `y`.
  --
  -- `Ryx` and `R⁺xz` are acculumators.
  lemma-incl : {x z : A} → R y x → TransClosure (ExcludeRel R y) x z → TransClosure R z y → PassCycle R y
  lemma-incl Ryx R⁺xz [ Rzy ] = cycleₙ Ryx R⁺xz Rzy
  lemma-incl Ryx R⁺xz (_∷_ {_} {w} Rzw R⁺wy) with eq-dec w
  lemma-incl Ryx R⁺xz (_∷_ {_} {w} Rzw R⁺wy) | yes refl = cycleₙ Ryx R⁺xz Rzw
  lemma-incl Ryx R⁺xz (_∷_ {_} {w} Rzw R⁺wy) | no  w≢y  =
    let z≢y = ⁺-lift-predʳ (proj₂ ∘ proj₂) R⁺xz
    in lemma-incl Ryx (R⁺xz ∷ʳ (Rzw , z≢y , w≢y)) R⁺wy

  -- First step of a chain that starts with `y`.
  lemma-incl₀ : {x : A} → R y x → TransClosure R x y → PassCycle R y
  lemma-incl₀ {x} Ryx R⁺xy with eq-dec x
  lemma-incl₀ {x} Ryx R⁺xy                   | yes refl = cycle₁ Ryx
  lemma-incl₀ {x} Ryx [ Rxy ]                | no  x≢y  = cycle₂ x≢y Ryx Rxy
  lemma-incl₀ {x} Ryx (_∷_ {_} {z} Rxz R⁺zy) | no x≢y with eq-dec z
  lemma-incl₀ {x} Ryx (_∷_ {x} {z} Rxz R⁺zy) | no x≢y | yes refl = cycle₂ x≢y Ryx Rxz
  lemma-incl₀ {x} Ryx (_∷_ {x} {z} Rxz R⁺zy) | no x≢y | no  z≢y  = lemma-incl Ryx [ Rxz , x≢y , z≢y ] R⁺zy

  -- Chain that does /not/ (yet) pass through `y`.
  lemma-excl : {z : A} → TransClosure (ExcludeRel R y) x z → TransClosure R z x → PassCycle R y ⊎ TransClosure (ExcludeRel R y) x x
  lemma-excl R⁺xz [ Rzx ] =
    let z≢y = ⁺-lift-predʳ (proj₂ ∘ proj₂) R⁺xz
        x≢y = ⁺-lift-predˡ (proj₁ ∘ proj₂) R⁺xz
    in inj₂ (R⁺xz ∷ʳ (Rzx , z≢y , x≢y))
  lemma-excl R⁺xz (_∷_ {_} {w} Rzw R⁺wx) with eq-dec w
  lemma-excl R⁺xz (_∷_ {_} {_} Rzw [ Rwx ])      | yes refl = inj₁ (cycleₙ Rwx R⁺xz Rzw)
  lemma-excl R⁺xz (_∷_ {_} {_} Rzw (Rwq ∷ R⁺qx)) | yes refl = inj₁ (lemma-incl₀ Rwq (R⁺qx ++ (⁺-map _ proj₁ R⁺xz) ∷ʳ Rzw))
  lemma-excl R⁺xz (_∷_ {_} {_} Rzw R⁺wx)         | no  w≢y =
    let z≢y = ⁺-lift-predʳ (proj₂ ∘ proj₂) R⁺xz
    in lemma-excl (R⁺xz ∷ʳ (Rzw , z≢y , w≢y)) R⁺wx

  lemma : {w : A} → R x w → TransClosure R w x → PassCycle R y ⊎ TransClosure (ExcludeRel R y) x x
  lemma {_} Rxw R⁺wx with eq-dec x
  lemma {_} Rxw R⁺wx           | yes refl = inj₁ (lemma-incl₀ Rxw R⁺wx)
  lemma {w} Rxw R⁺wx           | no  x≢y with eq-dec w
  lemma {_} Rxw [ Rwx ]        | no  x≢y | yes refl = inj₁ (cycle₂ x≢y Rwx Rxw)
  lemma {_} Rxw ( Rwz ∷ R⁺zx ) | no  x≢y | yes refl = inj₁ (lemma-incl₀ Rwz (R⁺zx ∷ʳ Rxw))
  lemma {_} Rxw R⁺wx           | no  x≢y | no  w≢y  = lemma-excl [ Rxw , x≢y , w≢y ] R⁺wx

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


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

-- A "canonical" presentation of limits in Setoid.
--
-- These limits are obviously isomorphic to those created by
-- the Completeness proof, but are far less unweildy to work with.
-- This isomorphism is witnessed by Categories.Diagram.Pullback.up-to-iso

module Categories.Category.Instance.Properties.Setoids.Limits.Canonical where

open import Level

open import Data.Product using (_,_; _×_)

open import Relation.Binary.Bundles using (Setoid)
open import Function.Equality as SΠ renaming (id to ⟶-id)
import Relation.Binary.Reasoning.Setoid as SR

open import Categories.Diagram.Pullback

open import Categories.Category.Instance.Setoids

open Setoid renaming (_≈_ to [_][_≈_])

--------------------------------------------------------------------------------
-- Pullbacks

record FiberProduct {o ℓ} {X Y Z : Setoid o ℓ} (f : X ⟶ Z) (g : Y ⟶ Z) : Set (o ⊔ ℓ) where
  field
    elem₁ : Carrier X
    elem₂ : Carrier Y
    commute : [ Z ][ f ⟨$⟩ elem₁ ≈ g ⟨$⟩ elem₂ ]

open FiberProduct

pullback : ∀ (o ℓ : Level) {X Y Z : Setoid (o ⊔ ℓ) ℓ} → (f : X ⟶ Z) → (g : Y ⟶ Z) → Pullback (Setoids (o ⊔ ℓ) ℓ) f g
pullback _ _ {X = X} {Y = Y} {Z = Z} f g = record
  { P = record
    { Carrier = FiberProduct f g
    ; _≈_ =  λ p q → [ X ][ elem₁ p ≈ elem₁ q ] × [ Y ][ elem₂ p ≈ elem₂ q ]
    ; isEquivalence = record
      { refl = (refl X) , (refl Y)
      ; sym = λ (eq₁ , eq₂) → sym X eq₁ , sym Y eq₂
      ; trans = λ (eq₁ , eq₂) (eq₁′ , eq₂′) → (trans X eq₁ eq₁′) , (trans Y eq₂ eq₂′)
      }
    }
    ; p₁ = record { _⟨$⟩_ = elem₁ ; cong = λ (eq₁ , _) → eq₁ }
    ; p₂ = record { _⟨$⟩_ = elem₂ ; cong = λ (_ , eq₂) → eq₂ }
    ; isPullback = record
      { commute = λ {p} {q} (eq₁ , eq₂) → trans Z (cong f eq₁) (commute q)
      ; universal = λ {A} {h₁} {h₂} eq → record
        { _⟨$⟩_ = λ a → record
          { elem₁ = h₁ ⟨$⟩ a
          ; elem₂ = h₂ ⟨$⟩ a
          ; commute = eq (refl A)
          }
        ; cong = λ eq → cong h₁ eq , cong h₂ eq }
      ; unique = λ eq₁ eq₂ x≈y → eq₁ x≈y , eq₂ x≈y
      ; p₁∘universal≈h₁ = λ {_} {h₁} {_} eq → cong h₁ eq
      ; p₂∘universal≈h₂ = λ {_} {_} {h₂} eq → cong h₂ eq
      }
    }

max_stars_repo_name: tetrapharmakon/agda-categories

max_issues_repo_name: andrejbauer/agda-categories

max_forks_repo_name: andrejbauer/agda-categories


text:
module ImportTests.ExtractCaseSplit where
open import  ExtractCaseSplit
open import Data.Maybe
open import Data.Bool

test : Bool
test = func (just false)


text:
-- Andreas, 2016-06-11, issue reported by Mietek Bak

data Foo : Foo → Set where

-- WAS: Panic: unbound name Foo

-- NOW: Not in scope: Foo


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

open import lib.Basics
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Sigma

module lib.types.Pointed where

Ptd : ∀ i → Type (lsucc i)
Ptd i = Σ (Type i) (λ A → A)

Ptd₀ = Ptd lzero

⊙[_,_] : ∀ {i} (A : Type i) (a : A) → Ptd i
⊙[_,_] = _,_

infixr 0 _⊙→_
_⊙→_ : ∀ {i j} → Ptd i → Ptd j → Ptd (lmax i j)
(A , a₀) ⊙→ (B , b₀) = ⊙[ Σ (A → B) (λ f → f a₀ == b₀) , ((λ _ → b₀), idp) ]

infix 30 _⊙≃_
_⊙≃_ : ∀ {i j} → Ptd i → Ptd j → Type (lmax i j)
X ⊙≃ Y = Σ (fst (X ⊙→ Y)) (λ {(f , _) → is-equiv f})

⊙≃-in : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  (e : fst X ≃ fst Y) (p : –> e (snd X) == snd Y)
  → X ⊙≃ Y
⊙≃-in (f , ie) p = ((f , p) , ie)

⊙≃-out : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → X ⊙≃ Y
  → Σ (fst X ≃ fst Y) (λ e → –> e (snd X) == snd Y)
⊙≃-out ((f , p) , ie) = (f , ie) , p

⊙idf : ∀ {i} (X : Ptd i) → fst (X ⊙→ X)
⊙idf A = ((λ x → x) , idp)

⊙cst : ∀ {i j} {X : Ptd i} {Y : Ptd j} → fst (X ⊙→ Y)
⊙cst {Y = Y} = ((λ x → snd Y) , idp)

infixr 80 _⊙∘_
_⊙∘_ : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (g : fst (Y ⊙→ Z)) (f : fst (X ⊙→ Y)) → fst (X ⊙→ Z)
(g , gpt) ⊙∘ (f , fpt) = (g ∘ f) , (ap g fpt ∙ gpt)

infixr 80 _⊙∘e_
_⊙∘e_ : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (g : Y ⊙≃ Z) (f : X ⊙≃ Y) → X ⊙≃ Z
(g , g-eq) ⊙∘e (f , f-eq) = (g ⊙∘ f , g-eq ∘ise f-eq)

⊙∘-unit-l : ∀ {i j} {X : Ptd i} {Y : Ptd j} (f : fst (X ⊙→ Y))
  → ⊙idf Y ⊙∘ f == f
⊙∘-unit-l (f , idp) = idp

⊙∘-unit-r : ∀ {i j} {X : Ptd i} {Y : Ptd j} (f : fst (X ⊙→ Y))
  → f ⊙∘ ⊙idf X == f
⊙∘-unit-r f = idp

⊙∘-assoc : ∀ {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (h : fst (Z ⊙→ W)) (g : fst (Y ⊙→ Z)) (f : fst (X ⊙→ Y))
  → ((h ⊙∘ g) ⊙∘ f) == (h ⊙∘ (g ⊙∘ f))
⊙∘-assoc (h , hpt) (g , gpt) (f , fpt) = pair= idp (lemma fpt gpt hpt)
  where
  lemma : ∀ {x₁ x₂} (fpt : x₁ == x₂) → ∀ gpt → ∀ hpt →
          ap (h ∘ g) fpt ∙ ap h gpt ∙ hpt == ap h (ap g fpt ∙ gpt) ∙ hpt
  lemma idp gpt hpt = idp

⊙Σ : ∀ {i j} (X : Ptd i) → (fst X → Ptd j) → Ptd (lmax i j)
⊙Σ (A , a₀) Y = ⊙[ Σ A (fst ∘ Y) , (a₀ , snd (Y a₀)) ]

infixr 80 _⊙×_
_⊙×_ : ∀ {i j} → Ptd i → Ptd j → Ptd (lmax i j)
X ⊙× Y = ⊙Σ X (λ _ → Y)

⊙dfst : ∀ {i j} {X : Ptd i} (Y : fst X → Ptd j) → fst (⊙Σ X Y ⊙→ X)
⊙dfst Y = (fst , idp)

⊙fst : ∀ {i j} {X : Ptd i} {Y : Ptd j} → fst (X ⊙× Y ⊙→ X)
⊙fst = ⊙dfst _

⊙snd : ∀ {i j} {X : Ptd i} {Y : Ptd j} → fst (X ⊙× Y ⊙→ Y)
⊙snd = (snd , idp)

⊙diag : ∀ {i} {X : Ptd i} → fst (X ⊙→ X ⊙× X)
⊙diag = ((λ x → (x , x)) , idp)

⊙×-in : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  → fst (X ⊙→ Y) → fst (X ⊙→ Z) → fst (X ⊙→ Y ⊙× Z)
⊙×-in (f , fpt) (g , gpt) = (λ x → (f x , g x)) , ap2 _,_ fpt gpt

⊙fst-⊙×-in : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (f : fst (X ⊙→ Y)) (g : fst (X ⊙→ Z))
  → ⊙fst ⊙∘ ⊙×-in f g == f
⊙fst-⊙×-in (f , idp) (g , idp) = idp

⊙snd-⊙×-in : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (f : fst (X ⊙→ Y)) (g : fst (X ⊙→ Z))
  → ⊙snd ⊙∘ ⊙×-in f g == g
⊙snd-⊙×-in (f , idp) (g , idp) = idp

⊙×-in-pre∘ : ∀ {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (f : fst (Y ⊙→ Z)) (g : fst (Y ⊙→ W)) (h : fst (X ⊙→ Y))
  → ⊙×-in f g ⊙∘ h == ⊙×-in (f ⊙∘ h) (g ⊙∘ h)
⊙×-in-pre∘ (f , idp) (g , idp) (h , idp) = idp

pair⊙→ : ∀ {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  → fst (X ⊙→ Y) → fst (Z ⊙→ W)
  → fst ((X ⊙× Z) ⊙→ (Y ⊙× W))
pair⊙→ (f , fpt) (g , gpt) =
  ((λ {(x , z) → (f x , g z)}) , pair×= fpt gpt)

{- ⊙→ preserves hlevel -}
⊙→-level : ∀ {i j} {X : Ptd i} {Y : Ptd j} {n : ℕ₋₂}
  → has-level n (fst Y) → has-level n (fst (X ⊙→ Y))
⊙→-level pY = Σ-level (Π-level (λ _ → pY)) (λ _ → =-preserves-level _ pY)

{- function extensionality for pointed functions -}
⊙λ= : ∀ {i j} {X : Ptd i} {Y : Ptd j} {f g : fst (X ⊙→ Y)}
  (p : ∀ x → fst f x == fst g x) (α : snd f == p (snd X) ∙ snd g)
  → f == g
⊙λ= {g = g} p α =
  pair= (λ= p) (↓-app=cst-in (α ∙ ap (λ w → w ∙ snd g) (! (app=-β p _))))

{- Extracting data from an pointed equivalence -}
module _ {i j} {X : Ptd i} {Y : Ptd j} (⊙e : X ⊙≃ Y) where

  private
    e : fst X ≃ fst Y
    e = (fst (fst ⊙e) , snd ⊙e)

    p = snd (fst ⊙e)

  ⊙≃-to-≃ = e

  ⊙–> : fst (X ⊙→ Y)
  ⊙–> = fst ⊙e

  ⊙<– : fst (Y ⊙→ X)
  ⊙<– = (<– e , ap (<– e) (! p) ∙ <–-inv-l e (snd X))

  ⊙<–-inv-l : ⊙<– ⊙∘ ⊙–> == ⊙idf _
  ⊙<–-inv-l = ⊙λ= (<–-inv-l e) $
    ap (<– e) p ∙ ap (<– e) (! p) ∙ <–-inv-l e (snd X)
      =⟨ ! (∙-assoc (ap (<– e) p) (ap (<– e) (! p)) (<–-inv-l e (snd X))) ⟩
    (ap (<– e) p ∙ ap (<– e) (! p)) ∙ <–-inv-l e (snd X)
      =⟨ ∙-ap (<– e) p (! p) ∙ ap (ap (<– e)) (!-inv-r p)
         |in-ctx (λ w → w ∙ <–-inv-l e (snd X)) ⟩
    <–-inv-l e (snd X)
      =⟨ ! (∙-unit-r _) ⟩
    <–-inv-l e (snd X) ∙ idp ∎

  ⊙<–-inv-r : ⊙–> ⊙∘ ⊙<– == ⊙idf _
  ⊙<–-inv-r = ⊙λ= (<–-inv-r e) $
    ap (–> e) (ap (<– e) (! p) ∙ <–-inv-l e (snd X)) ∙ p
      =⟨ ap-∙ (–> e) (ap (<– e) (! p)) (<–-inv-l e (snd X))
         |in-ctx (λ w → w ∙ p) ⟩
    (ap (–> e) (ap (<– e) (! p)) ∙ ap (–> e) (<–-inv-l e (snd X))) ∙ p
      =⟨ <–-inv-adj e (snd X)
         |in-ctx (λ w → (ap (–> e) (ap (<– e) (! p)) ∙ w) ∙ p) ⟩
    (ap (–> e) (ap (<– e) (! p)) ∙ <–-inv-r e (–> e (snd X))) ∙ p
      =⟨ ∘-ap (–> e) (<– e) (! p)
         |in-ctx (λ w → (w ∙ <–-inv-r e (–> e (snd X))) ∙ p) ⟩
    (ap (–> e ∘ <– e) (! p) ∙ <–-inv-r e (–> e (snd X))) ∙ p
      =⟨ htpy-lemma (<–-inv-r e) p ⟩
    <–-inv-r e (snd Y)
      =⟨ ! (∙-unit-r _) ⟩
    <–-inv-r e (snd Y) ∙ idp ∎
    where
    htpy-lemma : ∀ {i} {A : Type i} {f : A → A}
      (p : ∀ z → f z == z) {x y : A} (q : x == y)
      → (ap f (! q) ∙ p x) ∙ q == p y
    htpy-lemma p idp = ∙-unit-r _

{- Equality of pointed types -}
⊙ua : ∀ {i} {X Y : Ptd i} → X ⊙≃ Y → X == Y
⊙ua ((f , p) , ie) = pair= (ua (f , ie)) (↓-idf-ua-in (f , ie) p)

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
------------------------------------------------------------------------
-- Indices
------------------------------------------------------------------------

module Parallel.Index where

open import Data.Product.Record
import Data.Product as Prod; open Prod using () renaming (_,_ to pair)

open import Data.Bool using (Bool; true; false; _∨_; _∧_; if_then_else_)
open import Data.Bool.Properties as Bool

open import Data.Nat using (ℕ; zero; suc; _⊔_)
open import Data.Nat.Properties

open import Algebra
import Algebra.Props.BooleanAlgebra as BAlg
import Algebra.Props.DistributiveLattice as DL
private
  module NR = CommutativeSemiringWithoutOne
                ⊔-⊓-0-commutativeSemiringWithoutOne
  module NL = DL distributiveLattice
  module BR = CommutativeSemiring Bool.commutativeSemiring-∨-∧
  module BA = BAlg Bool.booleanAlgebra

import Relation.Binary.PropositionalEquality as PropEq
open PropEq hiding (setoid)
open ≡-Reasoning
open import Data.Function
open import Relation.Nullary

------------------------------------------------------------------------
-- The index type

-- Does the parser accept the empty string?

Empty : Set
Empty = Bool

-- The maximum "distance" to the next parser which is guaranteed to
-- either consume a token or fail.

Distance : Set
Distance = ℕ

-- Parser indices. Note that it is important that the record type used
-- here has η-equality, since otherwise it would be harder to infer
-- the types.

Index : Set
Index = Empty × Distance

import Algebra.FunctionProperties as P; open P (PropEq.setoid Index)

------------------------------------------------------------------------
-- The basic operations on indices

infixl 50 _·I_
infixl 40 _∣I_

0I : Index
0I = (false , zero)

1I : Index
1I = (true , zero)

_·I_ : Index -> Index -> Index
i₁ ·I i₂ = ( proj₁ i₁ ∧ proj₁ i₂
           , (if proj₁ i₁ then proj₂ i₁ ⊔ proj₂ i₂
                          else proj₂ i₁)
           )

_∣I_ : Index -> Index -> Index
i₁ ∣I i₂ = (proj₁ i₁ ∨ proj₁ i₂ , proj₂ i₁ ⊔ proj₂ i₂)

------------------------------------------------------------------------
-- These operations satisfy some algebraic properties

private

  -- TODO: General code for taking the product of two commutative
  -- monoids. However, I don't want to define this operation for both
  -- Data.Product and Data.Product.Record. Hence I'll probably wait
  -- (at least) until pattern matching on records is possible, since I
  -- plan to merge Data.Product and Data.Product.Record then.

  ∣-assoc : Associative _∣I_
  ∣-assoc i₁ i₂ i₃ =
    cong₂ _,_ (BR.+-assoc (proj₁ i₁) (proj₁ i₂) (proj₁ i₃))
              (NR.+-assoc (proj₂ i₁) (proj₂ i₂) (proj₂ i₃))

  ∣-comm : Commutative _∣I_
  ∣-comm i₁ i₂ =
    cong₂ _,_ (BR.+-comm (proj₁ i₁) (proj₁ i₂))
              (NR.+-comm (proj₂ i₁) (proj₂ i₂))

  ∣-identity : Identity 0I _∣I_
  ∣-identity = pair
    (\i -> cong₂ _,_ (Prod.proj₁ BR.+-identity (proj₁ i))
                     (Prod.proj₁ NR.+-identity (proj₂ i)))
    (\i -> cong₂ _,_ (Prod.proj₂ BR.+-identity (proj₁ i))
                     (Prod.proj₂ NR.+-identity (proj₂ i)))

  ·-assoc : Associative _·I_
  ·-assoc i₁ i₂ i₃ with proj₁ i₁ | proj₁ i₂
  ·-assoc i₁ i₂ i₃ | false | e₂    = refl
  ·-assoc i₁ i₂ i₃ | true  | false = refl
  ·-assoc i₁ i₂ i₃ | true  | true  =
    cong (_,_ (proj₁ i₃)) (NR.+-assoc (proj₂ i₁) (proj₂ i₂) (proj₂ i₃))

  ·-identity : Identity 1I _·I_
  ·-identity = pair (\_ -> refl) (\x -> helper (proj₁ x) (proj₂ x))
    where
    helper : forall e d ->
             _≡_ {a = Index} (e ∧ true , (if e then d ⊔ zero else d))
                             (e        , d)
    helper false d = refl
    helper true  d = cong (_,_ true) (Prod.proj₂ NR.+-identity d)

  ·-∣-distrib : _·I_ DistributesOver _∣I_
  ·-∣-distrib = pair
    (\i₁ i₂ i₃ ->
        cong₂ _,_
              (Prod.proj₁ BR.distrib (proj₁ i₁) (proj₁ i₂) (proj₁ i₃))
              (distribˡ₂ (proj₂ i₁) (proj₂ i₂) (proj₂ i₃) (proj₁ i₁)))
    (\i₁ i₂ i₃ ->
        cong₂ _,_
              (Prod.proj₂ BR.distrib (proj₁ i₁) (proj₁ i₂) (proj₁ i₃))
              (distribʳ₂ (proj₂ i₁) (proj₂ i₂) (proj₂ i₃)
                                    (proj₁ i₂) (proj₁ i₃)))
    where
    lemma : forall d₁ d₂ d₃ -> d₁ ⊔ (d₂ ⊔ d₃) ≡ d₁ ⊔ d₂ ⊔ (d₁ ⊔ d₃)
    lemma d₁ d₂ d₃ = begin
      d₁       ⊔ (d₂ ⊔ d₃)   ≡⟨ sym (NL.∧-idempotent d₁)
                                  ⟨ NR.+-pres-≈ ⟩
                                byDef {x = d₂ ⊔ d₃} ⟩
      d₁ ⊔  d₁ ⊔ (d₂ ⊔ d₃)   ≡⟨ NR.+-assoc d₁ d₁ (d₂ ⊔ d₃) ⟩
      d₁ ⊔ (d₁ ⊔ (d₂ ⊔ d₃))  ≡⟨ byDef {x = d₁} ⟨ NR.+-pres-≈ ⟩
                                sym (NR.+-assoc d₁ d₂ d₃) ⟩
      d₁ ⊔ (d₁ ⊔  d₂ ⊔ d₃)   ≡⟨ byDef {x = d₁} ⟨ NR.+-pres-≈ ⟩
                                  (NR.+-comm d₁ d₂ ⟨ NR.+-pres-≈ ⟩
                                   byDef {x = d₃}) ⟩
      d₁ ⊔ (d₂ ⊔  d₁ ⊔ d₃)   ≡⟨ byDef {x = d₁} ⟨ NR.+-pres-≈ ⟩
                                NR.+-assoc d₂ d₁ d₃ ⟩
      d₁ ⊔ (d₂ ⊔ (d₁ ⊔ d₃))  ≡⟨ sym $ NR.+-assoc d₁ d₂ (d₁ ⊔ d₃) ⟩
      d₁ ⊔ d₂  ⊔ (d₁ ⊔ d₃)   ∎

    distribˡ₂ : forall d₁ d₂ d₃ e₁ ->
                (if e₁ then d₁ ⊔ (d₂ ⊔ d₃) else d₁) ≡
                (if e₁ then d₁ ⊔ d₂        else d₁) ⊔
                (if e₁ then d₁ ⊔ d₃        else d₁)
    distribˡ₂ d₁ d₂ d₃ true  = lemma d₁ d₂ d₃
    distribˡ₂ d₁ d₂ d₃ false = sym (NL.∧-idempotent d₁)

    distribʳ₂ : forall d₁ d₂ d₃ e₂ e₃ ->
                (if e₂ ∨ e₃ then d₂ ⊔ d₃ ⊔ d₁ else d₂ ⊔ d₃)
                ≡
                (if e₂ then d₂ ⊔ d₁ else d₂) ⊔
                (if e₃ then d₃ ⊔ d₁ else d₃)
    distribʳ₂ d₁ d₂ d₃ true true = begin
      d₂ ⊔ d₃ ⊔ d₁         ≡⟨ NR.+-comm (d₂ ⊔ d₃) d₁ ⟩
      d₁ ⊔ (d₂ ⊔ d₃)       ≡⟨ lemma d₁ d₂ d₃ ⟩
      d₁ ⊔ d₂ ⊔ (d₁ ⊔ d₃)  ≡⟨ NR.+-comm d₁ d₂ ⟨ NR.+-pres-≈ ⟩
                              NR.+-comm d₁ d₃ ⟩
      d₂ ⊔ d₁ ⊔ (d₃ ⊔ d₁)  ∎
    distribʳ₂ d₁ d₂ d₃ true false = begin
      d₂ ⊔  d₃ ⊔ d₁   ≡⟨ NR.+-assoc d₂ d₃ d₁ ⟩
      d₂ ⊔ (d₃ ⊔ d₁)  ≡⟨ byDef {x = d₂} ⟨ NR.+-pres-≈ ⟩
                         NR.+-comm d₃ d₁ ⟩
      d₂ ⊔ (d₁ ⊔ d₃)  ≡⟨ sym $ NR.+-assoc d₂ d₁ d₃ ⟩
      d₂ ⊔  d₁ ⊔ d₃   ∎
    distribʳ₂ d₁ d₂ d₃ false true  = NR.+-assoc d₂ d₃ d₁
    distribʳ₂ d₁ d₂ d₃ false false = refl

·-idempotent : Idempotent _·I_
·-idempotent i = cong₂ _,_ (BA.∧-idempotent (proj₁ i))
                           (lemma (proj₁ i) (proj₂ i))
  where
  lemma : forall b x -> (if b then x ⊔ x else x) ≡ x
  lemma true  x = NL.∧-idempotent x
  lemma false x = refl

∣-idempotent : Idempotent _∣I_
∣-idempotent i = cong₂ _,_ (BA.∨-idempotent (proj₁ i))
                           (NL.∧-idempotent (proj₂ i))

-- Not quite a semiring, but the proper name is too long...

indexSemiring : SemiringWithoutAnnihilatingZero
indexSemiring = record
  { setoid = PropEq.setoid Index
  ; _+_    = _∣I_
  ; _*_    = _·I_
  ; 0#     = 0I
  ; 1#     = 1I
  ; isSemiringWithoutAnnihilatingZero = record
    { +-isCommutativeMonoid = record
      { isMonoid = record
        { isSemigroup = record
          { assoc    = ∣-assoc
          ; ∙-pres-≈ = cong₂ _∣I_
          }
        ; identity = ∣-identity
        }
      ; comm = ∣-comm
      }
    ; *-isMonoid = record
      { isSemigroup = record
        { assoc    = ·-assoc
        ; ∙-pres-≈ = cong₂ _·I_
        }
      ; identity = ·-identity
      }
    ; distrib = ·-∣-distrib
    }
  }

module IndexSemiring =
  SemiringWithoutAnnihilatingZero indexSemiring

nearSemiring : NearSemiring
nearSemiring = record
  { setoid = setoid
  ; _+_    = _+_
  ; _*_    = _*_
  ; 0#     = 0#
  ; isNearSemiring = record
    { +-isMonoid    = +-isMonoid
    ; *-isSemigroup = *-isSemigroup
    ; distribʳ      = Prod.proj₂ distrib
    ; zeroˡ         = \_ -> PropEq.refl
    }
  }
  where open IndexSemiring

private

  lemma : suc zero ≢ zero
  lemma ()

  -- The indices very nearly form a semiring (∣I, ·I, 0I, 1I). The
  -- only missing piece is that 0I is not a right zero for ·I:

  notRightZero : ¬ RightZero 0I _·I_
  notRightZero zeroʳ = lemma $ cong proj₂ $
    zeroʳ (false , suc zero)

  -- It might also be worth noting that ·I is not commutative:

  notCommutative : ¬ Commutative _·I_
  notCommutative comm = lemma $ cong proj₂ $
    comm (true , suc zero) (false , zero)

  -- Note that we don't want these properties to be true. The second
  -- one implies the first, and the first implies that
  --   p = p ⊛> symbol
  -- is an OK definition, even though it is left recursive.

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
------------------------------------------------------------------------
-- Small coinductive higher lenses with erased "proofs"
------------------------------------------------------------------------

{-# OPTIONS --guardedness #-}

import Equality.Path as P

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

open P.Derived-definitions-and-properties eq

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

open import Bijection equality-with-J as B using (_↔_)
open import Equality.Decidable-UIP equality-with-J using (Constant)
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq
  using (_≃_; Is-equivalence)
open import Equivalence.Erased.Cubical eq as EEq using (_≃ᴱ_)
open import Equivalence.Erased.Contractible-preimages.Cubical eq as ECP
  using (_⁻¹ᴱ_)
open import Erased.Cubical eq
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 using (∥_∥)
open import Preimage equality-with-J using (_⁻¹_)
open import Tactic.Sigma-cong equality-with-J
open import Univalence-axiom equality-with-J

open import Lens.Non-dependent eq
import Lens.Non-dependent.Higher.Capriotti.Variant.Erased.Variant eq
  as V
open import Lens.Non-dependent.Higher.Coherently.Coinductive eq
import Lens.Non-dependent.Higher.Coinductive eq as C
import Lens.Non-dependent.Higher.Coinductive.Erased eq as CE
import Lens.Non-dependent.Higher.Coinductive.Small eq as S
import Lens.Non-dependent.Higher.Erased eq as E

private
  variable
    a b c d : Level
    A B     : Type a
    l g p s : A
    P       : A → Type p
    f       : (x : A) → P x
    univ    : Univalence a

------------------------------------------------------------------------
-- Weakly constant functions

-- Weakly constant type-valued functions.
--
-- Note that the definition does not use _≃ᴱ_: the right-to-left
-- directions of the equivalences are erased.

Constantᴱ :
  {A : Type a} →
  (A → Type p) → Type (a ⊔ p)
Constantᴱ P = ∀ x y → ∃ λ (f : P x → P y) → Erased (Is-equivalence f)

-- In erased contexts Constantᴱ is pointwise equivalent to Constant
-- (assuming univalence).

@0 Constantᴱ≃Constant :
  {P : A → Type p} →
  Univalence p →
  Constantᴱ P ≃ Constant P
Constantᴱ≃Constant {P = P} univ =
  Constantᴱ P                                                ↔⟨⟩
  (∀ x y → ∃ λ (f : P x → P y) → Erased (Is-equivalence f))  ↔⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → ∃-cong λ _ → erased Erased↔) ⟩
  (∀ x y → ∃ λ (f : P x → P y) → Is-equivalence f)           ↔⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → inverse Eq.≃-as-Σ) ⟩
  (∀ x y → P x ≃ P y)                                        ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → inverse $ ≡≃≃ univ) ⟩
  (∀ x y → P x ≡ P y)                                        ↔⟨⟩
  Constant P                                                 □

-- In erased contexts Constantᴱ is pointwise equivalent to
-- S.Constant-≃.

@0 Constantᴱ≃Constant-≃ : Constantᴱ P ≃ S.Constant-≃ P
Constantᴱ≃Constant-≃ {P = P} =
  Constantᴱ P                                                ↔⟨⟩
  (∀ x y → ∃ λ (f : P x → P y) → Erased (Is-equivalence f))  ↔⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → ∃-cong λ _ → erased Erased↔) ⟩
  (∀ x y → ∃ λ (f : P x → P y) → Is-equivalence f)           ↔⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → inverse Eq.≃-as-Σ) ⟩
  (∀ x y → P x ≃ P y)                                        ↔⟨⟩
  S.Constant-≃ P                                             □

-- In erased contexts Constantᴱ (f ⁻¹ᴱ_) is pointwise equivalent to
-- S.Constant-≃ (f ⁻¹_).

@0 Constantᴱ-⁻¹ᴱ-≃-Constant-≃-⁻¹ :
  Constantᴱ (f ⁻¹ᴱ_) ≃ S.Constant-≃ (f ⁻¹_)
Constantᴱ-⁻¹ᴱ-≃-Constant-≃-⁻¹ {f = f} =
  Constantᴱ (f ⁻¹ᴱ_)               ↝⟨ Constantᴱ≃Constant-≃ ⟩
  S.Constant-≃ (f ⁻¹ᴱ_)            ↔⟨⟩
  (∀ b₁ b₂ → f ⁻¹ᴱ b₁ ≃ f ⁻¹ᴱ b₂)  ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ →
                                       Eq.≃-preserves ext (inverse ECP.⁻¹≃⁻¹ᴱ) (inverse ECP.⁻¹≃⁻¹ᴱ)) ⟩
  (∀ b₁ b₂ → f ⁻¹ b₁ ≃ f ⁻¹ b₂)    ↔⟨⟩
  S.Constant-≃ (f ⁻¹_)             □

-- In erased contexts Constantᴱ (f ⁻¹ᴱ_) is pointwise equivalent to
-- Constant (f ⁻¹_) (assuming univalence).

@0 Constantᴱ-⁻¹ᴱ-≃-Constant-⁻¹ :
  Block "Constantᴱ-⁻¹ᴱ-≃-Constant-⁻¹" →
  {A : Type a} {B : Type b} {f : A → B} →
  Univalence (a ⊔ b) →
  Constantᴱ (f ⁻¹ᴱ_) ≃ Constant (f ⁻¹_)
Constantᴱ-⁻¹ᴱ-≃-Constant-⁻¹ ⊠ {f = f} univ =
  Constantᴱ (f ⁻¹ᴱ_)    ↝⟨ Constantᴱ-⁻¹ᴱ-≃-Constant-≃-⁻¹ ⟩
  S.Constant-≃ (f ⁻¹_)  ↝⟨ inverse $ S.Constant≃Constant-≃ univ ⟩□
  Constant (f ⁻¹_)      □

-- A "computation" rule for Constantᴱ-⁻¹ᴱ-≃-Constant-⁻¹.

@0 proj₁-from-Constantᴱ-⁻¹ᴱ-≃-Constant-⁻¹ :
  (bl : Block "Constantᴱ-⁻¹ᴱ-≃-Constant-⁻¹") →
  ∀ {A : Type a} {B : Type b} {f : A → B} {univ : Univalence (a ⊔ b)}
    {c : Constant (f ⁻¹_)} {b₁ b₂} →
  proj₁ (_≃_.from (Constantᴱ-⁻¹ᴱ-≃-Constant-⁻¹ bl univ) c b₁ b₂) ≡
  ECP.⁻¹→⁻¹ᴱ ∘ subst P.id (c b₁ b₂) ∘ ECP.⁻¹ᴱ→⁻¹
proj₁-from-Constantᴱ-⁻¹ᴱ-≃-Constant-⁻¹ ⊠ {c = c} {b₁ = b₁} {b₂ = b₂} =
  ⟨ext⟩ λ (a , [ eq ]) →

  ECP.⁻¹→⁻¹ᴱ (≡⇒→ (c b₁ b₂) (a , eq))         ≡⟨ cong ECP.⁻¹→⁻¹ᴱ $ sym $
                                                 subst-id-in-terms-of-≡⇒↝ equivalence ⟩∎
  ECP.⁻¹→⁻¹ᴱ (subst P.id (c b₁ b₂) (a , eq))  ∎

-- Constantᴱ (get ⁻¹ᴱ_) can be expressed (up to _≃ᴱ_) in terms of a
-- "setter" and an erased "get-set" law that, in a certain way, form
-- an erased family of equivalences.
--
-- This lemma is based on a lemma suggested by Andrea Vezzosi, see
-- S.Constant-≃-get-⁻¹-≃.

Constantᴱ-⁻¹ᴱ-≃ᴱ :
  {A : Type a} {B : Type b} {get : A → B} →
  Block "Constantᴱ-⁻¹ᴱ-≃ᴱ" →
  Constantᴱ (get ⁻¹ᴱ_) ≃ᴱ
  (∃ λ (set : A → B → A) →
   Erased (∃ λ (get-set : ∀ a b → get (set a b) ≡ b) →
           ∀ b₁ b₂ →
           let f : get ⁻¹ b₁ → get ⁻¹ b₂
               f = λ (a , _) → set a b₂ , get-set a b₂
           in
           Is-equivalence f))
Constantᴱ-⁻¹ᴱ-≃ᴱ {A = A} {B = B} {get = get} ⊠ =
  Constantᴱ (get ⁻¹ᴱ_)                                                    ↔⟨⟩

  (∀ b₁ b₂ →
   ∃ λ (f : get ⁻¹ᴱ b₁ → get ⁻¹ᴱ b₂) →
   Erased (Is-equivalence f))                                             ↔⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → ∃-cong λ f → Erased-cong (
                                                                              Is-equivalence≃Is-equivalence-∘ˡ {k = equivalence} ext $
                                                                              _≃_.is-equivalence $ from-bijection $
                                                                              ∃-cong λ _ → erased Erased↔)) ⟩
  (∀ b₁ b₂ →
   ∃ λ (f : get ⁻¹ᴱ b₁ → get ⁻¹ᴱ b₂) →
   Erased (Is-equivalence (Σ-map P.id erased ∘ f)))                       ↔⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → ∃-cong λ f → Erased-cong (
                                                                              Is-equivalence≃Is-equivalence-∘ʳ {k = equivalence} ext $
                                                                              _≃_.is-equivalence $ from-bijection $
                                                                              ∃-cong λ _ → inverse $ erased Erased↔)) ⟩
  (∀ b₁ b₂ →
   ∃ λ (f : get ⁻¹ᴱ b₁ → get ⁻¹ᴱ b₂) →
   Erased (Is-equivalence (Σ-map P.id erased ∘ f ∘ Σ-map P.id [_]→)))     ↔⟨ Π-comm ⟩

  (∀ b₂ b₁ →
   ∃ λ (f : get ⁻¹ᴱ b₁ → get ⁻¹ᴱ b₂) →
   Erased (Is-equivalence (Σ-map P.id erased ∘ f ∘ Σ-map P.id [_]→)))     ↔⟨ (∀-cong ext λ _ → ΠΣ-comm) ⟩

  (∀ b₂ →
   ∃ λ (f : ∀ b₁ → get ⁻¹ᴱ b₁ → get ⁻¹ᴱ b₂) →
   ∀ b₁ →
   Erased (Is-equivalence (Σ-map P.id erased ∘ f b₁ ∘ Σ-map P.id [_]→)))  ↔⟨ (∀-cong ext λ _ → ∃-cong λ _ → inverse Erased-Π↔Π) ⟩

  (∀ b₂ →
   ∃ λ (f : ∀ b₁ → get ⁻¹ᴱ b₁ → get ⁻¹ᴱ b₂) →
   Erased (∀ b₁ →
           Is-equivalence (Σ-map P.id erased ∘ f b₁ ∘ Σ-map P.id [_]→)))  ↔⟨ (∀-cong ext λ _ →
                                                                              Σ-cong {k₂ = equivalence}
                                                                                (inverse (∀-cong ext λ _ → currying) F.∘
                                                                                Π-comm F.∘
                                                                                (∀-cong ext λ _ → currying))
                                                                                (λ _ → Eq.id)) ⟩
  (∀ b₂ →
   ∃ λ (f : ∀ a → (∃ λ b₁ → Erased (get a ≡ b₁)) → get ⁻¹ᴱ b₂) →
   Erased (∀ b₁ →
           let g : get ⁻¹ b₁ → get ⁻¹ b₂
               g = λ (a , eq) → Σ-map P.id erased (f a (b₁ , [ eq ]))
           in
           Is-equivalence g))                                             ↝⟨ (∀-cong ext λ _ →
                                                                              EEq.Σ-cong-≃ᴱ-Erased
                                                                                (∀-cong ext λ _ →
                                                                                EEq.drop-⊤-left-Π-≃ᴱ ext
                                                                                Erased-other-singleton≃ᴱ⊤
                                                                                (λ _ _ → F.id)) λ f →
                                                                              Erased-cong (
                                                                              ∀-cong ext λ b₁ →
                                                                              Is-equivalence-cong ext λ (a , eq) →
      Σ-map P.id erased (f a (b₁ , [ eq ]))                                       ≡⟨ cong (Σ-map P.id erased ∘ f a) $ sym $
                                                                                erased (proj₂ Contractibleᴱ-Erased-other-singleton) _ ⟩

      Σ-map P.id erased (f a (get a , [ refl _ ]))                                ≡⟨ cong (Σ-map P.id erased) $ sym $ subst-refl _ _ ⟩∎

      Σ-map P.id erased
        (subst (const _) (refl _) (f a (get a , [ refl _ ])))                   ∎)) ⟩

  (∀ b₂ →
   ∃ λ (f : A → get ⁻¹ᴱ b₂) →
   Erased (∀ b₁ →
           let g : get ⁻¹ b₁ → get ⁻¹ b₂
               g = λ (a , _) → Σ-map P.id erased (f a)
           in
           Is-equivalence g))                                             ↔⟨ ΠΣ-comm ⟩

  (∃ λ (f : ∀ b → A → get ⁻¹ᴱ b) →
   ∀ b₂ →
   Erased (∀ b₁ →
           let g : get ⁻¹ b₁ → get ⁻¹ b₂
               g = λ (a , _) → Σ-map P.id erased (f b₂ a)
           in
           Is-equivalence g))                                             ↔⟨ (∃-cong λ _ → inverse Erased-Π↔Π) ⟩

  (∃ λ (f : ∀ b → A → get ⁻¹ᴱ b) →
   Erased (∀ b₂ b₁ →
           let g : get ⁻¹ b₁ → get ⁻¹ b₂
               g = λ (a , _) → Σ-map P.id erased (f b₂ a)
           in
           Is-equivalence g))                                             ↔⟨ Σ-cong Π-comm (λ _ → Erased-cong Π-comm) ⟩

  (∃ λ (f : A → ∀ b → get ⁻¹ᴱ b) →
   Erased (∀ b₁ b₂ →
           let g : get ⁻¹ b₁ → get ⁻¹ b₂
               g = λ (a , _) → Σ-map P.id erased (f a b₂)
           in
           Is-equivalence g))                                             ↔⟨ Σ-cong (∀-cong ext λ _ → ΠΣ-comm) (λ _ → Eq.id) ⟩

  (∃ λ (f : A → ∃ λ (set : B → A) →
                ∀ b → Erased (get (set b) ≡ b)) →
   Erased (∀ b₁ b₂ →
           let g : get ⁻¹ b₁ → get ⁻¹ b₂
               g = λ (a , _) → proj₁ (f a) b₂ , erased (proj₂ (f a) b₂)
           in
           Is-equivalence g))                                             ↔⟨ Σ-cong
                                                                               (∀-cong ext λ _ → ∃-cong λ _ → inverse Erased-Π↔Π)
                                                                               (λ _ → Eq.id) ⟩
  (∃ λ (f : A → ∃ λ (set : B → A) →
                Erased (∀ b → get (set b) ≡ b)) →
   Erased (∀ b₁ b₂ →
           let g : get ⁻¹ b₁ → get ⁻¹ b₂
               g = λ (a , _) → proj₁ (f a) b₂ , erased (proj₂ (f a)) b₂
           in
           Is-equivalence g))                                             ↔⟨ Σ-cong-id {k₂ = equivalence} ΠΣ-comm ⟩

  (∃ λ ((set , get-set) :
        ∃ λ (set : A → B → A) →
        ∀ a → Erased (∀ b → get (set a b) ≡ b)) →
   Erased (∀ b₁ b₂ →
           let f : get ⁻¹ b₁ → get ⁻¹ b₂
               f = λ (a , _) → set a b₂ , erased (get-set a) b₂
           in
           Is-equivalence f))                                             ↔⟨ Σ-cong (∃-cong λ _ → inverse Erased-Π↔Π) (λ _ → Eq.id) ⟩

  (∃ λ ((set , [ get-set ]) :
        ∃ λ (set : A → B → A) →
        Erased (∀ a b → get (set a b) ≡ b)) →
   Erased (∀ b₁ b₂ →
           let f : get ⁻¹ b₁ → get ⁻¹ b₂
               f = λ (a , _) → set a b₂ , get-set a b₂
           in
           Is-equivalence f))                                             ↔⟨ inverse Σ-assoc ⟩

  (∃ λ (set : A → B → A) →
   ∃ λ (([ get-set ]) : Erased (∀ a b → get (set a b) ≡ b)) →
   Erased (∀ b₁ b₂ →
           Is-equivalence λ (a , _) → set a b₂ , get-set a b₂))           ↔⟨ (∃-cong λ _ → inverse
                                                                              Erased-Σ↔Σ) ⟩□
  (∃ λ (set : A → B → A) →
   Erased (∃ λ (get-set : ∀ a b → get (set a b) ≡ b) →
           ∀ b₁ b₂ →
           Is-equivalence λ (a , _) → set a b₂ , get-set a b₂))           □

-- A lemma relating S.Constant-≃-get-⁻¹-≃,
-- Constantᴱ-⁻¹ᴱ-≃-Constant-≃-⁻¹ and Constantᴱ-⁻¹ᴱ-≃ᴱ.

@0 to-Constant-≃-get-⁻¹-≃-to-Constantᴱ-⁻¹ᴱ-≃-Constant-≃-⁻¹-≡ :
  (bl : Block "Constant-≃-get-⁻¹-≃")
  {A : Type a} {B : Type b} {get : A → B} →
  (c : Constantᴱ (get ⁻¹ᴱ_)) →
  _≃_.to (S.Constant-≃-get-⁻¹-≃ bl)
    (_≃_.to Constantᴱ-⁻¹ᴱ-≃-Constant-≃-⁻¹ c) ≡
  Σ-map P.id erased
    (_≃ᴱ_.to (Constantᴱ-⁻¹ᴱ-≃ᴱ bl) c)
to-Constant-≃-get-⁻¹-≃-to-Constantᴱ-⁻¹ᴱ-≃-Constant-≃-⁻¹-≡
  bl {get = get} c =
  _≃_.from (Eq.≃-≡ $ Eq.↔⇒≃ $ inverse Σ-assoc) $
  Σ-≡,≡→≡
    (lemma bl)
    ((Π-closure ext 1 λ _ →
      Π-closure ext 1 λ _ →
      Eq.propositional ext _)
       _ _)
  where
  lemma :
    (bl : Block "Constant-≃-get-⁻¹-≃") →
    (proj₁ $ _↔_.to Σ-assoc $
     _≃_.to (S.Constant-≃-get-⁻¹-≃ bl)
       (_≃_.to Constantᴱ-⁻¹ᴱ-≃-Constant-≃-⁻¹ c)) ≡
    (proj₁ $ _↔_.to Σ-assoc $
     Σ-map P.id erased (_≃ᴱ_.to (Constantᴱ-⁻¹ᴱ-≃ᴱ bl) c))
  lemma ⊠ =
    Σ-≡,≡→≡
      (⟨ext⟩ λ a → ⟨ext⟩ λ b →

       proj₁ (proj₁ (c (get a) b) (a , [ refl _ ]))      ≡⟨ cong proj₁ $ sym $ subst-refl _ _ ⟩∎
       proj₁ (subst (λ _ → get ⁻¹ᴱ b) (refl _)
                (proj₁ (c (get a) b) (a , [ refl _ ])))  ∎)
      (⟨ext⟩ λ a → ⟨ext⟩ λ b →

       subst (λ set → ∀ a b → get (set a b) ≡ b)
         (⟨ext⟩ λ a → ⟨ext⟩ λ b →
          cong {x = proj₁ (c (get a) b) (a , [ refl _ ])} proj₁ $ sym $
          subst-refl _ _)
         (λ a b → erased (proj₂ (proj₁ (c (get a) b) (a , [ refl _ ]))))
         a b                                                              ≡⟨ sym $
                                                                             trans (push-subst-application _ _) $
                                                                             cong (_$ b) $ push-subst-application _ _ ⟩
       subst (λ set → get (set a b) ≡ b)
         (⟨ext⟩ λ _ → ⟨ext⟩ λ _ → cong proj₁ $ sym $ subst-refl _ _)
         (erased (proj₂ (proj₁ (c (get a) b) (a , [ refl _ ]))))          ≡⟨ trans (subst-ext _ _) $
                                                                             subst-ext _ _ ⟩
       subst (λ s → get s ≡ b)
         (cong proj₁ $ sym $ subst-refl _ _)
         (erased (proj₂ (proj₁ (c (get a) b) (a , [ refl _ ]))))          ≡⟨ sym $ subst-∘ _ _ _ ⟩

       subst (λ (s , _) → get s ≡ b)
         (sym $ subst-refl _ _)
         (erased (proj₂ (proj₁ (c (get a) b) (a , [ refl _ ]))))          ≡⟨ elim¹
                                                                               (λ {p} eq →
                                                                                subst (λ (s , _) → get s ≡ b) eq
                                                                                (erased (proj₂ (proj₁ (c (get a) b) (a , [ refl _ ])))) ≡
                                                                                erased (proj₂ p))
                                                                               (subst-refl _ _)
                                                                               _ ⟩∎
       erased
         (proj₂ (subst (λ _ → get ⁻¹ᴱ b) (refl _)
                   (proj₁ (c (get a) b) (a , [ refl _ ]))))               ∎)

------------------------------------------------------------------------
-- Coherently constant families of fibres

-- Coherently constant families of fibres (with erased proofs),
-- defined using univalence.

Coherently-constant-fibres :
  {A : Type a} {B : Type b} →
  @0 Univalence (a ⊔ b) →
  (A → B) → Type (a ⊔ b)
Coherently-constant-fibres {A = A} {B = B} univ get =
  ∃ λ (set : A → B → A) →
    Erased
      (∃ λ (c : S.Coherently-constant univ (get ⁻¹_)) →
       set ≡
       S.Lens.set {univ = univ}
         (record { get⁻¹-coherently-constant = c }))

-- Coherently-constant-fibres univ get is equivalent (with erased
-- proofs) to CE.Coherently-constant (get ⁻¹ᴱ_) (assuming univalence).

Coherently-constant-fibres≃ᴱCoherently-constant-⁻¹ᴱ :
  {A : Type a} {B : Type b} {get : A → B} →
  @0 Univalence (lsuc (a ⊔ b)) →
  (@0 univ : Univalence (a ⊔ b)) →
  Coherently-constant-fibres univ get ≃ᴱ
  CE.Coherently-constant (get ⁻¹ᴱ_)
Coherently-constant-fibres≃ᴱCoherently-constant-⁻¹ᴱ
  {a = a} {b = b} {A = A} {B = B} {get = get} univ′ univ =
  block λ bl →

  Coherently-constant-fibres univ get                                     ↔⟨⟩

  (∃ λ (set : A → B → A) →
   Erased
     (∃ λ (c : S.Coherently-constant univ (get ⁻¹_)) →
      set ≡
      S.Lens.set {univ = univ}
        (record { get⁻¹-coherently-constant = c })))                      ↔⟨ (∃-cong λ _ → Erased-cong (∃-cong λ c →
                                                                              ≡⇒≃ $ cong (_ ≡_) $
                                                                              S.Lens.set≡ {univ = univ}
                                                                                (record { get⁻¹-coherently-constant = c })
                                                                                bl)) ⟩
  (∃ λ (set : A → B → A) →
   Erased
     (∃ λ (c : S.Coherently-constant univ (get ⁻¹_)) →
      set ≡ proj₁ (_≃_.to (S.Constant-≃-get-⁻¹-≃ bl) (c .property))))     ↔⟨ (∃-cong λ _ → Erased-cong (∃-cong λ _ → inverse $
                                                                              ≡-comm F.∘
                                                                              drop-⊤-right λ _ →
                                                                              _⇔_.to contractible⇔↔⊤ $
                                                                              other-singleton-contractible _)) ⟩
  (∃ λ (set : A → B → A) →
   Erased
     (∃ λ (c : S.Coherently-constant univ (get ⁻¹_)) →
      ∃ λ (p : proj₁ (_≃_.to (S.Constant-≃-get-⁻¹-≃ bl) (c .property)) ≡
               set) →
      ∃ λ (q : ∃ λ (get-set : (a : A) (b : B) → get (set a b) ≡ b) →
               ∀ b₁ b₂ →
               let f : get ⁻¹ b₁ → get ⁻¹ b₂
                   f = λ (a , _) → set a b₂ , get-set a b₂
               in Is-equivalence f) →
      subst
        (λ set →
           ∃ λ (get-set : (a : A) (b : B) → get (set a b) ≡ b) →
           ∀ b₁ b₂ →
           let f : get ⁻¹ b₁ → get ⁻¹ b₂
               f = λ (a , _) → set a b₂ , get-set a b₂
           in
           Is-equivalence f)
        p
        (proj₂ (_≃_.to (S.Constant-≃-get-⁻¹-≃ bl) (c .property))) ≡
        q))                                                               ↔⟨ (∃-cong λ _ → Erased-cong (∃-cong λ _ →
                                                                              (∃-cong λ _ → ∃-comm) F.∘
                                                                              ∃-comm F.∘
                                                                              (∃-cong λ _ → inverse Σ-assoc))) ⟩
  (∃ λ (set : A → B → A) →
   Erased
     (∃ λ (c : S.Coherently-constant univ (get ⁻¹_)) →
      ∃ λ (get-set : (a : A) (b : B) → get (set a b) ≡ b) →
      ∃ λ (eq : ∀ b₁ b₂ →
                let f : get ⁻¹ b₁ → get ⁻¹ b₂
                    f = λ (a , _) → set a b₂ , get-set a b₂
                in Is-equivalence f) →
      ∃ λ (p : proj₁ (_≃_.to (S.Constant-≃-get-⁻¹-≃ bl) (c .property)) ≡
               set) →
      subst
        (λ set →
           ∃ λ (get-set : (a : A) (b : B) → get (set a b) ≡ b) →
           ∀ b₁ b₂ →
           let f : get ⁻¹ b₁ → get ⁻¹ b₂
               f = λ (a , _) → set a b₂ , get-set a b₂
           in
           Is-equivalence f)
        p
        (proj₂ (_≃_.to (S.Constant-≃-get-⁻¹-≃ bl) (c .property))) ≡
        (get-set , eq)))                                                  ↔⟨ (∃-cong λ _ → Erased-cong (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                              B.Σ-≡,≡↔≡)) ⟩
  (∃ λ (set : A → B → A) →
   Erased
     (∃ λ (c : S.Coherently-constant univ (get ⁻¹_)) →
      ∃ λ (get-set : (a : A) (b : B) → get (set a b) ≡ b) →
      ∃ λ (eq : ∀ b₁ b₂ →
                let f : get ⁻¹ b₁ → get ⁻¹ b₂
                    f = λ (a , _) → set a b₂ , get-set a b₂
                in Is-equivalence f) →
      _≃_.to (S.Constant-≃-get-⁻¹-≃ bl) (c .property) ≡
      (set , get-set , eq)))                                              ↔⟨ (∃-cong λ _ → Erased-cong (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                              ≡⇒≃ (cong (_≡ _) $ _≃_.left-inverse-of (S.Constant-≃-get-⁻¹-≃ bl) _) F.∘
                                                                              inverse (Eq.≃-≡ $ inverse $ S.Constant-≃-get-⁻¹-≃ bl))) ⟩
  (∃ λ (set : A → B → A) →
   Erased
     (∃ λ (c : S.Coherently-constant univ (get ⁻¹_)) →
      ∃ λ (get-set : (a : A) (b : B) → get (set a b) ≡ b) →
      ∃ λ (eq : ∀ b₁ b₂ →
                let f : get ⁻¹ b₁ → get ⁻¹ b₂
                    f = λ (a , _) → set a b₂ , get-set a b₂
                in Is-equivalence f) →
      c .property ≡ S.Constant-≃-get-⁻¹-≃⁻¹ (set , get-set , eq)))        ↔⟨ (Σ-assoc F.∘
                                                                              (∃-cong λ _ →
                                                                               Erased-Σ↔Σ F.∘
                                                                               Erased-cong
                                                                                (Σ-assoc F.∘
                                                                                (∃-cong λ _ → ∃-comm) F.∘
                                                                                ∃-comm))) ⟩
  (∃ λ ((set , [ get-set , eq ]) :
        ∃ λ (set : A → B → A) →
        Erased
          (∃ λ (get-set : (a : A) (b : B) → get (set a b) ≡ b) →
           ∀ b₁ b₂ →
           let f : get ⁻¹ b₁ → get ⁻¹ b₂
               f = λ (a , _) → set a b₂ , get-set a b₂
           in
           Is-equivalence f)) →
   Erased
     (∃ λ (c : S.Coherently-constant univ (get ⁻¹_)) →
      c .property ≡ S.Constant-≃-get-⁻¹-≃⁻¹ (set , get-set , eq)))        ↝⟨ (inverse $
                                                                              EEq.Σ-cong-≃ᴱ-Erased (Constantᴱ-⁻¹ᴱ-≃ᴱ bl) λ c →
                                                                              Erased-cong (∃-cong λ c′ →
                                                                              ≡⇒↝ _ (cong (c′ .property ≡_) (
       _≃_.to Constantᴱ-⁻¹ᴱ-≃-Constant-≃-⁻¹ c                                   ≡⟨ sym $ _≃_.to-from (S.Constant-≃-get-⁻¹-≃ bl) $
                                                                                to-Constant-≃-get-⁻¹-≃-to-Constantᴱ-⁻¹ᴱ-≃-Constant-≃-⁻¹-≡
                                                                                bl c ⟩∎
       S.Constant-≃-get-⁻¹-≃⁻¹
         (Σ-map P.id erased $ _≃ᴱ_.to (Constantᴱ-⁻¹ᴱ-≃ᴱ bl) c)                  ∎)))) ⟩

  (∃ λ (c : Constantᴱ (get ⁻¹ᴱ_)) →
   Erased
     (∃ λ (c′ : S.Coherently-constant univ (get ⁻¹_)) →
      c′ .property ≡ _≃_.to Constantᴱ-⁻¹ᴱ-≃-Constant-≃-⁻¹ c))             ↔⟨ (∃-cong λ c → Erased-cong (inverse $
                                                                              Σ-cong (S.Coinductive-coherently-constant≃Coherently-constant
                                                                                univ′ univ) λ c′ →
                                                                              lemma₁ bl c (c′ .property))) ⟩
  (∃ λ (c : Constantᴱ (get ⁻¹ᴱ_)) →
   Erased
     (∃ λ (c′ : C.Coherently-constant (get ⁻¹_)) →
      c′ .property ≡ _≃_.to (Constantᴱ-⁻¹ᴱ-≃-Constant-⁻¹ bl univ) c))     ↔⟨ (∃-cong λ c → Erased-cong (lemma₃ bl c)) ⟩

  (∃ λ (c : Constantᴱ (get ⁻¹ᴱ_)) →
   Erased (
   ∃ λ (c′ : C.Coherently-constant (get ⁻¹ᴱ_)) →
   ∀ b₁ b₂ → proj₁ (c b₁ b₂) ≡ subst P.id (c′ .property b₁ b₂)))          ↔⟨ inverse Σ-assoc F.∘
                                                                             (Σ-cong (ΠΣ-comm F.∘ ∀-cong ext λ _ → ΠΣ-comm) λ _ → F.id) ⟩
  (∃ λ (get⁻¹ᴱ-const : ∀ b₁ b₂ → get ⁻¹ᴱ b₁ → get ⁻¹ᴱ b₂) →
   (∀ b₁ b₂ → Erased (Is-equivalence (get⁻¹ᴱ-const b₁ b₂))) ×
   Erased (
   ∃ λ (c′ : C.Coherently-constant (get ⁻¹ᴱ_)) →
   ∀ b₁ b₂ → get⁻¹ᴱ-const b₁ b₂ ≡ subst P.id (c′ .property b₁ b₂)))       ↔⟨ (∃-cong {k = bijection} λ _ →
                                                                              drop-⊤-left-× λ ([ _ , eq ]) →
                                                                              _⇔_.to contractible⇔↔⊤ $
                                                                              propositional⇒inhabited⇒contractible
                                                                                (Π-closure ext 1 λ _ →
                                                                                Π-closure ext 1 λ _ →
                                                                                H-level-Erased 1 (Eq.propositional ext _))
                                                                                (λ x y →
                                                                                [ Eq.respects-extensional-equality
                                                                                (ext⁻¹ (sym (eq x y)))
                                                                                (_≃_.is-equivalence $ Eq.subst-as-equivalence _ _)
                                                                                ])) ⟩
  (∃ λ (get⁻¹ᴱ-const : ∀ b₁ b₂ → get ⁻¹ᴱ b₁ → get ⁻¹ᴱ b₂) →
   Erased (
   ∃ λ (c′ : C.Coherently-constant (get ⁻¹ᴱ_)) →
   ∀ b₁ b₂ → get⁻¹ᴱ-const b₁ b₂ ≡ subst P.id (c′ .property b₁ b₂)))       ↔⟨⟩

  CE.Coherently-constant (get ⁻¹ᴱ_)                                       □
  where
  @0 lemma₁ : ∀ _ _ _ → _ ≃ _
  lemma₁ bl c c′ =
    c′ ≡ _≃_.to (Constantᴱ-⁻¹ᴱ-≃-Constant-⁻¹ bl univ) c  ↝⟨ ≡⇒≃ $ cong (c′ ≡_) $
                                                            unblock bl
                                                              (λ bl → _≃_.to (Constantᴱ-⁻¹ᴱ-≃-Constant-⁻¹ bl univ) c ≡
                                                                      _≃_.from (S.Constant≃Constant-≃ univ)
                                                                        (_≃_.to Constantᴱ-⁻¹ᴱ-≃-Constant-≃-⁻¹ c))
                                                              (refl _) ⟩
    c′ ≡
    _≃_.from (S.Constant≃Constant-≃ univ)
      (_≃_.to Constantᴱ-⁻¹ᴱ-≃-Constant-≃-⁻¹ c)           ↝⟨ inverse $ Eq.≃-≡ (S.Constant≃Constant-≃ univ) ⟩

    _≃_.to (S.Constant≃Constant-≃ univ) c′ ≡
    _≃_.to (S.Constant≃Constant-≃ univ)
      (_≃_.from (S.Constant≃Constant-≃ univ)
         (_≃_.to Constantᴱ-⁻¹ᴱ-≃-Constant-≃-⁻¹ c))       ↝⟨ ≡⇒≃ $
                                                            cong (_≃_.to (S.Constant≃Constant-≃ univ) c′ ≡_) $
                                                            _≃_.right-inverse-of (S.Constant≃Constant-≃ univ) _ ⟩□
    _≃_.to (S.Constant≃Constant-≃ univ) c′ ≡
    _≃_.to Constantᴱ-⁻¹ᴱ-≃-Constant-≃-⁻¹ c               □

  @0 lemma₂ : ∀ _ _ _ _ → _
  lemma₂ bl c′ b₁ b₂ =
    proj₁ (_≃_.from (Constantᴱ-⁻¹ᴱ-≃-Constant-⁻¹ bl univ)
             (c′ .property) b₁ b₂)                                      ≡⟨ proj₁-from-Constantᴱ-⁻¹ᴱ-≃-Constant-⁻¹ bl ⟩

    ECP.⁻¹→⁻¹ᴱ ∘ subst P.id (c′ .property b₁ b₂) ∘ ECP.⁻¹ᴱ→⁻¹           ≡⟨ sym $
                                                                           cong₂ (λ f g → f ∘ subst P.id (c′ .property b₁ b₂) ∘ g)
                                                                             (trans (⟨ext⟩ λ _ →
                                                                                subst-id-in-terms-of-≡⇒↝ equivalence) $
                                                                              cong _≃_.to $ _≃_.right-inverse-of (≡≃≃ univ) _)
                                                                             (trans (⟨ext⟩ λ _ →
                                                                                subst-id-in-terms-of-inverse∘≡⇒↝ equivalence) $
                                                                              cong _≃_.from $ _≃_.right-inverse-of (≡≃≃ univ) _) ⟩
    subst P.id (≃⇒≡ univ ECP.⁻¹≃⁻¹ᴱ) ∘
    subst P.id (c′ .property b₁ b₂) ∘
    subst P.id (sym (≃⇒≡ univ ECP.⁻¹≃⁻¹ᴱ))                              ≡⟨ (⟨ext⟩ λ _ →
                                                                            trans (subst-subst _ _ _ _) $
                                                                            subst-subst _ _ _ _) ⟩
    subst P.id
      (trans (sym (≃⇒≡ univ (ECP.⁻¹≃⁻¹ᴱ {y = b₁})))
         (trans (c′ .property b₁ b₂)
           (≃⇒≡ univ (ECP.⁻¹≃⁻¹ᴱ {y = b₂}))))                           ≡⟨ sym $
                                                                           cong (λ f → subst P.id
                                                                                (trans (sym (f b₁))
                                                                                (trans (c′ .property b₁ b₂) (f b₂)))) $
                                                                           _≃_.left-inverse-of (Eq.extensionality-isomorphism bad-ext) _ ⟩
    subst P.id
      (trans (sym (cong (_$ b₁) $ ⟨ext⟩ λ _ → ≃⇒≡ univ ECP.⁻¹≃⁻¹ᴱ))
         (trans (c′ .property b₁ b₂)
           (cong (_$ b₂) $ ⟨ext⟩ λ b₂ →
            ≃⇒≡ univ (ECP.⁻¹≃⁻¹ᴱ {y = b₂}))))                           ≡⟨ cong (subst P.id) $
                                                                           elim¹
                                                                             (λ eq →
                                                                                trans (sym (cong (_$ b₁) eq))
                                                                                (trans (c′ .property b₁ b₂) (cong (_$ b₂) eq)) ≡
                                                                                ≡⇒→ (cong C.Coherently-constant eq) c′ .property b₁ b₂)
                                                                             (
        trans (sym (cong (_$ b₁) (refl _)))
          (trans (c′ .property b₁ b₂) (cong (_$ b₂) (refl (get ⁻¹_))))        ≡⟨ trans (cong (flip trans _) $
                                                                                trans (cong sym $ cong-refl _) $
                                                                                sym-refl) $
                                                                                trans (trans-reflˡ _) $
                                                                                trans (cong (trans _) $ cong-refl _) $
                                                                                trans-reflʳ _ ⟩

        c′ .property b₁ b₂                                                    ≡⟨ cong (λ eq → _≃_.to eq c′ .property b₁ b₂) $ sym $
                                                                                trans (cong ≡⇒≃ $ cong-refl C.Coherently-constant)
                                                                                ≡⇒↝-refl ⟩∎
        ≡⇒→ (cong C.Coherently-constant (refl _)) c′ .property b₁ b₂          ∎)
                                                                             _ ⟩∎
    subst P.id (≡⇒→ (cong C.Coherently-constant $
                     ⟨ext⟩ λ _ → ≃⇒≡ univ ECP.⁻¹≃⁻¹ᴱ)
                c′ .property b₁ b₂)                                     ∎

  @0 lemma₃ : ∀ _ _ → _ ≃ _
  lemma₃ bl c =
    (∃ λ (c′ : C.Coherently-constant (get ⁻¹_)) →
     c′ .property ≡ _≃_.to (Constantᴱ-⁻¹ᴱ-≃-Constant-⁻¹ bl univ) c)  ↝⟨ (∃-cong λ _ →
                                                                         (∀-cong ext λ _ → ∀-cong ext λ _ → from-bijection $ inverse $
                                                                          ≡-comm F.∘
                                                                          ignore-propositional-component
                                                                            (H-level-Erased 1 (Eq.propositional ext _))) F.∘
                                                                         inverse
                                                                           (Eq.extensionality-isomorphism bad-ext F.∘
                                                                            (∀-cong ext λ _ → Eq.extensionality-isomorphism bad-ext)) F.∘
                                                                         (≡⇒≃ $ cong (_ ≡_) $
                                                                          _≃_.left-inverse-of (Constantᴱ-⁻¹ᴱ-≃-Constant-⁻¹ bl univ) _) F.∘
                                                                         (inverse $
                                                                          Eq.≃-≡ $ inverse $ Constantᴱ-⁻¹ᴱ-≃-Constant-⁻¹ bl univ)) ⟩
    (∃ λ (c′ : C.Coherently-constant (get ⁻¹_)) →
     ∀ b₁ b₂ →
     proj₁ (c b₁ b₂) ≡
     proj₁ (_≃_.from (Constantᴱ-⁻¹ᴱ-≃-Constant-⁻¹ bl univ)
              (c′ .property) b₁ b₂))                                 ↝⟨ (Σ-cong (≡⇒≃ $ cong C.Coherently-constant $ ⟨ext⟩ λ _ →
                                                                                ≃⇒≡ univ ECP.⁻¹≃⁻¹ᴱ) λ c′ →
                                                                         ∀-cong ext λ b₁ → ∀-cong ext λ b₂ →
                                                                         ≡⇒≃ $ cong (proj₁ (c b₁ b₂) ≡_) (lemma₂ bl c′ b₁ b₂)) ⟩□
    (∃ λ (c′ : C.Coherently-constant (get ⁻¹ᴱ_)) →
     ∀ b₁ b₂ → proj₁ (c b₁ b₂) ≡ subst P.id (c′ .property b₁ b₂))    □

-- In erased contexts Coherently-constant-fibres univ get is
-- equivalent to S.Coherently-constant univ (get ⁻¹_).

@0 Coherently-constant-fibres≃Coherently-constant-⁻¹ :
  (bl : Block "Constant-≃-get-⁻¹-≃")
  {A : Type a} {B : Type b} {get : A → B} →
  (univ : Univalence (a ⊔ b)) →
  Coherently-constant-fibres univ get ≃
  S.Coherently-constant univ (get ⁻¹_)
Coherently-constant-fibres≃Coherently-constant-⁻¹
  bl {A = A} {B = B} {get = get} univ =
  Coherently-constant-fibres univ get                               ↔⟨⟩

  (∃ λ (set : A → B → A) →
   Erased
     (∃ λ (c : S.Coherently-constant univ (get ⁻¹_)) →
      set ≡
      S.Lens.set {univ = univ}
        (record { get⁻¹-coherently-constant = c })))                ↔⟨ (∃-cong λ _ → erased Erased↔) ⟩

  (∃ λ (set : A → B → A) →
   ∃ λ (c : S.Coherently-constant univ (get ⁻¹_)) →
   set ≡
   S.Lens.set {univ = univ}
     (record { get⁻¹-coherently-constant = c }))                    ↔⟨ ∃-comm ⟩

  (∃ λ (c : S.Coherently-constant univ (get ⁻¹_)) →
   ∃ λ (set : A → B → A) →
   set ≡
   S.Lens.set {univ = univ}
     (record { get⁻¹-coherently-constant = c }))                    ↔⟨ (drop-⊤-right λ _ →
                                                                        _⇔_.to contractible⇔↔⊤ $
                                                                        singleton-contractible _) ⟩□
  S.Coherently-constant univ (get ⁻¹_)                              □

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

-- Small coinductive lenses.
--
-- The lens type is defined using (erased) univalence. The use of a
-- record type makes it easier for Agda to infer the argument univ
-- from a value of type Lens univ A B.
--
-- Note that everything is erased, except for the getter and the
-- setter.

record Lens (@0 univ : Univalence (a ⊔ b))
            (A : Type a) (B : Type b) : Type (a ⊔ b) where
  field

    -- A getter.

    get : A → B

    -- A setter.

    set : A → B → A

    -- The family get ⁻¹_ is coherently constant (in erased contexts).

    @0 get⁻¹-coherently-constant : S.Coherently-constant univ (get ⁻¹_)

  -- Using get and get⁻¹-coherently-constant we can construct an
  -- erased lens.

  @0 erased-lens : S.Lens univ A B
  erased-lens = record
    { get                       = get
    ; get⁻¹-coherently-constant = get⁻¹-coherently-constant
    }

  field

    -- The setter that we get from this lens is equal to set.

    @0 set≡set : set ≡ S.Lens.set erased-lens

  -- The family of fibres of the getter is coherently constant.

  coherently-constant-fibres-get : Coherently-constant-fibres univ get
  coherently-constant-fibres-get =
    set , [ (get⁻¹-coherently-constant , set≡set) ]

instance

  -- The lenses defined above have getters and setters.

  has-getter-and-setter :
    {@0 univ : Univalence (a ⊔ b)} →
    Has-getter-and-setter (Lens {a = a} {b = b} univ)
  has-getter-and-setter = record
    { get = Lens.get
    ; set = Lens.set
    }

-- Lens can be expressed as a Σ-type.

Lens-as-Σ :
  {A : Type a} {B : Type b} {@0 univ : Univalence (a ⊔ b)} →
  Lens univ A B ≃
  ∃ λ (get : A → B) → Coherently-constant-fibres univ get
Lens-as-Σ =
  Eq.↔→≃
    (λ l → Lens.get l , Lens.coherently-constant-fibres-get l)
    _ refl refl

-- Lens univ A B is equivalent to CE.Lens A B (with erased proofs,
-- assuming univalence).

Lens≃ᴱLens :
  Block "Lens≃ᴱLens" →
  {A : Type a} {B : Type b} →
  @0 Univalence (lsuc (a ⊔ b)) →
  (@0 univ : Univalence (a ⊔ b)) →
  Lens univ A B ≃ᴱ CE.Lens A B
Lens≃ᴱLens ⊠ {A = A} {B = B} univ′ univ =
  Lens univ A B                                              ↔⟨ Lens-as-Σ ⟩
  (∃ λ (get : A → B) → Coherently-constant-fibres univ get)  ↝⟨ (∃-cong λ _ →
                                                                 Coherently-constant-fibres≃ᴱCoherently-constant-⁻¹ᴱ univ′ univ) ⟩□
  (∃ λ (get : A → B) → CE.Coherently-constant (get ⁻¹ᴱ_))    □

-- The equivalence preserves getters and setters.

Lens≃ᴱLens-preserves-getters-and-setters :
  (bl : Block "Lens≃ᴱLens")
  {A : Type a} {B : Type b}
  (@0 univ′ : Univalence (lsuc (a ⊔ b)))
  (@0 univ : Univalence (a ⊔ b)) →
  Preserves-getters-and-setters-⇔ A B
    (_≃ᴱ_.logical-equivalence (Lens≃ᴱLens bl univ′ univ))
Lens≃ᴱLens-preserves-getters-and-setters ⊠ univ′ univ =
    (λ _ → refl _ , refl _)
  , (λ l →
       let open CE.Lens l in
         refl _
       , ⟨ext⟩ λ a → ⟨ext⟩ λ b →
         proj₁
           (subst (λ _ → get ⁻¹ᴱ b) (refl tt)
              (get⁻¹ᴱ-const (get a) b (a , [ refl (get a) ])))  ≡⟨ cong proj₁ $ subst-refl _ _ ⟩∎

         proj₁ (get⁻¹ᴱ-const (get a) b (a , [ refl (get a) ]))  ∎)

-- Lens univ A B is equivalent to E.Lens A B (with erased proofs,
-- assuming univalence).

Lens≃ᴱLensᴱ :
  Block "Lens≃ᴱLensᴱ" →
  {A : Type a} {B : Type b}
  {@0 univ : Univalence (a ⊔ b)} →
  @0 Univalence (lsuc (a ⊔ b)) →
  Lens univ A B ≃ᴱ E.Lens A B
Lens≃ᴱLensᴱ bl {A = A} {B = B} {univ = univ} univ′ =
  Lens univ A B  ↝⟨ Lens≃ᴱLens bl univ′ univ ⟩
  CE.Lens A B    ↝⟨ CE.Lens≃ᴱLens bl univ′ univ ⟩
  V.Lens A B     ↝⟨ V.Lens≃ᴱHigher-lens bl univ ⟩□
  E.Lens A B     □

-- The equivalence preserves getters and setters (in erased contexts).

@0 Lens≃ᴱLensᴱ-preserves-getters-and-setters :
  (bl : Block "Lens→Lens")
  {A : Type a} {B : Type b}
  (@0 univ′ : Univalence (lsuc (a ⊔ b)))
  (@0 univ : Univalence (a ⊔ b)) →
  Preserves-getters-and-setters-⇔ A B
    (_≃ᴱ_.logical-equivalence (Lens≃ᴱLensᴱ bl {univ = univ} univ′))
Lens≃ᴱLensᴱ-preserves-getters-and-setters bl univ′ univ =
  Preserves-getters-and-setters-⇔-∘
    {f = _≃ᴱ_.logical-equivalence (V.Lens≃ᴱHigher-lens bl univ) F.∘
         _≃ᴱ_.logical-equivalence (CE.Lens≃ᴱLens bl univ′ univ)}
    {g = _≃ᴱ_.logical-equivalence (Lens≃ᴱLens bl univ′ univ)}
    (Preserves-getters-and-setters-⇔-∘
       {f = _≃ᴱ_.logical-equivalence (V.Lens≃ᴱHigher-lens bl univ)}
       {g = _≃ᴱ_.logical-equivalence (CE.Lens≃ᴱLens bl univ′ univ)}
       (V.Lens≃ᴱHigher-lens-preserves-getters-and-setters bl univ)
       (CE.Lens≃ᴱLens-preserves-getters-and-setters bl univ′ univ))
    (Lens≃ᴱLens-preserves-getters-and-setters bl univ′ univ)

-- In erased contexts Lens univ A B is equivalent to S.Lens univ A B.

@0 Lens≃Lens :
  (bl : Block "Constant-≃-get-⁻¹-≃") →
  Lens univ A B ≃ S.Lens univ A B
Lens≃Lens {univ = univ} {A = A} {B = B} bl =
  Lens univ A B                                               ↝⟨ Lens-as-Σ ⟩
  (∃ λ (get : A → B) → Coherently-constant-fibres univ get)   ↝⟨ (∃-cong λ _ → Coherently-constant-fibres≃Coherently-constant-⁻¹ bl univ) ⟩
  (∃ λ (get : A → B) → S.Coherently-constant univ (get ⁻¹_))  ↝⟨ inverse S.Lens-as-Σ ⟩□
  S.Lens univ A B                                             □

-- Lens≃Lens preserves getters and setters.

@0 Lens≃Lens-preserves-getters-and-setters :
  (bl : Block "Lens≃Lens")
  {A : Type a} {B : Type b}
  {univ : Univalence (a ⊔ b)} →
  Preserves-getters-and-setters-⇔ A B
    (_≃_.logical-equivalence (Lens≃Lens {univ = univ} bl))
Lens≃Lens-preserves-getters-and-setters ⊠ =
    (λ l →
       let open Lens l in
         refl _
       , (S.Lens.set erased-lens  ≡⟨ sym set≡set ⟩∎
          set                     ∎))
  , (λ _ → refl _ , refl _)

-- Lenses with stable view types are equal if their setters are equal
-- (in erased contexts, assuming univalence).

@0 lenses-equal-if-setters-equal :
  {A : Type a} {B : Type b} →
  Univalence (lsuc (a ⊔ b)) →
  (univ : Univalence (a ⊔ b)) →
  (l₁ l₂ : Lens univ A B) →
  (∥ B ∥ → B) →
  Lens.set l₁ ≡ Lens.set l₂ →
  l₁ ≡ l₂
lenses-equal-if-setters-equal univ′ univ l₁ l₂ stable =
  block λ bl →

  Lens.set l₁ ≡ Lens.set l₂                            ↔⟨ ≡⇒≃ $ sym $ cong₂ _≡_
                                                            (proj₂ $ proj₁ (Lens≃Lens-preserves-getters-and-setters bl) l₁)
                                                            (proj₂ $ proj₁ (Lens≃Lens-preserves-getters-and-setters bl) l₂) ⟩
  S.Lens.set (_≃_.to (Lens≃Lens bl) l₁) ≡
  S.Lens.set (_≃_.to (Lens≃Lens bl) l₂)                ↝⟨ S.lenses-equal-if-setters-equal univ′ _ _ _ stable ⟩

  _≃_.to (Lens≃Lens bl) l₁ ≡ _≃_.to (Lens≃Lens bl) l₂  ↔⟨ Eq.≃-≡ $ Lens≃Lens bl ⟩□

  l₁ ≡ l₂                                              □

------------------------------------------------------------------------
-- Changing the implementation of the getter and the setter

-- One can change the getter of a lens, provided that the new
-- implementation is extensionally equal to the old one.

with-other-getter :
  {A : Type a} {B : Type b}
  (@0 univ : Univalence (a ⊔ b))
  (l : Lens univ A B)
  (get : A → B) →
  @0 get ≡ Lens.get l →
  Lens univ A B
with-other-getter {A = A} {B = B} univ l get p = record l
  { get                       = get
  ; get⁻¹-coherently-constant =
      subst (S.Coherently-constant univ ∘ _⁻¹_)
        (sym p) L.get⁻¹-coherently-constant
  ; set≡set =
      L.set          ≡⟨ L.set≡set ⟩
      S.Lens.set l₁  ≡⟨ cong S.Lens.set $ sym l₂≡l₁ ⟩∎
      S.Lens.set l₂  ∎
  }
  where
  module L = Lens l

  @0 l₁ l₂ : S.Lens univ A B

  l₁ = record
    { get                       = L.get
    ; get⁻¹-coherently-constant = L.get⁻¹-coherently-constant
    }

  l₂ = record
    { get                       = get
    ; get⁻¹-coherently-constant =
        subst (S.Coherently-constant univ ∘ _⁻¹_) (sym p)
          L.get⁻¹-coherently-constant
    }

  @0 l₂≡l₁ : l₂ ≡ l₁
  l₂≡l₁ =
    _≃_.to (Eq.≃-≡ S.Lens-as-Σ) $ Σ-≡,≡→≡ p
      (subst (S.Coherently-constant univ ∘ _⁻¹_) p
         (subst (S.Coherently-constant univ ∘ _⁻¹_) (sym p)
            L.get⁻¹-coherently-constant)                     ≡⟨ subst-subst-sym _ _ _ ⟩∎

       L.get⁻¹-coherently-constant                           ∎)

_ : Lens.get (with-other-getter univ l g p) ≡ g
_ = refl _

_ : Lens.set (with-other-getter univ l g p) ≡ Lens.set l
_ = refl _

-- The resulting lens is equal to the old one (if the equality proof
-- is not erased).

with-other-getter≡ :
  {A : Type a} {B : Type b}
  (@0 univ : Univalence (a ⊔ b))
  (l : Lens univ A B)
  (get : A → B)
  (p : get ≡ Lens.get l) →
  with-other-getter univ l get p ≡ l
with-other-getter≡ {A = A} {B = B} univ l get p =
  _≃_.to (Eq.≃-≡ Lens-as-Σ) $ Σ-≡,≡→≡ p
    (subst (Coherently-constant-fibres univ) p
       L′.coherently-constant-fibres-get                             ≡⟨ push-subst-pair-× _ _ ⟩

     L.set ,
     subst
       (λ get →
          Erased
            (∃ λ (c : S.Coherently-constant univ (get ⁻¹_)) →
             L.set ≡
             S.Lens.set {univ = univ}
               (record { get⁻¹-coherently-constant = c })))
       p
       [ (L′.get⁻¹-coherently-constant , L′.set≡set) ]               ≡⟨ cong (L.set ,_) push-subst-[] ⟩

     L.set ,
     [ subst
         (λ get →
            ∃ λ (c : S.Coherently-constant univ (get ⁻¹_)) →
            L.set ≡
            S.Lens.set {univ = univ}
              (record { get⁻¹-coherently-constant = c }))
         p
         (L′.get⁻¹-coherently-constant , L′.set≡set)
     ]                                                               ≡⟨ cong (L.set ,_) $ []-cong [ push-subst-pair′ _ _ _ ] ⟩

     L.set ,
     [ ( L.get⁻¹-coherently-constant
       , subst
           (λ ((get , c) : ∃ (S.Coherently-constant univ ∘ _⁻¹_)) →
              L.set ≡
              S.Lens.set {univ = univ}
                (record { get⁻¹-coherently-constant = c }))
           (Σ-≡,≡→≡ p (subst-subst-sym _ _ _))
           L′.set≡set
       )
     ]                                                               ≡⟨⟩

     L.set ,
     [ ( L.get⁻¹-coherently-constant
       , let q = Σ-≡,≡→≡ {p₂ = _ , L.get⁻¹-coherently-constant}
                   p
                   (subst-subst-sym _ _ _)
         in
         subst
           (λ ((get , c) : ∃ (S.Coherently-constant univ ∘ _⁻¹_)) →
              L.set ≡
              S.Lens.set {univ = univ}
                (record { get⁻¹-coherently-constant = c }))
           q
           (trans L.set≡set
              (cong (S.Lens.set {univ = univ}) $ sym $
               _≃_.to (Eq.≃-≡ S.Lens-as-Σ) q))
       )
     ]                                                               ≡⟨ cong (L.set ,_) $ []-cong
                                                                        [ cong (L.get⁻¹-coherently-constant ,_) $
                                                                          elim₁
                                                                            (λ q →
                                                                               subst
                                                                                (λ ((get , c) : ∃ (S.Coherently-constant univ ∘ _⁻¹_)) →
                                                                                L.set ≡
                                                                                S.Lens.set {univ = univ}
                                                                                (record { get⁻¹-coherently-constant = c }))
                                                                                q
                                                                                (trans L.set≡set
                                                                                (cong (S.Lens.set {univ = univ}) $ sym $
                                                                                _≃_.to (Eq.≃-≡ S.Lens-as-Σ) q)) ≡
                                                                               L.set≡set)
                                                                            (trans (subst-refl _ _) $
                                                                             trans (cong (trans _) $
                                                                                trans (cong (cong _) $
                                                                                trans (cong sym (Eq.to-≃-≡-refl S.Lens-as-Σ))
                                                                                sym-refl) $
                                                                                cong-refl _) $
                                                                             trans-reflʳ _)
                                                                            _
                                                                        ] ⟩
     L.set , [ (L.get⁻¹-coherently-constant , L.set≡set) ]           ≡⟨⟩

     L.coherently-constant-fibres-get                                ∎)
  where
  module L = Lens l

  l′ : Lens univ A B
  l′ = record
    { get                       = get
    ; get⁻¹-coherently-constant =
        subst (S.Coherently-constant univ ∘ _⁻¹_) (sym p)
          L.get⁻¹-coherently-constant
    }

  module L′ = Lens l′

-- One can change the setter of a lens, provided that the new
-- implementation is extensionally equal to the old one.

with-other-setter :
  {A : Type a} {B : Type b}
  {@0 univ : Univalence (a ⊔ b)}
  (l : Lens univ A B)
  (set : A → B → A) →
  @0 set ≡ Lens.set l →
  Lens univ A B
with-other-setter l set p = record l
  { set     = set
  ; set≡set = trans p (Lens.set≡set l)
  }

_ : Lens.get (with-other-setter l s p) ≡ Lens.get l
_ = refl _

_ : Lens.set (with-other-setter l s p) ≡ s
_ = refl _

-- The resulting lens is equal to the old one (if the equality proof
-- is not erased).

with-other-setter≡ :
  {A : Type a} {B : Type b}
  {@0 univ : Univalence (a ⊔ b)}
  (l : Lens univ A B)
  (set : A → B → A)
  (p : set ≡ Lens.set l) →
  with-other-setter l set p ≡ l
with-other-setter≡ {univ = univ} l set p =
  _≃_.to (Eq.≃-≡ Lens-as-Σ) $ cong (get ,_) $ Σ-≡,≡→≡ p
    (subst
       (λ set → Erased
                  (∃ λ (c : S.Coherently-constant univ (get ⁻¹_)) →
                   set ≡
                   S.Lens.set {univ = univ}
                     (record { get⁻¹-coherently-constant = c })))
       p
       [ (get⁻¹-coherently-constant , trans p set≡set) ]             ≡⟨ push-subst-[] ⟩

     [ subst
         (λ set → ∃ λ (c : S.Coherently-constant univ (get ⁻¹_)) →
                  set ≡
                  S.Lens.set {univ = univ}
                    (record { get⁻¹-coherently-constant = c }))
         p
         (get⁻¹-coherently-constant , trans p set≡set)
     ]                                                               ≡⟨ []-cong [ push-subst-pair-× _ _ ] ⟩

     [ ( get⁻¹-coherently-constant
       , subst (_≡ S.Lens.set {univ = univ}
                     (record { get⁻¹-coherently-constant =
                                 get⁻¹-coherently-constant }))
           p
           (trans p set≡set)
       )
     ]                                                               ≡⟨ []-cong [ cong (_ ,_) subst-trans-sym ] ⟩

     [ ( get⁻¹-coherently-constant
       , trans (sym p) (trans p set≡set)
       )
     ]                                                               ≡⟨ []-cong [ cong (_ ,_) $ trans-sym-[trans] _ _ ] ⟩∎

     [ (get⁻¹-coherently-constant , set≡set) ]                       ∎)
  where
  open Lens l

------------------------------------------------------------------------
-- Code for converting from S.Lens to Lens

-- Data corresponding to the erased proofs of a lens.

record Erased-proofs
         {A : Type a} {B : Type b}
         (univ : Univalence (a ⊔ b))
         (get : A → B) (set : A → B → A) : Type (a ⊔ b) where
  field
    @0 get⁻¹-coherently-constant : S.Coherently-constant univ (get ⁻¹_)

  @0 erased-lens : S.Lens univ A B
  erased-lens = record
    { get                       = get
    ; get⁻¹-coherently-constant = get⁻¹-coherently-constant
    }

  field
    @0 set≡set : set ≡ S.Lens.set erased-lens

-- Extracts "erased proofs" from a lens (in erased contexts).

@0 Lens→Erased-proofs :
  (l : S.Lens univ A B) →
  Erased-proofs univ (S.Lens.get l) (S.Lens.set l)
Lens→Erased-proofs {univ = univ} l = proofs ⊠
  where
  module _ (bl : Unit) where

    open Erased-proofs

    l′ = _≃_.from (Lens≃Lens bl) l

    proofs : Erased-proofs univ (Lens.get l′) (Lens.set l′)
    proofs .get⁻¹-coherently-constant =
      Lens.get⁻¹-coherently-constant l′
    proofs .set≡set = Lens.set≡set l′

-- Converts two functions and some erased proofs to a lens.
--
-- Note that Agda can in many cases infer "get" and "set" from the
-- first explicit argument, see (for instance) id below.

Erased-proofs→Lens :
  {A : Type a} {B : Type b} {get : A → B} {set : A → B → A}
  {@0 univ : Univalence (a ⊔ b)} →
  @0 Erased-proofs univ get set →
  Lens univ A B
Erased-proofs→Lens {get = get} {set = set} ep = λ where
  .Lens.get                       → get
  .Lens.set                       → set
  .Lens.get⁻¹-coherently-constant →
    Erased-proofs.get⁻¹-coherently-constant ep
  .Lens.set≡set → Erased-proofs.set≡set ep

------------------------------------------------------------------------
-- Identity and composition

-- An identity lens.

id :
  {A : Type a}
  (@0 univ : Univalence a) →
  Lens univ A A
id univ = Erased-proofs→Lens (Lens→Erased-proofs (S.id univ))

-- Composition.

infix 9 ⟨_,_⟩_∘_

⟨_,_⟩_∘_ :
  {A : Type a} {B : Type b} {C : Type c}
  {@0 univ₁ : Univalence (b ⊔ c)}
  {@0 univ₂ : Univalence (a ⊔ b)}
  (@0 univ₃ : Univalence (a ⊔ c)) →
  @0 Univalence (a ⊔ b ⊔ c) →
  Lens univ₁ B C → Lens univ₂ A B → Lens univ₃ A C
⟨ univ₃ , univ ⟩ l₁ ∘ l₂ =
  Erased-proofs→Lens
    (subst (Erased-proofs _ _)
       (⟨ext⟩ λ a → ⟨ext⟩ λ c →
        S.Lens.set l₂′ a (S.Lens.set l₁′ (get l₂ a) c)  ≡⟨ cong (λ s → s a (S.Lens.set l₁′ (get l₂ a) c)) $
                                                           proj₂ $ proj₁ (Lens≃Lens-preserves-getters-and-setters ⊠) l₂ ⟩
        set l₂ a (S.Lens.set l₁′ (get l₂ a) c)          ≡⟨ cong (λ s → set l₂ a (s (get l₂ a) c)) $
                                                           proj₂ $ proj₁ (Lens≃Lens-preserves-getters-and-setters ⊠) l₁ ⟩∎
        set l₂ a (set l₁ (get l₂ a) c)                  ∎) $
     Lens→Erased-proofs (S.⟨ univ₃ , univ ⟩ l₁′ ∘ l₂′))
  where
  open Lens

  @0 l₁′ : _
  l₁′ = _≃_.to (Lens≃Lens ⊠) l₁

  @0 l₂′ : _
  l₂′ = _≃_.to (Lens≃Lens ⊠) l₂

-- The setter of a lens formed using composition is defined in the
-- "right" way.

set-∘ :
  ∀ {A : Type a} {B : Type b} {C : Type c}
    {@0 univ₁ : Univalence (b ⊔ c)}
    {@0 univ₂ : Univalence (a ⊔ b)}
  (@0 univ₃ : Univalence (a ⊔ c))
  (@0 univ₄ : Univalence (a ⊔ b ⊔ c))
  (l₁ : Lens univ₁ B C) (l₂ : Lens univ₂ A B) {a c} →
  Lens.set (⟨ univ₃ , univ₄ ⟩ l₁ ∘ l₂) a c ≡
  Lens.set l₂ a (Lens.set l₁ (Lens.get l₂ a) c)
set-∘ _ _ _ _ = refl _

-- Composition is associative if the view type of the resulting lens
-- is stable (in erased contexts, assuming univalence).

@0 associativity :
  {A : Type a} {B : Type b} {C : Type c} {D : Type d} →
  (∥ D ∥ → D) →
  (univ₁  : Univalence (c ⊔ d))
  (univ₂  : Univalence (b ⊔ c))
  (univ₃  : Univalence (a ⊔ b))
  (univ₄  : Univalence (a ⊔ d))
  (univ₅  : Univalence (a ⊔ c ⊔ d))
  (univ₆  : Univalence (a ⊔ c))
  (univ₇  : Univalence (a ⊔ b ⊔ c))
  (univ₈  : Univalence (a ⊔ b ⊔ d))
  (univ₉  : Univalence (b ⊔ d))
  (univ₁₀ : Univalence (b ⊔ c ⊔ d)) →
  Univalence (lsuc (a ⊔ d)) →
  (l₁ : Lens univ₁ C D) (l₂ : Lens univ₂ B C) (l₃ : Lens univ₃ A B) →
  ⟨ univ₄ , univ₅ ⟩ l₁ ∘ (⟨ univ₆ , univ₇ ⟩ l₂ ∘ l₃) ≡
  ⟨ univ₄ , univ₈ ⟩ (⟨ univ₉ , univ₁₀ ⟩ l₁ ∘ l₂) ∘ l₃
associativity stable _ _ _ univ₄ _ _ _ _ _ _ univ₁₁ l₁ l₂ l₃ =
  lenses-equal-if-setters-equal
    univ₁₁
    univ₄
    _
    _
    stable
    (refl _)

-- The identity lens is a left identity of composition if the view
-- type of the resulting lens is stable (assuming univalence).

@0 left-identity :
  {A : Type a} {B : Type b} →
  (∥ B ∥ → B) →
  (univ₁ : Univalence (a ⊔ b))
  (univ₂ : Univalence (a ⊔ b))
  (univ₃ : Univalence b) →
  Univalence (lsuc (a ⊔ b)) →
  (l : Lens univ₁ A B) →
  ⟨ univ₁ , univ₂ ⟩ id univ₃ ∘ l ≡ l
left-identity stable univ₁ univ₂ univ₃ univ₄ l =
  lenses-equal-if-setters-equal
    univ₄
    univ₁
    _
    _
    stable
    (refl _)

-- The identity lens is a right identity of composition if the view
-- type of the resulting lens is stable (assuming univalence).

@0 right-identity :
  {A : Type a} {B : Type b} →
  (∥ B ∥ → B) →
  (univ₁ : Univalence (a ⊔ b))
  (univ₂ : Univalence (a ⊔ b))
  (univ₃ : Univalence a) →
  Univalence (lsuc (a ⊔ b)) →
  (l : Lens univ₁ A B) →
  ⟨ univ₁ , univ₂ ⟩ l ∘ id univ₃ ≡ l
right-identity stable univ₁ univ₂ univ₃ univ₄ l =
  lenses-equal-if-setters-equal
    univ₄
    univ₁
    _
    _
    stable
    (refl _)

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


text:
module perm-keep-length where

open import nat
open import list
open import nondet
open import bool
open import bool-thms
open import eq
open import nat-thms
open import nondet-thms

-- Non-deterministic insert:
ndinsert : {a : Set} → a → 𝕃 a  → ND (𝕃 a)
ndinsert x []        = Val (x :: [])
ndinsert x (y :: ys) = Val (x :: y :: ys)
                    ?? (_::_ y) $* (ndinsert x ys)

-- Permutation:
perm : {a : Set} → 𝕃 a  → ND (𝕃 a)
perm []        = Val []
perm (x :: xs) = ndinsert x *$* (perm xs)

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

-- Non-deterministic insertion increases the list length by one:
insert-inc-length : {a : Set} (x : a) → (xs : 𝕃 a)
      → (ndinsert x xs) satisfy (λ ys → length ys =ℕ suc (length xs)) ≡ tt
insert-inc-length x [] = refl
insert-inc-length x (y :: ys)
 rewrite =ℕ-refl (length ys)
       | satisfy-$* (_::_ y) (ndinsert x ys)
                    (λ zs → length zs =ℕ suc (suc (length ys)))
       | insert-inc-length x ys = refl

-- If the length of the input list is n, ndinsert increases it to (suc n):
insert-suc-length : {a : Set} → (n : ℕ) (x : a) (xs : 𝕃 a)
       → length xs =ℕ n ≡ tt
       → ndinsert x xs satisfy (λ ys → length ys =ℕ suc n) ≡ tt
insert-suc-length n x [] p = p
insert-suc-length n x (y :: ys) p
 rewrite =ℕ-to-≡ {suc (length ys)} {n} p | =ℕ-refl n |
         satisfy-$* (_::_ y) (ndinsert x ys) (λ zs → length zs =ℕ suc n)
       | sym (=ℕ-to-≡ {suc (length ys)} {n} p)
       | insert-inc-length x ys
 = refl

-- The previous lemma is also valid on non-deterministic lists:
ins-suc-nondet : {a : Set} → (n : ℕ) → (x : a) → (t : ND (𝕃 a))
       → t satisfy (λ xs → length xs =ℕ n) ≡ tt
       → (ndinsert x *$* t) satisfy (λ xs → length xs =ℕ suc n) ≡ tt
ins-suc-nondet n x (Val xs) p = insert-suc-length n x xs p
ins-suc-nondet n x (t1 ?? t2) p
 rewrite ins-suc-nondet n x t1 (&&-fst p)
       | ins-suc-nondet n x t2 (&&-snd {t1 satisfy (λ xs → length xs =ℕ n)} p)
 = refl

-- The length of a permuted list is identical to the length of the list:
perm-length : {a : Set} → (xs : 𝕃 a)
       → (perm xs) satisfy (λ ys → length ys =ℕ length xs) ≡ tt
perm-length [] = refl
perm-length (x :: xs) = ins-suc-nondet (length xs) x (perm xs) (perm-length xs)

max_stars_repo_name: mihanus/curry-agda

max_issues_repo_name: mihanus/curry-agda

max_forks_repo_name: mihanus/curry-agda