text:
------------------------------------------------------------------------
-- Lenses defined in terms of a getter, equivalences between the
-- getter's "preimages", and a coherence property
------------------------------------------------------------------------

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

import Equality.Path as P

module Lens.Non-dependent.Equivalent-preimages
  {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 renaming (_∘_ to _⊚_)

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

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

private
  variable
    ℓ       : Level
    A B C   : Set ℓ
    a b c z : A

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

-- Lenses defined in terms of a getter, equivalences between the
-- getter's "preimages", and a coherence property.
--
-- This definition is based on a suggestion from Andrea Vezzosi. Note
-- that the fields and some derived properties correspond to things
-- discussed by Paolo Capriotti in the context of his higher lenses
-- (http://homotopytypetheory.org/2014/04/29/higher-lenses/).

record Lens (A : Set a) (B : Set b) : Set (a ⊔ b) where
  no-eta-equality
  pattern
  constructor lens
  field
    -- A getter.
    get : A → B

    -- A function from one "preimage" of get to another.
    get⁻¹-const : (b₁ b₂ : B) → get ⁻¹ b₁ → get ⁻¹ b₂

    -- This function is an equivalence.
    get⁻¹-const-equivalence :
      (b₁ b₂ : B) → Is-equivalence (get⁻¹-const b₁ b₂)

    -- A coherence property.
    get⁻¹-const-∘ :
      (b₁ b₂ b₃ : B) (p : get ⁻¹ b₁) →
      get⁻¹-const b₂ b₃ (get⁻¹-const b₁ b₂ p) ≡ get⁻¹-const b₁ b₃ p

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

  get⁻¹-constant : (b₁ b₂ : B) → get ⁻¹ b₁ ≃ get ⁻¹ b₂
  get⁻¹-constant b₁ b₂ = Eq.⟨ _ , get⁻¹-const-equivalence b₁ b₂ ⟩

  -- The inverse of get⁻¹-const.

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

  -- Some derived coherence properties.

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

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

  -- A setter.

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

  -- The lens laws can be proved.

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

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

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

    proj₁ (get⁻¹-const b₁ b₂ (set a b₁ , get-set a b₁))          ≡⟨⟩

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

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

  -- A traditional lens.

  traditional-lens : Traditional.Lens A B
  traditional-lens = record
    { get     = get
    ; set     = set
    ; get-set = get-set
    ; set-get = set-get
    ; set-set = set-set
    }

instance

  -- The lenses defined above have getters and setters.

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

-- The record type above is equivalent to a nested Σ-type.

Lens-as-Σ :
  Lens A B ≃
  ∃ λ (get : A → B) →
  ∃ λ (get⁻¹-const : (b₁ b₂ : B) → get ⁻¹ b₁ → get ⁻¹ b₂) →
    ((b₁ b₂ : B) → Is-equivalence (get⁻¹-const b₁ b₂)) ×
    ((b₁ b₂ b₃ : B) (p : get ⁻¹ b₁) →
     get⁻¹-const b₂ b₃ (get⁻¹-const b₁ b₂ p) ≡ get⁻¹-const b₁ b₃ p)
Lens-as-Σ = Eq.↔→≃
  (λ l → get l
       , get⁻¹-const l
       , get⁻¹-const-equivalence l
       , get⁻¹-const-∘ l)
  (λ (g , c , c-e , c-∘) → record
     { get                     = g
     ; get⁻¹-const             = c
     ; get⁻¹-const-equivalence = c-e
     ; get⁻¹-const-∘           = c-∘
     })
  refl
  (λ { (lens _ _ _ _) → refl _ })
  where
  open Lens

-- A variant of Lens-as-Σ.

Lens-as-Σ′ :
  Lens A B ≃
  ∃ λ (get : A → B) →
  ∃ λ (get⁻¹-constant : (b₁ b₂ : B) → get ⁻¹ b₁ ≃ get ⁻¹ b₂) →
    let get⁻¹-const : ∀ _ _ → _
        get⁻¹-const = λ b₁ b₂ → _≃_.to (get⁻¹-constant b₁ b₂) in
    (b₁ b₂ b₃ : B) (p : get ⁻¹ b₁) →
    get⁻¹-const b₂ b₃ (get⁻¹-const b₁ b₂ p) ≡ get⁻¹-const b₁ b₃ p
Lens-as-Σ′ {A = A} {B = B} =
  Lens A B                                                             ↝⟨ Lens-as-Σ ⟩

  (∃ λ (get : A → B) →
   ∃ λ (get⁻¹-const : (b₁ b₂ : B) → get ⁻¹ b₁ → get ⁻¹ b₂) →
     ((b₁ b₂ : B) → Is-equivalence (get⁻¹-const b₁ b₂)) ×
     ((b₁ b₂ b₃ : B) (p : get ⁻¹ b₁) →
      get⁻¹-const b₂ b₃ (get⁻¹-const b₁ b₂ p) ≡ get⁻¹-const b₁ b₃ p))  ↔⟨ (∃-cong λ _ → Σ-assoc) ⟩

  (∃ λ (get : A → B) →
   ∃ λ ((get⁻¹-const , _) :
        ∃ λ (get⁻¹-const : (b₁ b₂ : B) → get ⁻¹ b₁ → get ⁻¹ b₂) →
          (b₁ b₂ : B) → Is-equivalence (get⁻¹-const b₁ b₂)) →
     (b₁ b₂ b₃ : B) (p : get ⁻¹ b₁) →
     get⁻¹-const b₂ b₃ (get⁻¹-const b₁ b₂ p) ≡ get⁻¹-const b₁ b₃ p)    ↝⟨ (∃-cong λ _ →
                                                                           Σ-cong-contra (ΠΣ-comm F.∘ ∀-cong ext (λ _ → ΠΣ-comm)) λ _ → F.id) ⟩
  (∃ λ (get : A → B) →
   ∃ λ (f :
        (b₁ b₂ : B) →
        ∃ λ (get⁻¹-const : get ⁻¹ b₁ → get ⁻¹ b₂) →
          Is-equivalence get⁻¹-const) →
     let get⁻¹-const : ∀ _ _ → _
         get⁻¹-const = λ b₁ b₂ → proj₁ (f b₁ b₂) in
     (b₁ b₂ b₃ : B) (p : get ⁻¹ b₁) →
     get⁻¹-const b₂ b₃ (get⁻¹-const b₁ b₂ p) ≡ get⁻¹-const b₁ b₃ p)    ↝⟨ (∃-cong λ _ →
                                                                           Σ-cong-contra (∀-cong ext λ _ → ∀-cong ext λ _ → Eq.≃-as-Σ) λ _ →
                                                                                F.id) ⟩□
  (∃ λ (get : A → B) →
   ∃ λ (get⁻¹-constant : (b₁ b₂ : B) → get ⁻¹ b₁ ≃ get ⁻¹ b₂) →
     let get⁻¹-const : ∀ _ _ → _
         get⁻¹-const = λ b₁ b₂ → _≃_.to (get⁻¹-constant b₁ b₂) in
     (b₁ b₂ b₃ : B) (p : get ⁻¹ b₁) →
     get⁻¹-const b₂ b₃ (get⁻¹-const b₁ b₂ p) ≡ get⁻¹-const b₁ b₃ p)    □

------------------------------------------------------------------------
-- Some results related to h-levels

-- If the domain of a lens is inhabited and has h-level n,
-- then the codomain also has h-level n.

h-level-respects-lens-from-inhabited :
  ∀ n → Lens A B → A → H-level n A → H-level n B
h-level-respects-lens-from-inhabited {A = A} {B = B} n l a =
  H-level n A  ↝⟨ H-level.respects-surjection surj n ⟩□
  H-level n B  □
  where
  open Lens l

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

-- If A and B have h-level n given the assumption that the other type
-- is inhabited, then Lens A B has h-level n.

lens-preserves-h-level :
  ∀ n → (B → H-level n A) → (A → H-level n B) →
  H-level n (Lens A B)
lens-preserves-h-level {B = B} {A = A} n hA hB =
  H-level-cong _ n (inverse Lens-as-Σ′) $
  Σ-closure n (Π-closure ext n λ a →
               hB a) λ _ →
  Σ-closure n (Π-closure ext n λ b →
               Π-closure ext n λ _ →
               Eq.h-level-closure ext n
                 (⁻¹-closure (hA b) hB)
                 (⁻¹-closure (hA b) hB)) λ _ →
              (Π-closure ext n λ b →
               Π-closure ext n λ _ →
               Π-closure ext n λ _ →
               Π-closure ext n λ _ →
               ⇒≡ n (⁻¹-closure (hA b) hB))
  where
  ⁻¹-closure :
    {f : A → B} {x : B} →
    H-level n A → (A → H-level n B) →
    H-level n (f ⁻¹ x)
  ⁻¹-closure hA hB =
    Σ-closure n hA λ a →
    ⇒≡ n (hB a)

-- If A has positive h-level n, then Lens A B also has h-level n.

lens-preserves-h-level-of-domain :
  ∀ n → H-level (1 + n) A → H-level (1 + n) (Lens A B)
lens-preserves-h-level-of-domain n hA =
  [inhabited⇒+]⇒+ n λ l →
    lens-preserves-h-level (1 + n) (λ _ → hA) λ a →
      h-level-respects-lens-from-inhabited _ l a hA

------------------------------------------------------------------------
-- Some equality characterisation lemmas

-- An equality characterisation lemma.

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

  (l₁ ≡ l₂)
    ≃
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (gc : ∀ b₁ b₂ p →
             subst (λ get → ∀ b₁ b₂ → get ⁻¹ b₁ → get ⁻¹ b₂)
               (⟨ext⟩ g) (get⁻¹-const l₁) b₁ b₂ p ≡
             get⁻¹-const l₂ b₁ b₂ p) →
     subst
       (λ (get , gc) →
          ∀ b₁ b₂ b₃ (p : get ⁻¹ b₁) →
          gc b₂ b₃ (gc b₁ b₂ p) ≡ gc b₁ b₃ p)
       (Σ-≡,≡→≡ (⟨ext⟩ g)
          (⟨ext⟩ λ b₁ → ⟨ext⟩ λ b₂ → ⟨ext⟩ λ p → gc b₁ b₂ p))
       (get⁻¹-const-∘ l₁) ≡
     get⁻¹-const-∘ l₂)
equality-characterisation {l₁ = l₁} {l₂ = l₂} =
  l₁ ≡ l₂                                                      ↝⟨ inverse $ Eq.≃-≡ (lemma₁ F.∘ Lens-as-Σ) ⟩

  ( ((get l₁ , get⁻¹-const l₁) , get⁻¹-const-∘ l₁)
  , get⁻¹-const-equivalence l₁
  ) ≡
  ( ((get l₂ , get⁻¹-const l₂) , get⁻¹-const-∘ l₂)
  , get⁻¹-const-equivalence l₂
  )                                                            ↔⟨ inverse $
                                                                  ignore-propositional-component
                                                                    (Π-closure ext 1 λ _ →
                                                                     Π-closure ext 1 λ _ →
                                                                     Eq.propositional ext _) ⟩
  ((get l₁ , get⁻¹-const l₁) , get⁻¹-const-∘ l₁) ≡
  ((get l₂ , get⁻¹-const l₂) , get⁻¹-const-∘ l₂)               ↔⟨ inverse B.Σ-≡,≡↔≡ ⟩

  (∃ λ (p : (get l₁ , get⁻¹-const l₁) ≡
            (get l₂ , get⁻¹-const l₂)) →
     subst
       (λ (get , gc) →
          ∀ b₁ b₂ b₃ (p : get ⁻¹ b₁) →
          gc b₂ b₃ (gc b₁ b₂ p) ≡ gc b₁ b₃ p)
       p (get⁻¹-const-∘ l₁) ≡
     get⁻¹-const-∘ l₂)                                         ↝⟨ (Σ-cong-contra B.Σ-≡,≡↔≡ λ _ → F.id) ⟩

  (∃ λ (p : ∃ λ (g : get l₁ ≡ get l₂) →
              subst (λ get → ∀ b₁ b₂ → get ⁻¹ b₁ → get ⁻¹ b₂)
                g (get⁻¹-const l₁) ≡
              get⁻¹-const l₂) →
     subst
       (λ (get , gc) →
          ∀ b₁ b₂ b₃ (p : get ⁻¹ b₁) →
          gc b₂ b₃ (gc b₁ b₂ p) ≡ gc b₁ b₃ p)
       (uncurry Σ-≡,≡→≡ p) (get⁻¹-const-∘ l₁) ≡
     get⁻¹-const-∘ l₂)                                         ↔⟨ inverse Σ-assoc ⟩

  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (gc : subst (λ get → ∀ b₁ b₂ → get ⁻¹ b₁ → get ⁻¹ b₂)
               g (get⁻¹-const l₁) ≡
             get⁻¹-const l₂) →
     subst
       (λ (get , gc) →
          ∀ b₁ b₂ b₃ (p : get ⁻¹ b₁) →
          gc b₂ b₃ (gc b₁ b₂ p) ≡ gc b₁ b₃ p)
       (Σ-≡,≡→≡ g gc) (get⁻¹-const-∘ l₁) ≡
     get⁻¹-const-∘ l₂)                                         ↝⟨ (Σ-cong-contra (Eq.extensionality-isomorphism bad-ext) λ _ → F.id) ⟩

  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (gc : subst (λ get → ∀ b₁ b₂ → get ⁻¹ b₁ → get ⁻¹ b₂)
               (⟨ext⟩ g) (get⁻¹-const l₁) ≡
             get⁻¹-const l₂) →
     subst
       (λ (get , gc) →
          ∀ b₁ b₂ b₃ (p : get ⁻¹ b₁) →
          gc b₂ b₃ (gc b₁ b₂ p) ≡ gc b₁ b₃ p)
       (Σ-≡,≡→≡ (⟨ext⟩ g) gc) (get⁻¹-const-∘ l₁) ≡
     get⁻¹-const-∘ l₂)                                         ↝⟨ (∃-cong λ _ → Σ-cong-contra (inverse $ lemma₂ _) λ _ → F.id) ⟩□

  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (gc : ∀ b₁ b₂ p →
             subst (λ get → ∀ b₁ b₂ → get ⁻¹ b₁ → get ⁻¹ b₂)
               (⟨ext⟩ g) (get⁻¹-const l₁) b₁ b₂ p ≡
             get⁻¹-const l₂ b₁ b₂ p) →
     subst
       (λ (get , gc) →
          ∀ b₁ b₂ b₃ (p : get ⁻¹ b₁) →
          gc b₂ b₃ (gc b₁ b₂ p) ≡ gc b₁ b₃ p)
       (Σ-≡,≡→≡ (⟨ext⟩ g)
          (⟨ext⟩ λ b₁ → ⟨ext⟩ λ b₂ → ⟨ext⟩ λ p → gc b₁ b₂ p))
       (get⁻¹-const-∘ l₁) ≡
     get⁻¹-const-∘ l₂)                                         □
  where
  open Lens

  lemma₁ :
    {P : A → Set ℓ} {Q R : (x : A) → P x → Set ℓ} →
    (∃ λ (x : A) → ∃ λ (y : P x) → Q x y × R x y) ≃
    (∃ λ (((x , y) , _) : Σ (Σ A P) (uncurry R)) → Q x y)
  lemma₁ {A = A} {P = P} {Q = Q} {R = R} =
    (∃ λ (x : A) → ∃ λ (y : P x) → Q x y × R x y)                      ↔⟨ (∃-cong λ _ → ∃-cong λ _ → ×-comm) ⟩
    (∃ λ (x : A) → ∃ λ (y : P x) → R x y × Q x y)                      ↔⟨ (∃-cong λ _ → Σ-assoc) ⟩
    (∃ λ (x : A) → ∃ λ ((y , _) : ∃ λ (y : P x) → R x y) → Q x y)      ↔⟨ Σ-assoc ⟩
    (∃ λ ((x , y , _) : ∃ λ (x : A) → ∃ λ (y : P x) → R x y) → Q x y)  ↝⟨ (Σ-cong Σ-assoc λ _ → F.id) ⟩□
    (∃ λ (((x , y) , _) : Σ (Σ A P) (uncurry R)) → Q x y)              □

  lemma₂ : (g : ∀ a → get l₁ a ≡ get l₂ a) → _
  lemma₂ g =
    subst (λ get → ∀ b₁ b₂ → get ⁻¹ b₁ → get ⁻¹ b₂)
      (⟨ext⟩ g) (get⁻¹-const l₁) ≡
    get⁻¹-const l₂                                              ↝⟨ inverse $ Eq.extensionality-isomorphism bad-ext ⟩

    (∀ b₁ → subst (λ get → ∀ b₁ b₂ → get ⁻¹ b₁ → get ⁻¹ b₂)
               (⟨ext⟩ g) (get⁻¹-const l₁) b₁ ≡
            get⁻¹-const l₂ b₁)                                  ↝⟨ (∀-cong ext λ _ → inverse $ Eq.extensionality-isomorphism bad-ext) ⟩

    (∀ b₁ b₂ → subst (λ get → ∀ b₁ b₂ → get ⁻¹ b₁ → get ⁻¹ b₂)
                 (⟨ext⟩ g) (get⁻¹-const l₁) b₁ b₂ ≡
               get⁻¹-const l₂ b₁ b₂)                            ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → inverse $ Eq.extensionality-isomorphism bad-ext) ⟩□

    (∀ b₁ b₂ p →
     subst (λ get → ∀ b₁ b₂ → get ⁻¹ b₁ → get ⁻¹ b₂)
       (⟨ext⟩ g) (get⁻¹-const l₁) b₁ b₂ p ≡
     get⁻¹-const l₂ b₁ b₂ p)                                    □

-- An equality characterisation lemma for lenses from sets.

equality-characterisation-for-sets :
  let open Lens in
  {A : Set a} {B : Set b} {l₁ l₂ : Lens A B} →

  Is-set A →

  (l₁ ≡ l₂)
    ≃
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
     ∀ b₁ b₂ p →
     proj₁ (get⁻¹-const l₁ b₁ b₂ (subst (_⁻¹ b₁) (sym $ ⟨ext⟩ g) p)) ≡
     proj₁ (get⁻¹-const l₂ b₁ b₂ p))
equality-characterisation-for-sets
  {A = A} {B = B} {l₁ = l₁} {l₂ = l₂} A-set =
  l₁ ≡ l₂                                                                 ↝⟨ equality-characterisation ⟩

  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (gc : ∀ b₁ b₂ p →
             subst (λ get → ∀ b₁ b₂ → get ⁻¹ b₁ → get ⁻¹ b₂)
               (⟨ext⟩ g) (get⁻¹-const l₁) b₁ b₂ p ≡
             get⁻¹-const l₂ b₁ b₂ p) →
     subst
       (λ (get , gc) →
          ∀ b₁ b₂ b₃ (p : get ⁻¹ b₁) →
          gc b₂ b₃ (gc b₁ b₂ p) ≡ gc b₁ b₃ p)
       (Σ-≡,≡→≡
          (⟨ext⟩ g)
          (⟨ext⟩ λ b₁ → ⟨ext⟩ λ b₂ → ⟨ext⟩ λ p → gc b₁ b₂ p))
       (get⁻¹-const-∘ l₁) ≡
     get⁻¹-const-∘ l₂)                                                    ↔⟨ (∃-cong λ _ → drop-⊤-right λ _ → _⇔_.to contractible⇔↔⊤ $ +⇒≡ $
                                                                              Π-closure ext 1 λ _ →
                                                                              Π-closure ext 1 λ _ →
                                                                              Π-closure ext 1 λ _ →
                                                                              Π-closure ext 1 λ _ →
                                                                              ⁻¹-set) ⟩
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
     ∀ b₁ b₂ p →
     subst (λ get → ∀ b₁ b₂ → get ⁻¹ b₁ → get ⁻¹ b₂)
       (⟨ext⟩ g) (get⁻¹-const l₁) b₁ b₂ p ≡
     get⁻¹-const l₂ b₁ b₂ p)                                              ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                              ≡⇒↝ _ $ cong (_≡ _) $ lemma₁ _ _ _ _) ⟩
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
     ∀ b₁ b₂ p →
     subst (_⁻¹ b₂) (⟨ext⟩ g)
       (get⁻¹-const l₁ b₁ b₂ (subst (_⁻¹ b₁) (sym $ ⟨ext⟩ g) p)) ≡
     get⁻¹-const l₂ b₁ b₂ p)                                              ↔⟨ (∃-cong λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ → ∀-cong ext λ p →
                                                                              drop-⊤-right (λ _ → _⇔_.to contractible⇔↔⊤ $
                                                                                +⇒≡ (B-set (proj₁ p))) F.∘
                                                                              inverse B.Σ-≡,≡↔≡) ⟩
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
     ∀ b₁ b₂ p →
     proj₁ (subst (_⁻¹ b₂) (⟨ext⟩ g)
              (get⁻¹-const l₁ b₁ b₂
                 (subst (_⁻¹ b₁) (sym $ ⟨ext⟩ g) p))) ≡
     proj₁ (get⁻¹-const l₂ b₁ b₂ p))                                      ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                              ≡⇒↝ _ $ cong (_≡ _) $ lemma₂ _ _ _ _) ⟩□
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
     ∀ b₁ b₂ p →
     proj₁ (get⁻¹-const l₁ b₁ b₂ (subst (_⁻¹ b₁) (sym $ ⟨ext⟩ g) p)) ≡
     proj₁ (get⁻¹-const l₂ b₁ b₂ p))                                      □
  where
  open Lens

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

  ⁻¹-set : Is-set (get l₂ ⁻¹ b)
  ⁻¹-set =
    Σ-closure 2 A-set λ a →
    mono₁ 1 (B-set a)

  lemma₁ : ∀ g b₁ b₂ p → _
  lemma₁ g b₁ b₂ p =
    subst (λ get → ∀ b₁ b₂ → get ⁻¹ b₁ → get ⁻¹ b₂)
      (⟨ext⟩ g) (get⁻¹-const l₁) b₁ b₂ p                         ≡⟨ cong (λ f → f b₂ p) $ sym $
                                                                    push-subst-application (⟨ext⟩ g) (λ get b₁ → ∀ b₂ → get ⁻¹ b₁ → get ⁻¹ b₂) ⟩
    subst (λ get → ∀ b₂ → get ⁻¹ b₁ → get ⁻¹ b₂)
      (⟨ext⟩ g) (get⁻¹-const l₁ b₁) b₂ p                         ≡⟨ cong (λ f → f p) $ sym $
                                                                    push-subst-application (⟨ext⟩ g) (λ get b₂ → get ⁻¹ b₁ → get ⁻¹ b₂) ⟩
    subst (λ get → get ⁻¹ b₁ → get ⁻¹ b₂)
      (⟨ext⟩ g) (get⁻¹-const l₁ b₁ b₂) p                         ≡⟨ subst-→ {x₁≡x₂ = ⟨ext⟩ g} ⟩∎

    subst (_⁻¹ b₂) (⟨ext⟩ g)
      (get⁻¹-const l₁ b₁ b₂ (subst (_⁻¹ b₁) (sym $ ⟨ext⟩ g) p))  ∎

  lemma₂ : ∀ g b₁ b₂ p → _
  lemma₂ g b₁ b₂ p =
    proj₁ (subst (_⁻¹ b₂) (⟨ext⟩ g)
             (get⁻¹-const l₁ b₁ b₂
                (subst (_⁻¹ b₁) (sym $ ⟨ext⟩ g) p)))                 ≡⟨ cong proj₁ $
                                                                        push-subst-pair {y≡z = ⟨ext⟩ g} _ _ ⟩
    subst (λ _ → A) (⟨ext⟩ g)
      (proj₁ (get⁻¹-const l₁ b₁ b₂
                (subst (_⁻¹ b₁) (sym $ ⟨ext⟩ g) p)))                 ≡⟨ subst-const (⟨ext⟩ g) ⟩∎

    proj₁ (get⁻¹-const l₁ b₁ b₂ (subst (_⁻¹ b₁) (sym $ ⟨ext⟩ g) p))  ∎

------------------------------------------------------------------------
-- Conversions between different kinds of lenses

-- Higher lenses can be converted to the ones defined above.

higher→ : Higher.Lens A B → Lens A B
higher→ l@(Higher.⟨ _ , _ , _ ⟩) = _≃_.from Lens-as-Σ′
  ( Higher.Lens.get l
  , Higher.get⁻¹-constant l
  , Higher.get⁻¹-constant-∘ l
  )

-- The conversion preserves getters and setters.

higher→-preserves-getters-and-setters :
  Preserves-getters-and-setters-→ A B higher→
higher→-preserves-getters-and-setters Higher.⟨ _ , _ , _ ⟩ =
  refl _ , refl _

-- A lens of the kind defined above can be converted to a higher one
-- if the codomain is inhabited when it is merely inhabited.

→higher : (∥ B ∥ → B) → Lens A B → Higher.Lens A B
→higher {B = B} {A = A} ∥B∥→B l@(lens _ _ _ _) = record
  { R     = ∃ λ (b : ∥ B ∥) → Lens.get l ⁻¹ (∥B∥→B b)
  ; equiv =
      A                                                      ↔⟨ (inverse $ drop-⊤-right λ _ → _⇔_.to contractible⇔↔⊤ $
                                                                 other-singleton-contractible _) ⟩
      (∃ λ a → ∃ λ b → Lens.get l a ≡ b)                     ↔⟨ ∃-comm ⟩
      (∃ λ b → Lens.get l ⁻¹ b)                              ↝⟨ (Σ-cong (inverse PT.∥∥×≃) λ _ → Lens.get⁻¹-constant l _ _) ⟩
      (∃ λ ((b , _) : ∥ B ∥ × B) → Lens.get l ⁻¹ (∥B∥→B b))  ↔⟨ inverse Σ-assoc ⟩
      (∃ λ (b : ∥ B ∥) → B × Lens.get l ⁻¹ (∥B∥→B b))        ↔⟨ (∃-cong λ _ → ×-comm) ⟩
      (∃ λ (b : ∥ B ∥) → Lens.get l ⁻¹ (∥B∥→B b) × B)        ↔⟨ Σ-assoc ⟩□
      (∃ λ (b : ∥ B ∥) → Lens.get l ⁻¹ (∥B∥→B b)) × B        □
  ; inhabited = proj₁
  }

-- The conversion preserves getters and setters.

→higher-preserves-getters-and-setters :
  {B : Set b}
  (∥B∥→B : ∥ B ∥ → B) →
  Preserves-getters-and-setters-→ A B (→higher ∥B∥→B)
→higher-preserves-getters-and-setters {A = A} ∥B∥→B l@(lens _ _ _ _) =
    refl _

  , ⟨ext⟩ λ a → ⟨ext⟩ λ b →

    let a′ = set a b in

    _≃_.to-from (Higher.Lens.equiv (→higher ∥B∥→B l)) $ cong₂ _,_

      (∣ get a′ ∣ ,
       get⁻¹-const (get a′) (∥B∥→B ∣ get a′ ∣) (a′ , refl _)          ≡⟨ Σ-≡,≡→≡ (PT.truncation-is-proposition _ _)
                                                                           (
           subst (λ b → get ⁻¹ ∥B∥→B b)
             (PT.truncation-is-proposition _ _)
             (get⁻¹-const (get a′) (∥B∥→B ∣ get a′ ∣) (a′ , refl _))        ≡⟨ elim¹
                                                                                (λ {f} _ →
                                                                                subst (λ b → get ⁻¹ f b)
                                                                                (PT.truncation-is-proposition _ _)
                                                                                (get⁻¹-const (get a′) (f ∣ get a′ ∣) (a′ , refl _)) ≡
                                                                                get⁻¹-const (get a) (f ∣ get a ∣) (a , refl _))
                                                                                (
               subst (λ _ → get ⁻¹ ∥B∥→B ∣ b ∣)
                 (PT.truncation-is-proposition _ _)
                 (get⁻¹-const (get a′) (∥B∥→B ∣ b ∣) (a′ , refl _))               ≡⟨ subst-const (PT.truncation-is-proposition _ _) ⟩

               get⁻¹-const (get a′) (∥B∥→B ∣ b ∣) (a′ , refl _)                   ≡⟨ sym $ get⁻¹-const-∘ _ _ _ _ ⟩

               get⁻¹-const (get a) (∥B∥→B ∣ b ∣)
                 (get⁻¹-const (get a′) (get a) (a′ , refl _))                     ≡⟨ cong (get⁻¹-const (get a) (∥B∥→B ∣ b ∣)) $
                                                                                elim¹
                                                                                (λ {b} eq → get⁻¹-const (get a′) (get a) (a′ , refl _) ≡
                                                                                get⁻¹-const b        (get a) (a′ , eq))
                                                                                (refl _)
                                                                                (get-set a b) ⟩
               get⁻¹-const (get a) (∥B∥→B ∣ b ∣)
                 (get⁻¹-const b (get a) (set a b , get-set a b))                  ≡⟨⟩

               get⁻¹-const (get a) (∥B∥→B ∣ b ∣)
                 (get⁻¹-const b (get a)
                    (get⁻¹-const (get a) b (a , refl _)))                         ≡⟨ cong (λ p → get⁻¹-const (get a) (∥B∥→B ∣ b ∣)
                                                                                (get⁻¹-const b (get a) p)) $
                                                                                get⁻¹-const-inverse _ _ _ ⟩
               get⁻¹-const (get a) (∥B∥→B ∣ b ∣)
                 (get⁻¹-const b (get a)
                    (get⁻¹-const⁻¹ b (get a) (a , refl _)))                       ≡⟨ cong (get⁻¹-const (get a) (∥B∥→B ∣ b ∣)) $
                                                                                _≃_.right-inverse-of (get⁻¹-constant _ _) _ ⟩∎
               get⁻¹-const (get a) (∥B∥→B ∣ b ∣) (a , refl _)                     ∎)
                                                                                (⟨ext⟩ λ _ → cong ∥B∥→B $ PT.truncation-is-proposition _ _) ⟩∎
           get⁻¹-const (get a) (∥B∥→B ∣ get a ∣) (a , refl _)               ∎) ⟩∎

       ∣ get a ∣ ,
       get⁻¹-const (get a) (∥B∥→B ∣ get a ∣) (a , refl _)             ∎)

      (get (set a b)  ≡⟨ get-set a b ⟩∎
       b              ∎)

  where
  open Lens l

-- There is a split surjection from Lens A B to Higher.Lens A B if B
-- is inhabited when it is merely inhabited (assuming univalence).

↠higher :
  {A : Set a} {B : Set b} →
  Univalence (a ⊔ b) →
  (∥ B ∥ → B) →
  Lens A B ↠ Higher.Lens A B
↠higher {A = A} {B = B} univ ∥B∥→B = record
  { logical-equivalence = record
    { to   = →higher ∥B∥→B
    ; from = higher→
    }
  ; right-inverse-of = λ l →
      Higher.lenses-equal-if-setters-equal
        univ _ _
        (λ _ → ∥B∥→B)
        (set (→higher ∥B∥→B (higher→ l))  ≡⟨ proj₂ $ →higher-preserves-getters-and-setters ∥B∥→B (higher→ l) ⟩
         Lens.set (higher→ l)             ≡⟨ proj₂ $ higher→-preserves-getters-and-setters l ⟩∎
         set l                            ∎)
  }
  where
  open Higher.Lens

-- The split surjection preserves getters and setters.

↠higher-preserves-getters-and-setters :
  {A : Set a} {B : Set b}
  (univ : Univalence (a ⊔ b))
  (∥B∥→B : ∥ B ∥ → B) →
  Preserves-getters-and-setters-⇔ A B
    (_↠_.logical-equivalence (↠higher univ ∥B∥→B))
↠higher-preserves-getters-and-setters _ ∥B∥→B =
    →higher-preserves-getters-and-setters ∥B∥→B
  , higher→-preserves-getters-and-setters

-- If B is inhabited when it is merely inhabited and A has positive
-- h-level n, then Higher.Lens A B also has h-level n (assuming
-- univalence).

higher-lens-preserves-h-level-of-domain :
  {A : Set a} {B : Set b} →
  Univalence (a ⊔ b) →
  (∥ B ∥ → B) →
  ∀ n → H-level (1 + n) A → H-level (1 + n) (Higher.Lens A B)
higher-lens-preserves-h-level-of-domain {A = A} {B = B} univ ∥B∥→B n =
  H-level (1 + n) A                  ↝⟨ lens-preserves-h-level-of-domain n ⟩
  H-level (1 + n) (Lens A B)         ↝⟨ H-level.respects-surjection (↠higher univ ∥B∥→B) (1 + n) ⟩□
  H-level (1 + n) (Higher.Lens A B)  □

-- Traditional lenses that satisfy some coherence properties can be
-- translated to lenses of the kind defined above.

coherent→ :
  Block "conversion" →
  Traditional.Coherent-lens A B → Lens A B
coherent→ ⊠ l = _≃_.from Lens-as-Σ′
  ( get
  , (λ b₁ b₂ →
       Eq.↔→≃ (gg b₁ b₂) (gg b₂ b₁) (gg∘gg b₁ b₂) (gg∘gg b₂ b₁))
  , (λ b₁ b₂ b₃ (a , _) →
       Σ-≡,≡→≡
         (set (set a b₂) b₃  ≡⟨ set-set a b₂ b₃ ⟩∎
          set a b₃           ∎)
         (subst (λ a → get a ≡ b₃) (set-set a b₂ b₃)
            (get-set (set a b₂) b₃)                   ≡⟨ subst-∘ _ _ (set-set a b₂ b₃) ⟩

          subst (_≡ b₃) (cong get (set-set a b₂ b₃))
            (get-set (set a b₂) b₃)                   ≡⟨ subst-trans-sym {y≡x = cong get (set-set a b₂ b₃)} ⟩

          trans (sym (cong get (set-set a b₂ b₃)))
            (get-set (set a b₂) b₃)                   ≡⟨ get-set-set′ _ _ _ ⟩∎

          get-set a b₃                                ∎))
  )
  where
  open Traditional.Coherent-lens l

  get-set-set′ :
    ∀ a b₁ b₂ →
    trans (sym (cong get (set-set a b₁ b₂))) (get-set (set a b₁) b₂) ≡
    get-set a b₂
  get-set-set′ a b₁ b₂ =
    trans (sym (cong get (set-set a b₁ b₂))) (get-set (set a b₁) b₂)  ≡⟨ cong (λ eq → trans (sym eq) (get-set _ _)) $
                                                                         get-set-set _ _ _ ⟩
    trans (sym (trans (get-set (set a b₁) b₂) (sym (get-set a b₂))))
      (get-set (set a b₁) b₂)                                         ≡⟨ cong (flip trans (get-set _ _)) $
                                                                         sym-trans _ (sym (get-set _ _)) ⟩
    trans (trans (sym (sym (get-set a b₂)))
             (sym (get-set (set a b₁) b₂)))
      (get-set (set a b₁) b₂)                                         ≡⟨ trans-[trans-sym]- _ (get-set _ _) ⟩

    sym (sym (get-set a b₂))                                          ≡⟨ sym-sym (get-set _ _) ⟩∎

    get-set a b₂                                                      ∎

  gg : ∀ b₁ b₂ → get ⁻¹ b₁ → get ⁻¹ b₂
  gg b₁ b₂ (a , _) = set a b₂ , get-set a b₂

  gg∘gg : ∀ b₁ b₂ p → gg b₁ b₂ (gg b₂ b₁ p) ≡ p
  gg∘gg b₁ b₂ (a , get-a≡b₂) =
    Σ-≡,≡→≡ eq₁
      (subst (λ a → get a ≡ b₂) eq₁ (get-set (set a b₁) b₂)   ≡⟨ subst-∘ _ _ eq₁ ⟩

       subst (_≡ b₂) (cong get eq₁) (get-set (set a b₁) b₂)   ≡⟨ subst-trans-sym {y≡x = cong get eq₁} ⟩

       trans (sym (cong get eq₁)) (get-set (set a b₁) b₂)     ≡⟨ cong (flip trans (get-set (set a b₁) b₂))
                                                                 lemma₂ ⟩
       trans (trans (trans (sym (cong get (set-get a)))
                       (cong (get ⊚ set a) get-a≡b₂))
                (sym (cong get (set-set a b₁ b₂))))
         (get-set (set a b₁) b₂)                              ≡⟨ trans-assoc _ _ (get-set (set a b₁) b₂) ⟩

       trans (trans (sym (cong get (set-get a)))
                (cong (get ⊚ set a) get-a≡b₂))
         (trans (sym (cong get (set-set a b₁ b₂)))
            (get-set (set a b₁) b₂))                          ≡⟨ trans-assoc _ _ (trans (sym (cong get (set-set a b₁ b₂)))
                                                                                (get-set (set a b₁) b₂)) ⟩
       trans (sym (cong get (set-get a)))
         (trans (cong (get ⊚ set a) get-a≡b₂)
            (trans (sym (cong get (set-set a b₁ b₂)))
               (get-set (set a b₁) b₂)))                      ≡⟨ cong₂ (λ p q → trans (sym p) (trans (cong (get ⊚ set a) get-a≡b₂) q))
                                                                   (get-set-get _)
                                                                   (get-set-set′ _ _ _) ⟩
       trans (sym (get-set a (get a)))
         (trans (cong (get ⊚ set a) get-a≡b₂)
            (get-set a b₂))                                   ≡⟨ cong (λ eq → trans (sym (eq (get a)))
                                                                                (trans (cong (get ⊚ set a) get-a≡b₂) (eq b₂))) $ sym $
                                                                 _≃_.left-inverse-of (Eq.extensionality-isomorphism bad-ext) _ ⟩
       trans (sym (ext⁻¹ (⟨ext⟩ (get-set a)) (get a)))
         (trans (cong (get ⊚ set a) get-a≡b₂)
            (ext⁻¹ (⟨ext⟩ (get-set a)) b₂))                   ≡⟨ elim₁
                                                                   (λ {f} gs →
                                                                      trans (sym (ext⁻¹ gs (get a))) (trans (cong f get-a≡b₂) (ext⁻¹ gs b₂)) ≡
                                                                      get-a≡b₂)
                                                                   (
          trans (sym (ext⁻¹ (refl id) (get a)))
             (trans (cong id get-a≡b₂)
                (ext⁻¹ (refl id) b₂))                               ≡⟨ cong₂ (λ p q → trans (sym p) (trans (cong id get-a≡b₂) q))
                                                                         (ext⁻¹-refl _)
                                                                         (ext⁻¹-refl _) ⟩
          trans (sym (refl _))
             (trans (cong id get-a≡b₂) (refl _))                    ≡⟨ cong₂ trans sym-refl (trans-reflʳ _) ⟩

          trans (refl _) (cong id get-a≡b₂)                         ≡⟨ trans-reflˡ (cong id get-a≡b₂) ⟩

          cong id get-a≡b₂                                          ≡⟨ sym $ cong-id get-a≡b₂ ⟩∎

          get-a≡b₂                                                  ∎)
                                                                 (⟨ext⟩ (get-set a)) ⟩
       get-a≡b₂                                               ∎)
    where
    eq₁ =
      set (set a b₁) b₂  ≡⟨ set-set a b₁ b₂ ⟩
      set a b₂           ≡⟨ cong (set a) (sym get-a≡b₂) ⟩
      set a (get a)      ≡⟨ set-get a ⟩∎
      a                  ∎

    lemma₁ =
      sym (cong get (cong (set a) (sym get-a≡b₂)))  ≡⟨ cong sym $ cong-∘ _ _ (sym get-a≡b₂) ⟩
      sym (cong (get ⊚ set a) (sym get-a≡b₂))       ≡⟨ sym $ cong-sym _ (sym get-a≡b₂) ⟩
      cong (get ⊚ set a) (sym (sym get-a≡b₂))       ≡⟨ cong (cong (get ⊚ set a)) $ sym-sym get-a≡b₂ ⟩∎
      cong (get ⊚ set a) get-a≡b₂                   ∎

    lemma₂ =
      sym (cong get eq₁)                                          ≡⟨⟩

      sym (cong get
             (trans (set-set a b₁ b₂)
                (trans (cong (set a) (sym get-a≡b₂))
                   (set-get a))))                                 ≡⟨ cong sym $
                                                                     cong-trans _ _ (trans (cong (set a) (sym get-a≡b₂)) (set-get a)) ⟩
      sym (trans (cong get (set-set a b₁ b₂))
             (cong get (trans (cong (set a) (sym get-a≡b₂))
                          (set-get a))))                          ≡⟨ cong (λ eq → sym (trans _ eq)) $
                                                                     cong-trans _ _ (set-get a) ⟩
      sym (trans (cong get (set-set a b₁ b₂))
             (trans (cong get (cong (set a) (sym get-a≡b₂)))
                (cong get (set-get a))))                          ≡⟨ sym-trans _ (trans (cong get (cong (set a) (sym get-a≡b₂)))
                                                                                (cong get (set-get a))) ⟩
      trans (sym (trans (cong get (cong (set a) (sym get-a≡b₂)))
                    (cong get (set-get a))))
        (sym (cong get (set-set a b₁ b₂)))                        ≡⟨ cong (flip trans (sym (cong get (set-set a b₁ b₂)))) $
                                                                     sym-trans _ (cong get (set-get a)) ⟩
      trans (trans (sym (cong get (set-get a)))
               (sym (cong get (cong (set a) (sym get-a≡b₂)))))
        (sym (cong get (set-set a b₁ b₂)))                        ≡⟨ cong (λ eq → trans (trans (sym (cong get (set-get a))) eq)
                                                                                (sym (cong get (set-set a b₁ b₂))))
                                                                     lemma₁ ⟩∎
      trans (trans (sym (cong get (set-get a)))
               (cong (get ⊚ set a) get-a≡b₂))
        (sym (cong get (set-set a b₁ b₂)))                        ∎

-- The conversion preserves getters and setters.

coherent→-preserves-getters-and-setters :
  (b : Block "conversion") →
  Preserves-getters-and-setters-→ A B (coherent→ b)
coherent→-preserves-getters-and-setters ⊠ _ =
  refl _ , refl _

-- If A is a set, then Traditional.Lens A B is equivalent to Lens A B.

traditional≃ :
  Block "conversion" →
  Is-set A → Traditional.Lens A B ≃ Lens A B
traditional≃ {A = A} {B = B} b@⊠ A-set = Eq.↔→≃
  (Traditional.Lens A B           ↔⟨ Traditional.≃coherent A-set ⟩
   Traditional.Coherent-lens A B  ↝⟨ coherent→ b ⟩□
   Lens A B                       □)
  Lens.traditional-lens
  (λ l → _≃_.from (equality-characterisation-for-sets A-set)
     ( (λ _ → refl _)
     , (λ b₁ b₂ p@(a , _) →
          let l′ = traditional-lens l
              l″ = coherent→ b (_≃_.to (Traditional.≃coherent A-set) l′)
          in
          proj₁ (get⁻¹-const l″ b₁ b₂
                   (subst (_⁻¹ b₁) (sym $ ⟨ext⟩ λ _ → refl _) p))         ≡⟨ cong (λ eq → proj₁ (get⁻¹-const l″ b₁ b₂ (subst (_⁻¹ b₁) (sym eq) p)))
                                                                             ext-refl ⟩

          proj₁ (get⁻¹-const l″ b₁ b₂ (subst (_⁻¹ b₁) (sym (refl _)) p))  ≡⟨ cong (λ eq → proj₁ (get⁻¹-const l″ b₁ b₂ (subst (_⁻¹ b₁) eq p)))
                                                                             sym-refl ⟩

          proj₁ (get⁻¹-const l″ b₁ b₂ (subst (_⁻¹ b₁) (refl _) p))        ≡⟨ cong (proj₁ ⊚ get⁻¹-const l″ b₁ b₂) $
                                                                             subst-refl _ _ ⟩

          proj₁ (get⁻¹-const l″ b₁ b₂ p)                                  ≡⟨⟩

          set l (proj₁ p) b₂                                              ≡⟨⟩

          proj₁ (get⁻¹-const l (get l a) b₂ (a , refl _))                 ≡⟨ elim¹
                                                                               (λ {b} eq →
                                                                                proj₁ (get⁻¹-const l (get l a) b₂ (a , refl _)) ≡
                                                                                proj₁ (get⁻¹-const l b b₂ (a , eq)))
                                                                               (refl _)
                                                                               (proj₂ p) ⟩∎
          proj₁ (get⁻¹-const l b₁ b₂ p)                                   ∎)
     ))
  (λ _ →
     _↔_.from (Traditional.equality-characterisation-for-sets A-set)
       (refl _))
  where
  open Lens

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

-- The equivalence preserves getters and setters.

traditional≃-preserves-getters-and-setters :
  {A : Set a}
  (b : Block "conversion")
  (s : Is-set A) →
  Preserves-getters-and-setters-⇔ A B
    (_≃_.logical-equivalence (traditional≃ b s))
traditional≃-preserves-getters-and-setters ⊠ _ =
    (λ _ → refl _ , refl _)
  , (λ _ → refl _ , refl _)

-- If B is inhabited when it is merely inhabited, then
-- Traditional.Coherent-lens A B is logically equivalent to
-- Higher.Lens A B.

coherent⇔higher :
  Block "conversion" →
  (∥ B ∥ → B) →
  Traditional.Coherent-lens A B ⇔ Higher.Lens A B
coherent⇔higher {B = B} {A = A} b ∥B∥→B = record
  { to   = Traditional.Coherent-lens A B  ↝⟨ coherent→ b ⟩
           Lens A B                       ↝⟨ →higher ∥B∥→B ⟩□
           Higher.Lens A B                □
  ; from = Higher.Lens.coherent-lens
  }

-- The logical equivalence preserves getters and setters.

coherent⇔higher-preserves-getters-and-setters :
  {B : Set b}
  (bc : Block "conversion")
  (∥B∥→B : ∥ B ∥ → B) →
  Preserves-getters-and-setters-⇔ A B (coherent⇔higher bc ∥B∥→B)
coherent⇔higher-preserves-getters-and-setters b ∥B∥→B =
    Preserves-getters-and-setters-→-∘
      {f = →higher ∥B∥→B}
      {g = coherent→ b}
      (→higher-preserves-getters-and-setters ∥B∥→B)
      (coherent→-preserves-getters-and-setters b)
  , (λ _ → refl _ , refl _)

-- If B is inhabited when it is merely inhabited, then there is a
-- split surjection from Traditional.Coherent-lens A B to
-- Higher.Lens A B (assuming univalence).

coherent↠higher :
  {A : Set a} {B : Set b} →
  Block "conversion" →
  Univalence (a ⊔ b) →
  (∥ B ∥ → B) →
  Traditional.Coherent-lens A B ↠ Higher.Lens A B
coherent↠higher {A = A} {B = B} b univ ∥B∥→B = record
  { logical-equivalence = coherent⇔higher b ∥B∥→B
  ; right-inverse-of    = λ l →
      Higher.lenses-equal-if-setters-equal univ _ _ (λ _ → ∥B∥→B) $
      proj₂ (proj₁ (coherent⇔higher-preserves-getters-and-setters
                      b ∥B∥→B)
               _)
  }

-- The split surjection preserves getters and setters.

coherent↠higher-preserves-getters-and-setters :
  {A : Set a} {B : Set b}
  (bc : Block "conversion")
  (univ : Univalence (a ⊔ b))
  (∥B∥→B : ∥ B ∥ → B) →
  Preserves-getters-and-setters-⇔ A B
    (_↠_.logical-equivalence (coherent↠higher bc univ ∥B∥→B))
coherent↠higher-preserves-getters-and-setters b _ ∥B∥→B =
  coherent⇔higher-preserves-getters-and-setters b ∥B∥→B

------------------------------------------------------------------------
-- Composition

-- A lemma used to define composition.

∘⁻¹≃ :
  Block "∘⁻¹≃" →
  (f : B → C) (g : A → B) →
  f ⊚ g ⁻¹ z ≃ ∃ λ ((y , _) : f ⁻¹ z) → g ⁻¹ y
∘⁻¹≃ {z = z} ⊠ f g =
  f ⊚ g ⁻¹ z                                  ↔⟨⟩
  (∃ λ a → f (g a) ≡ z)                       ↔⟨ (∃-cong λ _ → ∃-intro _ _) ⟩
  (∃ λ a → ∃ λ y → f y ≡ z × y ≡ g a)         ↔⟨ (∃-cong λ _ → Σ-assoc) ⟩
  (∃ λ a → ∃ λ ((y , _) : f ⁻¹ z) → y ≡ g a)  ↔⟨ ∃-comm ⟩
  (∃ λ ((y , _) : f ⁻¹ z) → ∃ λ a → y ≡ g a)  ↔⟨ (∃-cong λ _ → ∃-cong λ _ → ≡-comm) ⟩
  (∃ λ ((y , _) : f ⁻¹ z) → g ⁻¹ y)           □

-- Composition.

infixr 9 _∘_

_∘_ : Lens B C → Lens A B → Lens A C
l₁@(lens _ _ _ _) ∘ l₂@(lens _ _ _ _) = block λ b → _≃_.from Lens-as-Σ′
  ( get l₁ ⊚ get l₂
  , (λ c₁ c₂ →
       get l₁ ⊚ get l₂ ⁻¹ c₁                         ↝⟨ ∘⁻¹≃ b _ _ ⟩
       (∃ λ ((b , _) : get l₁ ⁻¹ c₁) → get l₂ ⁻¹ b)  ↝⟨ (Σ-cong (get⁻¹-constant l₁ c₁ c₂) λ p@(b , _) →
                                                         get⁻¹-constant l₂ b (proj₁ (get⁻¹-const l₁ c₁ c₂ p))) ⟩
       (∃ λ ((b , _) : get l₁ ⁻¹ c₂) → get l₂ ⁻¹ b)  ↝⟨ inverse $ ∘⁻¹≃ b _ _ ⟩□
       get l₁ ⊚ get l₂ ⁻¹ c₂                         □)
  , (λ c₁ c₂ c₃ p →
       _≃_.from (∘⁻¹≃ b _ _)
         (Σ-map (get⁻¹-const l₁ c₂ c₃)
            (λ {p@(b , _)} →
               get⁻¹-const l₂ b (proj₁ (get⁻¹-const l₁ c₂ c₃ p)))
            (_≃_.to (∘⁻¹≃ b _ _)
               (_≃_.from (∘⁻¹≃ b _ _)
                  (Σ-map (get⁻¹-const l₁ c₁ c₂)
                     (λ {p@(b , _)} →
                        get⁻¹-const l₂ b
                          (proj₁ (get⁻¹-const l₁ c₁ c₂ p)))
                     (_≃_.to (∘⁻¹≃ b _ _) p)))))                      ≡⟨ cong (λ x → _≃_.from (∘⁻¹≃ b _ _)
                                                                                (Σ-map (get⁻¹-const l₁ c₂ c₃)
                                                                                (λ {p@(b , _)} →
                                                                                get⁻¹-const l₂ b
                                                                                (proj₁ (get⁻¹-const l₁ c₂ c₃ p))) x)) $
                                                                         _≃_.right-inverse-of (∘⁻¹≃ b _ _) _ ⟩
       _≃_.from (∘⁻¹≃ b _ _)
         (Σ-map (get⁻¹-const l₁ c₂ c₃)
            (λ {p@(b , _)} →
               get⁻¹-const l₂ b (proj₁ (get⁻¹-const l₁ c₂ c₃ p)))
            (Σ-map (get⁻¹-const l₁ c₁ c₂)
               (λ {p@(b , _)} →
                  get⁻¹-const l₂ b (proj₁ (get⁻¹-const l₁ c₁ c₂ p)))
               (_≃_.to (∘⁻¹≃ b _ _) p)))                              ≡⟨⟩

       _≃_.from (∘⁻¹≃ b _ _)
         (Σ-map (get⁻¹-const l₁ c₂ c₃ ⊚ get⁻¹-const l₁ c₁ c₂)
            (λ {p@(b , _)} →
               get⁻¹-const l₂ (proj₁ (get⁻¹-const l₁ c₁ c₂ p))
                 (proj₁ (get⁻¹-const l₁ c₂ c₃
                           (get⁻¹-const l₁ c₁ c₂ p))) ⊚
               get⁻¹-const l₂ b (proj₁ (get⁻¹-const l₁ c₁ c₂ p)))
            (_≃_.to (∘⁻¹≃ b _ _) p))                                  ≡⟨ cong (λ f → _≃_.from (∘⁻¹≃ b _ _)
                                                                                (Σ-map (get⁻¹-const l₁ c₂ c₃ ⊚ get⁻¹-const l₁ c₁ c₂)
                                                                                (λ {p} → f {p})
                                                                                (_≃_.to (∘⁻¹≃ b _ _) p))) $
                                                                         (implicit-extensionality ext λ p →
                                                                          ⟨ext⟩ (get⁻¹-const-∘ l₂ _ (proj₁ (get⁻¹-const l₁ c₁ c₂ p)) _)) ⟩
       _≃_.from (∘⁻¹≃ b _ _)
         (Σ-map (get⁻¹-const l₁ c₂ c₃ ⊚ get⁻¹-const l₁ c₁ c₂)
            (λ {p@(b , _)} →
               get⁻¹-const l₂ b
                 (proj₁ (get⁻¹-const l₁ c₂ c₃
                           (get⁻¹-const l₁ c₁ c₂ p))))
            (_≃_.to (∘⁻¹≃ b _ _) p))                                  ≡⟨ cong (λ f → _≃_.from (∘⁻¹≃ b _ _)
                                                                                (Σ-map f (λ {p@(b , _)} → get⁻¹-const l₂ b (proj₁ (f p)))
                                                                                (_≃_.to (∘⁻¹≃ b _ _) p))) $
                                                                         ⟨ext⟩ (get⁻¹-const-∘ l₁ _ _ _) ⟩∎
       _≃_.from (∘⁻¹≃ b _ _)
         (Σ-map (get⁻¹-const l₁ c₁ c₃)
            (λ {p@(b , _)} →
               get⁻¹-const l₂ b (proj₁ (get⁻¹-const l₁ c₁ c₃ p)))
            (_≃_.to (∘⁻¹≃ b _ _) p))                                  ∎)
  )
  where
  open Lens

-- The setter of the resulting lens is defined in the "right" way.

set-∘≡ :
  (l₁ : Lens B C) (l₂ : Lens A B) →
  Lens.set (l₁ ∘ l₂) a c ≡
  Lens.set l₂ a (Lens.set l₁ (Lens.get l₂ a) c)
set-∘≡ {a = a} {c = c} l₁@(lens _ _ _ _) l₂@(lens _ _ _ _) =
  proj₁ (get⁻¹-const l₂ (get l₂ a)
           (proj₁ (get⁻¹-const l₁ c′ c
                     ( get l₂ a
                     , _↔_.to (subst (λ b → get l₁ b ≡ c′ ↔ c′ ≡ c′)
                                 (refl _) F.id)
                         (refl _))
                     ))
           (a , sym (refl _)))                                        ≡⟨ cong₂ (λ f eq → proj₁ (get⁻¹-const l₂ _
                                                                                (proj₁ (get⁻¹-const l₁ _ _
                                                                                (_ , _↔_.to f (refl _)))) (_ , eq)))
                                                                           (subst-refl _ _)
                                                                           sym-refl ⟩
  proj₁ (get⁻¹-const l₂ (get l₂ a)
           (proj₁ (get⁻¹-const l₁ c′ c (get l₂ a , refl _)))
           (a , refl _))                                              ≡⟨⟩

  set l₂ a (set l₁ (get l₂ a) c)                                      ∎
  where
  open Lens

  c′ = get l₁ (get l₂ a)

-- Composition for higher lenses, defined under the assumption that
-- the resulting codomain is inhabited if it is merely inhabited.

infix 9 ⟨_⟩_⊚_

⟨_⟩_⊚_ :
  (∥ C ∥ → C) →
  Higher.Lens B C → Higher.Lens A B → Higher.Lens A C
⟨_⟩_⊚_ {C = C} {B = B} {A = A} ∥C∥→C = curry (
  Higher.Lens B C × Higher.Lens A B  ↝⟨ Σ-map higher→ higher→ ⟩
  Lens B C × Lens A B                ↝⟨ uncurry _∘_ ⟩
  Lens A C                           ↝⟨ →higher ∥C∥→C ⟩□
  Higher.Lens A C                    □)

-- The setter of the resulting lens is defined in the "right" way.

set-⊚≡ :
  ∀ ∥C∥→C (l₁ : Higher.Lens B C) (l₂ : Higher.Lens A B) →
  Higher.Lens.set (⟨ ∥C∥→C ⟩ l₁ ⊚ l₂) a c ≡
  Higher.Lens.set l₂ a (Higher.Lens.set l₁ (Higher.Lens.get l₂ a) c)
set-⊚≡ {a = a} {c = c} ∥C∥→C l₁ l₂ =
  set (⟨ ∥C∥→C ⟩ l₁ ⊚ l₂) a c                                   ≡⟨ cong (λ f → f a c) $ proj₂ $
                                                                   →higher-preserves-getters-and-setters ∥C∥→C (higher→ l₁ ∘ higher→ l₂) ⟩

  Lens.set (higher→ l₁ ∘ higher→ l₂) a c                        ≡⟨ set-∘≡ (higher→ l₁) (higher→ l₂) ⟩

  Lens.set (higher→ l₂) a
    (Lens.set (higher→ l₁) (Lens.get (higher→ l₂) a) c)         ≡⟨ cong (λ f → Lens.set (higher→ l₂) a (Lens.set (higher→ l₁) (f a) c)) $ proj₁ $
                                                                   higher→-preserves-getters-and-setters l₂ ⟩

  Lens.set (higher→ l₂) a (Lens.set (higher→ l₁) (get l₂ a) c)  ≡⟨ cong (λ f → Lens.set (higher→ l₂) a (f (get l₂ a) c)) $ proj₂ $
                                                                   higher→-preserves-getters-and-setters l₁ ⟩

  Lens.set (higher→ l₂) a (set l₁ (get l₂ a) c)                 ≡⟨ cong (λ f → f a (set l₁ (get l₂ a) c)) $ proj₂ $
                                                                   higher→-preserves-getters-and-setters l₂ ⟩∎
  set l₂ a (set l₁ (get l₂ a) c)                                ∎
  where
  open Higher.Lens

-- The implementation of composition for higher lenses given above
-- matches the one in Higher when both are defined (assuming
-- univalence).

⊚≡∘ :
  ∀ a b {A : Set (a ⊔ b ⊔ c)} {B : Set (b ⊔ c)} {C : Set c} →
  Univalence (a ⊔ b ⊔ c) →
  (∥C∥→C : ∥ C ∥ → C) →
  ⟨_⟩_⊚_ {B = B} {A = A} ∥C∥→C ≡
  Higher.Lens-combinators.⟨ a , b ⟩_∘_
⊚≡∘ a b {A = A} {B = B} {C = C} univ ∥C∥→C =
  Higher.Lens-combinators.composition≡∘
    a b univ ∥C∥→C ⟨ ∥C∥→C ⟩_⊚_
    (λ l₁ l₂ _ _ → set-⊚≡ ∥C∥→C l₁ l₂)

max_stars_repo_name: Saizan/dependent-lenses

max_issues_repo_name: Saizan/dependent-lenses

max_forks_repo_name: Saizan/dependent-lenses


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Join where

open import Cubical.HITs.Join.Base public

-- open import Cubical.HITs.Join.Properties public

ext: agda

max_stars_repo_name: loic-p/cubical

max_issues_repo_name: loic-p/cubical

max_forks_repo_name: loic-p/cubical


text:
-- imports
open import Data.Nat as ℕ     using (ℕ; suc; zero; _+_; _∸_)
open import Data.Vec as Vec   using (Vec; _∷_; []; tabulate; foldr)
open import Data.Fin as Fin   using (Fin; suc; zero)
open import Function          using (_∘_; const; id)
open import Data.List as List using (List; _∷_; [])
open import Data.Maybe        using (Maybe; just; nothing)

-- Without square cutoff optimization
module Simple where
  primes : ∀ n → List (Fin n)
  primes zero = []
  primes (suc zero) = []
  primes (suc (suc zero)) = []
  primes (suc (suc (suc m))) = sieve (tabulate (just ∘ suc))
    where
    sieve : ∀ {n} → Vec (Maybe (Fin (2 + m))) n → List (Fin (3 + m))
    sieve [] = []
    sieve (nothing ∷ xs) =         sieve xs
    sieve (just x  ∷ xs) = suc x ∷ sieve (foldr B remove (const []) xs x)
      where
      B = λ n → ∀ {i} → Fin i → Vec (Maybe (Fin (2 + m))) n

      remove : ∀ {n} → Maybe (Fin (2 + m)) → B n → B (suc n)
      remove _ ys zero    = nothing ∷ ys x
      remove y ys (suc z) = y       ∷ ys z

-- With square cutoff optimization
module SquareOpt where
  primes : ∀ n → List (Fin n)
  primes zero = []
  primes (suc zero) = []
  primes (suc (suc zero)) = []
  primes (suc (suc (suc m))) = sieve 1 m (Vec.tabulate (just ∘ Fin.suc ∘ Fin.suc))
    where
    sieve : ∀ {n} → ℕ → ℕ → Vec (Maybe (Fin (3 + m))) n → List (Fin (3 + m))
    sieve _ zero = List.mapMaybe id ∘ Vec.toList
    sieve _ (suc _) [] = []
    sieve i (suc l) (nothing ∷ xs) =     sieve (suc i) (l ∸ i ∸ i) xs
    sieve i (suc l) (just x  ∷ xs) = x ∷ sieve (suc i) (l ∸ i ∸ i) (Vec.foldr B remove (const []) xs i)
      where
      B = λ n → ℕ → Vec (Maybe (Fin (3 + m))) n

      remove : ∀ {i} → Maybe (Fin (3 + m)) → B i → B (suc i)
      remove _ ys zero    = nothing ∷ ys i
      remove y ys (suc j) = y       ∷ ys j

max_issues_repo_name: seanwallawalla-forks/RosettaCodeData

max_forks_repo_name: seanwallawalla-forks/RosettaCodeData


text:
-- Andreas, 2020-09-28, issue #4950
-- Ranges for missing definitions should not include
-- non-missing definitions.

A B C : Set₁  -- only B should be highlighted

A = Set
C = Set

-- The following names are declared but not accompanied by a
-- definition: B

-- Error range was:
-- line,3-13

-- The error range should not include C nor Set₁.
-- line,3-4

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


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

module Dodo.Binary.Filter where

-- Stdlib imports
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; _≢_; refl; subst; cong; cong₂) renaming (sym to ≡-sym; trans to ≡-trans)
open import Level using (Level; _⊔_)
open import Data.Empty using (⊥)
open import Data.Product using (∃-syntax; _,_)
open import Relation.Unary using (Pred; _∈_)
open import Relation.Binary using (Rel; Transitive)
open import Relation.Binary.Construct.Closure.Transitive using (TransClosure; [_]; _∷_)
-- Local imports
open import Dodo.Unary.Equality
open import Dodo.Unary.Unique
open import Dodo.Binary.Equality
open import Dodo.Binary.Transitive

-- # Definitions

-- | A value of type `A` with a proof that it satisfies the given predicate `P`.
--
--
-- # Design Decision: Alternative to `P x`
--
-- One might argue that a function could just as well take:
-- > f : {x : A} → P x → ...
--
-- In that case, the `with-pred` constructor adds nothing. However, crucially,
-- the inhabitant of `A` is /not/ included in the type signature of `WithPred`.
-- This means, a relation may be defined over elements of type `WithPred`.
-- While a relation /cannot/ be defined over elements of type `P x`, because
-- `x` varies.
data WithPred {a ℓ : Level} {A : Set a} (P : Pred A ℓ) : Set (a ⊔ ℓ) where
  with-pred : (x : A) → P x → WithPred P

-- | Helper for extracting element equality from an instance of `WithPred`.
--
-- This is tricky to unify otherwise in larger contexts, as `Px` and `Py` have
-- different /types/ when `x` and `y` are unequal.
with-pred-≡ : ∀ {a ℓ : Level} {A : Set a} {P : Pred A ℓ} {x y : A} {Px : P x} {Py : P y}
  → with-pred x Px ≡ with-pred y Py
    -------------------------------
  → x ≡ y
with-pred-≡ refl = refl

-- | Instances of `WithPred` are equal if they are defined over the same value,
-- and its predicate is unique.
with-pred-unique : ∀ {a ℓ : Level} {A : Set a} {P : Pred A ℓ}
  → UniquePred P
  → {x y : A}
  → x ≡ y
  → (Px : P x) (Py : P y)
    -------------------------------
  → with-pred x Px ≡ with-pred y Py
with-pred-unique uniqueP {x} refl Px Py = cong (with-pred x) (uniqueP _ Px Py)

with-pred-≢ : ∀ {a ℓ : Level} {A : Set a} {P : Pred A ℓ}
  → UniquePred P
  → {x y : A} {Px : P x} {Py : P y}
  → with-pred x Px ≢ with-pred y Py
    -------------------------------
  → x ≢ y
with-pred-≢ uniqueP Px≢Py x≡y = Px≢Py (with-pred-unique uniqueP x≡y _ _)

-- | A relation whose elements all satisfy `P`.
--
-- Note that this differs from defining:
-- > R ∩₂ ( P ×₂ P )
--
-- In that case, the type signature is still identical to the type signature of
-- `R` (except for the universe level). However, `filter-rel` alters the type,
-- which proves no other inhabitants can exist.
--
-- This is in particular useful for properties that are declared over an entire
-- relation (such as `Trichotomous`), while they should only hold over a subset
-- of it.
--
--
-- # Example
--
-- For instance, consider:
-- (1) > Trichotomous _≡_ (filter-rel P R)
-- and
-- (2) > Trichotomous _≡_ (R ∩₂ ( P ×₂ P ))
--
-- Where the corresponding types are:
-- > R : Rel A ℓzero
-- > P : Pred A ℓzero
--
-- The type of the relation in (1) is then:
-- > filter-rel P R : Rel (WithPred P) ℓzero
-- While the type of the relation in (2) is:
-- > (R ∩₂ (P ×₂ P)) : Rel A ℓzero
--
-- So, for (2), defining `Trichotomous` means that it finds an instance of
-- `P` for both elements, even when no such `P x` exists; Which leads to a
-- contradiction. Whereas (1) will only find the relation if `P` holds for both
-- elements.
--
-- Effectively, (2) implies:
-- > ∀ (x : A) → P x
--
-- Whereas (1) makes no such strong claims.
filter-rel : ∀ {a ℓ₁ ℓ₂ : Level} {A : Set a}
  → (P : Pred A ℓ₁)
  → Rel A ℓ₂
    -------------------
  → Rel (WithPred P) ℓ₂
filter-rel P R (with-pred x Px) (with-pred y Py) = R x y

-- | Effectively the inverse of `filter-rel`.
--
-- It loses the type-level restrictions, but preserves the restrictions on
-- value-level.
unfilter-rel : ∀ {a ℓ₁ ℓ₂ : Level} {A : Set a}
  → {P : Pred A ℓ₁}
  → Rel (WithPred P) ℓ₂
    -------------------
  → Rel A (ℓ₁ ⊔ ℓ₂)
unfilter-rel R x y = ∃[ Px ] ∃[ Py ] R (with-pred x Px) (with-pred y Py)

-- | Helper for unwrapping the value from the `with-pred` constructor.
un-with-pred : {a ℓ : Level} {A : Set a} {P : Pred A ℓ}
  → WithPred P
    ----------
  → A
un-with-pred (with-pred x _) = x

⁺-strip-filter : {a ℓ₁ ℓ₂ : Level} {A : Set a}
  → {P : Pred A ℓ₁}
  → {R : Rel A ℓ₂}
  → {x y : A}
  → {Px : P x} {Py : P y}
  → TransClosure (filter-rel P R) (with-pred x Px) (with-pred y Py)
    ---------------------------------------------------------------
  → TransClosure R x y
⁺-strip-filter [ x∼y ] = [ x∼y ]
⁺-strip-filter (_∷_ {_} {with-pred z Pz} Rxz R⁺zy) = Rxz ∷ ⁺-strip-filter R⁺zy

-- | Apply a relation filter to a chain /from right to left/.
--
-- This applies when a predicate `P x` is true whenever `R x y` and `P y` are true.
-- Then, for any chain where `P` holds for the final element, it holds for every
-- element in the chain.
⁺-filter-relˡ : {a ℓ₁ ℓ₂ : Level} {A : Set a} {P : Pred A ℓ₁} {R : Rel A ℓ₂}
  → (f : ∀ {x y : A} → P y → R x y → P x)
  → {x y : A}
  → (Px : P x) (Py : P y)
  → (R⁺xy : TransClosure R x y)
    ---------------------------------------------------------------
  → TransClosure (filter-rel P R) (with-pred x Px) (with-pred y Py)
⁺-filter-relˡ f Px Py [ Rxy ]        = [ Rxy ]
⁺-filter-relˡ f Px Py ( Rxz ∷ R⁺zy ) = Rxz ∷ ⁺-filter-relˡ f (⁺-predˡ f R⁺zy Py) Py R⁺zy

-- | Apply a relation filter to a chain /from left to right/.
--
-- This applies when a predicate `P y` is true whenever `R x y` and `P x` are true.
-- Then, for any chain where `P` holds for the first element, it holds for every
-- element in the chain.
⁺-filter-relʳ : {a ℓ₁ ℓ₂ : Level} {A : Set a} {P : Pred A ℓ₁} {R : Rel A ℓ₂}
  → (f : ∀ {x y : A} → P x → R x y → P y)
  → {x y : A}
  → (Px : P x) (Py : P y)
  → (R⁺xy : TransClosure R x y)
    ---------------------------------------------------------------
  → TransClosure (filter-rel P R) (with-pred x Px) (with-pred y Py)
⁺-filter-relʳ f Px Py [ Rxy ]        = [ Rxy ]
⁺-filter-relʳ f Px Py ( Rxz ∷ R⁺zy ) = Rxz ∷ ⁺-filter-relʳ f (f Px Rxz) Py R⁺zy

-- # Properties

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a} {P : Pred A ℓ₁} {Q : Pred A ℓ₂} where

  with-pred-⊆₁ :
      P ⊆₁ Q
    → WithPred P
      ----------
    → WithPred Q
  with-pred-⊆₁ P⊆Q (with-pred x Px) = with-pred x (⊆₁-apply P⊆Q Px)

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

  filter-rel-⊆₂ :
      (R : Rel A ℓ₁)
    → {P : Pred A ℓ₂}
      ----------------------------------
    → unfilter-rel (filter-rel P R) ⊆₂ R
  filter-rel-⊆₂ R {P} = ⊆: ⊆-proof
    where
    ⊆-proof : unfilter-rel (filter-rel P R) ⊆₂' R
    ⊆-proof _ _ (_ , _ , Rxy) = Rxy

module _ {a ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {P : Pred A ℓ₁} {Q : Pred A ℓ₂} {R : Rel A ℓ₃} where

  filter-rel-preserves-⊆₁ :
      P ⊆₁ Q
      --------------------------------------------------------------
    → unfilter-rel (filter-rel P R) ⊆₂ unfilter-rel (filter-rel Q R)
  filter-rel-preserves-⊆₁ P₁⊆P₂ = ⊆: lemma
    where
    lemma : unfilter-rel (filter-rel P R) ⊆₂' unfilter-rel (filter-rel Q R)
    lemma _ _ (P₁x , P₁y , Qxy) = (⊆₁-apply P₁⊆P₂ P₁x , ⊆₁-apply P₁⊆P₂ P₁y , Qxy)

  -- |
  --
  -- Note that this does /not/ hold in general for subsets of relations.
  -- That is, the following does /not/ hold:
  -- > Q ⊆₂ R → Transitive R → Transitive Q
  --
  -- After all, if `Q x y` and `Q y z` hold, then `R x y` and `R y z` hold,
  -- then `R x z` holds. However, it does not mean that `Q x z` holds.
  trans-filter-rel-⊆₁ :
      P ⊆₁ Q
    → Transitive (filter-rel Q R)
      ---------------------------
    → Transitive (filter-rel P R)
  trans-filter-rel-⊆₁ P⊆Q transQR {Pi} {Pj} {Pk} Rij Rjk =
    let Qi = with-pred-⊆₁ P⊆Q Pi
        Qj = with-pred-⊆₁ P⊆Q Pj
        Qk = with-pred-⊆₁ P⊆Q Pk
    in Q⇒P {Pi} {Pk} (transQR {Qi} {Qj} {Qk} (P⇒Q {Pi} {Pj} Rij) (P⇒Q {Pj} {Pk} Rjk))
    where
    P⇒Q : ∀ {x y : WithPred P} → filter-rel P R x y → filter-rel Q R (with-pred-⊆₁ P⊆Q x) (with-pred-⊆₁ P⊆Q y)
    P⇒Q {with-pred _ _} {with-pred _ _} Rxy = Rxy

    Q⇒P : ∀ {x y : WithPred P} → filter-rel Q R (with-pred-⊆₁ P⊆Q x) (with-pred-⊆₁ P⊆Q y) → filter-rel P R x y
    Q⇒P {with-pred _ _} {with-pred _ _} Rxy = Rxy

module _ {a ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {P : Pred A ℓ₁} {R : Rel A ℓ₂} {Q : Rel A ℓ₃} where

  filter-rel-preserved-⊆₂ :
      R ⊆₂ Q
      --------------------------------------------------------------
    → unfilter-rel (filter-rel P R) ⊆₂ unfilter-rel (filter-rel P Q)
  filter-rel-preserved-⊆₂ R⊆Q = ⊆: lemma
    where
    lemma : unfilter-rel (filter-rel P R) ⊆₂' unfilter-rel (filter-rel P Q)
    lemma x y (Px , Py , Rxy) = Px , Py , ⊆₂-apply R⊆Q Rxy

-- # Operations

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a} {R : Rel A ℓ₁} {P : Pred A ℓ₂} {x y : A} where

  filter-rel-dom :
      unfilter-rel (filter-rel P R) x y
      ---------------------------------
    → x ∈ P
  filter-rel-dom (Px , Py , Rxy) = Px

  filter-rel-codom :
      unfilter-rel (filter-rel P R) x y
      ---------------------------------
    → y ∈ P
  filter-rel-codom (Px , Py , Rxy) = Py

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
module _ where

open import DeadCodePatSyn.Lib

typeOf : {A : Set} → A → Set
typeOf {A} _ = A

-- Check that pattern synonyms count when computing dead code
f : typeOf not-hidden → Set₁
f not-hidden = Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Hide where

record 𝔹ottom : Set₁ where
  field
    ⊥ : Set

open 𝔹ottom ⦃ … ⦄ public

𝔹ottomPrelude : 𝔹ottom
𝔹ottomPrelude = record { ⊥ = P.⊥ } where
  open import Prelude.Empty as P

instance instance𝔹ottom : 𝔹ottom
instance𝔹ottom = 𝔹ottomPrelude


text:
module All where

import Prelude
import Star
import Nat
import List
import Vec
import Elem
import Fin
import Modal
import Lambda
import Span
import MapTm
import Examples


text:
-- Andreas, 2020-12-15, re PR #5020
-- Test error message "Must not specify multiple frontends"

-- See respective .flags file

-- Expected error:
-- Must not specify multiple frontends (--interaction, --interaction-json)


text:
{- reported by Guillaume Brunerie on 2015-09-17 -}

{-# OPTIONS --rewriting #-}

data _==_ {A : Set} (a : A) : A → Set where
  idp : a == a
{-# BUILTIN REWRITE _==_ #-}

postulate
  A B : Set
  f g : A → B

module M (x : A) where

  postulate
    rx : f x == g x
  {-# REWRITE rx #-}

  -- This shouldn't work
  test : (y : A) → f y == g y
  test y = idp


text:
module NF {A : Set} where

open import Relation.Binary.PropositionalEquality

record Sing (a : A) : Set where
  field
    unpack : A
    eq : unpack ≡ a

{-# INLINE Sing.unpack #-}

record NF (v : A) : Set where
  field !! : Sing v

{-# INLINE NF.!! #-}

open NF {{...}}

open import Function.Reasoning

nf : (v : A){{nfv : NF v}} -> A
nf v = Sing.unpack (!! ∶ Sing v)

{-# INLINE nf #-}

nf≡ : {v : A}{{nfv : NF v}} -> nf v ≡ v
nf≡ = Sing.eq !!

max_stars_repo_name: yanok/normalize-via-instances

max_issues_repo_name: yanok/normalize-via-instances

max_forks_repo_name: yanok/normalize-via-instances


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Functor.Construction.Constant where

open import Level

open import Categories.Category
open import Categories.Category.Instance.One
open import Categories.Category.Product
open import Categories.Functor renaming (id to idF)
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e : Level
    C D : Category o ℓ e

const : (d : Category.Obj D) → Functor C D
const {D = D} d = record
  { F₀           = λ _ → d
  ; F₁           = λ _ → id
  ; identity     = refl
  ; homomorphism = sym identity²
  ; F-resp-≈     = λ _ → refl
  }
  where open Category D
        open Equiv

const! : (d : Category.Obj D) → Functor (One {0ℓ} {0ℓ} {0ℓ}) D
const! = const

constˡ : (c : Category.Obj C) → Functor D (Product C D)
constˡ c = const c ※ idF

constʳ : (c : Category.Obj C) → Functor D (Product D C)
constʳ c = idF ※ (const c)

constNat : ∀ {A B} → Category._⇒_ D A B → NaturalTransformation (const {D = D} {C = C} A) (const B)
constNat {D = D} f = ntHelper record
  { η       = λ _ → f
  ; commute = λ _ → MR.id-comm D
  }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module Structure.Relator.Equivalence where

import      Lvl
open import Logic
open import Logic.Propositional
open import Structure.Relator.Properties
  hiding (reflexivity ; symmetry ; transitivity)
open import Type

private variable ℓ₁ ℓ₂ : Lvl.Level

-- An equivalence relation is a reflexive, symmetric and transitive relation.
record Equivalence {T : Type{ℓ₁}} (_≡_ : T → T → Stmt{ℓ₂}) : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
  instance constructor intro
  field
    instance ⦃ reflexivity ⦄  : Reflexivity  (_≡_)
    instance ⦃ symmetry ⦄     : Symmetry     (_≡_)
    instance ⦃ transitivity ⦄ : Transitivity (_≡_)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import HoTT
open import groups.Exactness
open import homotopy.CofiberSequence
open import cohomology.Theory

{- Finite additivity is provable (and in a stronger form) without using
 - the additivity axiom. We have

         Cⁿ(X ∨ Y) == Cⁿ(X) × Cⁿ(Y)

 - and over this path
 -   ∙ Cⁿ(winl) corresponds to fst : Cⁿ(X) × Cⁿ(Y) → Cⁿ(X),
 -   ∙ Cⁿ(winr) corresponds to snd : Cⁿ(X) × Cⁿ(Y) → Cⁿ(Y),
 -   ∙ Cⁿ(Wedge-rec winl* winr* wglue*) : Cⁿ(Z) → Cⁿ(X ∨ Y)
       corresponds to Cⁿ(winl*) × Cⁿ(winr*).
 -   ∙ Cⁿ(f) : Cⁿ(X ∨ Y) → Cⁿ(Z)
       corresponds to Cⁿ(projl ∘ f) + Cⁿ(projr ∘ f) : Cⁿ(X) × Cⁿ(Y) → Cⁿ(Z)
 -}

module cohomology.Wedge {i} (CT : CohomologyTheory i)
  (n : ℤ) (X Y : Ptd i) where

  open import homotopy.WedgeCofiber X Y

  open CohomologyTheory CT
  open import cohomology.PtdMapSequence CT

  private
    abstract
      βl : ∀ x → CEl-fmap n ⊙winl (CEl-fmap n (⊙projl X Y) x) == x
      βl = CEl-fmap-inverse n ⊙winl (⊙projl X Y) λ _ → idp

      βr : ∀ y → CEl-fmap n ⊙winr (CEl-fmap n (⊙projr X Y) y) == y
      βr = CEl-fmap-inverse n ⊙winr (⊙projr X Y) λ _ → idp

      C-projr-C-winl-is-exact : is-exact (C-fmap n (⊙projr X Y)) (C-fmap n ⊙winl)
      C-projr-C-winl-is-exact = equiv-preserves'-exact
        (C-comm-square n cfcod-winl-projr-comm-sqr)
        (C-comm-square n $ comm-sqr λ _ → idp)
        (snd (C-emap n CofWinl.⊙eq))
        (C-isemap n (⊙idf _) (idf-is-equiv _))
        (C-isemap n (⊙idf _) (idf-is-equiv _))
        (C-exact n ⊙winl)

      C-projl-C-winr-is-exact : is-exact (C-fmap n (⊙projl X Y)) (C-fmap n ⊙winr)
      C-projl-C-winr-is-exact = equiv-preserves'-exact
        (C-comm-square n cfcod-winr-projl-comm-sqr)
        (C-comm-square n $ comm-sqr λ _ → idp)
        (snd (C-emap n CofWinr.⊙eq))
        (C-isemap n (⊙idf _) (idf-is-equiv _))
        (C-isemap n (⊙idf _) (idf-is-equiv _))
        (C-exact n ⊙winr)

  import groups.ProductRepr
    (C-fmap n (⊙projl X Y)) (C-fmap n (⊙projr X Y))
    (C-fmap n ⊙winl) (C-fmap n ⊙winr) βl βr
    C-projl-C-winr-is-exact
    C-projr-C-winl-is-exact as PR

  C-Wedge : C n (X ⊙∨ Y) ≃ᴳ C n X ×ᴳ C n Y
  C-Wedge = PR.iso

{-
  ⊙Wedge-rec-over : {Z : Ptd i} (winl* : X ⊙→ Z) (winr* : Y ⊙→ Z)
    → CF-hom n (⊙Wedge-rec winl* winr*)
      == ×ᴳ-fanout (CF-hom n winl*) (CF-hom n (winr*))
      [ (λ K → C n Z →ᴳ K) ↓ path ]
  ⊙Wedge-rec-over winl* winr* = codomain-over-iso $
    codomain-over-equiv (CF n R.⊙f) _
    ▹ ap2 (λ f g z → (f z , g z))
          (ap GroupHom.f $ ! (CF-comp n R.⊙f ⊙winl) ∙ ap (CF-hom n) R.⊙winl-β)
          (ap GroupHom.f $ ! (CF-comp n R.⊙f ⊙winr) ∙ ap (CF-hom n) R.⊙winr-β)
    where
    module R = ⊙WedgeRec winl* winr*

  Wedge-hom-η : {Z : Ptd i} (φ : C n (⊙Wedge X Y) →ᴳ C n Z)
    → φ == ×ᴳ-fanin (C-is-abelian n _) (φ ∘ᴳ CF-hom n (⊙projl X Y))
                                       (φ ∘ᴳ CF-hom n (⊙projr X Y))
      [ (λ G → G →ᴳ C n Z) ↓ path ]
  Wedge-hom-η φ =
    lemma (C-is-abelian n _) (C-is-abelian n _) inl-over inr-over
    where
    lemma : {G H K L : Group i}
      (aG : is-abelian G) (aL : is-abelian L) {p : G == H ×ᴳ K}
      {φ : H →ᴳ G} {ψ : K →ᴳ G} {χ : G →ᴳ L}
      → φ == ×ᴳ-inl [ (λ J → H →ᴳ J) ↓ p ]
      → ψ == ×ᴳ-inr {G = H} [ (λ J → K →ᴳ J) ↓ p ]
      → χ == ×ᴳ-fanin aL (χ ∘ᴳ φ) (χ ∘ᴳ ψ) [ (λ J → J →ᴳ L) ↓ p ]
    lemma {H = H} {K = K} aG aL {p = idp} {χ = χ} idp idp =
      ap (λ α → χ ∘ᴳ α) (×ᴳ-fanin-η H K aG)
      ∙ ! (×ᴳ-fanin-pre∘ aG aL χ (×ᴳ-inl {G = H}) (×ᴳ-inr {G = H}))

  Wedge-in-over : {Z : Ptd i} (f : Z ⊙→ ⊙Wedge X Y)
    → CF-hom n f
      == ×ᴳ-fanin (C-is-abelian n _) (CF-hom n (⊙projl X Y ⊙∘ f))
                                     (CF-hom n (⊙projr X Y ⊙∘ f))
      [ (λ G → G →ᴳ C n Z) ↓ path ]
  Wedge-in-over f =
    Wedge-hom-η (CF-hom n f)
    ▹ ap2 (×ᴳ-fanin (C-is-abelian n _))
        (! (CF-comp n (⊙projl X Y) f))
        (! (CF-comp n (⊙projr X Y) f))
-}

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
-- Test case extracted from The Agda standard library
-- Properties related to Any

{-# OPTIONS --show-implicit #-}

module ProjectionNotNormalized where

open import Common.Level renaming (lsuc to suc)

record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infix 4 _≈_
  field
    Carrier       : Set c
    _≈_           : Carrier → Carrier → Set ℓ
    refl          : ∀ {x} → x ≈ x

open import Common.Equality

setoid : ∀ {a} → Set a → Setoid _ _
setoid A = record
  { Carrier       = A
  ; _≈_           = _≡_
  ; refl          = refl
  }

infixr 4 _,_

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public

∃ : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
∃ = Σ _

pmap : ∀ {a b p q}
         {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q} →
       (f : A → B) → (∀ {x} → P x → Q (f x)) →
       Σ A P → Σ B Q
pmap f g (x , y) = (f x , g y)

data List {a} (A : Set a) : Set a where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A

-- Any P xs means that at least one element in xs satisfies P.

data Any {a p} {A : Set a}
         (P : A → Set p) : List A → Set (a ⊔ p) where
  here  : ∀ {x xs} (px  : P x)      → Any P (x ∷ xs)
  there : ∀ {x xs} (pxs : Any P xs) → Any P (x ∷ xs)

-- Map.

map : ∀ {a p q} {A : Set a} {P : A → Set p} → {Q : A → Set q} →
      (∀ {x} → P x → Q x) → ∀ {x} → Any P x → Any Q x
map g (here px)   = here (g px)
map g (there pxs) = there (map g pxs)

------------------------------------------------------------------------
-- List membership and some related definitions

module Membership {c ℓ : Level} (S : Setoid c ℓ) where

  open module S = Setoid S using (_≈_) renaming (Carrier to A)

  -- List membership.

  infix 4 _∈_

  _∈_ : A → List A → Set _
  x ∈ xs = Any (_≈_ x) xs

  -- Finds an element satisfying the predicate.

  find : ∀ {p} {P : A → Set p} {xs} →
         Any P xs → ∃ λ x → Σ (x ∈ xs) λ _ → P x
  find (here px)   = (_ , here S.refl , px)
  find (there pxs) = pmap (λ x → x) (pmap there (λ x → x)) (find pxs)

  lose : ∀ {p} {P : A → Set p} {x xs} →
         (resp : ∀ {x y} → x ≈ y → P x → P y) →
         x ∈ xs → P x → Any P xs
  lose resp x∈xs px = map (λ eq → resp eq px) x∈xs

-- The code above instantiated (and slightly changed) for
-- propositional equality, along with some additional definitions.

open module M {a} {A : Set a} = Membership (setoid A)
  hiding (lose)

lose : ∀ {a p} {A : Set a} {P : A → Set p} {x xs} →
       x ∈ xs → P x → Any P xs
lose {P = P} = M.lose (subst P)

------------------------------------------------------------------------
-- Some lemmas related to map, find and lose

-- Lemmas relating map and find.

find∘map : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q}
           {xs : List A} (p : Any P xs) (f : ∀ {x} → P x → Q x) →
           find (map f p) ≡ pmap (λ x → x) (pmap (λ x → x) f) (find p)
find∘map (here  p) f = refl
find∘map (there p) f rewrite find∘map p f = refl

-- find satisfies a simple equality when the predicate is a
-- propositional equality.

find-∈ : ∀ {a} {A : Set a} {x : A} {xs : List A} (x∈xs : x ∈ xs) →
         find x∈xs ≡ (x , x∈xs , refl)
find-∈ (here refl)  = refl
find-∈ (there x∈xs) rewrite find-∈ x∈xs = refl

-- find and lose are inverses (more or less).

{-
find∘lose : ∀ {a p} {A : Set a} (P : A → Set p)
            {x : {!!}} {xs : List {!!}}
            (x∈xs : x ∈ xs) (pp : P x) →
            find {P = P} (lose x∈xs pp) ≡ (x , x∈xs , pp)
find∘lose P x∈xs p = {!!}
-}
find∘lose : ∀ {a p} {A : Set a} (P : A → Set p)
            {x : _} {xs : _}
            (x∈xs : x ∈ xs) (pp : P x) →
            find {P = P} (lose x∈xs pp) ≡ (x , x∈xs , pp)
find∘lose P x∈xs p
  rewrite find∘map x∈xs (λ y → subst P y p)
        | find-∈ x∈xs
        = refl

{- Problem WAS:

applySection
new  = ProjectionNotNormalized.Membership.S
ptel = EmptyTel
old  = ProjectionNotNormalized.Setoid
ts   = [[]r{Var 2 []},[]r{Var 1 []},[]r(Var 0 [])]
S.refl  :  {c ℓ : Level} (S : Setoid c ℓ) {x : Setoid.Carrier S} →
           (S Setoid.≈ x) x
 is projection like in argument 2 for type ProjectionNotNormalized.Setoid
A  :  {c ℓ : Level} (S : Setoid c ℓ) → Set c
 is projection like in argument 2 for type ProjectionNotNormalized.Setoid
_≈_  :  {c ℓ : Level} (S : Setoid c ℓ) →
        Setoid.Carrier S → Setoid.Carrier S → Set ℓ
 is projection like in argument 2 for type ProjectionNotNormalized.Setoid
applySection
new  = ProjectionNotNormalized.M
ptel = ExtendTel []r{El {getSort = Type (Max [Plus 0 (MetaLevel _224 [])]), unEl = MetaV _225 []}} (Abs "a" ExtendTel []r{El {getSort = Type (Max [Plus 1 (NeutralLevel (Var 0 []))]), unEl = Sort (Type (Max [Plus 0 (NeutralLevel (Var 0 []))]))}} (Abs "A" EmptyTel))
old  = ProjectionNotNormalized.Membership
ts   = [[]r{Var 1 []},[]r{Var 1 []},[]r(Def ProjectionNotNormalized.setoid [Apply []r{Var 1 []},Apply []r(Var 0 [])])]
conApp: constructor ProjectionNotNormalized.recCon-NOT-PRINTED with fields [ProjectionNotNormalized.Setoid.Carrier,ProjectionNotNormalized.Setoid._≈_,ProjectionNotNormalized.Setoid.refl] projected by ProjectionNotNormalized.Membership.S.Carrier
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Substitute.hs:82
-}

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.ImplShared.Consensus.Types.EpochIndep
open import Optics.All
open import Util.ByteString
open import Util.Encode
open import Util.Hash
open import Util.Lemmas
open import Util.PKCS
open import Util.Prelude

-- This module postulates a collision-resistant cryptographic hash
-- function (we call it sha256 for concreteness, but it could be any
-- collision-resistant cryptographic hash function), and defines hash
-- functions used in (an earlier version of) LibraBFT, properties
-- about it, and how Votes and Blocks are signed.

module LibraBFT.ImplShared.Util.Crypto where
  -- Note that this is an abstraction of a hash function.  It could be any such hash function, not
  -- necessarily sha256.  We just call it sha256 for "concreteness", to remind ourselves it's
  -- modeling such a function.
  postulate -- valid assumption (hash function)
    sha256    : BitString → Hash

  -- For two values x and y, if their hashes are equal, then either there is a hash collision, or x
  -- and y are equal.
  sha256-cr : ∀{x y} → sha256 x ≡ sha256 y → Collision sha256 x y ⊎ x ≡ y
  sha256-cr {x} {y} hyp
     with x ≟BitString y
  ...| no  col  = inj₁ (col , hyp)
  ...| yes refl = inj₂ refl

  open WithCryptoHash sha256 sha256-cr

  -- We do not yet have sufficient support to model precisely the hashing used in the Haskell code,
  -- so it is better that we postulate its intended properties to ensure proofs have the desired
  -- properties available.  Note that a simpler injectivity property such as
  --
  -- hashBD-inj' : ∀ {bd1} {bd2}
  --             → hashBD bd1 ≡ hashBD bd2
  --             → NonInjective-≡ sha256
  --             ⊎ bd1 ≡L bd2
  --
  -- does *not* hold because the input to the hash function used in hashBD does *not* include all
  -- components of the BlockData being hashed.

  -- TODO-2: Similarly express other hashing functions and their intended injectivity properties where
  -- the Agda implementation does not accurately reflect the Haskell implementation.

  -- TODO-2: Enable support for the hashS function we use in the Haskell code, which hashes tuples
  -- of serializable types), and then define hashBD using this and prove that it ensures hashBD-inj.
  -- Note also the TODO below related to HashTags.

  record _BlockDataInjectivityProps_ (bd1 bd2 : BlockData) : Set where
    constructor mkBdInjProps
    field
      bdInjEpoch  : bd1 ≡L bd2 at bdEpoch
      bdInjRound  : bd1 ≡L bd2 at bdRound
      bdInjVD     : bd1 ≡L bd2 at (bdQuorumCert ∙ qcVoteData)
      bdInjLI     : bd1 ≡L bd2 at (bdQuorumCert ∙ qcSignedLedgerInfo ∙ liwsLedgerInfo)
      bdInjBTNil  : bd1 ^∙ bdBlockType ≡ NilBlock → bd2 ^∙ bdBlockType ≡ NilBlock
      bdInjBTGen  : bd1 ^∙ bdBlockType ≡ Genesis  → bd2 ^∙ bdBlockType ≡ Genesis
      bdInjBTProp : ∀ {tx}{auth} → bd1 ^∙ bdBlockType ≡ Proposal tx auth
                                 → bd1 ^∙ bdBlockType ≡ bd2 ^∙ bdBlockType
  open _BlockDataInjectivityProps_

  sameBlockData⇒≈ : ∀ {b1 b2}
                    → b1 ^∙ bId ≡ b2 ^∙ bId
                    → (b1 ^∙ bBlockData) BlockDataInjectivityProps (b2 ^∙ bBlockData)
                    → b1 ≈Block b2
  sameBlockData⇒≈ {b1} {b2} refl (mkBdInjProps refl refl refl refl nil gen prop)
     with b1 ^∙ bBlockData ∙ bdBlockType
  ...| NilBlock         rewrite nil  refl = refl
  ...| Genesis          rewrite gen  refl = refl
  ...| Proposal tx auth rewrite prop refl = refl

  BSL : Set
  BSL = List ByteString

  _≟-BSL_ : ∀ (bsl1 bsl2 : List ByteString) → Dec (bsl1 ≡ bsl2)
  _≟-BSL_ = List-≡-dec _≟ByteString_

  hashBSL = sha256 ∘ bs-concat

  postulate  -- TODO-2: implement after adding support for "HashTag" (see below)
    blockData-bsl     : BlockData → List ByteString

  hashBD : BlockData → HashValue
  hashBD = hashBSL ∘ blockData-bsl

  Injective-BlockData : Set
  Injective-BlockData = Injective-int _BlockDataInjectivityProps_ hashBSL blockData-bsl blockData-bsl

  postulate  -- TODO-1: prove it using bs-concat-inj
    hashBD-inj : Injective-BlockData

  hashBlock : Block → HashValue
  hashBlock = hashBD ∘ (_^∙ bBlockData)

  blockInfoBSList : BlockInfo → List ByteString
  blockInfoBSList (BlockInfo∙new epoch round id execStId ver mes) =
    encode epoch ∷ encode round ∷ encode id ∷ encode execStId ∷ encode ver ∷ encode mes ∷ []

  hashBI : BlockInfo → HashValue
  hashBI = sha256 ∘ bs-concat ∘ blockInfoBSList

  hashBI-inj : ∀ {bi1 bi2} → hashBI bi1 ≡ hashBI bi2 → NonInjective-≡ sha256 ⊎ bi1 ≡ bi2
  hashBI-inj {bi1} {bi2} hyp with sha256-cr hyp
  ...| inj₁ col = inj₁ (_ , col)
  ...| inj₂ res with bs-concat-inj (blockInfoBSList bi1) (blockInfoBSList bi2) res
  ...| final = inj₂ (BlockInfo-η (encode-inj (proj₁ (∷-injective final)))
                                 (encode-inj (proj₁ (∷-injective (proj₂ (∷-injective final)))))
                                 (encode-inj (proj₁ (∷-injective (proj₂ (∷-injective (proj₂ (∷-injective final)))))))
                                 (encode-inj (proj₁ (∷-injective (proj₂ (∷-injective (proj₂ (∷-injective (proj₂ (∷-injective final)))))))))
                                 (encode-inj (proj₁ (∷-injective (proj₂ (∷-injective (proj₂ (∷-injective (proj₂ (∷-injective (proj₂ (∷-injective final)))))))))))
                                 (encode-inj (proj₁ (∷-injective (proj₂ (∷-injective (proj₂ (∷-injective (proj₂ (∷-injective (proj₂ (∷-injective (proj₂ (∷-injective final))))))))))))))

  voteDataHashList : VoteData → List Hash
  voteDataHashList (VoteData∙new proposed parent) =
    hProposed ∷ hParent ∷ []
   where
    hProposed = hashBI proposed
    hParent   = hashBI parent

  hashVD : VoteData → HashValue
  hashVD = hash-concat ∘ voteDataHashList

  VoteData-≢-eid : ∀ {vd1 vd2 : VoteData}
                 → vd1 ^∙ vdProposed ∙ biEpoch ≢ vd2 ^∙ vdProposed ∙ biEpoch
                 → vd1 ≢ vd2
  VoteData-≢-eid neq = λ x → neq (cong (_^∙ vdProposed ∙ biEpoch) x)

  VoteData-hb : ∀ {vd1 vd2 : VoteData}
              → vd1 ^∙ vdProposed ∙ biEpoch ≢ vd2 ^∙ vdProposed ∙ biEpoch
              → hashVD vd1 ≡ hashVD vd2
              → NonInjective-≡ sha256
  VoteData-hb {vd1} {vd2} neq hvd≡
    with hash-concat-inj {voteDataHashList vd1} {voteDataHashList vd2} hvd≡
  ...| inj₁ hb = hb
  ...| inj₂ xxx
     with cong head xxx
  ...| yyy
     with cong tail xxx
  ...| yyy'
     with cong head (just-injective yyy')
  ...| yyy''
     with just-injective yyy | just-injective yyy''
  ...| zzz | zzz'
     with hashBI-inj {vd1 ^∙ vdProposed} {vd2 ^∙ vdProposed} zzz |
          hashBI-inj {vd1 ^∙ vdParent}   {vd2 ^∙ vdParent}   zzz'
  ...| inj₁ hb  | _         = hb
  ...| inj₂ _   | inj₁ hb   = hb
  ...| inj₂ aaa | inj₂ aaa' = ⊥-elim (VoteData-≢-eid {vd1} {vd2} neq (VoteData-η aaa aaa'))

  hashVD-inj : ∀ {vd1 vd2} → hashVD vd1 ≡ hashVD vd2 → NonInjective-≡ sha256 ⊎ vd1 ≡ vd2
  hashVD-inj {vd1} {vd2} prf
    with hash-concat-inj {voteDataHashList vd1} {voteDataHashList vd2} prf
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ vdLists≡
     with hashBI-inj (proj₁ (∷-injective vdLists≡)) | hashBI-inj (proj₁ (∷-injective (proj₂ (∷-injective vdLists≡))))
  ...| inj₁ hb    | _         = inj₁ hb
  ...| inj₂ _     | inj₁ hb   = inj₁ hb
  ...| inj₂ prop≡ | inj₂ par≡ = inj₂ (VoteData-η prop≡ par≡)

  -- The Haskell implementation includes "HashTag"s when hashing in order to ensure that it is not
  -- possible (modulo hash collisions) for the encodings of two values of different types (e.g.,
  -- Vote and Block) to yield the same bitstring and thus the same hash (and therefore potentially
  -- the same signature, where hashes are signed).  For example, the Haskell hashLI function is:
  --
  -- hashLI :: LedgerInfo -> HashValue
  -- hashLI (LedgerInfo commitInfo (HashValue consensusDataHash)) =
  --   hashS (HLI, biParts commitInfo, consensusDataHash)
  --
  -- Note the HashTag HLI, which is not yet reflected in the Agda implementation.
  -- TODO-2: include HashTags in hash functions, consistent with the Haskell code.
  --
  -- As an aside, it is not clear whether these HashTags are necessary for all of the "inner"
  -- hashes.  They are needed to ensure that, for example, a dishonest peer cannot notice that the
  -- bits signed for a Vote happen to decode to a valid Block, and therefore take a Vote signature
  -- and use it to masquerade as a Block signture.  However, the implementation does include
  -- HashTags at each level, so we should too unless and until that changes.
  hashLI : LedgerInfo → HashValue
  hashLI (LedgerInfo∙new commitInfo consensusDataHash) =
    hash-concat (hashBI commitInfo ∷ consensusDataHash ∷ [])

  hashLI-inj : ∀ {li1 li2} → hashLI li1 ≡ hashLI li2 → NonInjective-≡ sha256 ⊎ li1 ≡ li2
  hashLI-inj {LedgerInfo∙new ci1 cd1} {LedgerInfo∙new ci2 cd2} prf
     with hash-concat-inj {hashBI ci1 ∷ cd1 ∷ []} {hashBI ci2 ∷ cd2 ∷ []} prf
  ...| inj₁ hb      = inj₁ hb
  ...| inj₂ li1≡li2
     with ∷-injective li1≡li2
  ...| ci≡ , rest≡
     with ∷-injective rest≡
  ...| cdh≡ , _
     with hashBI-inj ci≡
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ cis≡
     = inj₂ (LedgerInfo-η cis≡ cdh≡)

  record Ledger2WaypointConverterInjectivityProps (l1 l2 : Ledger2WaypointConverter) : Set where
    {- TODO-2 : implement Ledger2WaypointConverterInjectivityProps
    field
      l2wcInjEpoch          : ?
      l2wcInjRootHash       : ?
      l2wcInjVersion        : ?
      --timestamp
      l2wcInjNextEpochState : ?
    -}
  postulate -- TODO-2: prove after defining Ledger2WaypointConverterInjectivityProps
    hashL2WC     : Ledger2WaypointConverter → HashValue
    hashL2WC-inj : ∀ {l1 l2}
                 → hashL2WC l1 ≡ hashL2WC l2
                 → NonInjective-≡ sha256 ⊎ Ledger2WaypointConverterInjectivityProps l1 l2

  constructLI : Vote → LedgerInfo
  constructLI v = LedgerInfo∙new (_liCommitInfo (_vLedgerInfo v)) (hashVD (_vVoteData v))

  hashVote : Vote → HashValue
  hashVote = hashLI ∘ constructLI

  hashVote-inj1 : ∀ {v1 v2} → hashVote v1 ≡ hashVote v2
                → NonInjective-≡ sha256 ⊎ _vVoteData v1 ≡ _vVoteData v2
  hashVote-inj1 {v1} {v2} hyp with hashLI-inj {constructLI v1} {constructLI v2} hyp
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ ok = hashVD-inj {_vVoteData v1} {_vVoteData v2} (cong _liConsensusDataHash ok)

  -- A vote is always signed; as seen by the 'Unit'
  -- in the definition of Signed.
  instance
    sig-Vote : WithSig Vote
    sig-Vote = record
       { Signed         = λ _ → Unit
       ; Signed-pi      = λ _ _ _ → Unit-pi
       ; isSigned?      = λ _ → yes unit
       ; signature      = λ v _ → _vSignature v
       ; signableFields = encodeH ∘ hashVote
       }

  sameSig⇒sameVoteData : ∀ {v1 v2 : Vote} {pk}
                       → WithVerSig pk v1
                       → WithVerSig pk v2
                       → v1 ^∙ vSignature ≡ v2 ^∙ vSignature
                       → NonInjective-≡ sha256 ⊎ v2 ^∙ vVoteData ≡ v1 ^∙ vVoteData
  sameSig⇒sameVoteData {v1} {v2} wvs1 wvs2 refl
     with verify-bs-inj (verified wvs1) (verified wvs2)
       -- The signable fields of the votes must be the same (we do not model signature collisions)
  ...| bs≡
       -- Therefore the LedgerInfo is the same for the new vote as for the previous vote
       = sym <⊎$> (hashVote-inj1 {v1} {v2} (sameBS⇒sameHash bs≡))

  -- Captures a proof that a vote was cast by α by recording that 'verify' returns true.
  VoteSigVerifies : PK → Vote → Set
  VoteSigVerifies pk v = T (verify (signableFields ⦃ sig-Vote ⦄ v) (_vSignature v) pk)

  Signed-pi-Blk : (b : Block)
                → (is1 is2 : (Is-just ∘ _bSignature) b)
                → is1 ≡ is2
  Signed-pi-Blk (Block∙new _ _ .(just _)) (just _) (just _) = cong just refl

  -- A Block might carry a signature
  instance
    sig-Block : WithSig Block
    sig-Block = record
       { Signed         = Is-just ∘ _bSignature
       ; Signed-pi      = Signed-pi-Blk
       ; isSigned?      = λ b → Maybe-Any-dec (λ _ → yes tt) (b ^∙ bSignature)
       ; signature      = λ { _ prf → to-witness prf }
       ; signableFields = λ b → concat (encodeH (_bId b) ∷ encode (b ^∙ bBlockData) ∷ [])
       }


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

open import Categories.Category

module Categories.Diagram.Pullback.Properties {o ℓ e} (C : Category o ℓ e) where

open import Function using (_$_)

open import Categories.Category.BinaryProducts C
open import Categories.Category.Cartesian C
open import Categories.Diagram.Pullback C
open import Categories.Diagram.Equalizer C hiding (up-to-iso)
open import Categories.Object.Product C hiding (up-to-iso)
open import Categories.Object.Terminal C hiding (up-to-iso)
open import Categories.Morphism C
open import Categories.Morphism.Reasoning C
open import Categories.Category.Complete.Finitely using (FinitelyComplete)
open import Data.Product using (∃; _,_)

private
  open Category C
  variable
    X Y Z : Obj
    f g h i : X ⇒ Y
open HomReasoning
open Equiv

-- pullbacks of a monomorphism along itself give us the identity arrow.
pullback-self-mono : Mono f → IsPullback id id f f
pullback-self-mono mono = record
  { commute = refl
  ; universal = λ {X} {h₁} {h₂} eq → h₁
  ; unique = λ id∘i≈h₁ _ → ⟺ identityˡ ○ id∘i≈h₁
  ; p₁∘universal≈h₁ = identityˡ
  ; p₂∘universal≈h₂ = λ {X} {h₁} {h₂} {eq} → identityˡ ○ mono h₁ h₂ eq
  }

-- pullback from a terminal object is the same as a product
module _ (t : Terminal) where
  open Terminal t

  pullback-⊤⇒product : Pullback (! {X}) (! {Y}) → Product X Y
  pullback-⊤⇒product p = record
    { A×B      = P
    ; π₁       = p₁
    ; π₂       = p₂
    ; ⟨_,_⟩    = λ f g → universal (!-unique₂ {f = ! ∘ f} {g = ! ∘ g})
    ; project₁ = p₁∘universal≈h₁
    ; project₂ = p₂∘universal≈h₂
    ; unique   = λ eq eq′ → ⟺ (unique eq eq′)
    }
    where open Pullback p

  product⇒pullback-⊤ : Product X Y → Pullback (! {X}) (! {Y})
  product⇒pullback-⊤ p = record
    { p₁              = π₁
    ; p₂              = π₂
    ; isPullback = record
      { commute         = !-unique₂
      ; universal       = λ {_ f g} _ → ⟨ f , g ⟩
      ; unique          = λ eq eq′ → ⟺ (unique eq eq′)
      ; p₁∘universal≈h₁ = project₁
      ; p₂∘universal≈h₂ = project₂
      }
    }
    where open Product p

-- pullbacks respect _≈_
module _ (p : Pullback f g) where
  open Pullback p

  pullback-resp-≈ : f ≈ h → g ≈ i → Pullback h i
  pullback-resp-≈ eq eq′ = record
    { p₁              = p₁
    ; p₂              = p₂
    ; isPullback = record
      { commute         = ∘-resp-≈ˡ (⟺ eq) ○ commute ○ ∘-resp-≈ˡ eq′
      ; universal       = λ eq″ → universal (∘-resp-≈ˡ eq ○ eq″ ○ ∘-resp-≈ˡ (⟺ eq′))
      ; unique          = unique
      ; p₁∘universal≈h₁ = p₁∘universal≈h₁
      ; p₂∘universal≈h₂ = p₂∘universal≈h₂
      }
    }

-- Some facts about pulling back along identity
module _ (p : Pullback id f) where
  open Pullback p

  -- This is a more subtle way of saying that 'p₂ ≈ id', without involving heterogenous equality.
  pullback-identity : universal id-comm-sym ∘ p₂ ≈ id
  pullback-identity = begin
    universal Basic.id-comm-sym ∘ p₂ ≈⟨ unique ( pullˡ p₁∘universal≈h₁ ) (pullˡ p₂∘universal≈h₂)  ⟩
    universal eq                     ≈⟨ universal-resp-≈ (⟺ commute ○ identityˡ) identityˡ ⟩
    universal commute                ≈˘⟨ Pullback.id-unique p ⟩
    id ∎
    where
      eq : id ∘ f ∘ p₂ ≈ f ∘ id ∘ p₂
      eq = begin
        (id ∘ f ∘ p₂) ≈⟨ elimˡ Equiv.refl ⟩
        (f ∘ p₂)      ≈˘⟨ refl⟩∘⟨ identityˡ ⟩
        (f ∘ id ∘ p₂) ∎

-- pullbacks in Cartesian categories create equalizers
module _ (pullbacks : ∀ {X Y Z} (f : X ⇒ Z) (g : Y ⇒ Z) → Pullback f g)
         (cartesian : Cartesian) where
  open Cartesian cartesian
  open BinaryProducts products using (⟨_,_⟩; π₁; π₂; ⟨⟩-cong₂; ⟨⟩∘; project₁; project₂)

  pullback×cartesian⇒equalizer : Equalizer f g
  pullback×cartesian⇒equalizer {f = f} {g = g} = record
    { arr       = p.p₁
    ; isEqualizer = record
      { equality  = equality
      ; equalize  = λ {_ h} eq → p.universal $ begin
        ⟨ f , g ⟩ ∘ h               ≈⟨ ⟨⟩∘ ⟩
        ⟨ f ∘ h , g ∘ h ⟩           ≈˘⟨ ⟨⟩-cong₂ identityˡ (identityˡ ○ eq) ⟩
        ⟨ id ∘ f ∘ h , id ∘ f ∘ h ⟩ ≈˘⟨ ⟨⟩∘ ⟩
        ⟨ id , id ⟩ ∘ f ∘ h         ∎
      ; universal = ⟺ p.p₁∘universal≈h₁
      ; unique    = λ eq → p.unique (⟺ eq)
                                    (⟺ (pullˡ eq′) ○ ⟺ (∘-resp-≈ʳ eq))
      }
    }
    where p : Pullback ⟨ f , g ⟩ ⟨ id , id ⟩
          p = pullbacks _ _
          module p = Pullback p
          eq : ⟨ f ∘ p.p₁ , g ∘ p.p₁ ⟩ ≈ ⟨ p.p₂ , p.p₂ ⟩
          eq = begin
            ⟨ f ∘ p.p₁ , g ∘ p.p₁ ⟩      ≈˘⟨ ⟨⟩∘ ⟩
            ⟨ f , g ⟩ ∘ p.p₁             ≈⟨ p.commute ⟩
            ⟨ id , id ⟩ ∘ p.p₂           ≈⟨ ⟨⟩∘ ⟩
            ⟨ id ∘ p.p₂ , id ∘ p.p₂ ⟩    ≈⟨ ⟨⟩-cong₂ identityˡ identityˡ ⟩
            ⟨ p.p₂ , p.p₂ ⟩              ∎
          eq′ : f ∘ p.p₁ ≈  p.p₂
          eq′ = begin
            f ∘ p.p₁                     ≈˘⟨ project₁ ⟩
            π₁ ∘ ⟨ f ∘ p.p₁ , g ∘ p.p₁ ⟩ ≈⟨ refl⟩∘⟨ eq ⟩
            π₁ ∘ ⟨ p.p₂ , p.p₂ ⟩         ≈⟨ project₁ ⟩
            p.p₂                         ∎
          equality : f ∘ p.p₁ ≈ g ∘ p.p₁
          equality = begin
            f ∘ p.p₁                     ≈⟨ eq′ ⟩
            p.p₂                         ≈˘⟨ project₂ ⟩
            π₂ ∘ ⟨ p.p₂ , p.p₂ ⟩         ≈˘⟨ refl⟩∘⟨ eq ⟩
            π₂ ∘ ⟨ f ∘ p.p₁ , g ∘ p.p₁ ⟩ ≈⟨ project₂ ⟩
            g ∘ p.p₁                     ∎

-- all pullbacks and a terminal object make a category finitely complete
pullback-⊤⇒FinitelyComplete : (∀ {X Y Z} (f : X ⇒ Z) (g : Y ⇒ Z) → Pullback f g) → Terminal → FinitelyComplete C
pullback-⊤⇒FinitelyComplete pullbacks ⊤ = record
  { cartesian = cartesian
  ; equalizer = λ _ _ → pullback×cartesian⇒equalizer pullbacks cartesian
  }
    where
      open Category hiding (Obj)
      open Pullback
      open Terminal ⊤ hiding (⊤)

      _×_ : (A B : Obj) → Pullback (IsTerminal.! ⊤-is-terminal) (IsTerminal.! ⊤-is-terminal)
      A × B = pullbacks (IsTerminal.! ⊤-is-terminal) (IsTerminal.! ⊤-is-terminal)

      cartesian = record
        { terminal = ⊤
        ; products = record
            { product = λ {A B} → record
                { A×B = P {A}{_}{B} (A × B)
                ; π₁ = p₁ (A × B)
                ; π₂ = p₂ (A × B)
                ; ⟨_,_⟩ =  λ _ _ → universal (A × B) (!-unique₂)
                ; project₁ = p₁∘universal≈h₁ (A × B)
                ; project₂ = p₂∘universal≈h₂ (A × B)
                ; unique = λ eq₁ eq₂ → Equiv.sym C (unique (A × B) eq₁ eq₂)
                }
            }
        }

-- extra properties of "up-to-iso"
module IsoPb {X Y Z} {f : X ⇒ Z} {g : Y ⇒ Z} (pull₀ pull₁ : Pullback f g) where
  open Pullback using (P; p₁; p₂; p₁∘universal≈h₁; p₂∘universal≈h₂; commute; universal)

  P₀≅P₁ : P pull₀ ≅ P pull₁
  P₀≅P₁ = up-to-iso pull₀ pull₁

  P₀⇒P₁ : P pull₀ ⇒ P pull₁
  P₀⇒P₁ = _≅_.from P₀≅P₁

  p₁-≈ : p₁ pull₁ ∘ P₀⇒P₁ ≈ p₁ pull₀
  p₁-≈ = p₁∘universal≈h₁ pull₁ {eq = commute pull₀}

  p₂-≈ : p₂ pull₁ ∘ P₀⇒P₁ ≈ p₂ pull₀
  p₂-≈ = p₂∘universal≈h₂ pull₁ {eq = commute pull₀}

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Sandbox.Pred where

open import Data.Num
open import Data.Num.Properties

open import Data.Nat
open import Data.Fin using (Fin; suc; zero; #_)
open import Data.Vec
open import Relation.Nullary.Decidable using (True; fromWitness)
open import Relation.Binary.PropositionalEquality hiding ([_])
-- open import Relation.Binary
open ≡-Reasoning

data Term : ℕ → Set where
    var : ∀ {n}
        → Fin n     -- the index of this variable
        → Term n
    _∔_ : ∀ {n} → Term n → Term n → Term n

data Pred : ℕ → Set where
  _≣_ : ∀ {n} → Term n → Term n → Pred n
  _⇒_ : ∀ {n} → Pred n → Pred n → Pred n
  -- captures 1 free variable in the Pred
  All : ∀ {n} → Pred (suc n) → Pred n

record Signature : Set₁ where
    constructor signature
    field
        carrier : Set
        _⊕_ : carrier → carrier → carrier
        _≈_ : carrier → carrier → Set

open Signature

-- signatures
ℕ-sig : Signature
ℕ-sig = signature ℕ _+_ _≡_

Num-sig : (b d o : ℕ) → True (Surjective? b d o) → Signature
Num-sig b d o surj = signature (Num b d o) (_⊹_ {surj = surj}) _≋_

⟦_⟧Term : ∀ {n}
    → Term n
    → (sig : Signature)
    → let A = carrier sig in Vec A n
    → A
⟦ var x ⟧Term sig env = lookup x env
⟦ a ∔ b ⟧Term sig env = let (signature A _⊕_ _≈_) = sig in
                        (⟦ a ⟧Term sig env) ⊕ (⟦ b ⟧Term sig env)

⟦_⟧ : ∀ {n}
    → Pred n
    → (sig : Signature)
    → Vec (carrier sig) n
    → Set
⟦ p ≣ q ⟧ sig env = let (signature carrier _⊕_ _≈_) = sig in
                    ⟦ p ⟧Term sig env ≈ ⟦ q ⟧Term sig env
⟦ p ⇒ q ⟧ sig env = ⟦ p ⟧ sig env → ⟦ q ⟧ sig env
⟦ All p ⟧ sig env = ∀ x → ⟦ p ⟧ sig (x ∷ env)

-- lemma for env
lookup-map : ∀ {i j} → {A : Set i} {B : Set j}
           → (f : A → B) →
           ∀ {n} → (xs : Vec A n) (i : Fin n)
           → lookup i (map f xs) ≡ f (lookup i xs)
lookup-map f []        ()
lookup-map f (x ∷ env) zero    = refl
lookup-map f (x ∷ env) (suc i) = lookup-map f env i

toℕ-term-homo : ∀ {b d o}
    → {surj : True (Surjective? b d o)}
    → ∀ {n}
    → (t : Term n)
    → (env : Vec (Num b d o) n)
    → ⟦ t ⟧Term ℕ-sig (map toℕ env) ≡ toℕ (⟦ t ⟧Term (Num-sig b d o surj) env )
toℕ-term-homo (var x) env = lookup-map toℕ env x
toℕ-term-homo {b} {d} {o} {surj} (s ∔ t) env =
    begin
        ⟦ s ∔ t ⟧Term ℕ-sig (map toℕ env)
    ≡⟨ cong₂ _+_ (toℕ-term-homo {surj = surj} s env) (toℕ-term-homo {surj = surj} t env) ⟩
        toℕ (⟦ s ⟧Term _ env) + toℕ (⟦ t ⟧Term _ env)
    ≡⟨ sym (toℕ-⊹-homo (⟦ s ⟧Term _ env) (⟦ t ⟧Term _ env)) ⟩
        toℕ (⟦ s ∔ t ⟧Term (Num-sig b d o surj) env)
    ∎

mutual
    toℕ-pred-ℕ⇒Num : ∀ {b d o}
        → {surj : True (Surjective? b d o)}
        → ∀ {n}
        → (p : Pred n)
        → (env : Vec (Num b d o) n)
        → ⟦ p ⟧ ℕ-sig (map toℕ env)
        → ⟦ p ⟧ (Num-sig b d o surj) env
    -- toℕ-pred-ℕ⇒Num (p ≣ q) env ⟦p≡q⟧ℕ = {!   !}
    toℕ-pred-ℕ⇒Num {b} {d} {o} {surj} (p ≣ q) env a =
        -- a : ⟦ p ⟧Term ℕ-sig (ℕ-env) ≡ ⟦ q ⟧Term ℕ-sig (ℕ-env)

        let p' = ⟦ p ⟧Term {! Num-sig b d o surj  !} {!   !} {!   !}
            temp = toℕ-injective p' {!   !} a
        in
        {! toℕ-injective  !}
    toℕ-pred-ℕ⇒Num (p ⇒ q) env a = {!   !}
    toℕ-pred-ℕ⇒Num (All p) env a = {!   !}

    toℕ-pred-Num→ℕ : ∀ {b d o}
        → {surj : True (Surjective? b d o)}
        → ∀ {n}
        → (p : Pred n)
        → (env : Vec (Num b d o) n)
        → ⟦ p ⟧ (Num-sig b d o surj) env
        → ⟦ p ⟧ ℕ-sig (map toℕ env)
    toℕ-pred-Num→ℕ (p ≣ q) env a = {!   !}
    toℕ-pred-Num→ℕ (p ⇒ q) env a = {!   !}
    toℕ-pred-Num→ℕ (All p) env a = {!   !}

-- begin
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ∎

--
-- toℕ-term-homo : ∀ {b n}
--     → (t : Term n)
--     → (env : Vec (BijN b) n)
--     → ⟦ t ⟧Term ℕ-sig (map toℕ env) ≡ toℕ (⟦ t ⟧Term (BijN-sig b) env)
-- toℕ-term-homo     (var i)   env = ?
-- toℕ-term-homo {b} (t₁ ∔ t₂) env = ?

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
{-# OPTIONS --show-implicit #-}
{-# OPTIONS --sized-types #-}

module Issue298 where

postulate
  Size : Set
  ↑_   : Size → Size
  ∞    : Size

{-# BUILTIN SIZE    Size #-}
{-# BUILTIN SIZESUC ↑_   #-}
{-# BUILTIN SIZEINF ∞    #-}

data BTree : {i : Size} → Set where
  leaf : ∀ {i} → BTree {↑ i}
  node : ∀ {i} → BTree {i} → BTree {i} → BTree {↑ i}

recId : ∀ {i} → BTree {i} → BTree {i}
recId leaf = leaf
recId (node l r) = node (recId l) (recId r)

deepId : ∀ {i} → BTree {i} → BTree {i}
deepId leaf = leaf
deepId (node leaf leaf) = node leaf leaf
deepId (node leaf (node r1 r2)) = node leaf (node (deepId r1) (deepId r2))
deepId (node (node l1 l2) r) = node (node (deepId l1) (deepId l2)) (deepId r)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso