text:
------------------------------------------------------------------------
-- Small coinductive higher lenses
------------------------------------------------------------------------

{-# OPTIONS --cubical --guardedness #-}

import Equality.Path as P

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

open P.Derived-definitions-and-properties eq

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

open import Bijection equality-with-J as B using (_↔_)
import Coherently-constant eq as CC
open import Equality.Decidable-UIP equality-with-J using (Constant)
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq
  using (_≃_; Is-equivalence)
open import 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 using (∥_∥)
open import H-level.Truncation.Propositional.One-step eq as O
  using (∥_∥¹; ∣_∣)
open import Preimage equality-with-J as Preimage using (_⁻¹_)
open import Tactic.Sigma-cong equality-with-J
open import Univalence-axiom equality-with-J

open import Lens.Non-dependent eq
import Lens.Non-dependent.Higher eq as Higher
import Lens.Non-dependent.Higher.Combinators eq as HC
import Lens.Non-dependent.Higher.Capriotti eq as Capriotti
import Lens.Non-dependent.Higher.Coinductive eq as Coinductive
open import Lens.Non-dependent.Higher.Coherently.Coinductive eq
import Lens.Non-dependent.Higher.Coherently.Not-coinductive eq as NC

private
  variable
    a b c d p q : Level
    A B C       : Type a
    P           : A → Type p
    z           : A
    n           : ℕ

------------------------------------------------------------------------
-- Constant-≃

-- A variant of Constant for type-valued functions.

Constant-≃ :
  {A : Type a} →
  (A → Type p) → Type (a ⊔ p)
Constant-≃ P = ∀ x y → P x ≃ P y

-- Constant and Constant-≃ are pointwise equivalent (assuming
-- univalence).

Constant≃Constant-≃ :
  {P : A → Type p} →
  Univalence p → Constant P ≃ Constant-≃ P
Constant≃Constant-≃ univ =
  ∀-cong ext λ _ →
  ∀-cong ext λ _ →
  ≡≃≃ univ

-- The right-to-left direction of Constant-≃-get-⁻¹-≃ (which is
-- defined below).

Constant-≃-get-⁻¹-≃⁻¹ :
  {get : A → B} →
  (∃ λ (set : A → B → A) →
   ∃ λ (get-set : (a : A) (b : B) → get (set a b) ≡ b) →
   ∀ b₁ b₂ →
   let f : get ⁻¹ b₁ → get ⁻¹ b₂
       f = λ (a , _) → set a b₂ , get-set a b₂
   in
   Is-equivalence f) →
  Constant-≃ (get ⁻¹_)
Constant-≃-get-⁻¹-≃⁻¹ (_ , _ , eq) b₁ b₂ = Eq.⟨ _ , eq b₁ b₂ ⟩

-- Constant-≃ (get ⁻¹_) can be expressed in terms of a "setter" and a
-- "get-set" law that form a family of equivalences in a certain way.
--
-- This lemma was suggested by Andrea Vezzosi when we discussed
-- coinductive lenses with erased "proofs".
--
-- The left-to-right direction of the lemma is not blocked, but the
-- rest is.

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

    (∀ b₁ b₂ → get ⁻¹ b₁ ≃ get ⁻¹ b₂)                               ↔⟨ (∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                        Eq.≃-as-Σ) ⟩
    (∀ b₁ b₂ →
     ∃ λ (f : get ⁻¹ b₁ → get ⁻¹ b₂) →
     Is-equivalence f)                                              ↔⟨ Π-comm ⟩

    (∀ b₂ b₁ →
     ∃ λ (f : get ⁻¹ b₁ → get ⁻¹ b₂) →
     Is-equivalence f)                                              ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                        Σ-cong-id currying) ⟩
    (∀ b₂ b₁ →
     ∃ λ (f : ∀ a → get a ≡ b₁ → get ⁻¹ b₂) →
     Is-equivalence (uncurry f))                                    ↔⟨ (∀-cong ext λ _ →
                                                                        ΠΣ-comm) ⟩
    (∀ b₂ →
     ∃ λ (f : ∀ b₁ a → get a ≡ b₁ → get ⁻¹ b₂) →
     ∀ b₁ → Is-equivalence (uncurry (f b₁)))                        ↝⟨ (∀-cong ext λ _ →
                                                                        Σ-cong-id Π-comm) ⟩
    (∀ b₂ →
     ∃ λ (f : ∀ a b₁ → get a ≡ b₁ → get ⁻¹ b₂) →
     ∀ b₁ → Is-equivalence (uncurry (flip f b₁)))                   ↝⟨ (∀-cong ext λ _ →
                                                                        Σ-cong (∀-cong ext λ _ → inverse $ ∀-intro {k = equivalence} ext _) λ f →
                                                                        ∀-cong ext λ b₁ →
                                                                        Is-equivalence-cong {k = equivalence} ext λ (a , eq) →
        uncurry (f a) (b₁ , eq)                                           ≡⟨ cong (uncurry (f a)) $ sym $
                                                                             proj₂ (other-singleton-contractible _) _ ⟩∎
        uncurry (f a) (get a , refl _)                                    ∎) ⟩

    (∀ b₂ →
     ∃ λ (f : A → get ⁻¹ b₂) →
     ∀ b₁ → Is-equivalence (f ∘ proj₁))                             ↔⟨ ΠΣ-comm ⟩

    (∃ λ (f : (b : B) → A → get ⁻¹ b) →
     ∀ b₂ b₁ → Is-equivalence (f b₂ ∘ proj₁))                       ↝⟨ Σ-cong-refl Π-comm (λ _ → Π-comm) ⟩

    (∃ λ (f : A → (b : B) → get ⁻¹ b) →
     ∀ b₁ b₂ → Is-equivalence ((_$ b₂) ∘ f ∘ proj₁))                ↝⟨ Σ-cong-refl (∀-cong ext λ _ → ΠΣ-comm) (λ _ → Eq.id) ⟩

    (∃ λ (f : A → ∃ λ (set : B → A) → (b : B) → get (set b) ≡ b) →
     ∀ b₁ b₂ → Is-equivalence (Σ-map (_$ b₂) (_$ b₂) ∘ f ∘ proj₁))  ↝⟨ Σ-cong-id ΠΣ-comm ⟩

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

    (∃ λ (set : A → B → A) →
     ∃ λ (get-set : (a : A) (b : B) → get (set a b) ≡ b) →
     ∀ b₁ b₂ → Is-equivalence λ (a , _) → set a b₂ , get-set a b₂)  □

  equiv₂ =
    Eq.with-other-function
      (inverse equiv₁)
      Constant-≃-get-⁻¹-≃⁻¹
      (λ (set , get-set , _) → ⟨ext⟩ λ b₁ → ⟨ext⟩ λ b₂ →
         Eq.lift-equality ext $ ⟨ext⟩ λ (a , _) →
           subst (λ _ → get ⁻¹ b₂) _ (set a b₂ , get-set a b₂)  ≡⟨ subst-const _ ⟩∎
           (set a b₂ , get-set a b₂)                            ∎)

  equiv₃ : Unit → _ ≃ _
  equiv₃ _ ._≃_.to             = _≃_.to equiv₂
  equiv₃ ⊠ ._≃_.is-equivalence = _≃_.is-equivalence equiv₂

-- Constant-≃-get-⁻¹-≃ computes in a certain way.

_ :
  ∀ {bl : Block "Constant-≃-get-⁻¹-≃"}
    {get : A → B} {set : A → B → A}
    {get-set : (a : A) (b : B) → get (set a b) ≡ b}
    {eq :
     ∀ b₁ b₂ →
     let f : get ⁻¹ b₁ → get ⁻¹ b₂
         f = λ (a , _) → set a b₂ , get-set a b₂
     in
     Is-equivalence f}
    {b₁ b₂} →
  _≃_.to (_≃_.from (Constant-≃-get-⁻¹-≃ bl) (set , get-set , eq) b₁ b₂) ≡
  (λ (a , _) → set a b₂ , get-set a b₂)
_ = refl _

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

-- Coherently constant type-valued functions.

Coherently-constant :
  Univalence p →
  {A : Type a} → (A → Type p) → Type (a ⊔ p)
Coherently-constant univ =
  Coherently
    Constant-≃
    (λ P c → O.rec′ P (λ x y → ≃⇒≡ univ (c x y)))

-- Two variants of Coherently-constant are pointwise equivalent
-- (when applicable, assuming univalence).

Coinductive-coherently-constant≃Coherently-constant :
  {A : Type a} {P : A → Type p} →
  Univalence (a ⊔ lsuc p) →
  (univ : Univalence p) →
  Coinductive.Coherently-constant P ≃ Coherently-constant univ P
Coinductive-coherently-constant≃Coherently-constant univ′ univ =
  Coherently-cong
    univ′
    (λ _ → Constant≃Constant-≃ univ)
    (λ _ _ → refl _)

-- Two variants of Coherently-constant are pointwise equivalent
-- (when applicable, assuming univalence).

Coherently-constant≃Coherently-constant :
  {A : Type a} {P : A → Type p} →
  Univalence (a ⊔ lsuc p) →
  (univ : Univalence p) →
  CC.Coherently-constant P ≃ Coherently-constant univ P
Coherently-constant≃Coherently-constant {P = P} univ′ univ =
  CC.Coherently-constant P           ↝⟨ Coinductive.Coherently-constant≃Coherently-constant univ′ ⟩
  Coinductive.Coherently-constant P  ↝⟨ Coinductive-coherently-constant≃Coherently-constant univ′ univ ⟩□
  Coherently-constant univ P         □

-- A map lemma for Coherently-constant.

Coherently-constant-map :
  {P : A → Type p} {Q : B → Type q}
  (univ₁ : Univalence p) →
  (univ₂ : Univalence q) →
  (f : B → A) →
  (∀ x → P (f x) ≃ Q x) →
  Coherently-constant univ₁ P → Coherently-constant univ₂ Q
Coherently-constant-map {P = P} {Q = Q} _ _ f P≃Q c .property x y =
  Q x      ↝⟨ inverse $ P≃Q x ⟩
  P (f x)  ↝⟨ c .property (f x) (f y) ⟩
  P (f y)  ↝⟨ P≃Q y ⟩□
  Q y      □
Coherently-constant-map {P = P} {Q = Q} univ₁ univ₂ f P≃Q c .coherent =
  Coherently-constant-map univ₁ univ₂ (O.∥∥¹-map f)
    (O.elim λ where
       .O.Elim.∣∣ʳ → P≃Q
       .O.Elim.∣∣-constantʳ x y → Eq.lift-equality ext
         (_≃_.to (subst (λ z → O.rec′ P g (O.∥∥¹-map f z) ≃
                               O.rec′ Q h z)
                    (O.∣∣-constant x y) (P≃Q x))                         ≡⟨ Eq.to-subst ⟩

          subst (λ z → O.rec′ P g (O.∥∥¹-map f z) → O.rec′ Q h z)
            (O.∣∣-constant x y) (_≃_.to (P≃Q x))                         ≡⟨ (⟨ext⟩ λ _ → subst-→) ⟩

          subst (O.rec′ Q h) (O.∣∣-constant x y) ∘
          _≃_.to (P≃Q x) ∘
          subst (O.rec′ P g ∘ O.∥∥¹-map f) (sym (O.∣∣-constant x y))     ≡⟨ cong₂ (λ f g → f ∘ _≃_.to (P≃Q x) ∘ g)
                                                                              (⟨ext⟩ λ q → subst-∘ P.id (O.rec′ Q h) (O.∣∣-constant x y) {p = q})
                                                                              (⟨ext⟩ λ p →
                                                                               trans (subst-∘ P.id (O.rec′ P g ∘ O.∥∥¹-map f)
                                                                                (sym (O.∣∣-constant x y)) {p = p}) $
                                                                               cong (λ eq → subst P.id eq p) $
                                                                               trans (cong-sym _ _) $
                                                                               cong sym $ sym $ cong-∘ _ _ _) ⟩
          subst P.id (cong (O.rec′ Q h) (O.∣∣-constant x y)) ∘
          _≃_.to (P≃Q x) ∘
          subst P.id (sym (cong (O.rec′ P g)
                             (cong (O.∥∥¹-map f) (O.∣∣-constant x y))))  ≡⟨ cong₂ (λ p q → subst P.id p ∘ _≃_.to (P≃Q x) ∘ subst P.id (sym q))
                                                                              O.rec-∣∣-constant
                                                                              (trans (cong (cong (O.rec′ P g)) O.rec-∣∣-constant) $
                                                                               O.rec-∣∣-constant) ⟩

          subst P.id (h x y) ∘
          _≃_.to (P≃Q x) ∘
          subst P.id (sym (g (f x) (f y)))                               ≡⟨ cong₂ (λ p q → p ∘ _≃_.to (P≃Q x) ∘ q)
                                                                              (trans (⟨ext⟩ λ _ → subst-id-in-terms-of-≡⇒↝ equivalence) $
                                                                               cong _≃_.to $ _≃_.right-inverse-of (≡≃≃ univ₂) _)
                                                                              (trans (⟨ext⟩ λ _ → subst-id-in-terms-of-inverse∘≡⇒↝ equivalence) $
                                                                               cong _≃_.from $ _≃_.right-inverse-of (≡≃≃ univ₁) _) ⟩
          _≃_.to (P≃Q y) ∘
          _≃_.to (c .property (f x) (f y)) ∘
          _≃_.from (P≃Q x) ∘
          _≃_.to (P≃Q x) ∘
          _≃_.from (c .property (f x) (f y))                             ≡⟨ (⟨ext⟩ λ _ → cong (_≃_.to (P≃Q y) ∘ _≃_.to (c .property (f x) (f y))) $
                                                                            _≃_.left-inverse-of (P≃Q x) _) ⟩
          _≃_.to (P≃Q y) ∘
          _≃_.to (c .property (f x) (f y)) ∘
          _≃_.from (c .property (f x) (f y))                             ≡⟨ (⟨ext⟩ λ _ → cong (_≃_.to (P≃Q y)) $
                                                                             _≃_.right-inverse-of (c .property (f x) (f y)) _) ⟩∎
          _≃_.to (P≃Q y)                                                 ∎))
    (c .coherent)
  where
  g = λ x y → ≃⇒≡ univ₁ (c .property x y)
  h = λ x y → ≃⇒≡ univ₂ ((P≃Q y F.∘ c .property (f x) (f y)) F.∘
                         inverse (P≃Q x))

private

  -- A lemma used below.

  elim-Σ-≡,≡→≡-∣∣-constant :
    ∀ (e : O.Elim (λ x → P x → A)) {x y p} →

    let p′ = subst P (O.∣∣-constant x y) p in

    cong (uncurry $ O.elim e) (Σ-≡,≡→≡ (O.∣∣-constant x y) (refl p′)) ≡

    trans
      (O.∣∣ʳ e x p                                            ≡⟨ cong (O.∣∣ʳ e x) $ sym $ subst-sym-subst _ ⟩

       O.∣∣ʳ e x
         (subst P (sym (O.∣∣-constant x y))
            (subst P (O.∣∣-constant x y) p))                  ≡⟨ sym $ subst-→-domain _ _ ⟩∎

       subst (λ x → P x → A) (O.∣∣-constant x y) (O.∣∣ʳ e x)
         (subst P (O.∣∣-constant x y) p)                      ∎)
      (cong (_$ p′) (e .O.∣∣-constantʳ x y))

  elim-Σ-≡,≡→≡-∣∣-constant {P = P} {A = A} e {x = x} {y = y} {p = p} =

    cong (uncurry $ O.elim e)
      (Σ-≡,≡→≡ (O.∣∣-constant x y) (refl _))                 ≡⟨ elim¹
                                                                  (λ eq →
                                                                     cong (uncurry $ O.elim e) (Σ-≡,≡→≡ eq (refl _)) ≡
                                                                     trans
                                                                       (trans (cong (O.∣∣ʳ e x) $ sym $ subst-sym-subst _)
                                                                          (sym $ subst-→-domain _ _))
                                                                       (cong (_$ subst P eq p) (dcong (O.elim e) eq)))
                                                                  (
      cong (uncurry $ O.elim e)
        (Σ-≡,≡→≡ (refl ∣ x ∣) (refl _))                            ≡⟨ cong (cong (uncurry $ O.elim e)) Σ-≡,≡→≡-refl-refl ⟩

      cong (uncurry $ O.elim e)
        (cong (∣ x ∣ ,_) (sym (subst-refl _ _)))                   ≡⟨ cong-∘ _ _ _ ⟩

      cong (O.elim e ∣ x ∣) (sym (subst-refl _ _))                 ≡⟨⟩

      cong (O.∣∣ʳ e x) (sym (subst-refl _ _))                      ≡⟨ sym $
                                                                      trans (cong (flip trans _) $
                                                                             trans (sym $ trans-assoc _ _ _) $
                                                                             trans (cong (flip trans _) $
                                                                                trans-[trans]-sym _ _) $
                                                                             trans (sym $ trans-assoc _ _ _) $
                                                                             cong (flip trans _) $
                                                                             trans-[trans]-sym _ _) $
                                                                      trans-[trans-sym]- _ _ ⟩
      trans
        (trans (trans (trans (cong (O.∣∣ʳ e x)
                                (sym (subst-refl _ _)))
                         (cong (O.∣∣ʳ e x)
                            (sym (subst-refl _ _))))
                  (cong (O.∣∣ʳ e x) $
                   sym (cong (flip (subst P) _) sym-refl)))
           (trans
              (sym $
               cong (O.∣∣ʳ e x) $
               sym (cong (flip (subst P) _) sym-refl))
              (trans
                 (sym $
                  cong (O.∣∣ʳ e x) (sym (subst-refl _ _)))
                 (sym $
                  cong (_$ subst P (refl _) p)
                    (subst-refl _ _)))))
        (cong (_$ subst P (refl _) p) (subst-refl _ _))            ≡⟨ sym $
                                                                      cong (flip trans _) $
                                                                      cong₂ trans
                                                                        (trans (cong (cong (O.∣∣ʳ e x)) $ sym-trans _ _) $
                                                                         trans (cong-trans _ _ _) $
                                                                         cong (flip trans _) $
                                                                         trans (cong (cong (O.∣∣ʳ e x)) $ sym-trans _ _) $
                                                                         cong-trans _ _ _)
                                                                        (trans (sym-trans _ _) $
                                                                         trans (cong (flip trans _) $
                                                                                trans (sym-trans _ _) $
                                                                                cong (flip trans _) $ cong sym $
                                                                                trans (sym $ cong-∘ _ _ _) $
                                                                                cong (cong (O.∣∣ʳ e x)) $ cong-sym _ _) $
                                                                         trans-assoc _ _ _) ⟩
      trans
        (trans (cong (O.∣∣ʳ e x) $ sym $
                trans (cong (flip (subst P) _) sym-refl)
                  (trans (subst-refl _ _)
                     (subst-refl _ _)))
           (sym $
            trans (cong (_$ subst P (refl _) p)
                     (subst-refl _ _))
              (trans (cong (O.∣∣ʳ e x)
                        (sym (subst-refl _ _)))
                 (cong (O.∣∣ʳ e x ∘ flip (subst P) _)
                    (sym sym-refl)))))
        (cong (_$ subst P (refl _) p) (subst-refl _ _))            ≡⟨ sym $
                                                                      cong₂ (λ eq₁ eq₂ → trans
                                                                                (trans (cong (O.∣∣ʳ e x) $ sym eq₁) (sym eq₂))
                                                                                (cong (_$ subst P (refl _) p) (subst-refl _ _)))
                                                                        (subst-sym-subst-refl _)
                                                                        subst-→-domain-refl ⟩
      trans
        (trans (cong (O.∣∣ʳ e x) $ sym $ subst-sym-subst _)
           (sym $ subst-→-domain _ _))
        (cong (_$ subst P (refl _) p) (subst-refl _ _))            ≡⟨ cong (trans _) $ cong (cong _) $ sym $
                                                                      dcong-refl _ ⟩∎
      trans
        (trans (cong (O.∣∣ʳ e x) $ sym $ subst-sym-subst _)
           (sym $ subst-→-domain _ _))
        (cong (_$ subst P (refl _) p)
           (dcong (O.elim e) (refl _)))                            ∎)
                                                                  _ ⟩
    trans
      (trans (cong (O.∣∣ʳ e x) $ sym $ subst-sym-subst _)
         (sym $ subst-→-domain _ _))
      (cong (_$ subst P (O.∣∣-constant x y) p)
         (dcong (O.elim e) (O.∣∣-constant x y)))             ≡⟨ cong (trans _) $ cong (cong _)
                                                                O.elim-∣∣-constant ⟩∎
    trans
      (trans (cong (O.∣∣ʳ e x) $ sym $ subst-sym-subst _)
         (sym $ subst-→-domain _ _))
      (cong (_$ subst P (O.∣∣-constant x y) p)
         (e .O.∣∣-constantʳ x y))                            ∎

-- Coherently-constant is, in a certain sense, closed under Σ.
--
-- This lemma is based on a lemma due to Paolo Capriotti (see
-- Capriotti.Coherently-constant-Σ).
--
-- TODO: Can the ".coherent" clause be simplified?

Coherently-constant-Σ :
  {P : A → Type p} {Q : ∃ P → Type q}
  (univ₁ : Univalence p)
  (univ₂ : Univalence q)
  (univ₃ : Univalence (p ⊔ q)) →
  Coherently-constant univ₁ P →
  Coherently-constant univ₂ Q →
  Coherently-constant univ₃ (λ x → ∃ λ (y : P x) → Q (x , y))
Coherently-constant-Σ {p = p} {q = q} univ₁ univ₂ univ₃ =
  Coherently-constant-Σ′ (λ _ → F.id)
  where
  Coherently-constant-Σ′ :
    {P : A → Type p} {Q : ∃ P → Type q} {R : A → Type (p ⊔ q)} →
    (∀ x → R x ≃ ∃ λ (p : P x) → Q (x , p)) →
    Coherently-constant univ₁ P →
    Coherently-constant univ₂ Q →
    Coherently-constant univ₃ R
  Coherently-constant-Σ′
    {P = P} {Q = Q} {R = R} R≃ c₁ c₂ .property x y =

    R x                          ↝⟨ R≃ _ ⟩
    (∃ λ (p : P x) → Q (x , p))  ↝⟨ (Σ-cong (c₁ .property _ _) λ _ → c₂ .property _ _) ⟩
    (∃ λ (p : P y) → Q (y , p))  ↝⟨ inverse $ R≃ _ ⟩□
    R y                          □

  Coherently-constant-Σ′ {P = P} {Q = Q} {R = R} R≃ c₁ c₂ .coherent =
    Coherently-constant-Σ′
      {P = P′}
      {Q = Q′}
      (O.elim λ where
         .O.Elim.∣∣ʳ → R≃
         .O.Elim.∣∣-constantʳ x y → Eq.lift-equality ext $ ⟨ext⟩ λ r →
           let
             p′ , q′ = _≃_.from (Σ-cong (c₁ .property _ _) λ p →
                                 c₂ .property (_ , p) _)
                                (_≃_.to (R≃ y) r)

             lemma₁ =
               subst P′ (O.∣∣-constant x y) p′               ≡⟨ subst-∘ _ _ _ ⟩
               subst P.id (cong P′ (O.∣∣-constant x y)) p′   ≡⟨ cong (λ eq → subst P.id eq _) O.rec-∣∣-constant ⟩
               subst P.id (≃⇒≡ univ₁ (c₁ .property x y)) p′  ≡⟨ subst-id-in-terms-of-≡⇒↝ equivalence ⟩
               ≡⇒→ (≃⇒≡ univ₁ (c₁ .property x y)) p′         ≡⟨ cong (λ eq → _≃_.to eq p′) $ _≃_.right-inverse-of (≡≃≃ univ₁) _ ⟩∎
               _≃_.to (c₁ .property x y) p′                  ∎

             lemma₂ =
               subst (λ p → Q (y , p)) lemma₁
                 (subst Q′ (Σ-≡,≡→≡ (O.∣∣-constant x y) (refl _)) q′)    ≡⟨ cong (subst (λ p → Q (y , p)) lemma₁) $
                                                                            subst-∘ _ _ _ ⟩
               subst (λ p → Q (y , p)) lemma₁
                 (subst (O.rec′ Q λ x y → ≃⇒≡ univ₂ (c₂ .property x y))
                    (cong f (Σ-≡,≡→≡ (O.∣∣-constant x y) (refl _))) q′)  ≡⟨ cong (λ eq →
                                                                                subst (λ p → Q (y , p)) lemma₁
                                                                                (subst (O.rec′ Q λ x y → ≃⇒≡ univ₂ (c₂ .property x y))
                                                                                eq q′)) $
                                                                            elim-Σ-≡,≡→≡-∣∣-constant e ⟩
               subst (λ p → Q (y , p)) lemma₁
                 (subst (O.rec′ Q λ x y → ≃⇒≡ univ₂ (c₂ .property x y))
                    (trans
                       (trans (cong (λ p → ∣ x , p ∣)
                                 (sym (subst-sym-subst _)))
                          (sym (subst-→-domain _ _)))
                       (cong (_$ subst P′ (O.∣∣-constant x y) p′)
                          (⟨ext⟩ λ p →
                           trans (subst-→-domain _ _)
                             (O.∣∣-constant _ (_ , p)))))
                    q′)                                                  ≡⟨ cong (λ eq →
                                                                                subst (λ p → Q (y , p))
                                                                                lemma₁
                                                                                (subst (O.rec′ Q λ x y → ≃⇒≡ univ₂ (c₂ .property x y))
                                                                                (trans
                                                                                (trans (cong (λ p → ∣ x , p ∣)
                                                                                (sym (subst-sym-subst _)))
                                                                                (sym $ subst-→-domain _ _))
                                                                                eq)
                                                                                q′)) $
                                                                            cong-ext
                                                                              (λ p → trans (subst-→-domain P′ {f = λ p → ∣ x , p ∣}
                                                                                (O.∣∣-constant x y))
                                                                                (O.∣∣-constant _ (_ , p))) ⟩
               subst (λ p → Q (y , p)) lemma₁
                 (subst (O.rec′ Q λ x y → ≃⇒≡ univ₂ (c₂ .property x y))
                    (trans
                       (trans (cong (λ p → ∣ x , p ∣)
                                 (sym (subst-sym-subst _)))
                          (sym (subst-→-domain _ _)))
                       (trans (subst-→-domain _ _)
                          (O.∣∣-constant _ _)))
                    q′)                                                  ≡⟨ cong (λ eq → subst (λ p → Q (y , p))
                                                                                lemma₁
                                                                                (subst (O.rec′ Q λ x y → ≃⇒≡ univ₂ (c₂ .property x y))
                                                                                eq q′)) $
                                                                            trans (trans-assoc _ _ _) $
                                                                            cong (trans (cong (λ p → ∣ x , p ∣) $ sym $ subst-sym-subst _)) $
                                                                            trans-sym-[trans] _ (O.∣∣-constant _ _) ⟩
               subst (λ p → Q (y , p)) lemma₁
                 (subst (O.rec′ Q λ x y → ≃⇒≡ univ₂ (c₂ .property x y))
                    (trans (cong (λ p → ∣ x , p ∣)
                              (sym (subst-sym-subst _)))
                       (O.∣∣-constant _ _))
                    q′)                                                  ≡⟨ cong (λ q → subst (λ p → Q (y , p)) lemma₁ q) $
                                                                            trans (subst-∘ _ _ _) $
                                                                            cong (λ eq → subst P.id eq q′) $
                                                                            trans (cong-trans _ _ _) $
                                                                            cong₂ trans
                                                                              (cong-∘ _ _ _)
                                                                              O.rec-∣∣-constant ⟩
               subst (λ p → Q (y , p)) lemma₁
                 (subst P.id
                    (trans
                       (cong (λ p → Q (x , p))
                          (sym (subst-sym-subst _)))
                       (≃⇒≡ univ₂ (c₂ .property _ _)))
                    q′)                                                  ≡⟨ cong (subst (λ p → Q (y , p)) lemma₁) $
                                                                            trans (subst-id-in-terms-of-≡⇒↝ equivalence) $
                                                                            trans (cong (_$ q′) $ ≡⇒↝-trans equivalence) $
                                                                            trans (cong (λ eq → _≃_.to eq (≡⇒→ (cong (λ p → Q (x , p))
                                                                                (sym (subst-sym-subst _)))
                                                                                q′)) $
                                                                                _≃_.right-inverse-of (≡≃≃ univ₂) _) $
                                                                            cong (_≃_.to (c₂ .property _ _)) $ sym $
                                                                            subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩
               subst (λ p → Q (y , p)) lemma₁
                 (_≃_.to (c₂ .property _ _) $
                  subst (λ p → Q (x , p)) (sym (subst-sym-subst _)) q′)  ≡⟨⟩

               subst (λ p → Q (y , p)) lemma₁
                 (_≃_.to (c₂ .property
                            (x , subst P′ (sym (O.∣∣-constant x y))
                                   (subst P′ (O.∣∣-constant x y) p′))
                            (y , subst P′ (O.∣∣-constant x y) p′)) $
                  subst (λ p → Q (x , p)) (sym (subst-sym-subst _)) q′)  ≡⟨ elim¹
                                                                              (λ {p″} eq →
                                                                                subst (λ p → Q (y , p)) lemma₁
                                                                                (_≃_.to (c₂ .property (x , p″)
                                                                                (y , subst P′ (O.∣∣-constant x y) p′)) $
                                                                                subst (λ p → Q (x , p)) eq q′) ≡
                                                                                subst (λ p → Q (y , p)) lemma₁
                                                                                (_≃_.to (c₂ .property (x , p′)
                                                                                (y , subst P′ (O.∣∣-constant x y) p′)) q′))
                                                                              (cong (λ q → subst (λ p → Q (y , p)) lemma₁
                                                                                (_≃_.to (c₂ .property _ _) q)) $
                                                                               subst-refl _ _)
                                                                              _ ⟩
               subst (λ p → Q (y , p)) lemma₁
                 (_≃_.to (c₂ .property
                            (x , p′)
                            (y , subst P′ (O.∣∣-constant x y) p′)) q′)   ≡⟨ elim₁
                                                                              (λ {p″} eq →
                                                                                subst (λ p → Q (y , p)) eq
                                                                                (_≃_.to (c₂ .property (x , p′) (y , p″)) q′) ≡
                                                                                _≃_.to (c₂ .property _ _) q′)
                                                                              (subst-refl _ _)
                                                                              _ ⟩∎
               _≃_.to (c₂ .property
                         (x , p′)
                         (y , _≃_.to (c₁ .property x y) p′)) q′          ∎
           in
           _≃_.to (subst (λ x →
                            O.rec′ R (λ x y → ≃⇒≡ univ₃ (pr x y)) x ≃
                            ∃ λ (p : P′ x) → Q′ (x , p))
                     (O.∣∣-constant x y) (R≃ x))
                  r                                                       ≡⟨ cong (_$ r) Eq.to-subst ⟩

           subst (λ x → O.rec′ R (λ x y → ≃⇒≡ univ₃ (pr x y)) x →
                        ∃ λ (p : P′ x) → Q′ (x , p))
             (O.∣∣-constant x y) (_≃_.to (R≃ x)) r                        ≡⟨ subst-→ ⟩

           subst (λ x → ∃ λ (p : P′ x) → Q′ (x , p)) (O.∣∣-constant x y)
             (_≃_.to (R≃ x)
                (subst (O.rec′ R (λ x y → ≃⇒≡ univ₃ (pr x y)))
                   (sym (O.∣∣-constant x y)) r))                          ≡⟨ cong (subst (λ x → ∃ λ p → Q′ (x , p)) (O.∣∣-constant x y)) $
                                                                             cong (_≃_.to (R≃ x)) $
                                                                             trans (subst-∘ _ _ _) $
                                                                             cong (flip (subst P.id) r) $
                                                                             trans (cong-sym _ _) $
                                                                             cong sym O.rec-∣∣-constant ⟩
           subst (λ x → ∃ λ (p : P′ x) → Q′ (x , p)) (O.∣∣-constant x y)
             (_≃_.to (R≃ x) (subst P.id (sym (≃⇒≡ univ₃ (pr x y))) r))    ≡⟨ cong (subst (λ x → ∃ λ p → Q′ (x , p)) (O.∣∣-constant x y)) $
                                                                             cong (_≃_.to (R≃ x)) $
                                                                             trans (subst-id-in-terms-of-inverse∘≡⇒↝ equivalence) $
                                                                             cong (λ eq → _≃_.from eq r) $ _≃_.right-inverse-of (≡≃≃ univ₃) _ ⟩
           subst (λ x → ∃ λ (p : P′ x) → Q′ (x , p)) (O.∣∣-constant x y)
             (_≃_.to (R≃ x) (_≃_.from (pr x y) r))                        ≡⟨⟩

           subst (λ x → ∃ λ (p : P′ x) → Q′ (x , p)) (O.∣∣-constant x y)
             (_≃_.to (R≃ x) $ _≃_.from (R≃ x) $
              _≃_.from (Σ-cong (c₁ .property _ _) λ _ →
                        c₂ .property _ _) $
              _≃_.to (R≃ y) r)                                            ≡⟨⟩

           subst (λ x → ∃ λ (p : P′ x) → Q′ (x , p)) (O.∣∣-constant x y)
             (_≃_.to (R≃ x) (_≃_.from (R≃ x) (p′ , q′)))                  ≡⟨ cong (subst (λ x → ∃ λ p → Q′ (x , p)) (O.∣∣-constant x y)) $
                                                                             _≃_.right-inverse-of (R≃ x) _ ⟩
           subst (λ x → ∃ λ (p : P′ x) → Q′ (x , p)) (O.∣∣-constant x y)
             (p′ , q′)                                                    ≡⟨ push-subst-pair _ _ ⟩

           subst P′ (O.∣∣-constant x y) p′ ,
           subst Q′ (Σ-≡,≡→≡ (O.∣∣-constant x y) (refl _)) q′             ≡⟨ Σ-≡,≡→≡ lemma₁ lemma₂ ⟩

           _≃_.to (c₁ .property _ _) p′ ,
           _≃_.to (c₂ .property _ _) q′                                   ≡⟨⟩

           _≃_.to (Σ-cong (c₁ .property _ _) λ p →
                   c₂ .property (x , p) _)
             (_≃_.from (Σ-cong (c₁ .property _ _) λ _ →
                        c₂ .property _ _)
                (_≃_.to (R≃ y) r))                                        ≡⟨ _≃_.right-inverse-of
                                                                               (Σ-cong (c₁ .property _ _) λ p →
                                                                                c₂ .property (_ , p) _)
                                                                               _ ⟩∎
           _≃_.to (R≃ y) r                                                ∎)
      (c₁ .coherent)
      (Coherently-constant-map
         univ₂ univ₂ f (λ _ → F.id)
         (c₂ .coherent))

    where

    mutual

      P′ = O.rec′ P (λ x y → ≃⇒≡ univ₁ (c₁ .property x y))
      Q′ = O.rec′ Q (λ x y → ≃⇒≡ univ₂ (c₂ .property x y)) ∘ f

      e = λ where
        .O.Elim.∣∣ʳ x p → ∣ x , p ∣
        .O.Elim.∣∣-constantʳ x y → ⟨ext⟩ λ p →
          subst (λ x → P′ x → ∥ ∃ P ∥¹) (O.∣∣-constant x y)
             (λ p → ∣ x , p ∣) p                             ≡⟨ subst-→-domain _ _ ⟩

          ∣ x , subst P′ (sym (O.∣∣-constant x y)) p ∣       ≡⟨ O.∣∣-constant _ _ ⟩∎

          ∣ y , p ∣                                          ∎

      f = uncurry $ O.elim e

    pr : ∀ _ _ → _
    pr x y =
      (inverse (R≃ y) F.∘
       (Σ-cong (c₁ .property _ _) λ _ → c₂ .property _ _)) F.∘
      R≃ x

private

  -- A unit test that ensures that Coherently-constant-Σ satisfies a
  -- certain definitional equality.

  _ :
    ∀ {P : A → Type p} {Q : ∃ P → Type q}
      {univ₁ : Univalence p}
      {univ₂ : Univalence q}
      {univ₃ : Univalence (p ⊔ q)}
      {c₁ : Coherently-constant univ₁ P}
      {c₂ : Coherently-constant univ₂ Q}
      {x y} →
    _≃_.to (Coherently-constant-Σ
              univ₁ univ₂ univ₃ c₁ c₂ .property x y) ≡
    Σ-map (_≃_.to (c₁ .property _ _)) (_≃_.to (c₂ .property _ _))
  _ = refl _

-- A different proof of Coherently-constant-Σ, with three extra
-- univalence assumptions.
--
-- This proof does not, at the time of writing, satisfy the
-- definitional equality above (rephrased in an obvious way).

Coherently-constant-Σ′ :
  {A : Type a} {P : A → Type p} {Q : ∃ P → Type q}
  (univ₁ : Univalence p)
  (univ₂ : Univalence q)
  (univ₃ : Univalence (p ⊔ q)) →
  Univalence (a ⊔ lsuc p) →
  Univalence (a ⊔ p ⊔ lsuc q) →
  Univalence (a ⊔ lsuc (p ⊔ q)) →
  Coherently-constant univ₁ P →
  Coherently-constant univ₂ Q →
  Coherently-constant univ₃ (λ x → ∃ λ (y : P x) → Q (x , y))
Coherently-constant-Σ′ {P = P} {Q = Q}
  univ₁ univ₂ univ₃ univ₄ univ₅ univ₆ =
  curry
    (Coherently-constant univ₁ P × Coherently-constant univ₂ Q    ↔⟨ inverse
                                                                       (Coherently-constant≃Coherently-constant univ₄ univ₁ ×-cong
                                                                        Coherently-constant≃Coherently-constant univ₅ univ₂) ⟩
     CC.Coherently-constant P × CC.Coherently-constant Q          ↝⟨ uncurry Capriotti.Coherently-constant-Σ ⟩
     CC.Coherently-constant (λ x → ∃ λ (y : P x) → Q (x , y))     ↔⟨ Coherently-constant≃Coherently-constant univ₆ univ₃ ⟩□
     Coherently-constant univ₃ (λ x → ∃ λ (y : P x) → Q (x , y))  □)

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

-- Small coinductive lenses, based on an idea due to Paolo Capriotti.
--
-- The lenses are defined as a record type to make it easier for Agda
-- to infer the argument univ from a value of type Lens univ A B.

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

    -- A getter.
    get : A → B

    -- The family of fibres of the getter is coherently constant.
    get⁻¹-coherently-constant : Coherently-constant univ (get ⁻¹_)

  -- All the getter's fibres are equivalent.

  get⁻¹-constant : (b₁ b₂ : B) → get ⁻¹ b₁ ≃ get ⁻¹ b₂
  get⁻¹-constant = get⁻¹-coherently-constant .property

  -- A setter.

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

  -- The setter could have been defined using Constant-≃-get-⁻¹-≃.

  set≡ :
    ∀ bl →
    set ≡ proj₁ (_≃_.to (Constant-≃-get-⁻¹-≃ bl) get⁻¹-constant)
  set≡ ⊠ = refl _

instance

  -- The lenses defined above have getters and setters.

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

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

Lens-as-Σ :
  {A : Type a} {B : Type b} {univ : Univalence (a ⊔ b)} →
  Lens univ A B ≃
  (∃ λ (get : A → B) → Coherently-constant univ (get ⁻¹_))
Lens-as-Σ = Eq.↔→≃
  (λ l → Lens.get l , Lens.get⁻¹-coherently-constant l)
  (λ (g , c) → record { get = g; get⁻¹-coherently-constant = c })
  refl
  refl

-- Lens is pointwise equivalent to Coinductive.Lens (assuming
-- univalence).

Coinductive-lens≃Lens :
  Block "Coinductive-lens≃Lens" →
  {A : Type a} {B : Type b} →
  Univalence (lsuc (a ⊔ b)) →
  (univ : Univalence (a ⊔ b)) →
  Coinductive.Lens A B ≃ Lens univ A B
Coinductive-lens≃Lens ⊠ {A = A} {B = B} univ₁ univ₂ =
  Coinductive.Lens A B                                             ↔⟨⟩
  (∃ λ (get : A → B) → Coinductive.Coherently-constant (get ⁻¹_))  ↝⟨ (∃-cong λ _ →
                                                                       Coinductive-coherently-constant≃Coherently-constant univ₁ univ₂) ⟩
  (∃ λ (get : A → B) → Coherently-constant univ₂ (get ⁻¹_))        ↝⟨ inverse Lens-as-Σ ⟩□
  Lens univ₂ A B                                                   □

-- The equivalence preserves getters and setters.

Coinductive-lens≃Lens-preserves-getters-and-setters :
  (bl : Block "Coinductive-lens≃Lens")
  {A : Type a} {B : Type b}
  (univ₁ : Univalence (lsuc (a ⊔ b)))
  (univ₂ : Univalence (a ⊔ b)) →
  Preserves-getters-and-setters-⇔ A B
    (_≃_.logical-equivalence (Coinductive-lens≃Lens bl univ₁ univ₂))
Coinductive-lens≃Lens-preserves-getters-and-setters ⊠ univ₁ univ₂ =
  Preserves-getters-and-setters-→-↠-⇔
    (_≃_.surjection (Coinductive-lens≃Lens ⊠ univ₁ univ₂))
    (λ _ → refl _ , refl _)

private

  -- A lemma used to implement Higher-lens≃Lens and
  -- Higher-lens≃Lens-preserves-getters-and-setters.

  Higher-lens≃Lens′ :
    Block "Higher-lens≃Lens" →
    {A : Type a} {B : Type b} →
    Univalence (lsuc (a ⊔ b)) →
    (univ : Univalence (a ⊔ b)) →
    ∃ λ (eq : Higher.Lens A B ≃ Lens univ A B) →
    Preserves-getters-and-setters-⇔ A B (_≃_.logical-equivalence eq)
  Higher-lens≃Lens′ ⊠ {A = A} {B = B} univ₁ univ₂ =
    block λ b →

      (Higher.Lens A B       ↝⟨ inverse $ Capriotti.Lens≃Higher-lens b univ₂ ⟩
       Capriotti.Lens A B    ↝⟨ Coinductive.Higher-lens≃Lens b univ₁ ⟩
       Coinductive.Lens A B  ↝⟨ Coinductive-lens≃Lens b univ₁ univ₂ ⟩□
       Lens univ₂ A B        □)
    , Preserves-getters-and-setters-⇔-∘
        {f = _≃_.logical-equivalence
               (Coinductive-lens≃Lens b univ₁ univ₂) F.∘
             _≃_.logical-equivalence
               (Coinductive.Higher-lens≃Lens b univ₁)}
        {g = inverse $ _≃_.logical-equivalence $
             Capriotti.Lens≃Higher-lens b univ₂}
        (Preserves-getters-and-setters-⇔-∘
           {f = _≃_.logical-equivalence
                  (Coinductive-lens≃Lens b univ₁ univ₂)}
           {g = _≃_.logical-equivalence
                  (Coinductive.Higher-lens≃Lens b univ₁)}
           (Coinductive-lens≃Lens-preserves-getters-and-setters
              b univ₁ univ₂)
           (Coinductive.Higher-lens≃Lens-preserves-getters-and-setters
              b univ₁))
        (Preserves-getters-and-setters-⇔-inverse
           {f = _≃_.logical-equivalence
                  (Capriotti.Lens≃Higher-lens b univ₂)} $
         Capriotti.Lens≃Higher-lens-preserves-getters-and-setters
           b univ₂)

-- Lens is pointwise equivalent to Higher.Lens (assuming univalence).

Higher-lens≃Lens :
  Block "Higher-lens≃Lens" →
  {A : Type a} {B : Type b} →
  Univalence (lsuc (a ⊔ b)) →
  (univ : Univalence (a ⊔ b)) →
  Higher.Lens A B ≃ Lens univ A B
Higher-lens≃Lens b univ₁ univ₂ =
  proj₁ $ Higher-lens≃Lens′ b univ₁ univ₂

-- The equivalence preserves getters and setters.

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

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

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

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

  _≃_.from equiv l₁ ≡ _≃_.from equiv l₂  ↔⟨ Eq.≃-≡ (inverse equiv) ⟩□

  l₁ ≡ l₂                                □

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

-- An identity lens.

id :
  {A : Type a}
  (univ : Univalence a) →
  Lens univ A A
id univ .Lens.get                       = P.id
id univ .Lens.get⁻¹-coherently-constant =
  coherently-constant λ x →
                              $⟨ Preimage.id⁻¹-contractible x ⟩
    Contractible (P.id ⁻¹ x)  ↝⟨ Eq.↔⇒≃ ∘ _⇔_.to contractible⇔↔⊤ ⟩□
    P.id ⁻¹ x ≃ ⊤             □
  where
  coherently-constant :
    (∀ x → P x ≃ ⊤) →
    Coherently-constant univ P
  coherently-constant {P = P} P≃⊤ .property x y =
    P x  ↝⟨ P≃⊤ x ⟩
    ⊤    ↝⟨ inverse $ P≃⊤ y ⟩□
    P y  □
  coherently-constant P≃⊤ .coherent =
    coherently-constant
      (O.elim λ where
         .O.Elim.∣∣ʳ → P≃⊤
         .O.Elim.∣∣-constantʳ _ _ →
           Eq.lift-equality ext $ refl (λ _ → tt))

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

-- Composition.
--
-- Paolo Capriotti came up with the idea to use Coherently-constant-Σ.
-- At first we had a problem related to universe levels. Andrea
-- Vezzosi came up with a first workaround (involving lifting), and
-- later I found a more direct solution.

infix 9 ⟨_,_⟩_∘_

⟨_,_⟩_∘_ :
  {A : Type a} {B : Type b} {C : Type c}
  {univ₁ : Univalence (b ⊔ c)}
  {univ₂ : Univalence (a ⊔ b)}
  (univ₃ : Univalence (a ⊔ c)) →
  Univalence (a ⊔ b ⊔ c) →
  Lens univ₁ B C → Lens univ₂ A B → Lens univ₃ A C
(⟨ _ , _ ⟩ l₁ ∘ l₂) .Lens.get = get l₁ ∘ get l₂
  where
  open Lens
⟨_,_⟩_∘_ {b = ℓb} {univ₁ = univ₁} {univ₂ = univ₂} univ₃ univ₄ l₁ l₂
  .Lens.get⁻¹-coherently-constant =
                                                       $⟨ Coherently-constant-Σ
                                                            {P = get l₁ ⁻¹_}
                                                            {Q = λ (_ , b , _) → get l₂ ⁻¹ b}
                                                            univ₁ univ₂ univ₄
                                                            (get⁻¹-coherently-constant l₁)
                                                            (Coherently-constant-map univ₂ univ₂
                                                               (proj₁ ∘ proj₂) (λ _ → F.id)
                                                               (get⁻¹-coherently-constant l₂)) ⟩
  Coherently-constant univ₄
    (λ c → ∃ λ ((b , _) : get l₁ ⁻¹ c) → get l₂ ⁻¹ b)  ↝⟨ Coherently-constant-map univ₄ univ₃ P.id
                                                            (λ _ → inverse $ ∘⁻¹≃ (get l₁) (get l₂)) ⟩□
  Coherently-constant univ₃ ((get l₁ ∘ get l₂) ⁻¹_)    □
  where
  open Lens

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

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

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

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

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

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

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

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

-- The definitions in the following module use seven instances of
-- univalence.

module _
  {A : Type a} {B : Type b} {C : Type c}
  (univ₁ : Univalence (b ⊔ c))
  (univ₂ : Univalence (lsuc (b ⊔ c)))
  (univ₃ : Univalence (a ⊔ b))
  (univ₄ : Univalence (lsuc (a ⊔ b)))
  (univ₅ : Univalence (a ⊔ c))
  (univ₆ : Univalence (lsuc (a ⊔ c)))
  (univ₇ : Univalence (a ⊔ b ⊔ c))
  where

  -- An unrestricted composition operator for Higher.Lens (defined using
  -- univalence).

  infix 9 ⟨_,_,_,_,_,_,_,_⟩_⊚_

  ⟨_,_,_,_,_,_,_,_⟩_⊚_ :
    Block "Higher-lens≃Lens" →
    Higher.Lens B C → Higher.Lens A B → Higher.Lens A C
  ⟨_,_,_,_,_,_,_,_⟩_⊚_ b l₁ l₂ =
    _≃_.from (Higher-lens≃Lens b univ₆ univ₅)
      (⟨ univ₅ , univ₇ ⟩
         _≃_.to (Higher-lens≃Lens b univ₂ univ₁) l₁ ∘
         _≃_.to (Higher-lens≃Lens b univ₄ univ₃) l₂)

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

  set-⊚ :
    (b : Block "Higher-lens≃Lens") →
    ∀ (l₁ : Higher.Lens B C) (l₂ : Higher.Lens A B) a c →
    Higher.Lens.set (⟨_,_,_,_,_,_,_,_⟩_⊚_ b l₁ l₂) a c ≡
    Higher.Lens.set l₂ a (Higher.Lens.set l₁ (Higher.Lens.get l₂ a) c)
  set-⊚ b l₁ l₂ a c =
    Higher.Lens.set
      (_≃_.from (Higher-lens≃Lens b univ₆ univ₅)
         (⟨ univ₅ , univ₇ ⟩
            _≃_.to (Higher-lens≃Lens b univ₂ univ₁) l₁ ∘
            _≃_.to (Higher-lens≃Lens b univ₄ univ₃) l₂))
      a c                                                               ≡⟨ cong (λ f → f a c) $
                                                                           proj₂ $
                                                                           proj₂ (Higher-lens≃Lens-preserves-getters-and-setters b univ₆ univ₅)
                                                                             (⟨ univ₅ , univ₇ ⟩
                                                                                _≃_.to (Higher-lens≃Lens b univ₂ univ₁) l₁ ∘
                                                                                _≃_.to (Higher-lens≃Lens b univ₄ univ₃) l₂) ⟩
    Lens.set
      (⟨ univ₅ , univ₇ ⟩
         _≃_.to (Higher-lens≃Lens b univ₂ univ₁) l₁ ∘
         _≃_.to (Higher-lens≃Lens b univ₄ univ₃) l₂)
      a c                                                               ≡⟨⟩

    Lens.set (_≃_.to (Higher-lens≃Lens b univ₄ univ₃) l₂)
      a
      (Lens.set (_≃_.to (Higher-lens≃Lens b univ₂ univ₁) l₁)
         (Lens.get (_≃_.to (Higher-lens≃Lens b univ₄ univ₃) l₂) a) c)   ≡⟨ cong (λ f →
                                                                                f a (Lens.set (_≃_.to (Higher-lens≃Lens b univ₂ univ₁) l₁)
                                                                                (Lens.get (_≃_.to (Higher-lens≃Lens b univ₄ univ₃) l₂) a)
                                                                                c)) $
                                                                           proj₂ $
                                                                           proj₁ (Higher-lens≃Lens-preserves-getters-and-setters b univ₄ univ₃) l₂ ⟩
    Higher.Lens.set l₂
      a
      (Lens.set (_≃_.to (Higher-lens≃Lens b univ₂ univ₁) l₁)
         (Lens.get (_≃_.to (Higher-lens≃Lens b univ₄ univ₃) l₂) a) c)   ≡⟨ cong (Higher.Lens.set l₂ a) $
                                                                           cong₂ (λ f g → f (g a) c)
                                                                             (proj₂ $
                                                                              proj₁ (Higher-lens≃Lens-preserves-getters-and-setters b univ₂ univ₁)
                                                                                l₁)
                                                                             (proj₁ $
                                                                              proj₁ (Higher-lens≃Lens-preserves-getters-and-setters b univ₄ univ₃)
                                                                                l₂) ⟩∎
    Higher.Lens.set l₂ a (Higher.Lens.set l₁ (Higher.Lens.get l₂ a) c)  ∎

-- If the view type of the resulting lens is stable, then the
-- definition of composition above matches the one in higher (when
-- applicable).

⊚≡∘ :
  (bl : Block "Higher-lens≃Lens") →
  ∀ a b {A : Type (a ⊔ b ⊔ c)} {B : Type (b ⊔ c)} {C : Type c}
  (univ₁ : Univalence (b ⊔ c))
  (univ₂ : Univalence (lsuc (b ⊔ c)))
  (univ₃ : Univalence (a ⊔ b ⊔ c))
  (univ₄ : Univalence (lsuc (a ⊔ b ⊔ c)))
  (univ₅ : Univalence (a ⊔ b ⊔ c))
  (univ₆ : Univalence (lsuc (a ⊔ b ⊔ c)))
  (univ₇ : Univalence (a ⊔ b ⊔ c))
  (l₁ : Higher.Lens B C) (l₂ : Higher.Lens A B) →
  (∥ C ∥ → C) →
  ⟨ univ₁ , univ₂ , univ₃ , univ₄ , univ₅ , univ₆ , univ₇ , bl ⟩
    l₁ ⊚ l₂ ≡
  HC.⟨ a , b ⟩ l₁ ∘ l₂
⊚≡∘ bl a b univ₁ univ₂ univ₃ univ₄ univ₅ univ₆ univ₇ l₁ l₂ stable =
  cong (λ f → f l₁ l₂) $
  HC.composition≡∘ a b univ₇ stable
    ⟨ univ₁ , univ₂ , univ₃ , univ₄ , univ₅ , univ₆ , univ₇ , bl ⟩_⊚_
    (set-⊚ univ₁ univ₂ univ₃ univ₄ univ₅ univ₆ univ₇ bl)

------------------------------------------------------------------------
-- An alternative definition that does not make use of coinduction

-- A variant of Lens.
--
-- This definition does not make use of coinduction, but it is not
-- small.

Not-coinductive-lens :
  Univalence (a ⊔ b) → Type a → Type b → Type (lsuc (a ⊔ b))
Not-coinductive-lens univ A B =
  ∃ λ (get : A → B) →
    NC.Coherently
      Constant-≃
      (λ P c → O.rec′ P (λ x y → ≃⇒≡ univ (c x y)))
      (get ⁻¹_)

-- Not-coinductive-lens is pointwise equivalent to Lens (assuming
-- univalence).

Not-coinductive-lens≃Lens :
  {univ : Univalence (a ⊔ b)} {A : Type a} {B : Type b} →
  Univalence (lsuc (a ⊔ b)) →
  Not-coinductive-lens univ A B ≃ Lens univ A B
Not-coinductive-lens≃Lens {univ = univ} {A = A} {B = B} univ′ =
  Not-coinductive-lens univ A B                             ↝⟨ (∃-cong λ _ → inverse $ Coherently≃Not-coinductive-coherently univ′ univ′) ⟩
  (∃ λ (get : A → B) → Coherently-constant univ (get ⁻¹_))  ↝⟨ inverse Lens-as-Σ ⟩□
  Lens univ A B                                             □

------------------------------------------------------------------------
-- H-levels

-- If P has h-level n (pointwise), then Coherently-constant univ P has
-- h-level n (assuming univalence).
--
-- I think that Paolo Capriotti suggested that something like this
-- could be proved by using the result (due to Ahrens, Capriotti and
-- Spadotti, see "Non-wellfounded trees in Homotopy Type Theory") that
-- M-types for indexed containers have h-level n if all shapes have
-- h-level n.

H-level-Coherently-constant :
  {A : Type a} {P : A → Type p} →
  Univalence (lsuc (a ⊔ p)) →
  (univ : Univalence p) →
  ((a : A) → H-level n (P a)) →
  H-level n (Coherently-constant univ P)
H-level-Coherently-constant {a = a} {p = p} {n = n} univ _ h =
  H-level-Coherently-→Type univ univ h lemma P.id
  where
  lemma :
    {A : Type a} {P : A → Type p} →
    ((a : A) → H-level n (P a)) →
    H-level n (Constant-≃ P)
  lemma h =
    Π-closure ext n λ _ →
    Π-closure ext n λ _ →
    Eq.h-level-closure ext n (h _) (h _)

-- If P has h-level n (pointwise), then
-- Coinductive.Coherently-constant P has h-level n (assuming
-- univalence).

H-level-Coinductive-Coherently-constant :
  {A : Type a} {P : A → Type p} →
  Univalence (lsuc (a ⊔ p)) →
  Univalence (a ⊔ lsuc p) →
  Univalence p →
  ((a : A) → H-level n (P a)) →
  H-level n (Coinductive.Coherently-constant P)
H-level-Coinductive-Coherently-constant {n = n} {P = P} univ₁ univ₂ univ₃ =
  (∀ a → H-level n (P a))                        ↝⟨ H-level-Coherently-constant univ₁ univ₃ ⟩
  H-level n (Coherently-constant univ₃ P)        ↝⟨ H-level-cong _ n (inverse $ Coinductive-coherently-constant≃Coherently-constant univ₂ univ₃) ⟩□
  H-level n (Coinductive.Coherently-constant P)  □

-- If A and B have h-level n given the assumption that the other type
-- is inhabited, then Lens univ A B has h-level n (assuming
-- univalence).
--
-- I do not remember who came up with the idea to prove this for the
-- coinductive lenses (rather than the ones in
-- Lens.Non-dependent.Higher). It may have been Paolo Capriotti or
-- Andrea Vezzosi.

lens-preserves-h-level :
  {A : Type a} {B : Type b} →
  Univalence (lsuc (a ⊔ b)) →
  (univ : Univalence (a ⊔ b)) →
  ∀ n → (B → H-level n A) → (A → H-level n B) →
  H-level n (Lens univ A B)
lens-preserves-h-level univ′ univ n hA hB =
  H-level-cong _ n (inverse Lens-as-Σ) $
  Σ-closure n
    (Π-closure ext n λ a →
     hB a) λ _ →
  H-level-Coherently-constant univ′ univ λ b →
  Σ-closure n (hA b) λ a →
  H-level.⇒≡ n (hB a)

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

h-level-respects-lens-from-inhabited :
  {A : Type a} {B : Type b} →
  Univalence (lsuc (a ⊔ b)) →
  (univ : Univalence (a ⊔ b)) →
  ∀ n → Lens univ A B → A → H-level n A → H-level n B
h-level-respects-lens-from-inhabited univ′ univ n =
  Higher.h-level-respects-lens-from-inhabited n ∘
  _≃_.from (Higher-lens≃Lens ⊠ univ′ univ)

-- If A has positive h-level n, then Lens univ A B also has h-level n
-- (assuming univalence).

lens-preserves-h-level-of-domain :
  {A : Type a} {B : Type b} →
  Univalence (lsuc (a ⊔ b)) →
  (univ : Univalence (a ⊔ b)) →
  ∀ n → H-level (1 + n) A → H-level (1 + n) (Lens univ A B)
lens-preserves-h-level-of-domain univ′ univ n hA =
  H-level.[inhabited⇒+]⇒+ n λ l →
  lens-preserves-h-level univ′ univ (1 + n) (λ _ → hA) λ a →
  h-level-respects-lens-from-inhabited univ′ univ _ l a hA

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


text:
module test where

data Bool : Set where
    True  : Bool
    False : Bool

!_ : Bool → Bool
! True  = False
! False = True

if_then_else_ : {A : Set} → Bool → A → A → A
if True then x else y = x
if False then x else y = y

data ℕ : Set where
    zero : ℕ
    suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + a = a
suc a + b = suc (a + b)

low = suc zero
high = low + (low + low)

data List (A : Set) : Set where
    Nil  : List A
    Cons : A → List A → List A

length : {A : Set} → List A → ℕ
length Nil = zero
length (Cons x x₁) = suc (length x₁)

map : {A B : Set} → (A → B) → List A → List B
map f Nil = Nil
map f (Cons x l) = Cons (f x) (map f l)

concat : {A : Set} → List A → List A → List A
concat Nil m = m
concat (Cons x l) m = Cons x (concat l m)

ext: agda


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

module Data.Binary.Conversion.Fast.Strict where

open import Data.Binary.Definition
open import Data.Nat.DivMod
open import Data.Nat.Base using (ℕ; suc; zero)
open import Strict
open import Data.Bool

⟦_⇑⟧⟨_⟩ : ℕ → ℕ → 𝔹
⟦ suc n ⇑⟧⟨ suc w ⟩ =
  let! m =! even n in!
  let! ms =! ⟦ n ÷ 2 ⇑⟧⟨ w ⟩ in!
  if m then 1ᵇ ms else 2ᵇ ms
⟦ zero  ⇑⟧⟨ _    ⟩ = 0ᵇ
⟦ suc _ ⇑⟧⟨ zero ⟩ = 0ᵇ -- will not happen

⟦_⇑⟧ : ℕ → 𝔹
⟦ n ⇑⟧ = ⟦ n ⇑⟧⟨ n ⟩
{-# INLINE ⟦_⇑⟧ #-}

-- Without the added argument to the recursor, the function does not
-- pass the termination checker:
-- {-# TERMINATING #-}
-- ⟦_⇑⟧″ : ℕ → 𝔹
-- ⟦ zero  ⇑⟧″ = 0ᵇ
-- ⟦ suc n ⇑⟧″ =
--   if rem n 2 ℕ.≡ᴮ 0
--   then 1ᵇ ⟦ n ÷ 2 ⇑⟧″
--   else 2ᵇ ⟦ n ÷ 2 ⇑⟧″

-- The "principled" version (which uses well-founded recursion) is
-- incredibly slow. (and the following doesn't even compute, because of
-- cubical)

-- open import Data.Nat.WellFounded

-- ⟦_⇑⟧‴ : ℕ → 𝔹
-- ⟦ n ⇑⟧‴ = go n (≤-wellFounded n)
--   where
--   go : ∀ n → Acc _<_ n → 𝔹
--   go zero    wf = 0ᵇ
--   go (suc n) (acc wf) =
--     if rem n 2 ℕ.≡ᴮ 0
--     then 1ᵇ go (n ÷ 2) (wf (n ÷ 2) (s≤s (div2≤ n)))
--     else 2ᵇ go (n ÷ 2) (wf (n ÷ 2) (s≤s (div2≤ n)))

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Andreas, 2017-10-04, issue #2753, reported by nad

-- Here, late solving of size constraints, prevented assignment
-- of instance metas to their solutions, since the metaOccurs
-- check then had more information through meta instantiation
-- and saw the loop.

-- To solve this issue, we switch off the meta-occurs check
-- for instance metas.  Instance search termination responsiblity
-- rests already in the hand of the user.

-- {-# OPTIONS -v tc.instance:30 #-}
-- {-# OPTIONS -v tc.constr.solve:30 #-}
-- {-# OPTIONS -v tc.size.solve:30 #-}
-- {-# OPTIONS -v tc.meta.assign:10 #-}

open import Agda.Builtin.Size

-- Worked without sized types since instance search succeeds
-- then quicker (not having to wait on the size constraint solver).

-- postulate
--   Size : Set

-- Size<_ : Size → Set
-- Size< i = Size

mutual

  data D (i : Size) : Set where
    c : D′ i → D i

  data D′ (i : Size) : Set where
    box : (j : Size< i) → D j → D′ i

record Fun (A B : Set) : Set where
  field
    applyTo : A → B

open Fun ⦃ … ⦄ public

mutual

  instance

    r : ∀ {i} → Fun (D i) (D i)
    Fun.applyTo r (c y) = c (applyTo y)

    r′ : ∀ {i} → Fun (D′ i) (D′ i)
    Fun.applyTo r′ (box j e) = box j (applyTo e)

-- Andreas' analysis as put on the bug tracker:
--
-- @UlfNorell is correct: the metaOccurs check prevents the
-- solution. However, why does it work without the sized types then? The
-- meta-occurs check does not go into solutions of metas. Thus, in the
-- case without sized types, where instance search succeeds immediately
-- (solving the hidden argument i by the conversion check), we are lucky
-- enough to slip through the meta-occurs check. However, in the case
-- with sized types, instance search does not succeed immediately because
-- the constraint on size i does not give a solution for i
-- directly. After size solving, instance search is retried, but then
-- (when we solve the second instance variable), instantiateFull already
-- has put in the solution for the first instance variable. Thus, the
-- loop becomes apparent, and metaOccurs protests.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-

Matrix with coefficients in a commutative ring

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.Matrix.CommRingCoefficient where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Powerset

open import Cubical.Data.Nat hiding (_+_ ; _·_)
open import Cubical.Data.FinData

open import Cubical.Data.Sigma
open import Cubical.Data.Empty as Empty

open import Cubical.Relation.Nullary

open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.BigOps
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.RingSolver.Reflection

open import Cubical.Algebra.Matrix

private
  variable
    ℓ : Level
    m n k l : ℕ

module Coefficient (𝓡 : CommRing ℓ) where

  private
    R = 𝓡 .fst
    𝑹 = CommRing→Ring 𝓡
    AbR = Ring→AbGroup 𝑹

  open CommRingStr       (𝓡 .snd) renaming ( is-set to isSetR )

  open Sum                𝑹
  open FinMatrixAbGroup

  -- Convenient renaming

  Mat : (m n : ℕ) → Type ℓ
  Mat m n = FinMatrix R m n

  isSetMat : isSet (Mat m n)
  isSetMat = isSetΠ2 (λ _ _ → isSetR)

  isContrEmpty : {n : ℕ} → isContr (Mat 0 n)
  isContrEmpty =
    isOfHLevelRespectEquiv _ (equiv→ (uninhabEquiv (λ ()) ¬Fin0) (idEquiv _)) isContr⊥→A

  isContrEmptyᵗ : {m : ℕ} → isContr (Mat m 0)
  isContrEmptyᵗ =
    isContrΠ (λ _ → isOfHLevelRespectEquiv _ (equiv→ (uninhabEquiv (λ ()) ¬Fin0) (idEquiv _)) isContr⊥→A)

  𝟙 : Mat n n
  𝟙 = oneFinMatrix 𝑹

  𝟘 : Mat m n
  𝟘 = zeroFinMatrix AbR

  _⋆_ : Mat m n → Mat n k → Mat m k
  M ⋆ N = mulFinMatrix 𝑹 M N

  infixl 8 _⋆_

  ⋆lUnit : (M : Mat m n) → 𝟙 ⋆ M ≡ M
  ⋆lUnit = mulFinMatrix1r 𝑹

  ⋆rUnit : (M : Mat m n) → M ⋆ 𝟙 ≡ M
  ⋆rUnit = mulFinMatrixr1 𝑹

  ⋆Assoc : (M : Mat m n)(N : Mat n k)(K : Mat k l) → M ⋆ (N ⋆ K) ≡ (M ⋆ N) ⋆ K
  ⋆Assoc = mulFinMatrixAssoc 𝑹

  -- Transposition

  _ᵗ : Mat m n → Mat n m
  (M ᵗ) i j = M j i

  idemᵗ : (M : Mat m n) → (M ᵗ)ᵗ ≡ M
  idemᵗ M t i j = M i j

  compᵗ : (M : Mat m n)(N : Mat n k) → (M ⋆ N)ᵗ ≡ N ᵗ ⋆ M ᵗ
  compᵗ M N t i j = ∑ (λ l → ·Comm (M j l) (N l i) t)

  𝟙ᵗ : 𝟙 ᵗ ≡ 𝟙 {n = n}
  𝟙ᵗ t zero    zero    = 1r
  𝟙ᵗ t (suc i) zero    = 0r
  𝟙ᵗ t zero    (suc j) = 0r
  𝟙ᵗ t (suc i) (suc j) = 𝟙ᵗ t i j

  -- Invertible matrices

  isInv' : Mat n n → Mat n n → Type ℓ
  isInv' {n = n} M N = (M ⋆ N ≡ 𝟙) × (N ⋆ M ≡ 𝟙)

  isPropIsInv' : (M N : Mat n n) → isProp (isInv' M N)
  isPropIsInv' M N = isProp× (isSetMat _ _) (isSetMat _ _)

  invUniq : (M N N' : Mat n n) → isInv' M N → isInv' M N' → N ≡ N'
  invUniq M N N' p q =
      sym (⋆lUnit N)
    ∙ (λ i → q .snd (~ i) ⋆ N)
    ∙ sym (⋆Assoc N' M N)
    ∙ (λ i → N' ⋆ p .fst i)
    ∙ ⋆rUnit N'

  isInv : Mat n n → Type ℓ
  isInv {n = n} M = Σ[ N ∈ Mat n n ] isInv' M N

  isPropIsInv : (M : Mat n n) → isProp (isInv M)
  isPropIsInv M p q = Σ≡Prop (λ _ → isPropIsInv' M _) (invUniq M _ _ (p .snd) (q .snd))

  isInv⋆ : {M M' : Mat n n} → isInv M → isInv M' → isInv (M ⋆ M')
  isInv⋆ (N , p) (N' , q) .fst = N' ⋆ N
  isInv⋆ {M = M} {M' = M'} (N , p) (N' , q) .snd .fst =
      sym (⋆Assoc M M' (N' ⋆ N))
    ∙ (λ i → M ⋆ ⋆Assoc M' N' N i)
    ∙ (λ i → M ⋆ (q .fst i ⋆ N))
    ∙ (λ i → M ⋆ ⋆lUnit N i)
    ∙ p .fst
  isInv⋆ {M = M} {M' = M'} (N , p) (N' , q) .snd .snd =
      sym (⋆Assoc N' N (M ⋆ M'))
    ∙ (λ i → N' ⋆ ⋆Assoc N M M' i)
    ∙ (λ i → N' ⋆ (p .snd i ⋆ M'))
    ∙ (λ i → N' ⋆ ⋆lUnit M' i)
    ∙ q .snd

  InvMat : (n : ℕ) → Type ℓ
  InvMat n = Σ[ M ∈ Mat n n ] isInv M

  isInv𝟙 : isInv {n = n} 𝟙
  isInv𝟙 .fst = 𝟙
  isInv𝟙 .snd .fst = ⋆lUnit _
  isInv𝟙 .snd .snd = ⋆lUnit _

  isInvᵗ : {M : Mat n n} → isInv M → isInv (M ᵗ)
  isInvᵗ {M = M} isInvM .fst = (isInvM .fst)ᵗ
  isInvᵗ {M = M} isInvM .snd .fst = (sym (compᵗ _ M)) ∙ (λ t → (isInvM .snd .snd t)ᵗ) ∙ 𝟙ᵗ
  isInvᵗ {M = M} isInvM .snd .snd = (sym (compᵗ M _)) ∙ (λ t → (isInvM .snd .fst t)ᵗ) ∙ 𝟙ᵗ

  -- Inversion formula for 2 × 2 matrices

  dot2 : (V W : FinVec R 2) → (∑ λ i → V i · W i) ≡ V zero · W zero + V one · W one
  dot2 V W i = V zero · W zero + (+Rid (V one · W one) i)

  mul2 :
      (M : Mat m 2)(N : Mat 2 n)
    → (i : Fin m)(j : Fin n)
    → (M ⋆ N) i j ≡ M i zero · N zero j + M i one · N one j
  mul2 M N i j = dot2 (M i) (λ k → N k j)

  open Units 𝓡

  det2×2 : Mat 2 2 → R
  det2×2 M = M zero zero · M one one - M zero one · M one zero

  module _
    (M : Mat 2 2)(p : det2×2 M ∈ Rˣ) where

    private
      Δ   = det2×2 M
      Δ⁻¹ = (_⁻¹) Δ ⦃ p ⦄

      ·rInv : Δ · Δ⁻¹ ≡ 1r
      ·rInv = ·-rinv _ ⦃ p ⦄

      M⁻¹ : Mat 2 2
      M⁻¹ zero zero =   M one  one  · Δ⁻¹
      M⁻¹ zero one  = - M zero one  · Δ⁻¹
      M⁻¹ one  zero = - M one  zero · Δ⁻¹
      M⁻¹ one  one  =   M zero zero · Δ⁻¹

    isInvMat2x2 : isInv M
    isInvMat2x2 .fst = M⁻¹
    isInvMat2x2 .snd .fst i zero zero =
      (mul2 M M⁻¹ zero zero ∙ helper _ _ _ _ _ ∙ ·rInv) i
      where helper : (x y z w d : R) → x · (w · d) + y · (- z · d) ≡  (x · w - y · z) · d
            helper = solve 𝓡
    isInvMat2x2 .snd .fst i zero one  =
      (mul2 M M⁻¹ zero one  ∙ helper _ _ _) i
      where helper : (x y d : R) → x · (- y · d) + y · (x · d) ≡ 0r
            helper = solve 𝓡
    isInvMat2x2 .snd .fst i one  zero =
      (mul2 M M⁻¹ one  zero ∙ helper _ _ _) i
      where helper : (z w d : R) → z · (w · d) + w · (- z · d) ≡ 0r
            helper = solve 𝓡
    isInvMat2x2 .snd .fst i one  one  =
      (mul2 M M⁻¹ one  one  ∙ helper _ _ _ _ _ ∙ ·rInv) i
      where helper : (x y z w d : R) → z · (- y · d) + w · (x · d) ≡  (x · w - y · z) · d
            helper = solve 𝓡
    isInvMat2x2 .snd .snd i zero zero =
      (mul2 M⁻¹ M zero zero ∙ helper _ _ _ _ _ ∙ ·rInv) i
      where helper : (x y z w d : R) → (w · d) · x + (- y · d) · z ≡  (x · w - y · z) · d
            helper = solve 𝓡
    isInvMat2x2 .snd .snd i zero one  =
      (mul2 M⁻¹ M zero one  ∙ helper _ _ _) i
      where helper : (y w d : R) → (w · d) · y + (- y · d) · w ≡ 0r
            helper = solve 𝓡
    isInvMat2x2 .snd .snd i one  zero =
      (mul2 M⁻¹ M one  zero ∙ helper _ _ _) i
      where helper : (x z d : R) → (- z · d) · x + (x · d) · z ≡ 0r
            helper = solve 𝓡
    isInvMat2x2 .snd .snd i one  one  =
      (mul2 M⁻¹ M one  one  ∙ helper _ _ _ _ _ ∙ ·rInv) i
      where helper : (x y z w d : R) → (- z · d) · y + (x · d) · w ≡  (x · w - y · z) · d
            helper = solve 𝓡

  -- Similarity of matrices

  record SimRel (M N : Mat m n) : Type ℓ where
    field
      transMatL : Mat m m
      transMatR : Mat n n
      transEq : N ≡ transMatL ⋆ M ⋆ transMatR

      isInvTransL : isInv transMatL
      isInvTransR : isInv transMatR

  open SimRel

  record Sim (M : Mat m n) : Type ℓ where
    field
      result : Mat m n
      simrel : SimRel M result

  open Sim

  idSimRel : (M : Mat m n) → SimRel M M
  idSimRel _ .transMatL = 𝟙
  idSimRel _ .transMatR = 𝟙
  idSimRel M .transEq = sym ((λ t → ⋆lUnit M t ⋆ 𝟙) ∙ ⋆rUnit _)
  idSimRel _ .isInvTransL = isInv𝟙
  idSimRel _ .isInvTransR = isInv𝟙

  idSim : (M : Mat m n) → Sim M
  idSim M .result = M
  idSim M .simrel = idSimRel M

  ≡SimRel : {M N : Mat m n} → M ≡ N → SimRel M N
  ≡SimRel p .transMatL = 𝟙
  ≡SimRel p .transMatR = 𝟙
  ≡SimRel {M = M} p .transEq = sym p ∙ sym ((λ t → ⋆lUnit M t ⋆ 𝟙) ∙ ⋆rUnit _)
  ≡SimRel p .isInvTransL = isInv𝟙
  ≡SimRel p .isInvTransR = isInv𝟙

  ≡Sim : {M N : Mat m n} → M ≡ N → Sim M
  ≡Sim _ .result = _
  ≡Sim p .simrel = ≡SimRel p

  compSimRel : {M N K : Mat m n} → SimRel M N → SimRel N K → SimRel M K
  compSimRel p q .transMatL = q .transMatL ⋆ p .transMatL
  compSimRel p q .transMatR = p .transMatR ⋆ q .transMatR
  compSimRel {M = M} p q .transEq =
      let L  = p .transMatL
          R  = p .transMatR
          L' = q .transMatL
          R' = q .transMatR in
      q .transEq
    ∙ (λ t → L' ⋆ p .transEq t ⋆ R')
    ∙ (λ t → L' ⋆ ⋆Assoc L M R (~ t) ⋆ R')
    ∙ (λ t → ⋆Assoc L' (L ⋆ (M ⋆ R)) R' (~ t))
    ∙ (λ t → L' ⋆ ⋆Assoc L (M ⋆ R) R' (~ t))
    ∙ (λ t → L' ⋆ (L ⋆ ⋆Assoc M R R' (~ t)))
    ∙ (λ t → L' ⋆ ⋆Assoc L M (R ⋆ R') t)
    ∙ (λ t → ⋆Assoc L' (L ⋆ M) (R ⋆ R') t)
    ∙ (λ t → ⋆Assoc L' L M t ⋆ (R ⋆ R'))
  compSimRel p q .isInvTransL = isInv⋆ (q .isInvTransL) (p .isInvTransL)
  compSimRel p q .isInvTransR = isInv⋆ (p .isInvTransR) (q .isInvTransR)

  compSim : {M : Mat m n}(p : Sim M)(q : Sim (p .result)) → Sim M
  compSim p q .result = q .result
  compSim p q .simrel = compSimRel (p .simrel) (q .simrel)

  -- Add a new element at upper-left corner

  _⊕_ : R → Mat m n → Mat (suc m) (suc n)
  (a ⊕ M) zero    zero    = a
  (a ⊕ M) (suc i) zero    = 0r
  (a ⊕ M) zero    (suc j) = 0r
  (a ⊕ M) (suc i) (suc j) = M i j

  infixr 5 _⊕_

  sucMat : (M : Mat (suc m) (suc n)) → Mat m n
  sucMat M i j = M (suc i) (suc j)

  𝟙suc : (i j : Fin m) → 𝟙 i j ≡ sucMat 𝟙 i j
  𝟙suc zero    zero    = refl
  𝟙suc (suc i) zero    = refl
  𝟙suc zero    (suc j) = refl
  𝟙suc (suc i) (suc j) = refl

  1⊕𝟙 : 1r ⊕ 𝟙 {n = n} ≡ 𝟙
  1⊕𝟙 t zero    zero    = 1r
  1⊕𝟙 t (suc i) zero    = 0r
  1⊕𝟙 t zero    (suc j) = 0r
  1⊕𝟙 t (suc i) (suc j) = 𝟙suc i j t

  ⊕-⋆ : (a b : R)(M : Mat m n)(N : Mat n k) → (a ⊕ M) ⋆ (b ⊕ N) ≡ (a · b) ⊕ (M ⋆ N)
  ⊕-⋆ {n = n} a b M N t zero zero =
    ((λ t → a · b + ∑Mul0r {n = n} (λ i → 0r) t) ∙ helper _ _) t
    where helper : (a b : R) → a · b + 0r ≡ a · b
          helper = solve 𝓡
  ⊕-⋆ a b M N t zero (suc j) = (helper a _ ∙ ∑Mul0r (λ i → N i j)) t
    where helper : (a c : R) → a · 0r + c ≡ c
          helper = solve 𝓡
  ⊕-⋆ a b M N t (suc i) zero = (helper b _ ∙ ∑Mulr0 (λ j → M i j)) t
    where helper : (b c : R) → 0r · b + c ≡ c
          helper = solve 𝓡
  ⊕-⋆ _ _ M N t (suc i) (suc j) = helper ((M ⋆ N) i j) t
    where helper : (c : R) → 0r · 0r + c ≡ c
          helper = solve 𝓡

  isInv⊕ : (M : Mat m m) → isInv M → (isInv (1r ⊕ M))
  isInv⊕ M isInvM .fst = 1r ⊕ isInvM .fst
  isInv⊕ M isInvM .snd .fst = ⊕-⋆ _ _ _ _ ∙ (λ t → ·Lid 1r t ⊕ isInvM .snd .fst t) ∙ 1⊕𝟙
  isInv⊕ M isInvM .snd .snd = ⊕-⋆ _ _ _ _ ∙ (λ t → ·Rid 1r t ⊕ isInvM .snd .snd t) ∙ 1⊕𝟙

  ⊕SimRel : (a : R){M N : Mat m n} → (sim : SimRel M N) → SimRel (a ⊕ M) (a ⊕ N)
  ⊕SimRel _ sim .transMatL = 1r ⊕ sim .transMatL
  ⊕SimRel _ sim .transMatR = 1r ⊕ sim .transMatR
  ⊕SimRel a {M = M} sim .transEq =
    let P = sim .transMatL
        Q = sim .transMatR in
      (λ t → helper a t ⊕ sim .transEq t)
    ∙ sym (⊕-⋆ _ _ _ Q)
    ∙ (λ t → ⊕-⋆ 1r a P M (~ t) ⋆ (1r ⊕ Q))
    where helper : (a : R) → a ≡ (1r · a) · 1r
          helper = solve 𝓡
  ⊕SimRel _ sim .isInvTransL = isInv⊕ _ (sim .isInvTransL)
  ⊕SimRel _ sim .isInvTransR = isInv⊕ _ (sim .isInvTransR)

  ⊕Sim : (a : R){M : Mat m n} → (sim : Sim M) → Sim (a ⊕ M)
  ⊕Sim a sim .result = a ⊕ sim .result
  ⊕Sim _ sim .simrel = ⊕SimRel _ (sim .simrel)

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


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

module M-types.Coalg where
    open import M-types.Coalg.Core public
    open import M-types.Coalg.Bisim public
    open import M-types.Coalg.M public

max_stars_repo_name: DDOtten/M-types

max_issues_repo_name: DDOtten/M-types

max_forks_repo_name: DDOtten/M-types


text:
{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module PolynomialFunctors where

-- From: Ulf Norell. Dependently typed programming in Agda. In Koopman
-- et al., editors. Advanced Functional Programming (AFP 2008), volume
-- 5832 of LNCS. Springer-Verlag, 2009. pages 230–266.

infixr 50 _|+|_ _⊕_
infixr 60 _|x|_ _×_

record True : Set where

data _⊕_ (A B : Set) : Set where
  inl : A → A ⊕ B
  inr : B → A ⊕ B

data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B

data Functor : Set₁ where
  |Id|  : Functor
  |K|   : Set → Functor
  _|+|_ : Functor → Functor → Functor
  _|x|_ : Functor → Functor → Functor

[_] : Functor → Set → Set
[ |Id|    ] X = X
[ |K| A   ] X = A
[ F |+| G ] X = [ F ] X ⊕ [ G ] X
[ F |x| G ] X = [ F ] X × [ G ] X

data μ_ (F : Functor) : Set where
  <_> : [ F ] (μ F) → μ F

NatF : Functor
NatF = |K| True |+| |Id|

NAT : Set
NAT = μ NatF

Z : NAT
Z = < inl _ >

S : NAT → NAT
S n = < inr n >

_+_ : NAT → NAT → NAT
m + < inl _ > = m
m + < inr n > = S (m + n)

ListF : (A : Set) → Functor
ListF = λ A → |K| True |+| |K| A |x| |Id|

LIST : (A : Set) → Set
LIST = λ A → μ (ListF A)

nil : {A : Set} → LIST A
nil = < inl _ >

cons : {A : Set} → A → LIST A → LIST A
cons x xs = < inr (x , xs) >

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --safe --no-qualified-instances #-}
module JVM.Syntax.Instructions where

open import Level
open import Data.Unit
open import Data.Product hiding (swap)
open import Data.String using (String)
open import Data.List
open import Data.List.Membership.Propositional using () renaming (_∈_ to Reg)

open import JVM.Types
open import JVM.Syntax.Values
open import JVM.Model StackTy

open import Relation.Unary hiding (_∈_)
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Structures.Syntax
open import Relation.Ternary.Monad.Weakening

data NativeBinOp : Ty → Ty → Ty → Set where
  add sub mul div xor : NativeBinOp int int int

data Comparator : List Ty → Set where
  eq ne lt ge gt le : {{IsIntegral a}} → Comparator [ a ]
  icmpge icmpgt icmpeq icmpne icmplt icmple : Comparator (int ∷ [ int ])

{- Instructions -}
module _ (𝑭 : FrameTy) where

  open import Data.List.Membership.Propositional

  𝑹[_] : Ty → Set
  𝑹[ a ] = a ∈ 𝑭

  -- True to bytecode, the collection of registers is fixed.
  -- The stack typing varies.
  data ⟨_↝_⟩ : StackTy → StackTy → Pred Labels 0ℓ where

    noop : ε[ ⟨ ψ ↝ ψ ⟩ ]

    -- stack manipulation
    pop  :           ε[ ⟨ a ∷ ψ      ↝  ψ     ⟩ ]
    push : Const a → ε[ ⟨ ψ          ↝  a ∷ ψ ⟩ ]
    dup  : ε[ ⟨ a ∷ ψ      ↝  a ∷ a ∷ ψ ⟩ ]
    swap : ε[ ⟨ a ∷ b ∷ ψ  ↝  b ∷ a ∷ ψ ⟩ ]

    -- binary operations on primitive types
    bop   : NativeBinOp a b c → ε[ ⟨ b ∷ a ∷ ψ  ↝  c ∷ ψ ⟩ ]

    -- register manipulation
    load  : 𝑹[ a ] → ε[ ⟨ ψ ↝ a ∷ ψ ⟩ ]
    store : 𝑹[ a ] → ε[ ⟨ a ∷ ψ ↝ ψ ⟩ ]

    -- jumps
    goto  : ∀[ One ψ₁ ⇒ ⟨ ψ₁ ↝ ψ₂ ⟩ ]
    if    : ∀ {as} → Comparator as → ∀[ One ψ ⇒ ⟨ as ++ ψ ↝ ψ ⟩ ]

  ⟨_∣_↝_⟩ = ⟨_↝_⟩
  Instr = ⟨_↝_⟩

  open import JVM.Syntax.Bytecode StackTy ⟨_↝_⟩ as BC
  open BC using (Code) public

  ⟪_∣_↜_⟫   = ⟪_↜_⟫
  ⟪_∣_↝_⟫   = ⟪_↝_⟫
  ⟪_∣_↝_⟫+  = ⟪_↝_⟫+

module _ {𝑭} where
  open import JVM.Syntax.Bytecode StackTy ⟨ 𝑭 ∣_↝_⟩
    hiding (⟪_↜_⟫; ⟪_↝_⟫; ⟪_↝_⟫+; Code) public


text:
open import Nat
open import Prelude
open import dynamics-core
open import contexts
open import preservation

module complete-preservation where
  -- if you substitute a complete term into a complete term, the result is
  -- still complete.
  cp-subst : ∀ {x d1 d2} →
             d1 dcomplete →
             d2 dcomplete →
             ([ d2 / x ] d1) dcomplete
  cp-subst {x = y} (DCVar {x = x}) dc2 with natEQ x y
  cp-subst DCVar dc2 | Inl refl = dc2
  cp-subst DCVar dc2 | Inr x₂ = DCVar
  cp-subst DCNum dc2 = DCNum
  cp-subst (DCPlus dc1 dc2) dc3 = DCPlus (cp-subst dc1 dc3) (cp-subst dc2 dc3)
  cp-subst {x = x} (DCLam {x = y} dc1 x₂) dc2 with natEQ y x
  cp-subst (DCLam dc1 x₃) dc2 | Inl refl = DCLam dc1 x₃
  cp-subst (DCLam dc1 x₃) dc2 | Inr x₂ = DCLam (cp-subst dc1 dc2) x₃
  cp-subst (DCAp dc1 dc2) dc3 = DCAp (cp-subst dc1 dc3) (cp-subst dc2 dc3)
  cp-subst (DCCast dc1 x₁ x₂) dc2 = DCCast (cp-subst dc1 dc2) x₁ x₂
  cp-subst (DCInl x dc1) dc2 = DCInl x (cp-subst dc1 dc2)
  cp-subst (DCInr x dc1) dc2 = DCInr x (cp-subst dc1 dc2)
  cp-subst {x = x} (DCCase {x = y} {y = z} dc dc1 dc3) dc2
    with natEQ y x | natEQ z x
  ... | Inl refl | Inl refl = DCCase (cp-subst dc dc2) dc1 dc3
  ... | Inl refl | Inr z≠x  = DCCase (cp-subst dc dc2 ) dc1 (cp-subst dc3 dc2)
  ... | Inr y≠x  | Inl refl = DCCase (cp-subst dc dc2) (cp-subst dc1 dc2) dc3
  ... | Inr y≠x  | Inr z≠x  = DCCase (cp-subst dc dc2) (cp-subst dc1 dc2) (cp-subst dc3 dc2)
  cp-subst (DCPair dc1 dc3) dc2 = DCPair (cp-subst dc1 dc2) (cp-subst dc3 dc2)
  cp-subst (DCFst dc1) dc2 = DCFst (cp-subst dc1 dc2)
  cp-subst (DCSnd dc1) dc2 = DCSnd (cp-subst dc1 dc2)

  -- this just lets me pull the particular x out of a derivation; it's not
  -- bound in any of the constructors explicitly since it's only in the
  -- lambda case; so below i have no idea how else to get a name for it,
  -- instead of leaving it dotted in the context
  lem-proj : {x : Nat} {d : ihexp} { τ : htyp} →
             (·λ x ·[ τ ] d) dcomplete →
             Σ[ y ∈ Nat ] (y == x)
  lem-proj {x} (DCLam dc x₁) = x , refl

  -- a complete well typed term steps to a complete term.
  cp-rhs : ∀{d τ d' Δ} →
           d dcomplete →
           Δ , ∅ ⊢ d :: τ →
           d ↦ d' →
           d' dcomplete
  cp-rhs dc TANum (Step FHOuter () FHOuter)
  cp-rhs (DCPlus dc dc₁) (TAPlus wt wt₁) (Step FHOuter (ITPlus refl) FHOuter) = DCNum
  cp-rhs (DCPlus dc dc₁) (TAPlus wt wt₁) (Step (FHPlus1 x) x₁ (FHPlus1 x₂))
    with cp-rhs dc wt (Step x x₁ x₂)
  ... | q = DCPlus q dc₁
  cp-rhs (DCPlus dc dc₁) (TAPlus wt wt₁) (Step (FHPlus2 x) x₁ (FHPlus2 x₂))
    with cp-rhs dc₁ wt₁ (Step x x₁ x₂)
  ... | q = DCPlus dc q
  cp-rhs dc (TAVar x₁) stp = abort (somenotnone (! x₁))
  cp-rhs dc (TALam _ wt) (Step FHOuter () FHOuter)
  -- this case is a little more complicated than it feels like it ought to
  -- be, just from horsing around with agda implicit variables.
  cp-rhs (DCAp dc dc₁) (TAAp wt wt₁) (Step FHOuter ITLam FHOuter) with lem-proj dc
  cp-rhs (DCAp dc dc₁) (TAAp wt wt₁) (Step FHOuter ITLam FHOuter) | x , refl with cp-subst {x = x} dc dc₁
  ... | qq with natEQ x x
  cp-rhs (DCAp dc dc₁) (TAAp wt wt₁) (Step FHOuter ITLam FHOuter) | x , refl | DCLam qq x₁ | Inl refl = cp-subst qq dc₁
  cp-rhs (DCAp dc dc₁) (TAAp wt wt₁) (Step FHOuter ITLam FHOuter) | x , refl | qq | Inr x₁ = abort (x₁ refl)
  cp-rhs (DCAp (DCCast dc (TCArr x x₁) (TCArr x₂ x₃)) dc₁) (TAAp (TACast wt x₄) wt₁) (Step FHOuter ITApCast FHOuter) = DCCast (DCAp dc (DCCast dc₁ x₂ x)) x₁ x₃
  cp-rhs (DCAp dc dc₁) (TAAp wt wt₁) (Step (FHAp1 x) x₁ (FHAp1 x₂)) = DCAp (cp-rhs dc wt (Step x x₁ x₂)) dc₁
  cp-rhs (DCAp dc dc₁) (TAAp wt wt₁) (Step (FHAp2 x) x₁ (FHAp2 x₂)) = DCAp dc (cp-rhs dc₁ wt₁ (Step x x₁ x₂))
  cp-rhs () (TAEHole x x₁) stp
  cp-rhs () (TANEHole x wt x₁) stp
  cp-rhs (DCCast dc x x₁) (TACast wt x₂) (Step FHOuter ITCastID FHOuter) = dc
  cp-rhs (DCCast dc () x₁) (TACast wt x₂) (Step FHOuter (ITCastSucceed x₃) FHOuter)
  cp-rhs (DCCast dc () x₁) (TACast wt x₂) (Step FHOuter (ITCastFail x₃ x₄ x₅) FHOuter)
  cp-rhs (DCCast dc x ()) (TACast wt x₂) (Step FHOuter (ITGround x₃) FHOuter)
  cp-rhs (DCCast dc () x₁) (TACast wt x₂) (Step FHOuter (ITExpand x₃) FHOuter)
  cp-rhs (DCCast dc x x₁) (TACast wt x₂) (Step (FHCast x₃) x₄ (FHCast x₅)) = DCCast (cp-rhs dc wt (Step x₃ x₄ x₅)) x x₁
  cp-rhs () (TAFailedCast wt x x₁ x₂) stp
  cp-rhs (DCInl x dc) (TAInl wt) (Step (FHInl x₁) x₂ (FHInl x₃)) = DCInl x (cp-rhs dc wt (Step x₁ x₂ x₃))
  cp-rhs (DCInr x dc) (TAInr wt) (Step (FHInr x₁) x₂ (FHInr x₃)) = DCInr x (cp-rhs dc wt (Step x₁ x₂ x₃))
  cp-rhs (DCCase (DCInl x₂ dc) dc₁ dc₂) (TACase wt x wt₁ x₁ wt₂) (Step FHOuter ITCaseInl FHOuter) = cp-subst dc₁ dc
  cp-rhs (DCCase (DCInr x₂ dc) dc₁ dc₂) (TACase wt x wt₁ x₁ wt₂) (Step FHOuter ITCaseInr FHOuter) = cp-subst dc₂ dc
  cp-rhs (DCCase (DCCast dc (TCSum x₂ x₄) (TCSum x₃ x₅)) dc₁ dc₂) (TACase wt x wt₁ x₁ wt₂) (Step FHOuter ITCaseCast FHOuter) =  DCCase dc (cp-subst dc₁ (DCCast DCVar x₂ x₃)) (cp-subst dc₂ (DCCast DCVar x₄ x₅))
  cp-rhs (DCCase dc dc₁ dc₂) (TACase wt x wt₁ x₁ wt₂) (Step (FHCase x₂) x₃ (FHCase x₄)) = DCCase (cp-rhs dc wt (Step x₂ x₃ x₄)) dc₁ dc₂
  cp-rhs (DCInl x dc) (TAInl dc₁) (Step FHOuter () FHOuter)
  cp-rhs (DCInr x dc) (TAInr dc₁) (Step FHOuter () FHOuter)
  cp-rhs (DCPair dc dc₁) (TAPair dc₂ dc₃) (Step (FHPair1 x₁) x₂ (FHPair1 x₃)) = DCPair (cp-rhs dc dc₂ (Step x₁ x₂ x₃)) dc₁
  cp-rhs (DCPair dc dc₁) (TAPair dc₂ dc₃) (Step (FHPair2 x₁) x₂ (FHPair2 x₃)) = DCPair dc (cp-rhs dc₁ dc₃ (Step x₁ x₂ x₃))
  cp-rhs (DCFst (DCPair dc dc₃)) (TAFst dc₁) (Step FHOuter ITFstPair FHOuter) = dc
  cp-rhs (DCFst (DCCast dc (TCProd x x₁) (TCProd x₃ x₄))) (TAFst dc₁) (Step FHOuter ITFstCast FHOuter) = DCCast (DCFst dc) x x₃
  cp-rhs (DCFst dc) (TAFst dc₁) (Step (FHFst x₁) x₂ (FHFst x₃)) = DCFst (cp-rhs dc dc₁ (Step x₁ x₂ x₃))
  cp-rhs (DCSnd (DCPair dc dc₂)) (TASnd dc₁) (Step FHOuter ITSndPair FHOuter) = dc₂
  cp-rhs (DCSnd (DCCast dc (TCProd x x₁) (TCProd x₂ x₃))) (TASnd dc₁) (Step FHOuter ITSndCast FHOuter) = DCCast (DCSnd dc) x₁ x₃
  cp-rhs (DCSnd dc) (TASnd dc₁) (Step (FHSnd x₁) x₂ (FHSnd x₃)) = DCSnd (cp-rhs dc dc₁ (Step x₁ x₂ x₃))

  -- this is the main result of this file.
  complete-preservation : ∀{d τ d' Δ} →
                          binders-unique d →
                          d dcomplete →
                          Δ , ∅ ⊢ d :: τ →
                          d ↦ d' →
                          (Δ , ∅ ⊢ d' :: τ) × (d' dcomplete)
  complete-preservation bd dc wt stp = preservation bd wt stp , cp-rhs dc wt stp

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
module Logic.Congruence where

import Prelude
import Logic.Relations
import Logic.Equivalence

open Prelude
open Logic.Relations
open Logic.Equivalence using    (Equivalence)
                       renaming (module Equivalence to Proj)

data Congruence (A : Set) : Set1 where
  congruence :
    (Eq : Equivalence A) ->
    Congruent (Proj._==_ Eq) ->
    Congruence A

module Projections where

  eq : {A : Set} -> Congruence A -> Rel A
  eq (congruence Eq _) = Proj._==_ Eq

  refl : {A : Set}(Cong : Congruence A) -> Reflexive (eq Cong)
  refl (congruence Eq _) = Proj.refl Eq

  sym : {A : Set}(Cong : Congruence A) -> Symmetric (eq Cong)
  sym (congruence Eq _) = Proj.sym Eq

  trans : {A : Set}(Cong : Congruence A) -> Transitive (eq Cong)
  trans (congruence Eq _) = Proj.trans Eq

  cong : {A : Set}(Cong : Congruence A) -> Congruent (eq Cong)
  cong (congruence _ c) = c

module Congruence {A : Set}(Cong : Congruence A) where

  _==_  = Projections.eq    Cong
  refl  = Projections.refl  Cong
  sym   = Projections.sym   Cong
  trans = Projections.trans Cong
  cong  = Projections.cong  Cong

  cong2 : (f : A -> A -> A)(a b c d : A) -> a == c -> b == d -> f a b == f c d
  cong2 f a b c d ac bd = trans _ _ _ rem1 rem2
    where
      rem1 : f a b == f a d
      rem1 = cong (f a) _ _ bd

      rem2 : f a d == f c d
      rem2 = cong (flip f d) _ _ ac

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

syntax CommMonoid | CM

type
  * : 0-ary

term
  unit : * | ε
  add  : *  *  ->  * | _⊕_ l20

theory
  (εU⊕ᴸ) a |> add (unit, a) = a
  (εU⊕ᴿ) a |> add (a, unit) = a
  (⊕A) a b c |> add (add(a, b), c) = add (a, add(b, c))
  (⊕C) a b |> add(a, b) = add(b, a)
-}

module CommMonoid.Syntax where

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

open import SOAS.Metatheory.Syntax

open import CommMonoid.Signature

private
  variable
    Γ Δ Π : Ctx
    α : *T
    𝔛 : Familyₛ

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

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

    ε   : CM * Γ
    _⊕_ : CM * Γ → CM * Γ → CM * Γ

  infixl 20 _⊕_

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  CMᵃ : MetaAlg CM
  CMᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (unitₒ ⋮ _)     → ε
      (addₒ  ⋮ a , b) → _⊕_ a b
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module CMᵃ = MetaAlg CMᵃ

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

    open MetaAlg 𝒜ᵃ

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

    𝕤𝕖𝕞  ε        = 𝑎𝑙𝑔 (unitₒ ⋮ tt)
    𝕤𝕖𝕞 (_⊕_ a b) = 𝑎𝑙𝑔 (addₒ  ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)

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

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

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

      open MetaAlg⇒ gᵃ⇒

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

      𝕤𝕖𝕞! ε = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (_⊕_ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩

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

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

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

open import Algebra.Structures.Bundles.Field

module Algebra.Linear.Structures.FiniteDimensional
  {k ℓᵏ} (K : Field k ℓᵏ)
  where

open import Algebra.Linear.Core
open import Algebra.FunctionProperties
open import Relation.Binary using (Rel)

open import Algebra.Linear.Morphism.Bundles K

open import Algebra.Linear.Structures.VectorSpace K

open import Function.Equality

open import Level using (_⊔_; suc)
open import Data.Nat using (ℕ)
import Algebra.Linear.Construct.Vector K as Vec

private
  K' : Set k
  K' = Field.Carrier K

record IsFiniteDimensional
       {v ℓ} {V : Set v}
       (_≈_ : Rel V ℓ)
       (_+_ : Op₂ V) (_∙_ : K' → V → V) (-_ : Op₁ V) (0# : V)
       (n : ℕ) : Set (suc (v ⊔ k ⊔ ℓ ⊔ ℓᵏ))
    where
  field
    isVectorSpace : IsVectorSpace _≈_ _+_ _∙_ -_ 0#
    embed         : LinearIsomorphism (record { isVectorSpace = isVectorSpace })
                                      (record { isVectorSpace = Vec.isVectorSpace {n} })

  open IsVectorSpace isVectorSpace public

module Vector {n} where
  open Vec

  isFiniteDimensional : IsFiniteDimensional (Vec._≈_) (Vec._+_) (Vec._∙_) (Vec.-_) (Vec.0#) n
  isFiniteDimensional = record
    { isVectorSpace = Vec.isVectorSpace
    ; embed         = Vec.embed
    }

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
{-# OPTIONS --without-K #-}
infixr 1 _‘→’_

data Type : Set where
  _‘→’_ : Type → Type → Type
  ‘□’ : Type → Type

data □ : Type → Set where
  Lӧb : ∀ {X} → □ (‘□’ X ‘→’ X) → □ X

⌞_⌟ : Type → Set
⌞ A ‘→’ B ⌟ = ⌞ A ⌟ → ⌞ B ⌟
⌞ ‘□’ T ⌟   = □ T

⌞_⌟t : ∀ {T : Type} → □ T → ⌞ T ⌟
⌞ (Lӧb □‘X’→X) ⌟t = ⌞ □‘X’→X ⌟t (Lӧb □‘X’→X)

lӧb : ∀ {‘X’} → □ (‘□’ ‘X’ ‘→’ ‘X’) → ⌞ ‘X’ ⌟
lӧb f = ⌞ Lӧb f ⌟t

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob


text:
------------------------------------------------------------------------
-- Queue instances for the queues in Queue.Simple
------------------------------------------------------------------------

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

open import Equality

module Queue.Simple.Instances
  {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺)
  where

open Derived-definitions-and-properties eq

open import Prelude

open import Queue eq
open import Queue.Simple eq as Q using (Queue)

private
  variable
    ℓ ℓ₁ ℓ₂ : Level

instance

  -- Instances.

  Queue-is-queue : Is-queue (λ A → Queue A) (λ _ → ↑ _ ⊤) ℓ
  Queue-is-queue .Is-queue.to-List                   = λ _ → Q.to-List
  Queue-is-queue .Is-queue.from-List                 = Q.from-List
  Queue-is-queue .Is-queue.to-List-from-List         = Q.to-List-from-List
  Queue-is-queue .Is-queue.enqueue                   = Q.enqueue
  Queue-is-queue .Is-queue.to-List-enqueue {q = q}   = Q.to-List-enqueue q
  Queue-is-queue .Is-queue.dequeue                   = λ _ → Q.dequeue
  Queue-is-queue .Is-queue.to-List-dequeue {q = q}   = Q.to-List-dequeue q
  Queue-is-queue .Is-queue.dequeue⁻¹                 = Q.dequeue⁻¹
  Queue-is-queue .Is-queue.to-List-dequeue⁻¹ {x = x} = Q.to-List-dequeue⁻¹ x

  Queue-is-queue-with-map : Is-queue-with-map (λ A → Queue A) ℓ₁ ℓ₂
  Queue-is-queue-with-map .Is-queue-with-map.map                 = Q.map
  Queue-is-queue-with-map .Is-queue-with-map.to-List-map {q = q} =
    Q.to-List-map q

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- Andreas, 2015-11-28
-- Aliases in parentheses should also parse.

-- Parenthesized aliases are accepted in lets.

-- With type annotation, parenthesized aliases are accepted in wheres.

id0 : {A : Set} → A → A
id0 {A} x = let z = y in z
  where
    y : A
    y = x

id1 : {A : Set} → A → A
id1 {A} x = let (z) = y in z
  where
    y : A
    (y) = x

id2 : {A : Set} → A → A
id2 {A} x = let ((z)) = y in z
  where
    y : A
    ((y)) = x

works0 : {A : Set} → A → A
works0 x = let z = y in z
  where
    y = x

-- Without type annotation, parenthesized aliases should also be accepted in wheres.

-- Should work:
test1 : {A : Set} → A → A
test1 x = let (z) = y in z
  where
    (y) = x

-- Should work:
test2 : {A : Set} → A → A
test2 x = let ((z)) = y in z
  where
    ((y)) = x

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Structure.Operator.Vector.LinearMap where

open import Functional
open import Logic
open import Logic.Predicate
open import Logic.Propositional
import      Lvl
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Function.Multi
open import Structure.Operator
open import Structure.Operator.Field.VectorSpace
open import Structure.Operator.Properties using (Distributivityₗ ; Distributivityᵣ)
open import Structure.Operator.Vector
open import Structure.Setoid
open import Type
open import Syntax.Function
open import Syntax.Transitivity

private variable ℓ ℓᵥ ℓᵥₗ ℓᵥᵣ ℓₛ ℓᵥₑ ℓᵥₑₗ ℓᵥₑᵣ ℓᵥₑ₁ ℓᵥₑ₂ ℓᵥₑ₃ ℓₛₑ : Lvl.Level
private variable V Vₗ Vᵣ V₁ V₂ V₃ S : Type{ℓ}
private variable _+ᵥ_ _+ᵥₗ_ _+ᵥᵣ_ _+ᵥ₁_ _+ᵥ₂_ _+ᵥ₃_ : V → V → V
private variable _⋅ₛᵥ_ _⋅ₛᵥₗ_ _⋅ₛᵥᵣ_ _⋅ₛᵥ₁_ _⋅ₛᵥ₂_ _⋅ₛᵥ₃_ : S → V → V
private variable _+ₛ_ _⋅ₛ_ : S → S → S

module _
  ⦃ equiv-Vₗ : Equiv{ℓᵥₑₗ}(Vₗ) ⦄
  ⦃ equiv-Vᵣ : Equiv{ℓᵥₑᵣ}(Vᵣ) ⦄
  ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  (vectorSpaceₗ : VectorSpace{V = Vₗ}{S = S}(_+ᵥₗ_)(_⋅ₛᵥₗ_)(_+ₛ_)(_⋅ₛ_))
  (vectorSpaceᵣ : VectorSpace{V = Vᵣ}{S = S}(_+ᵥᵣ_)(_⋅ₛᵥᵣ_)(_+ₛ_)(_⋅ₛ_))
  (f : Vₗ → Vᵣ)
  where

  record LinearMap : Type{Lvl.of(Vₗ) Lvl.⊔ ℓᵥₑₗ Lvl.⊔ ℓᵥₑᵣ Lvl.⊔ Lvl.of(S)} where
    constructor intro
    field
      ⦃ function ⦄ : Function(f)
      ⦃ preserves-[+ᵥ]  ⦄ : Preserving₂(f)(_+ᵥₗ_)(_+ᵥᵣ_)
      ⦃ preserves-[⋅ₛᵥ] ⦄ : ∀{s} → Preserving₁(f)(s ⋅ₛᵥₗ_)(s ⋅ₛᵥᵣ_)

_→ˡⁱⁿᵉᵃʳᵐᵃᵖ_ : ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄ → VectorSpaceVObject{ℓᵥ = ℓᵥₗ}{ℓᵥₑ = ℓᵥₑₗ}{S = S}(_+ₛ_)(_⋅ₛ_) → VectorSpaceVObject{ℓᵥ = ℓᵥᵣ}{ℓᵥₑ = ℓᵥₑᵣ}{S = S}(_+ₛ_)(_⋅ₛ_) → Stmt
V₁ →ˡⁱⁿᵉᵃʳᵐᵃᵖ V₂ = ∃(LinearMap(VectorSpaceVObject.vectorSpace(V₁)) (VectorSpaceVObject.vectorSpace(V₂)))

_↔ˡⁱⁿᵉᵃʳᵐᵃᵖ_ : ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄ → VectorSpaceVObject{ℓᵥ = ℓᵥₗ}{ℓᵥₑ = ℓᵥₑₗ}{S = S}(_+ₛ_)(_⋅ₛ_) → VectorSpaceVObject{ℓᵥ = ℓᵥᵣ}{ℓᵥₑ = ℓᵥₑᵣ}{S = S}(_+ₛ_)(_⋅ₛ_) → Stmt
V₁ ↔ˡⁱⁿᵉᵃʳᵐᵃᵖ V₂ = ∃(f ↦ Invertible(f) ∧ LinearMap(VectorSpaceVObject.vectorSpace(V₁)) (VectorSpaceVObject.vectorSpace(V₂))(f))

module _
  ⦃ equiv-V : Equiv{ℓᵥₑ}(V) ⦄
  ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  (vectorSpace : VectorSpace{V = V}{S = S}(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_))
  (f : V → V)
  where

  LinearOperator = LinearMap(vectorSpace)(vectorSpace) (f)

module _
  ⦃ equiv-V : Equiv{ℓᵥₑ}(V) ⦄
  ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  (vectorSpace : VectorSpace{V = V}{S = S}(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_))
  (f : V → S)
  where

  LinearFunctional = LinearMap(vectorSpace)(fieldVectorSpace(VectorSpace.scalarField(vectorSpace))) (f)

module _
  ⦃ equiv-V₁ : Equiv{ℓᵥₑ₁}(V₁) ⦄
  ⦃ equiv-V₂ : Equiv{ℓᵥₑ₂}(V₂) ⦄
  ⦃ equiv-V₃ : Equiv{ℓᵥₑ₃}(V₃) ⦄
  ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  (vectorSpace₁ : VectorSpace{V = V₁}{S = S}(_+ᵥ₁_)(_⋅ₛᵥ₁_)(_+ₛ_)(_⋅ₛ_))
  (vectorSpace₂ : VectorSpace{V = V₂}{S = S}(_+ᵥ₂_)(_⋅ₛᵥ₂_)(_+ₛ_)(_⋅ₛ_))
  (vectorSpace₃ : VectorSpace{V = V₃}{S = S}(_+ᵥ₃_)(_⋅ₛᵥ₃_)(_+ₛ_)(_⋅ₛ_))
  (f : V₁ → V₂ → V₃)
  where

  record BilinearMap : Type{Lvl.of(V₁) Lvl.⊔ Lvl.of(V₂) Lvl.⊔ ℓᵥₑ₁ Lvl.⊔ ℓᵥₑ₂ Lvl.⊔ ℓᵥₑ₃ Lvl.⊔ Lvl.of(S)} where
    constructor intro
    field
      ⦃ linearMap₁ ⦄ : ∀{y} → LinearMap vectorSpace₁ vectorSpace₃ (x ↦ f(x)(y))
      ⦃ linearMap₂ ⦄ : ∀{x} → LinearMap vectorSpace₂ vectorSpace₃ (y ↦ f(x)(y))

    open module LinearMapₗ{y} = LinearMap(linearMap₁{y}) renaming (function to functionₗ ; preserves-[+ᵥ] to preserves-[+ᵥ]ₗ ; preserves-[⋅ₛᵥ] to preserves-[⋅ₛᵥ]ₗ) public
    open module LinearMapᵣ{x} = LinearMap(linearMap₂{x}) renaming (function to functionᵣ ; preserves-[+ᵥ] to preserves-[+ᵥ]ᵣ ; preserves-[⋅ₛᵥ] to preserves-[⋅ₛᵥ]ᵣ) public

    binaryOperator : BinaryOperator(f)
    binaryOperator = functions-to-binaryOperator(f) ⦃ functionₗ ⦄ ⦃ functionᵣ ⦄

module _
  ⦃ equiv-V : Equiv{ℓᵥₑ}(V) ⦄
  ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  (vectorSpace : VectorSpace{V = V}{S = S}(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_))
  (_▫_ : V → V → V)
  where

  BilinearOperator = BilinearMap(vectorSpace)(vectorSpace)(vectorSpace) (_▫_)
  module BilinearOperator(bilinearOper : BilinearOperator) where
    -- TODO: Move the proof for distributivity from preserving
    [+ᵥ]-distributivityₗ : Distributivityₗ(_▫_)(_+ᵥ_)
    Distributivityₗ.proof [+ᵥ]-distributivityₗ {x}{y}{z} =
      x ▫ (y +ᵥ z)       🝖[ _≡_ ]-[ preserving₂(x ▫_)(_+ᵥ_)(_+ᵥ_) ⦃ LinearMap.preserves-[+ᵥ] (BilinearMap.linearMap₂ bilinearOper) ⦄ ]
      (x ▫ y) +ᵥ (x ▫ z) 🝖-end

    [+ᵥ]-distributivityᵣ : Distributivityᵣ(_▫_)(_+ᵥ_)
    Distributivityᵣ.proof [+ᵥ]-distributivityᵣ {x}{y}{z} =
      (x +ᵥ y) ▫ z       🝖[ _≡_ ]-[ preserving₂(_▫ z)(_+ᵥ_)(_+ᵥ_) ⦃ LinearMap.preserves-[+ᵥ] (BilinearMap.linearMap₁ bilinearOper) ⦄ ]
      (x ▫ z) +ᵥ (y ▫ z) 🝖-end

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda