text:
open import Agda.Primitive using (lzero; lsuc; _⊔_ ;Level)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; setoid; cong; trans)
import Function.Equality
open import Relation.Binary using (Setoid)

import Categories.Category
import Categories.Functor
import Categories.Category.Instance.Setoids
import Categories.Monad.Relative
import Categories.Category.Equivalence
import Categories.Category.Cocartesian
import Categories.Category.Construction.Functors
import Categories.NaturalTransformation.Equivalence
import Relation.Binary.Core

import SecondOrder.Arity
import SecondOrder.Signature
import SecondOrder.Metavariable
import SecondOrder.VRenaming
import SecondOrder.MRenaming
import SecondOrder.Term
import SecondOrder.IndexedCategory
import SecondOrder.RelativeKleisli
import SecondOrder.Substitution

module SecondOrder.VRelativeMonad
  {ℓ}
  {𝔸 : SecondOrder.Arity.Arity}
  (Σ : SecondOrder.Signature.Signature ℓ 𝔸)
  where

  open SecondOrder.Signature.Signature Σ
  open SecondOrder.Metavariable Σ
  open SecondOrder.Term Σ
  open SecondOrder.VRenaming Σ
  open SecondOrder.MRenaming Σ
  open SecondOrder.Substitution Σ

  -- TERMS FORM A RELATIVE MONAD
  -- (FOR A FUNCTOR WHOSE DOMAIN IS THE
  -- CATEGORY OF VARIABLE CONTEXTS AND RENAMINGS)

  module _ where
    open Categories.Category
    open Categories.Functor using (Functor)
    open Categories.Category.Instance.Setoids
    open Categories.Monad.Relative
    open Function.Equality using () renaming (setoid to Π-setoid)
    open Categories.Category.Equivalence using (StrongEquivalence)
    open import SecondOrder.IndexedCategory
    open import SecondOrder.RelativeKleisli
    open Categories.Category.Construction.Functors
    open Categories.NaturalTransformation.Equivalence
    open Relation.Binary.Core hiding (_⇒_)

    -- The carrier of the codomain of Jⱽ (morally ∀ Γ → A ∈ Δ ,, Γ)

    record Codomain-Jⱽ-Elt : Set ((lsuc ℓ)) where
      open Category (Setoids ℓ ℓ)
      open Setoid
      field
        F₀ :  VContext → MContext → Obj
        F₁ : ∀ {Θ ψ Δ Ξ} (ρ : Δ ⇒ᵛ Ξ) (ι : Θ ⇒ᵐ ψ)
             → (F₀ Δ Θ) ⇒ (F₀ Ξ ψ)
        identity : ∀ {Θ Δ}
                   → Category._≈_ (Setoids ℓ ℓ) (F₁ (idᵛ {Δ}) (idᵐ {Θ})) (id {F₀ Δ Θ})
        homomorphism : ∀ {Θ ψ Ω Γ Δ Ξ} {ρ : Γ ⇒ᵛ Δ} {ι : Θ ⇒ᵐ ψ} {τ : Δ ⇒ᵛ Ξ} {μ : ψ ⇒ᵐ Ω}
                       → Category._≈_ (Setoids ℓ ℓ) (F₁ (τ ∘ᵛ ρ) (μ ∘ᵐ ι)) ((F₁ τ μ) ∘ (F₁ ρ ι))
        F-resp-≈ : ∀ {Θ ψ Γ Δ} {ρ τ : Γ ⇒ᵛ Δ} {ι μ : Θ ⇒ᵐ ψ}
                   → (ρ ≡ᵛ τ) → (ι ≡ᵐ μ) → (Category._≈_ (Setoids ℓ ℓ) (F₁ ρ ι) (F₁ τ μ))

    -- Transformation for Codomain-Jⱽ (analogue to natural transformations)

    record NaturalTransformation-Jⱽ (Fⱽ Gⱽ : Codomain-Jⱽ-Elt) : Set (lsuc ℓ)
      where
        private
          module Fⱽ = Codomain-Jⱽ-Elt Fⱽ
          module Gⱽ = Codomain-Jⱽ-Elt Gⱽ
        open Fⱽ using (F₀; F₁)
        open Category (Setoids ℓ ℓ)
        field
          η : ∀ Θ Γ → (F₀ Γ Θ) ⇒ (Gⱽ.F₀ Γ Θ)
          commute : ∀ {Θ ψ Γ Δ} (ρ : Γ ⇒ᵛ Δ) (ι : Θ ⇒ᵐ ψ)
                    → Category._≈_ (Setoids ℓ ℓ) ((η ψ Δ) ∘ (F₁ ρ ι)) ((Gⱽ.F₁ ρ ι) ∘ (η Θ Γ))
          -- ignore-MCtx : ∀ Θ Ω Γ → (∀ (x : F₀ Γ Θ))

    open NaturalTransformation-Jⱽ

    -- Equivalence of NaturalTransformation-Jⱽ (analogue to the one
    -- of the natural transformations)

    infix 4 _≃Jⱽ_

    _≃Jⱽ_ : ∀ {Fⱽ Gⱽ : Codomain-Jⱽ-Elt} → Rel (NaturalTransformation-Jⱽ Fⱽ Gⱽ) ℓ
    𝒩 ≃Jⱽ ℳ  = ∀ {Θ Γ} → Category._≈_ (Setoids ℓ ℓ)
                            (η 𝒩 Θ Γ)
                            (η ℳ Θ Γ)

    -- Identity transformation analogue to the one
    -- of the natural transformations, for NaturalTransformation-Jⱽ

    idN-Jⱽ : ∀ {Fⱽ : Codomain-Jⱽ-Elt} → NaturalTransformation-Jⱽ Fⱽ Fⱽ
    idN-Jⱽ {Fⱽ} =
           record
             { η = λ Θ Γ →
               record
                 { _⟨$⟩_ = λ x → x
                 ; cong = λ x → x }
             ; commute = λ {Θ} {ψ} {Γ} {Δ} ρ ι ξ
                         → Codomain-Jⱽ-Elt.F-resp-≈  Fⱽ {Θ} {ψ} {Γ} {Δ} {ρ} {ρ} {ι} {ι}
                                                (λ x₁ → refl) (λ M → refl) ξ }

    -- Composition of NaturalTransformation-Jⱽ (analogue to the one
    -- of the natural transformations)

    _∘-Jⱽ_ : ∀ {Fⱽ Gⱽ Hⱽ : Codomain-Jⱽ-Elt} (𝒩 : NaturalTransformation-Jⱽ Gⱽ Hⱽ) (ℳ : NaturalTransformation-Jⱽ Fⱽ Gⱽ) → NaturalTransformation-Jⱽ Fⱽ Hⱽ
    _∘-Jⱽ_ {Fⱽ} {Gⱽ} {Hⱽ} 𝒩 ℳ =
             let open Category (Setoids ℓ ℓ) in
             let open NaturalTransformation-Jⱽ in
             let open Codomain-Jⱽ-Elt in
             record
                 { η = λ Θ Γ → η 𝒩 Θ Γ ∘ η ℳ Θ Γ
                 ; commute = λ {Θ} {ψ} {Γ} {Δ} ρ ι →
                             let open HomReasoning {F₀ Fⱽ Γ Θ} {F₀ Hⱽ Δ ψ} in
                             begin
                             (Category._∘_ (Setoids ℓ ℓ) (η {Gⱽ} {Hⱽ} 𝒩 ψ Δ) ((η {Fⱽ} {Gⱽ} ℳ ψ Δ) ∘ (F₁ Fⱽ ρ ι))) ≈⟨ assoc {f = F₁ Fⱽ ρ ι} {g = η ℳ ψ Δ} {h = η 𝒩 ψ Δ} ⟩
                             (η 𝒩 ψ Δ ∘ (η ℳ ψ Δ) ∘ (F₁ Fⱽ ρ ι)) ≈⟨ refl⟩∘⟨_
                                                                      {f = η 𝒩 ψ Δ} {g = (η ℳ ψ Δ) ∘ (F₁ Fⱽ ρ ι)}
                                                                      {i = (F₁ Gⱽ ρ ι) ∘ (η ℳ Θ Γ)}
                                                                      (commute ℳ ρ ι) ⟩
                             (η 𝒩 ψ Δ ∘ ((F₁ Gⱽ ρ ι) ∘ (η ℳ Θ Γ))) ≈⟨ sym-assoc {f = η ℳ Θ Γ} {g = F₁ Gⱽ ρ ι} {h = η 𝒩 ψ Δ}⟩
                             ((η 𝒩 ψ Δ) ∘ (F₁ Gⱽ ρ ι)) ∘ (η ℳ Θ Γ) ≈⟨ _⟩∘⟨refl
                                                                      {f = (η 𝒩 ψ Δ) ∘ (F₁ Gⱽ ρ ι)} {h = (F₁ Hⱽ ρ ι) ∘ (η 𝒩 Θ Γ)}
                                                                      {g = η ℳ Θ Γ}
                                                                      (commute 𝒩 ρ ι) ⟩
                             (((F₁ Hⱽ ρ ι) ∘ (η 𝒩 Θ Γ)) ∘ (η ℳ Θ Γ)) ≈⟨ assoc {f = η ℳ Θ Γ} {g = η 𝒩 Θ Γ} {h = F₁ Hⱽ ρ ι} ⟩
                             (((F₁ Hⱽ ρ ι) ∘ (η 𝒩 Θ Γ)) ∘ (η ℳ Θ Γ)) ∎}

    -- Proof that the category of Codomain-Jⱽ and NaturalTransformation-Jⱽ is indeed a category

    -- associativity of composition
    -- (surprisingly enough, the proof of "sym-assoc-Jⱽ" is exactly the same :
    -- Is there a problem in the definitions ?)
    assoc-Jⱽ : {A B C D : Codomain-Jⱽ-Elt}
               {ℒ : NaturalTransformation-Jⱽ A B}
               {ℳ : NaturalTransformation-Jⱽ B C}
               {𝒩 : NaturalTransformation-Jⱽ C D}
               → ((𝒩 ∘-Jⱽ ℳ) ∘-Jⱽ ℒ) ≃Jⱽ (𝒩 ∘-Jⱽ (ℳ ∘-Jⱽ ℒ))
    assoc-Jⱽ  {A} {B} {C} {D} {ℒ} {ℳ} {𝒩} {Θ} {Γ} ξ = Function.Equality.Π.cong (η 𝒩 Θ Γ)
                                                          (Function.Equality.Π.cong (η ℳ Θ Γ)
                                                            (Function.Equality.cong (η ℒ Θ Γ) ξ))

    -- identity is identity
    identityˡ-Jⱽ : {A B : Codomain-Jⱽ-Elt}
                  {𝒩 : NaturalTransformation-Jⱽ A B}
                  → (idN-Jⱽ ∘-Jⱽ 𝒩) ≃Jⱽ 𝒩
    identityˡ-Jⱽ  {𝒩 = 𝒩} {Θ = Θ} {Γ = Γ} ξ = Function.Equality.cong (η 𝒩 Θ Γ) ξ

    -- Codomain of Jⱽ (the category with Codomain-Jⱽ-Elt as objects and NaturalTransformation-Jⱽ as maps)
    Codomain-Jⱽ : Category (lsuc ℓ) (lsuc ℓ)  ℓ
    Codomain-Jⱽ = record
                    { Obj = Codomain-Jⱽ-Elt
                    ; _⇒_ = NaturalTransformation-Jⱽ
                    ; _≈_ = _≃Jⱽ_
                    ; id = idN-Jⱽ
                    ; _∘_ = _∘-Jⱽ_
                    ; assoc = λ {Fⱽ} {Gⱽ} {Hⱽ} {Kⱽ} {𝒩} {ℳ} {ℒ} → assoc-Jⱽ  {ℒ = 𝒩} {ℳ = ℳ} {𝒩 = ℒ}
                    ; sym-assoc = λ {Fⱽ} {Gⱽ} {Hⱽ} {Kⱽ} {𝒩} {ℳ} {ℒ} → assoc-Jⱽ  {ℒ = 𝒩} {ℳ = ℳ} {𝒩 = ℒ}
                    ; identityˡ = λ {Fⱽ} {Gⱽ} {𝒩} → identityˡ-Jⱽ {𝒩 = 𝒩}
                    ; identityʳ = λ {Fⱽ} {Gⱽ} {𝒩} → identityˡ-Jⱽ {𝒩 = 𝒩}
                    ; identity² = λ {Fⱽ} ξ → ξ
                    ; equiv = λ {Fⱽ} {Gⱽ}
                              → record
                                  { refl = λ {𝒩 = 𝒩} {Θ = Θ} {Γ = Γ} {x} {y} ξ
                                           → Function.Equality.cong (η 𝒩 Θ Γ) ξ
                                  ; sym = λ {𝒩} {ℳ} ξᴺ {Θ} {Γ} ξ
                                          → Category.Equiv.sym (Setoids ℓ ℓ)
                                          {_} {_} {η 𝒩 Θ Γ} {η ℳ Θ Γ} ξᴺ ξ
                                  ; trans =  λ {𝒩} {ℳ} {ℒ} ξᴺ₂ ξᴺ₁ {Θ} {Γ} ξ
                                             → Category.Equiv.trans (Setoids ℓ ℓ)
                                             {_} {_} {η 𝒩 Θ Γ} {η ℳ Θ Γ} {η ℒ Θ Γ} ξᴺ₂ ξᴺ₁ ξ}
                    ; ∘-resp-≈ = λ {Fⱽ} {Gⱽ} {Hⱽ} {𝒩} {ℳ} {ℒ} {𝒦} ξᴺ₁ ξᴺ₂ {Θ} {Γ} ξ
                                 → Category.∘-resp-≈ (Setoids ℓ ℓ)
                                   {_} {_}  {_}
                                   {η 𝒩 Θ Γ} {η ℳ Θ Γ} {η ℒ Θ Γ} {η 𝒦 Θ Γ}
                                   ξᴺ₁ ξᴺ₂ ξ
                    }

    -- The embedding of contexts into setoids indexed by sorts, metavariable telescope and variable telescope

    Jⱽ : Functor VContexts (IndexedCategory sort Codomain-Jⱽ)
    Jⱽ = record
              { F₀ = λ Γ A →
                       record
                         { F₀ = λ Δ Θ → setoid (A ∈ (Γ ,, Δ))
                         ; F₁ = λ ρ ι → record
                                            { _⟨$⟩_ = [ inlᵛ , inrᵛ ∘ᵛ ρ ]ᵛ
                                            ; cong = λ {x} {y} ξ →  ρ-resp-≡ {ρ = [ var-inl , var-inr ∘ᵛ ρ ]ᵛ} ξ}
                         ; identity = λ {Θ} {Δ} {x} ξ → trans (idᵛ+idᵛ x) ξ
                         ; homomorphism = λ {Θ} {ψ} {Ω} {Δ} {Ξ} {Λ} {ρ} {ι} {τ} {μ} {x} {y} ξ
                                          → trans
                                            (ʳ⇑ᵛ-resp-∘ᵛ x)
                                            (ρ-resp-≡ {ρ = [ var-inl , (λ x₁ → var-inr (τ x₁)) ]ᵛ}
                                              (ρ-resp-≡ {ρ = [ var-inl , (λ x₁ → var-inr (ρ x₁)) ]ᵛ} ξ))
                         ; F-resp-≈ = λ {Θ} {ψ} {Δ} {Ξ} {ρ} {τ} {ι} {μ} ξᵛ ξᵐ {x} {y} ξ
                                      → trans
                                        ([,]ᵛ-resp-≡ᵛ (λ x₁ → refl) (∘ᵛ-resp-≡ᵛ {τ₁ = λ x₁ → var-inr x₁} (λ x₁ → refl) λ x₁ → ξᵛ x₁) x)
                                        (ρ-resp-≡ {ρ = [ var-inl , (λ x₁ → var-inr (τ x₁)) ]ᵛ} ξ)
                         }

              ; F₁ = λ ρ A → record
                               { η = λ Θ Γ → record { _⟨$⟩_ = ⇑ᵛ ρ ; cong = cong (⇑ᵛ ρ) }
                               ; commute = λ τ ι {x} ξ
                                           → trans
                                             (uniqueᵛ²
                                               {τ = [ (λ x₁ → var-inl (ρ x₁)) , (λ x₁ → var-inr x₁) ]ᵛ ∘ᵛ [ var-inl , (λ x₁ → var-inr (τ x₁)) ]ᵛ}
                                               {σ = [ var-inl , (λ x₁ → var-inr (τ x₁)) ]ᵛ ∘ᵛ [ (λ x₁ → var-inl (ρ x₁)) , (λ x₁ → var-inr x₁) ]ᵛ} (λ x₁ → refl) (λ x₁ → refl) x)
                                               (ρ-resp-≡
                                                 {ρ = [ var-inl , (λ x₁ → var-inr (τ x₁)) ]ᵛ ∘ᵛ [ (λ x₁ → var-inl (ρ x₁)) , (λ x₁ → var-inr x₁) ]ᵛ} ξ)}

              ; identity =  λ A {Θ} {Γ} {x} ξ → trans (idᵛ+idᵛ x) ξ
              ; homomorphism = λ {Δ} {Ξ} {Λ} {ρ} {τ} A {_} {_} {x} ξ
                               → trans
                                 (uniqueᵛ²
                                   {τ = [ (λ x₁ → var-inl (τ (ρ x₁))) , (λ x₁ → var-inr x₁) ]ᵛ}
                                   {σ = [ (λ x₁ → var-inl (τ x₁)) , (λ x₁ → var-inr x₁) ]ᵛ ∘ᵛ [ (λ x₁ → var-inl (ρ x₁)) , (λ x₁ → var-inr x₁) ]ᵛ}
                                   (λ x₁ → refl) (λ x₁ → refl) x)
                                 (ρ-resp-≡
                                   {ρ = [ (λ x₁ → var-inl (τ x₁)) , (λ x₁ → var-inr x₁) ]ᵛ ∘ᵛ [ (λ x₁ → var-inl (ρ x₁)) , (λ x₁ → var-inr x₁) ]ᵛ } ξ)
              ; F-resp-≈ = λ {_} {_} {ρ} {τ} ξρ A {_} {_} {x} {y} ξ
                           → trans
                             (([,]ᵛ-resp-≡ᵛ {ρ₁ = λ x₁ → var-inl (ρ x₁)} {τ₁ = var-inr} (λ x₁ → ∘ᵛ-resp-≡ᵛ {τ₁ = var-inl} (λ x₃ → refl) ξρ x₁) (λ x₁ → refl) x))
                             (ρ-resp-≡ {ρ = ⇑ᵛ τ} ξ)
              }

  factor-empty-ctx : ∀ {Θ Ω Γ Δ A} (x : Setoid.Carrier ((Codomain-Jⱽ-Elt.F₀((Categories.Functor.Functor.F₀ Jⱽ) Γ A)) Δ Θ)) → x ≡ ( Function.Equality._⟨$⟩_ ((NaturalTransformation-Jⱽ.η ((Categories.Functor.Functor.F₁ Jⱽ) idᵛ A)) Ω Δ) x)
  factor-empty-ctx (var-inl x) = refl
  factor-empty-ctx (var-inr x) = refl

  -- The relative monad over Jⱽ

  module _ {Θ : MContext} where
    open Categories.Category
    open Categories.Functor using (Functor)
    open Categories.Category.Instance.Setoids
    open Categories.Category.Category (Setoids ℓ ℓ)
    open Categories.Monad.Relative
    open Function.Equality using () renaming (setoid to Π-setoid)
    open Categories.Category.Equivalence using (StrongEquivalence)
    open import SecondOrder.IndexedCategory
    open import SecondOrder.RelativeKleisli
    open NaturalTransformation-Jⱽ
    open Function.Equality using (_⟨$⟩_) renaming (cong to func-cong)
    open import Relation.Binary.Reasoning.MultiSetoid

    -- Setoids≈-⟨$⟩ : ∀ {From To} (f g : From Function.Equality.⟶ To) → (Category._≈_ (Setoids ℓ ℓ) f g) → (∀ (x : Setoid.Carrier From) → Setoid._≈_ To (f ⟨$⟩ x) (g ⟨$⟩ x))
    -- Setoids≈-⟨$⟩ = {!!}

    VMonad : Monad Jⱽ
    Codomain-Jⱽ-Elt.F₀ (Monad.F₀ VMonad Γ A) Δ ψ = Term-setoid Θ (Γ ,, Δ) A
    _⟨$⟩_      (Codomain-Jⱽ-Elt.F₁ (Monad.F₀ VMonad Γ A) ρ ι) = [ ʳ⇑ᵛ ρ ]ᵛ_
    func-cong (Codomain-Jⱽ-Elt.F₁ (Monad.F₀ VMonad Γ A) ρ ι) ξ = []ᵛ-resp-≈ ξ
    Codomain-Jⱽ-Elt.identity     (Monad.F₀ VMonad Γ A) ξ = ≈-trans ([]ᵛ-resp-≡ᵛ idᵛ+idᵛ) (≈-trans [idᵛ] ξ)
    Codomain-Jⱽ-Elt.homomorphism (Monad.F₀ VMonad Γ A) {ρ = ρ} {ι = ι} {τ = τ} {μ = μ} {x = x} {y = y} ξ
      = begin⟨ Term-setoid Θ _ _ ⟩
          [ ʳ⇑ᵛ (τ ∘ᵛ ρ) ]ᵛ x ≈⟨ []ᵛ-resp-≈ ξ ⟩
          [ ʳ⇑ᵛ (τ ∘ᵛ ρ) ]ᵛ y ≈⟨ []ᵛ-resp-≡ᵛ (λ x₁ →
              uniqueᵛ² {τ = [ (λ x₂ → var-inl x₂) , (λ x₂ → var-inr (τ (ρ x₂))) ]ᵛ}
                       {σ = σ' }
                       (λ x₂ → refl) (λ x₂ → refl) x₁) ⟩
          [ σ' ]ᵛ y ≈⟨ [∘ᵛ] ⟩
         ((Codomain-Jⱽ-Elt.F₁ (Monad.F₀ VMonad Γ A) τ μ ∘
           Codomain-Jⱽ-Elt.F₁ (Monad.F₀ VMonad Γ A) ρ ι) ⟨$⟩ y)
         ∎
         where
           σ' : (Γ ,, _) ⇒ᵛ Γ ,, _
           σ' = [ var-inl
                , (λ x₁ → var-inr (τ x₁))
                ]ᵛ ∘ᵛ [ var-inl
                      , (λ x₁ → var-inr (ρ x₁))
                      ]ᵛ
    Codomain-Jⱽ-Elt.F-resp-≈  (Monad.F₀ VMonad Γ A) {ψ} {Ω} {Δ} {Ξ} {ρ} {τ} {ι} {μ} ξᵛ ξᵐ {t} {u} ξ  =
                                                          begin⟨ Term-setoid Θ _ _ ⟩
                                                          ([ [ (λ x₁ → var-inl x₁) , (λ x₁ → var-inr (ρ x₁)) ]ᵛ ]ᵛ t) ≈⟨ []ᵛ-resp-≈ ξ ⟩
                                                          ([ [ (λ x₁ → var-inl x₁) , (λ x₁ → var-inr (ρ x₁)) ]ᵛ ]ᵛ u)
                                                                                ≈⟨ []ᵛ-resp-≡ᵛ ([,]ᵛ-resp-≡ᵛ (λ x → refl) λ x → ρ-resp-≡ {ρ = var-inr} (ξᵛ x)) ⟩
                                                          ([ [ (λ x₁ → var-inl x₁) , (λ x₁ → var-inr (τ x₁)) ]ᵛ ]ᵛ u) ∎

    _⟨$⟩_ (η (Monad.unit VMonad A) ψ Γ) = tm-var
    func-cong (η (Monad.unit VMonad A) ψ Γ) ξ = congˢ-var {σ = tm-var} ξ
    commute (Monad.unit VMonad A) ρ ι ξ =  congˢ-var {σ = tm-var} (ρ-resp-≡ {ρ = [ var-inl , (λ x₁ → var-inr (ρ x₁)) ]ᵛ} ξ)

    _⟨$⟩_ (η (Monad.extend VMonad {Δ} {Ξ} σ A) ψ Γ) t =  [ (λ {B} x →  η (σ B) ψ  Γ  ⟨$⟩ x) ]ˢ t
    func-cong (η (Monad.extend VMonad σ A) ψ Γ) = []ˢ-resp-≈ ((λ {B} x → η (σ B) ψ Γ ⟨$⟩ x) )
    commute (Monad.extend VMonad {Υ} {Ω} σ A) {Ξ} {Ψ} {Γ} {Δ} ρ ι {x} {y} x≈y
      = begin⟨ Term-setoid Θ _ _ ⟩
               ([ (λ {B} → _⟨$⟩_ (η (σ B) Ψ Δ)) ]ˢ ([ [ (λ x₁ → var-inl x₁) , (λ x₁ → var-inr (ρ x₁)) ]ᵛ ]ᵛ x)) ≈⟨  ≈-sym ([ˢ∘ᵛ] x) ⟩
               ([(λ {B} → _⟨$⟩_ (η (σ B) Ψ Δ)) ˢ∘ᵛ [ (λ x₁ → var-inl x₁) , (λ x₁ → var-inr (ρ x₁)) ]ᵛ ]ˢ x) ≈⟨ {!!} ⟩
               {!!} ≈⟨ {!!} ⟩
               ([ [ (λ x₁ → var-inl x₁) , (λ x₁ → var-inr (ρ x₁)) ]ᵛ ]ᵛ ([ (λ {B} → _⟨$⟩_ (η (σ B) Ξ Γ)) ]ˢ y)) ∎

      --   where
      --     is-subst : ∀ (𝒩 : NaturalTransformation-Jⱽ (Jⱽ Γ A) (Monad.F₀ VMonad Ω i)) → Σ
      -- begin⟨ Term-setoid Θ _ _ ⟩
      --   (η (Monad.extend VMonad σ A) Ψ Δ ∘
      --     Codomain-Jⱽ-Elt.F₁ (Monad.F₀ VMonad Υ A) ρ ι
      --     ⟨$⟩ x)
      --     ≈⟨ ≈-sym ([ˢ∘ᵛ] x) ⟩
      --   ([ (λ {B} x₁ → η (σ B) Θ Δ ⟨$⟩ x₁) ˢ∘ᵛ (ʳ⇑ᵛ ρ) ]ˢ x) ≈⟨ []ˢ-resp-≈ ((λ {B} → _⟨$⟩_ (η (σ B) Θ Δ)) ˢ∘ᵛ(ʳ⇑ᵛ ρ)) x≈y ⟩
      --   ([ (λ {B} → _⟨$⟩_ (η (σ B) Θ Δ)) ˢ∘ᵛ (ʳ⇑ᵛ ρ) ]ˢ y) ≈⟨ []ˢ-resp-≈ˢ y (η-ˢ∘ᵛ ρ ι) ⟩
      --   ([ ʳ⇑ᵛ ρ ᵛ∘ˢ (λ {B} x₁ → η (σ B) Θ Γ ⟨$⟩ x₁) ]ˢ y) ≈⟨ [ᵛ∘ˢ] y ⟩
      --   (Codomain-Jⱽ-Elt.F₁ (Monad.F₀ VMonad Ω A) ρ ι ∘
      --     η (Monad.extend VMonad σ A) Ξ Γ
      --     ⟨$⟩ y)
      --     ∎
      where
        𝒩-to-subst : ∀  {Γ Δ Ξ} (𝒩 : ∀ A → NaturalTransformation-Jⱽ (Categories.Functor.Functor.F₀ Jⱽ Γ A) (Monad.F₀ VMonad Ξ A)) → (Θ ⊕ (Γ ,, Δ) ⇒ˢ (Ξ ,, Δ))
        𝒩-to-subst 𝒩 {A} (var-inl z) = η (𝒩 A) _ _ ⟨$⟩ (var-inl z)
        𝒩-to-subst 𝒩 {A} (var-inr z) = tm-var (var-inr z)

        𝒩-is-subst : ∀ {Ω Γ Ξ} (𝒩 : ∀ A → NaturalTransformation-Jⱽ (Categories.Functor.Functor.F₀ Jⱽ Γ A) (Monad.F₀ VMonad Ξ A)) x → SecondOrder.Term._≈_ Σ ((NaturalTransformation-Jⱽ.η (𝒩 A) Ω Γ) ⟨$⟩ x) (𝒩-to-subst 𝒩 x)
        𝒩-is-subst 𝒩 (var-inl z) = {!!}
        𝒩-is-subst 𝒩 (var-inr z) = {!!}

        η-ˢ∘ᵛ : ∀ {Ξ} {ψ} {Γ} {Δ} (ρ : Γ ⇒ᵛ Δ) (ι : Ξ ⇒ᵐ ψ)
               → (λ {B} → _⟨$⟩_ (η (σ B) ψ Δ)) ˢ∘ᵛ (ʳ⇑ᵛ ρ)
                 ≈ˢ ʳ⇑ᵛ ρ ᵛ∘ˢ (λ {B} x₁ → η (σ B) Ψ Γ ⟨$⟩ x₁)
        η-ˢ∘ᵛ {Ξ = Ξ′} {ψ = ψ} {Γ = Γ′} {Δ′} ρ ι (var-inl x) =
                   begin⟨ Term-setoid Θ _ _ ⟩
                     ((λ {B} → _⟨$⟩_ (η (σ B) ψ Δ′)) ˢ∘ᵛ (ʳ⇑ᵛ ρ)) (var-inl x) ≈⟨ {!!} ⟩
                     {![]!} ≈⟨ {!!} ⟩
                     {!!} ≈⟨ {! ˢ∘ᵛ-η (σ A₁) Θ Γ₁η (σ A₁) Θ Γ₁ᵛ∘ˢ-disjoint ˢ∘ᵛ-ᵛ∘uˢ-disjoint!} ⟩
                     (ʳ⇑ᵛ ρ ᵛ∘ˢ (λ {B} → _⟨$⟩_ (η (σ B) Ψ _))) (var-inl x) ∎
               where
                 ˢ∘ᵛ-ᵛ∘ˢ-disjoint : ∀ {ψ} {Γ Ξ Δ Λ} (σ : ψ ⊕ Ξ ⇒ˢ Λ) (ρ : Γ ⇒ᵛ Δ)
                                      →  ⇑ˢ σ ˢ∘ᵛ ʳ⇑ᵛ ρ  ≈ˢ ʳ⇑ᵛ ρ ᵛ∘ˢ ⇑ˢ σ
                 ˢ∘ᵛ-ᵛ∘ˢ-disjoint σ τ (var-inl x) =
                                        begin⟨ Term-setoid _ _ _ ⟩
                                          ([ var-inl ]ᵛ σ x) ≈⟨ []ᵛ-resp-≡ᵛ (λ x₃ → refl) ⟩
                                          ([ [ (λ x₃ → var-inl x₃) , (λ x₃ → var-inr (τ x₃)) ]ᵛ ∘ᵛ var-inl ]ᵛ σ x) ≈⟨ [∘ᵛ] ⟩
                                          ([ [ (λ x₃ → var-inl x₃) , (λ x₃ → var-inr (τ x₃)) ]ᵛ ]ᵛ ([ var-inl ]ᵛ σ x)) ∎
                 ˢ∘ᵛ-ᵛ∘ˢ-disjoint σ τ (var-inr x) = ≈-refl
        η-ˢ∘ᵛ ρ ι (var-inr x) = begin⟨ Term-setoid Θ _ _ ⟩ {!!}
    Monad.identityʳ VMonad {_} {_} {𝒩s} =
                           λ i {k = Ω} {Γ = Γ} {x = x} {y = y} x≈y → (func-cong (η (𝒩s i) Ω Γ) (x≈y))
    Monad.identityˡ VMonad = λ i x≈y →  ≈-trans [idˢ] x≈y
    Monad.assoc VMonad  {Γ} {Δ} {Ξ} {k} {l} = λ A {ψ} {Λ} {x} {y} ξ
                         → begin⟨ Term-setoid Θ _ _ ⟩
                             ([ (λ {B} x₁ → [ (λ {B = B₁} → _⟨$⟩_ (η (l B₁) ψ Λ)) ]ˢ (η (k B) ψ Λ ⟨$⟩ x₁)) ]ˢ x)
                                ≈⟨ []ˢ-resp-≈ (λ {B} x₁ → [ (λ {B = B₁} → _⟨$⟩_ (η (l B₁) ψ Λ)) ]ˢ (η (k B) ψ Λ ⟨$⟩ x₁)) ξ ⟩
                             ([ (λ {B} x₁ → [ (λ {B = B₁} → _⟨$⟩_ (η (l B₁) ψ Λ)) ]ˢ (η (k B) ψ Λ ⟨$⟩ x₁)) ]ˢ y) ≈⟨ [∘ˢ] y ⟩
                             ([ (λ {B} → _⟨$⟩_ (η (l B) ψ Λ)) ]ˢ ([ (λ {B} → _⟨$⟩_ (η (k B) ψ Λ)) ]ˢ y)) ∎
    Monad.extend-≈ VMonad {Γ} {Δ} {k} {h} = λ ξ A {ψ} {Λ} {t} {u} ξᵗ
                                            → begin⟨ Term-setoid Θ _ _ ⟩
                                              ([ (λ {B} → _⟨$⟩_ (η (k B) ψ Λ)) ]ˢ t) ≈⟨ []ˢ-resp-≈ (λ {B} → _⟨$⟩_ (η (k B) ψ Λ)) ξᵗ ⟩
                                              ([ (λ {B} → _⟨$⟩_ (η (k B) ψ Λ)) ]ˢ u) ≈⟨ []ˢ-resp-≈ˢ u (λ {A = C} x → ξ C refl) ⟩
                                              ([ (λ {B} → _⟨$⟩_ (η (h B) ψ Λ)) ]ˢ u) ∎

-- *************************************************************************************

-- open import Agda.Primitive using (lzero; lsuc; _⊔_ ;Level)
-- open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; setoid; cong; trans)
-- import Function.Equality
-- open import Relation.Binary using (Setoid)

-- import Categories.Category
-- import Categories.Functor
-- import Categories.Category.Instance.Setoids
-- import Categories.Monad.Relative
-- import Categories.Category.Equivalence
-- import Categories.Category.Cocartesian
-- import Categories.Category.Construction.Functors
-- import Categories.NaturalTransformation.Equivalence
-- import Relation.Binary.Core

-- import SecondOrder.Arity
-- import SecondOrder.Signature
-- import SecondOrder.Metavariable
-- import SecondOrder.VRenaming
-- import SecondOrder.MRenaming
-- import SecondOrder.Term
-- import SecondOrder.IndexedCategory
-- import SecondOrder.RelativeKleisli
-- import SecondOrder.Substitution

-- module SecondOrder.VRelMon
--   {ℓ}
--   {𝔸 : SecondOrder.Arity.Arity}
--   (Σ : SecondOrder.Signature.Signature ℓ 𝔸)
--   where

--   open SecondOrder.Signature.Signature Σ
--   open SecondOrder.Metavariable Σ
--   open SecondOrder.Term Σ
--   open SecondOrder.VRenaming Σ
--   open SecondOrder.MRenaming Σ
--   open SecondOrder.Substitution Σ

--   -- TERMS FORM A RELATIVE MONAD
--   -- (FOR A FUNCTOR WHOSE DOMAIN IS THE
--   -- CATEGORY OF VARIABLE CONTEXTS AND RENAMINGS)

--   module _ where
--     open Categories.Category
--     open Categories.Functor using (Functor)
--     open Categories.Category.Instance.Setoids
--     open Categories.Monad.Relative
--     open Function.Equality using () renaming (setoid to Π-setoid)
--     open Categories.Category.Equivalence using (StrongEquivalence)
--     open import SecondOrder.IndexedCategory
--     open import SecondOrder.RelativeKleisli
--     open Categories.Category.Construction.Functors
--     open Categories.NaturalTransformation.Equivalence
--     open Relation.Binary.Core hiding (_⇒_)

--     -- The carrier of the codomain of Jⱽ (morally ∀ Γ → A ∈ Δ ,, Γ)
--     record Codomain-Jⱽ-Elt : Set ((lsuc ℓ)) where
--       open Category (Setoids ℓ ℓ)
--       open Setoid
--       field
--         F₀ :  VContext → MContext → Obj
--         F₁ : ∀ {Θ ψ Δ Ξ} (ρ : Δ ⇒ᵛ Ξ) (ι : Θ ⇒ᵐ ψ)
--              → (F₀ Δ Θ) ⇒ (F₀ Ξ ψ)
--         identity : ∀ {Θ Δ}
--                    → Category._≈_ (Setoids ℓ ℓ) (F₁ (idᵛ {Δ}) (idᵐ {Θ})) (id {F₀ Δ Θ})
--         homomorphism : ∀ {Θ ψ Ω Γ Δ Ξ} {ρ : Γ ⇒ᵛ Δ} {ι : Θ ⇒ᵐ ψ} {τ : Δ ⇒ᵛ Ξ} {μ : ψ ⇒ᵐ Ω}
--                        → Category._≈_ (Setoids ℓ ℓ) (F₁ (τ ∘ᵛ ρ) (μ ∘ᵐ ι)) ((F₁ τ μ) ∘ (F₁ ρ ι))
--         F-resp-≈ : ∀ {Θ ψ Γ Δ} {ρ τ : Γ ⇒ᵛ Δ} {ι μ : Θ ⇒ᵐ ψ}
--                    → (ρ ≡ᵛ τ) → (ι ≡ᵐ μ) → (Category._≈_ (Setoids ℓ ℓ) (F₁ ρ ι) (F₁ τ μ))

--     -- Transformation for Codomain-Jⱽ (analogue to natural transformations)

--     record NaturalTransformation-Jⱽ (Fⱽ Gⱽ : Codomain-Jⱽ-Elt) : Set (lsuc ℓ)
--       where
--         private
--           module Fⱽ = Codomain-Jⱽ-Elt Fⱽ
--           module Gⱽ = Codomain-Jⱽ-Elt Gⱽ
--         open Fⱽ using (F₀; F₁)
--         open Category (Setoids ℓ ℓ)
--         field
--           η : ∀ Θ Γ → (F₀ Γ Θ) ⇒ (Gⱽ.F₀ Γ Θ)
--           commute : ∀ {Θ ψ Γ Δ} (ρ : Γ ⇒ᵛ Δ) (ι : Θ ⇒ᵐ ψ)
--                     → Category._≈_ (Setoids ℓ ℓ) ((η ψ Δ) ∘ (F₁ ρ ι)) ((Gⱽ.F₁ ρ ι) ∘ (η Θ Γ))

--     open NaturalTransformation-Jⱽ

--     -- Equivalence of NaturalTransformation-Jⱽ (analogue to the one
--     -- of the natural transformations)

--     infix 4 _≃Jⱽ_

--     _≃Jⱽ_ : ∀ {Fⱽ Gⱽ : Codomain-Jⱽ-Elt} → Rel (NaturalTransformation-Jⱽ Fⱽ Gⱽ) ℓ
--     𝒩 ≃Jⱽ ℳ  = ∀ {Θ Γ} → Category._≈_ (Setoids ℓ ℓ)
--                             (η 𝒩 Θ Γ)
--                             (η ℳ Θ Γ)

--     -- Identity transformation analogue to the one
--     -- of the natural transformations, for NaturalTransformation-Jⱽ

--     idN-Jⱽ : ∀ {Fⱽ : Codomain-Jⱽ-Elt} → NaturalTransformation-Jⱽ Fⱽ Fⱽ
--     idN-Jⱽ {Fⱽ} =
--            record
--              { η = λ Θ Γ →
--                record
--                  { _⟨$⟩_ = λ x → x
--                  ; cong = λ x → x }
--              ; commute = λ {Θ} {ψ} {Γ} {Δ} ρ ι ξ
--                          → Codomain-Jⱽ-Elt.F-resp-≈  Fⱽ {Θ} {ψ} {Γ} {Δ} {ρ} {ρ} {ι} {ι}
--                                                 (λ x₁ → refl) (λ M → refl) ξ }

--     -- Composition of NaturalTransformation-Jⱽ (analogue to the one
--     -- of the natural transformations)

--     _∘-Jⱽ_ : ∀ {Fⱽ Gⱽ Hⱽ : Codomain-Jⱽ-Elt} (𝒩 : NaturalTransformation-Jⱽ Gⱽ Hⱽ) (ℳ : NaturalTransformation-Jⱽ Fⱽ Gⱽ) → NaturalTransformation-Jⱽ Fⱽ Hⱽ
--     _∘-Jⱽ_ {Fⱽ} {Gⱽ} {Hⱽ} 𝒩 ℳ =
--              let open Category (Setoids ℓ ℓ) in
--              let open NaturalTransformation-Jⱽ in
--              let open Codomain-Jⱽ-Elt in
--              record
--                  { η = λ Θ Γ → η 𝒩 Θ Γ ∘ η ℳ Θ Γ
--                  ; commute = λ {Θ} {ψ} {Γ} {Δ} ρ ι →
--                              let open HomReasoning {F₀ Fⱽ Γ Θ} {F₀ Hⱽ Δ ψ} in
--                              begin
--                              (Category._∘_ (Setoids ℓ ℓ) (η {Gⱽ} {Hⱽ} 𝒩 ψ Δ) ((η {Fⱽ} {Gⱽ} ℳ ψ Δ) ∘ (F₁ Fⱽ ρ ι))) ≈⟨ assoc {f = F₁ Fⱽ ρ ι} {g = η ℳ ψ Δ} {h = η 𝒩 ψ Δ} ⟩
--                              (η 𝒩 ψ Δ ∘ (η ℳ ψ Δ) ∘ (F₁ Fⱽ ρ ι)) ≈⟨ refl⟩∘⟨_
--                                                                       {f = η 𝒩 ψ Δ} {g = (η ℳ ψ Δ) ∘ (F₁ Fⱽ ρ ι)}
--                                                                       {i = (F₁ Gⱽ ρ ι) ∘ (η ℳ Θ Γ)}
--                                                                       (commute ℳ ρ ι) ⟩
--                              (η 𝒩 ψ Δ ∘ ((F₁ Gⱽ ρ ι) ∘ (η ℳ Θ Γ))) ≈⟨ sym-assoc {f = η ℳ Θ Γ} {g = F₁ Gⱽ ρ ι} {h = η 𝒩 ψ Δ}⟩
--                              ((η 𝒩 ψ Δ) ∘ (F₁ Gⱽ ρ ι)) ∘ (η ℳ Θ Γ) ≈⟨ _⟩∘⟨refl
--                                                                       {f = (η 𝒩 ψ Δ) ∘ (F₁ Gⱽ ρ ι)} {h = (F₁ Hⱽ ρ ι) ∘ (η 𝒩 Θ Γ)}
--                                                                       {g = η ℳ Θ Γ}
--                                                                       (commute 𝒩 ρ ι) ⟩
--                              (((F₁ Hⱽ ρ ι) ∘ (η 𝒩 Θ Γ)) ∘ (η ℳ Θ Γ)) ≈⟨ assoc {f = η ℳ Θ Γ} {g = η 𝒩 Θ Γ} {h = F₁ Hⱽ ρ ι} ⟩
--                              (((F₁ Hⱽ ρ ι) ∘ (η 𝒩 Θ Γ)) ∘ (η ℳ Θ Γ)) ∎}

--     -- Proof that the category of Codomain-Jⱽ and NaturalTransformation-Jⱽ is indeed a category

--     -- associativity of composition
--     -- (surprisingly enough, the proof of "sym-assoc-Jⱽ" is exactly the same :
--     -- Is there a problem in the definitions ?)
--     assoc-Jⱽ : {A B C D : Codomain-Jⱽ-Elt}
--                {ℒ : NaturalTransformation-Jⱽ A B}
--                {ℳ : NaturalTransformation-Jⱽ B C}
--                {𝒩 : NaturalTransformation-Jⱽ C D}
--                → ((𝒩 ∘-Jⱽ ℳ) ∘-Jⱽ ℒ) ≃Jⱽ (𝒩 ∘-Jⱽ (ℳ ∘-Jⱽ ℒ))
--     assoc-Jⱽ  {A} {B} {C} {D} {ℒ} {ℳ} {𝒩} {Θ} {Γ} ξ = Function.Equality.Π.cong (η 𝒩 Θ Γ)
--                                                           (Function.Equality.Π.cong (η ℳ Θ Γ)
--                                                             (Function.Equality.cong (η ℒ Θ Γ) ξ))

--     -- identity is identity
--     identityˡ-Jⱽ : {A B : Codomain-Jⱽ-Elt}
--                   {𝒩 : NaturalTransformation-Jⱽ A B}
--                   → (idN-Jⱽ ∘-Jⱽ 𝒩) ≃Jⱽ 𝒩
--     identityˡ-Jⱽ  {𝒩 = 𝒩} {Θ = Θ} {Γ = Γ} ξ = Function.Equality.cong (η 𝒩 Θ Γ) ξ

--     -- Codomain of Jⱽ (the category with Codomain-Jⱽ-Elt as objects and NaturalTransformation-Jⱽ as maps)
--     Codomain-Jⱽ : Category (lsuc ℓ) (lsuc ℓ)  ℓ
--     Codomain-Jⱽ = record
--                     { Obj = Codomain-Jⱽ-Elt
--                     ; _⇒_ = NaturalTransformation-Jⱽ
--                     ; _≈_ = _≃Jⱽ_
--                     ; id = idN-Jⱽ
--                     ; _∘_ = _∘-Jⱽ_
--                     ; assoc = λ {Fⱽ} {Gⱽ} {Hⱽ} {Kⱽ} {𝒩} {ℳ} {ℒ} → assoc-Jⱽ  {ℒ = 𝒩} {ℳ = ℳ} {𝒩 = ℒ}
--                     ; sym-assoc = λ {Fⱽ} {Gⱽ} {Hⱽ} {Kⱽ} {𝒩} {ℳ} {ℒ} → assoc-Jⱽ  {ℒ = 𝒩} {ℳ = ℳ} {𝒩 = ℒ}
--                     ; identityˡ = λ {Fⱽ} {Gⱽ} {𝒩} → identityˡ-Jⱽ {𝒩 = 𝒩}
--                     ; identityʳ = λ {Fⱽ} {Gⱽ} {𝒩} → identityˡ-Jⱽ {𝒩 = 𝒩}
--                     ; identity² = λ {Fⱽ} ξ → ξ
--                     ; equiv = λ {Fⱽ} {Gⱽ}
--                               → record
--                                   { refl = λ {𝒩 = 𝒩} {Θ = Θ} {Γ = Γ} {x} {y} ξ
--                                            → Function.Equality.cong (η 𝒩 Θ Γ) ξ
--                                   ; sym = λ {𝒩} {ℳ} ξᴺ {Θ} {Γ} ξ
--                                           → Category.Equiv.sym (Setoids ℓ ℓ)
--                                           {_} {_} {η 𝒩 Θ Γ} {η ℳ Θ Γ} ξᴺ ξ
--                                   ; trans =  λ {𝒩} {ℳ} {ℒ} ξᴺ₂ ξᴺ₁ {Θ} {Γ} ξ
--                                              → Category.Equiv.trans (Setoids ℓ ℓ)
--                                              {_} {_} {η 𝒩 Θ Γ} {η ℳ Θ Γ} {η ℒ Θ Γ} ξᴺ₂ ξᴺ₁ ξ}
--                     ; ∘-resp-≈ = λ {Fⱽ} {Gⱽ} {Hⱽ} {𝒩} {ℳ} {ℒ} {𝒦} ξᴺ₁ ξᴺ₂ {Θ} {Γ} ξ
--                                  → Category.∘-resp-≈ (Setoids ℓ ℓ)
--                                    {_} {_}  {_}
--                                    {η 𝒩 Θ Γ} {η ℳ Θ Γ} {η ℒ Θ Γ} {η 𝒦 Θ Γ}
--                                    ξᴺ₁ ξᴺ₂ ξ
--                     }

--     -- The embedding of contexts into setoids indexed by sorts, metavariable telescope and variable telescope

--     Jⱽ : Functor VContexts (IndexedCategory sort Codomain-Jⱽ)
--     Jⱽ = record
--               { F₀ = λ Γ A →
--                        record
--                          { F₀ = λ Δ Θ → setoid (A ∈ (Γ ,, Δ))
--                          ; F₁ = λ ρ ι → record
--                                             { _⟨$⟩_ = [ inlᵛ , inrᵛ ∘ᵛ ρ ]ᵛ
--                                             ; cong = λ {x} {y} ξ →  ρ-resp-≡ {ρ = [ var-inl , var-inr ∘ᵛ ρ ]ᵛ} ξ}
--                          ; identity = λ {Θ} {Δ} {x} ξ → trans (idᵛ+idᵛ x) ξ
--                          ; homomorphism = λ {Θ} {ψ} {Ω} {Δ} {Ξ} {Λ} {ρ} {ι} {τ} {μ} {x} {y} ξ
--                                           → trans
--                                             (ʳ⇑ᵛ-resp-∘ᵛ x)
--                                             (ρ-resp-≡ {ρ = [ var-inl , (λ x₁ → var-inr (τ x₁)) ]ᵛ}
--                                               (ρ-resp-≡ {ρ = [ var-inl , (λ x₁ → var-inr (ρ x₁)) ]ᵛ} ξ))
--                          ; F-resp-≈ = λ {Θ} {ψ} {Δ} {Ξ} {ρ} {τ} {ι} {μ} ξᵛ ξᵐ {x} {y} ξ
--                                       → trans
--                                         ([,]ᵛ-resp-≡ᵛ (λ x₁ → refl) (∘ᵛ-resp-≡ᵛ {τ₁ = λ x₁ → var-inr x₁} (λ x₁ → refl) λ x₁ → ξᵛ x₁) x)
--                                         (ρ-resp-≡ {ρ = [ var-inl , (λ x₁ → var-inr (τ x₁)) ]ᵛ} ξ)
--                          }

--               ; F₁ = λ ρ A → record
--                                { η = λ Θ Γ → record { _⟨$⟩_ = ⇑ᵛ ρ ; cong = cong (⇑ᵛ ρ) }
--                                ; commute = λ τ ι {x} ξ
--                                            → trans
--                                              (uniqueᵛ²
--                                                {τ = [ (λ x₁ → var-inl (ρ x₁)) , (λ x₁ → var-inr x₁) ]ᵛ ∘ᵛ [ var-inl , (λ x₁ → var-inr (τ x₁)) ]ᵛ}
--                                                {σ = [ var-inl , (λ x₁ → var-inr (τ x₁)) ]ᵛ ∘ᵛ [ (λ x₁ → var-inl (ρ x₁)) , (λ x₁ → var-inr x₁) ]ᵛ} (λ x₁ → refl) (λ x₁ → refl) x)
--                                                (ρ-resp-≡
--                                                  {ρ = [ var-inl , (λ x₁ → var-inr (τ x₁)) ]ᵛ ∘ᵛ [ (λ x₁ → var-inl (ρ x₁)) , (λ x₁ → var-inr x₁) ]ᵛ} ξ)}

--               ; identity =  λ A {Θ} {Γ} {x} ξ → trans (idᵛ+idᵛ x) ξ
--               ; homomorphism = λ {Δ} {Ξ} {Λ} {ρ} {τ} A {_} {_} {x} ξ
--                                → trans
--                                  (uniqueᵛ²
--                                    {τ = [ (λ x₁ → var-inl (τ (ρ x₁))) , (λ x₁ → var-inr x₁) ]ᵛ}
--                                    {σ = [ (λ x₁ → var-inl (τ x₁)) , (λ x₁ → var-inr x₁) ]ᵛ ∘ᵛ [ (λ x₁ → var-inl (ρ x₁)) , (λ x₁ → var-inr x₁) ]ᵛ}
--                                    (λ x₁ → refl) (λ x₁ → refl) x)
--                                  (ρ-resp-≡
--                                    {ρ = [ (λ x₁ → var-inl (τ x₁)) , (λ x₁ → var-inr x₁) ]ᵛ ∘ᵛ [ (λ x₁ → var-inl (ρ x₁)) , (λ x₁ → var-inr x₁) ]ᵛ } ξ)
--               ; F-resp-≈ = λ {_} {_} {ρ} {τ} ξρ A {_} {_} {x} {y} ξ
--                            → trans
--                              (([,]ᵛ-resp-≡ᵛ {ρ₁ = λ x₁ → var-inl (ρ x₁)} {τ₁ = var-inr} (λ x₁ → ∘ᵛ-resp-≡ᵛ {τ₁ = var-inl} (λ x₃ → refl) ξρ x₁) (λ x₁ → refl) x))
--                              (ρ-resp-≡ {ρ = ⇑ᵛ τ} ξ)
--               }

--   -- The relative monad over Jⱽ

--   module _ {Θ : MContext} where
--     open Categories.Category
--     open Categories.Functor using (Functor)
--     open Categories.Category.Instance.Setoids
--     open Categories.Monad.Relative
--     open Function.Equality using () renaming (setoid to Π-setoid)
--     open Categories.Category.Equivalence using (StrongEquivalence)
--     open import SecondOrder.IndexedCategory
--     open import SecondOrder.RelativeKleisli
--     open NaturalTransformation-Jⱽ

--     VMonad : Monad Jⱽ
--     VMonad =
--       let open Function.Equality using (_⟨$⟩_) renaming (cong to func-cong) in
--       record
--         { F₀ = λ Γ A → record
--                          { F₀ = λ Δ ψ → Term-setoid Θ (Γ ,, Δ) A
--                          ; F₁ = λ ρ ι → record { _⟨$⟩_ = [_]ᵛ_ (ʳ⇑ᵛ ρ) ; cong = λ ξ → []ᵛ-resp-≈ ξ }
--                          ; identity = λ ξ → ≈-trans ([]ᵛ-resp-≡ᵛ idᵛ+idᵛ) (≈-trans [idᵛ] ξ)
--                          ; homomorphism = λ {_} {_} {_} {_} {_} {_} {ρ} {_} {τ} ξ
--                                           → ≈-trans
--                                           ([]ᵛ-resp-≈ ξ)
--                                           (≈-trans
--                                             ([]ᵛ-resp-≡ᵛ λ x₁
--                                               → uniqueᵛ²
--                                                 {τ = [ (λ x₂ → var-inl x₂) , (λ x₂ → var-inr (τ (ρ x₂))) ]ᵛ}
--                                                 {σ = [ (λ x₁ → var-inl x₁) , (λ x₁ → var-inr (τ x₁)) ]ᵛ  ∘ᵛ [ (λ x₁ → var-inl x₁) , (λ x₁ → var-inr (ρ x₁)) ]ᵛ }
--                                                 (λ x₂ → refl) (λ x₂ → refl) x₁)
--                                             [∘ᵛ])

--                          ; F-resp-≈ = λ ξᵛ ξᵐ ξ → ≈-trans ([]ᵛ-resp-≈ ξ) ([]ᵛ-resp-≡ᵛ λ x → [,]ᵛ-resp-≡ᵛ (λ x₁ → refl) (λ x₁ → ρ-resp-≡ {ρ = var-inr} (ξᵛ x₁)) x )
--                          }
--         ; unit = λ A
--                    → record
--                      { η = λ ψ Γ
--                        → record
--                          { _⟨$⟩_ = λ x → tm-var x
--                          ; cong = λ ξ → congˢ-var {σ = tm-var} ξ }
--                        ; commute = λ ρ ι ξ → congˢ-var {σ = tm-var} (ρ-resp-≡ {ρ = [ var-inl , (λ x₁ → var-inr (ρ x₁)) ]ᵛ} ξ) }
--         ; extend = {!!}
--         ; identityʳ = λ A ξ → {!!}
--         ; identityˡ = {!!}
--         ; assoc = {!!}
--         ; extend-≈ = {!!}
--         }

--     -- Other possibility, if the above doesn't work :

--     -- Jⱽ′ : Functor VContexts (Functors MContexts (Functors VContexts (IndexedCategory sort (Setoids ℓ ℓ))))
--     -- Jⱽ′ = record
--     --           { F₀ = {!!} -- λ Γ A → setoid (A ∈ Γ)
--     --           ; F₁ = {!!} -- λ ρ A → record { _⟨$⟩_ = ρ ; cong = cong ρ }
--     --           ; identity = {!!} -- λ A ξ → ξ
--     --           ; homomorphism = {!!} -- λ {_} {_} {_} {ρ} {σ} A {_} {_} ξ → cong σ (cong ρ ξ)
--     --           ; F-resp-≈ = {!!} -- λ ξ A ζ → trans (ξ _) (cong _ ζ)
--     --           }

max_stars_repo_name: andrejbauer/formal

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
module Issue759a where

import Common.Level

abstract
  record Wrap (A : Set) : Set where
    field wrapped : A
  open Wrap public

wrap : {A : Set} → A → Wrap A
wrap a = record { wrapped = a }

-- WAS: Broken error message:

-- Not in scope:
--   Issue759a.recCon-NOT-PRINTED at
-- when checking the definition of wrap

-- NOW:

-- Expected non-abstract record type, found Wrap
-- when checking that the expression record { wrapped = a } has type
-- Wrap .A

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import SOAS.Common

-- Free construction with respect to a forgetful functor between categories
module SOAS.Construction.Free {ℂ 𝕊 : Category 1ℓ 0ℓ 0ℓ}
                               (U : Functor 𝕊 ℂ) where

open import Categories.Adjoint
import Categories.Morphism.Reasoning as MR
open import Categories.Category.Equivalence using (WeakInverse; StrongEquivalence)
open import Categories.Adjoint.Properties
open import Categories.Monad

private module ℂ = Category ℂ
private module 𝕊 = Category 𝕊
private module U = Functor U

-- Mapping from an object of the carrier category to the carrier of an object
-- from the structure category
_↪_ : ℂ.Obj → 𝕊.Obj → Set
C ↪ S = ℂ [ C , U.₀ S ]

-- Definition of F being a free structure over a carrier C:
-- any carrier map c : C → S into the carrier of a structure S factorises
-- through a unique extension of c to a structure homomorphism ĉ : F C → S:
--
--           ⌊-⌋
--   C ────────────── FC
--  ╰─────── S ───────╯
--      c         ĉ

record FreeConstruction (F : ℂ.Obj → 𝕊.Obj)
                        (C : ℂ.Obj)
                        (embed : C ↪ F C)
                        (S : 𝕊.Obj)
                        (c : C ↪ S)
                        : Set₁ where

  field
    -- Given another structure S, any mapping from C to the carrier of S can be
    -- extended into a structure homomorphism from F C to S.
    extend : 𝕊 [ F C , S ]

    -- Any map from C to the carrier of a structure S factors through the
    -- embedding and extension
    factor : U.₁ extend ℂ.∘ embed ℂ.≈ c

    -- Extension is the unique factorising morphism
    unique : (e : 𝕊 [ F C , S ])
           → (p : (U.₁ e ℂ.∘ embed) ℂ.≈ c)
           → 𝕊 [ e ≈ extend ]

record FreeMapping (F : ℂ.Obj → 𝕊.Obj) : Set₁ where

  field
    embed : {C : ℂ.Obj} → C ↪ F C
    univ  : (C : ℂ.Obj) (S : 𝕊.Obj)(c : C ↪ S)
          → FreeConstruction F C embed S c

  module Universal C S c = FreeConstruction (univ C S c)

  module _ {C : ℂ.Obj} {S : 𝕊.Obj}(c : C ↪ S) where
    open Universal C S c public

  open MR ℂ
  open ℂ.HomReasoning
  private module 𝕊R = 𝕊.HomReasoning
  open NT

  -- The uniqueness of the factors means that any two morphisms
  -- that factorise the same arrow must be equal
  equate : {C : ℂ.Obj}{S : 𝕊.Obj}
        → (f g : 𝕊 [ F C , S ])
        → (p : U.₁ f ℂ.∘ embed ℂ.≈ U.₁ g ℂ.∘ embed)
        → 𝕊 [ f ≈ g ]
  equate f g p = unique _ f p 𝕊R.○ 𝕊R.⟺ (unique _ g ℂ.Equiv.refl)

  -- Infix shorthand
  [_≋_]! : {C : ℂ.Obj}{S : 𝕊.Obj}
        → (f g : 𝕊 [ F C , S ])
        → (p : U.₁ f ℂ.∘ embed ℂ.≈ U.₁ g ℂ.∘ embed)
        → 𝕊 [ f ≈ g ]
  [ f ≋ g ]! p = equate f g p

  -- Extensions of equal embeddings are equal
  extend-cong : {C : ℂ.Obj}{S : 𝕊.Obj}(c₁ c₂ : C ↪ S)
             → ℂ [ c₁ ≈ c₂ ] → 𝕊 [ extend c₁ ≈ extend c₂ ]
  extend-cong {C}{S} c₁ c₂ p = unique _ (extend c₁) (factor c₁ ○ p)

  -- | Freeness makes F into a functor

  map : {C D : ℂ.Obj} → C ℂ.⇒ D → F C 𝕊.⇒ F D
  map {C}{D} f = extend (embed ℂ.∘ f)

  embed-commute : {C D : ℂ.Obj}(f : C ℂ.⇒ D)
               → embed ℂ.∘ f ℂ.≈ (U.₁ (map f) ℂ.∘ embed)
  embed-commute {C}{D} f = ⟺ (factor (embed ℂ.∘ f))

  identity : {C : ℂ.Obj} → map (ℂ.id {C}) 𝕊.≈ 𝕊.id
  identity {C} = 𝕊R.⟺ $ᶠ unique _ 𝕊.id (begin
         U.₁ 𝕊.id ℂ.∘ embed  ≈⟨ U.identity ⟩∘⟨refl ⟩
         ℂ.id ℂ.∘ embed      ≈⟨ id-comm-sym ⟩
         embed ℂ.∘ ℂ.id      ∎)

  homomorphism : {C D E : ℂ.Obj} {f : ℂ [ C , D ]} {g : ℂ [ D , E ]}
              → 𝕊 [ map (ℂ [ g ∘ f ])
               ≈ 𝕊 [ map g ∘ map f ] ]
  homomorphism {C}{D}{E}{f}{g} = 𝕊R.⟺ $ᶠ unique _ (𝕊 [ map g ∘ map f ]) (begin
         U.₁ (map g 𝕊.∘ map f) ℂ.∘ embed           ≈⟨ pushˡ U.homomorphism ⟩
         U.₁ (map g)  ℂ.∘  U.₁ (map f)  ℂ.∘ embed  ≈⟨ pushʳ (⟺ (embed-commute f)) ⟩
         (U.₁ (map g)  ℂ.∘  embed) ℂ.∘ f           ≈⟨ pushˡ (⟺ (embed-commute g)) ⟩
         embed ℂ.∘ g ℂ.∘ f                          ∎)

  -- Free functor from ℂ to 𝕊
  Free : Functor ℂ 𝕊
  Free = record
    { F₀ = F
    ; F₁ = map
    ; identity = identity
    ; homomorphism = homomorphism
    ; F-resp-≈ = λ {C}{D}{f}{g} p →
          extend-cong (embed ℂ.∘ f) (embed ℂ.∘ g) (ℂ.∘-resp-≈ʳ p)
    }

  module F = Functor Free

  -- | Freeness also induces a free-forgetful adjunction

  -- Embedding is a natural transformation
  embed-NT : NT idF (U ∘F Free)
  embed-NT = ntHelper record
    { η = λ C → embed
    ; commute = embed-commute
    }

  -- Extension of the identity on US is a natural transformation
  extract : (S : 𝕊.Obj) → F (U.₀ S) 𝕊.⇒ S
  extract S = extend ℂ.id

  -- Extraction is a natural transformation
  extract-NT : NT (Free ∘F U) idF
  extract-NT = ntHelper record
    { η = extract
    ; commute = λ {S}{T} f → [ extract T 𝕊.∘ F.₁ (U.₁ f) ≋ f 𝕊.∘ extract S ]!
        (begin
             U.₁ (extract T 𝕊.∘ F.₁ (U.₁ f)) ℂ.∘ embed
        ≈⟨ pushˡ U.homomorphism ⟩
             U.₁ (extract T) ℂ.∘ U.₁ (F.₁ (U.₁ f)) ℂ.∘ embed
        ≈⟨ refl⟩∘⟨ sym-commute embed-NT (U.₁ f) ⟩
             U.₁ (extract T) ℂ.∘ embed ℂ.∘ U.₁ f
        ≈⟨ pullˡ (factor ℂ.id) ○ ℂ.identityˡ ⟩
             U.₁ f
        ≈˘⟨ (refl⟩∘⟨ factor ℂ.id) ○ ℂ.identityʳ ⟩
             U.₁ f ℂ.∘ U.₁ (extract S) ℂ.∘ embed
        ≈˘⟨ pushˡ U.homomorphism ⟩
             U.₁ (f 𝕊.∘ extract S) ℂ.∘ embed
        ∎)
    }

  -- The free-forgetful adjunction arising from the universal morphisms
  Free⊣Forgetful : Free ⊣ U
  Free⊣Forgetful = record
    { unit = embed-NT
    ; counit = extract-NT
    ; zig = λ {C} → [ extract (F.₀ C) 𝕊.∘ F.₁ embed ≋ 𝕊.id ]!
        (begin
             U.₁ (extract (F.₀ C) 𝕊.∘ F.₁ embed) ℂ.∘ embed
         ≈⟨ pushˡ U.homomorphism ⟩
             U.₁ (extract (F.₀ C)) ℂ.∘ U.₁ (F.₁ embed) ℂ.∘ embed
         ≈⟨ refl⟩∘⟨ (sym-commute embed-NT embed) ⟩
             U.₁ (extract (F.₀ C)) ℂ.∘ (embed ℂ.∘ embed)
         ≈⟨ pullˡ (factor (ℂ.id)) ⟩
             ℂ.id ℂ.∘ embed
         ≈˘⟨ U.identity ⟩∘⟨refl ⟩
             U.₁ 𝕊.id ℂ.∘ embed
         ∎)
    ; zag = factor ℂ.id
    }

  FreeMonad : Monad ℂ
  FreeMonad = adjoint⇒monad Free⊣Forgetful

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
-- The following deeply left-nested expression illustrates both a
-- problem in a previous implementation of the occurrence machinery,
-- and a problem in the one that is current at the time of writing.

F : Set → Set
F X = (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((X → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X)) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X) → X


text:
------------------------------------------------------------------------
-- Function setoids and related constructions
------------------------------------------------------------------------

module Relation.Binary.FunctionSetoid where

open import Data.Function
open import Relation.Binary

infixr 0 _↝_ _⟶_ _⇨_ _≡⇨_

-- A logical relation (i.e. a relation which relates functions which
-- map related things to related things).

_↝_ : ∀ {A B} → (∼₁ : Rel A) (∼₂ : Rel B) → Rel (A → B)
_∼₁_ ↝ _∼₂_ = λ f g → ∀ {x y} → x ∼₁ y → f x ∼₂ g y

-- Functions which preserve equality.

record _⟶_ (From To : Setoid) : Set where
  open Setoid
  infixl 5 _⟨$⟩_
  field
    _⟨$⟩_ : carrier From → carrier To
    pres  : _⟨$⟩_ Preserves _≈_ From ⟶ _≈_ To

open _⟶_ public

↝-isEquivalence : ∀ {A B C} {∼₁ : Rel A} {∼₂ : Rel B}
                  (fun : C → (A → B)) →
                  (∀ f → fun f Preserves ∼₁ ⟶ ∼₂) →
                  IsEquivalence ∼₁ → IsEquivalence ∼₂ →
                  IsEquivalence ((∼₁ ↝ ∼₂) on₁ fun)
↝-isEquivalence _ pres eq₁ eq₂ = record
  { refl  = λ {f} x∼₁y → pres f x∼₁y
  ; sym   = λ f∼g x∼y → sym eq₂ (f∼g (sym eq₁ x∼y))
  ; trans = λ f∼g g∼h x∼y → trans eq₂ (f∼g (refl eq₁)) (g∼h x∼y)
  } where open IsEquivalence

-- Function setoids.

_⇨_ : Setoid → Setoid → Setoid
S₁ ⇨ S₂ = record
  { carrier       = S₁ ⟶ S₂
  ; _≈_           = (_≈_ S₁ ↝ _≈_ S₂) on₁ _⟨$⟩_
  ; isEquivalence =
      ↝-isEquivalence _⟨$⟩_ pres (isEquivalence S₁) (isEquivalence S₂)
  } where open Setoid; open _⟶_

-- A generalised variant of (_↝_ _≡_).

≡↝ : ∀ {A} {B : A → Set} → (∀ x → Rel (B x)) → Rel ((x : A) → B x)
≡↝ R = λ f g → ∀ x → R x (f x) (g x)

≡↝-isEquivalence : {A : Set} {B : A → Set} {R : ∀ x → Rel (B x)} →
                   (∀ x → IsEquivalence (R x)) → IsEquivalence (≡↝ R)
≡↝-isEquivalence eq = record
  { refl  = λ _ → refl
  ; sym   = λ f∼g x → sym (f∼g x)
  ; trans = λ f∼g g∼h x → trans (f∼g x) (g∼h x)
  } where open module Eq {x} = IsEquivalence (eq x)

_≡⇨_ : (A : Set) → (A → Setoid) → Setoid
A ≡⇨ S = record
  { carrier       = (x : A) → carrier (S x)
  ; _≈_           = ≡↝ (λ x → _≈_ (S x))
  ; isEquivalence = ≡↝-isEquivalence (λ x → isEquivalence (S x))
  } where open Setoid

max_issues_repo_name: larrytheliquid/Lemmachine


text:
------------------------------------------------------------------------
-- A binary representation of natural numbers
------------------------------------------------------------------------

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

open import Equality
import Erased.Without-box-cong

module Nat.Binary
  {c⁺}
  (eq : ∀ {a p} → Equality-with-J a p c⁺)

  -- An instantiation of the []-cong axioms.
  (ax : ∀ {a} → Erased.Without-box-cong.[]-cong-axiomatisation eq a)
  where

open Derived-definitions-and-properties eq

open import Dec
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (suc; _^_) renaming (_+_ to _⊕_; _*_ to _⊛_)

open import Bijection eq using (_↔_)
open import Equality.Decision-procedures eq
open import Erased eq ax
open import Function-universe eq hiding (id; _∘_)
open import List eq
open import Nat.Solver eq
import Nat.Wrapper eq as Wrapper
open import Surjection eq using (_↠_)

private

  module N where
    open import Nat eq public
    open Prelude public using (zero; suc; _^_)

  variable
    A     : Type
    inv n : A
    b     : Bool
    bs    : List Bool

------------------------------------------------------------------------
-- The underlying representation

private

  module Bin′ where

    abstract

      -- The underlying representation of binary natural numbers. The
      -- least significant digit comes first; true stands for one and
      -- false for zero. Leading zeros (at the end of the lists) are
      -- not allowed.
      --
      -- The type is abstract to ensure that a change to a different
      -- representation does not break code that uses this module.

      mutual

        infixr 5 _∷_

        data Bin′ : Type where
          []  : Bin′
          _∷_ : (b : Bool) (n : Bin′)
                { @0 invariant : Invariant b n } → Bin′

        private

          Invariant : Bool → Bin′ → Type
          Invariant true  _       = ⊤
          Invariant false (_ ∷ _) = ⊤
          Invariant false []      = ⊥

          -- A variant of _∷_ with three explicit arguments.

          pattern _∷_⟨_⟩ b n inv = _∷_ b n {invariant = inv}

          -- Synonyms that can be used in type signatures (Bin′ is
          -- abstract, so the constructors cannot be used there).

          []′ : Bin′
          []′ = []

          _∷_⟨_⟩′ : (b : Bool) (n : Bin′) → @0 Invariant b n → Bin′
          _∷_⟨_⟩′ = _∷_⟨_⟩

      private

        -- The underlying list.

        to-List : Bin′ → List Bool
        to-List []       = []
        to-List (b ∷ bs) = b ∷ to-List bs

        -- The invariant implies that the last element in the
        -- underlying list, if any, is not false, so there are no
        -- leading zeros in the number.

        invariant-correct : ∀ n bs → ¬ to-List n ≡ bs ++ false ∷ []
        invariant-correct [] bs =
          [] ≡ bs ++ false ∷ []  ↝⟨ []≢++∷ bs ⟩□
          ⊥                      □
        invariant-correct (true ∷ n) [] =
          true ∷ to-List n ≡ false ∷ []  ↝⟨ List.cancel-∷-head ⟩
          true ≡ false                   ↝⟨ Bool.true≢false ⟩□
          ⊥                              □
        invariant-correct (false ∷ n@(_ ∷ _)) [] =
          false ∷ to-List n ≡ false ∷ []  ↝⟨ List.cancel-∷-tail ⟩
          to-List n ≡ []                  ↝⟨ List.[]≢∷ ∘ sym ⟩□
          ⊥                               □
        invariant-correct (b ∷ n) (b′ ∷ bs) =
          b ∷ to-List n ≡ b′ ∷ bs ++ false ∷ []  ↝⟨ List.cancel-∷-tail ⟩
          to-List n ≡ bs ++ false ∷ []           ↝⟨ invariant-correct n bs ⟩□
          ⊥                                      □

        -- The invariant is propositional.

        Invariant-propositional :
          {b : Bool} {n : Bin′} → Is-proposition (Invariant b n)
        Invariant-propositional {b = true}              _ _ = refl _
        Invariant-propositional {b = false} {n = _ ∷ _} _ _ = refl _

        -- Converts from Bool to ℕ.

        from-Bool : Bool → ℕ
        from-Bool = if_then 1 else 0

        -- Converts from List Bool to ℕ.

        List-to-ℕ : List Bool → ℕ
        List-to-ℕ = foldr (λ b n → from-Bool b ⊕ 2 ⊛ n) 0

      -- Converts from Bin′ to ℕ.

      to-ℕ′ : Bin′ → ℕ
      to-ℕ′ = List-to-ℕ ∘ to-List

      private

        -- A smart constructor.

        infixr 5 _∷ˢ_

        _∷ˢ_ : Bool → Bin′ → Bin′
        true  ∷ˢ n         = true ∷ n
        false ∷ˢ []        = []
        false ∷ˢ n@(_ ∷ _) = false ∷ n

        -- A lemma relating to-ℕ′ and _∷ˢ_.

        to-ℕ′-∷ˢ : ∀ b n → to-ℕ′ (b ∷ˢ n) ≡ from-Bool b ⊕ 2 ⊛ to-ℕ′ n
        to-ℕ′-∷ˢ true  _       = refl _
        to-ℕ′-∷ˢ false []      = refl _
        to-ℕ′-∷ˢ false (_ ∷ _) = refl _

      -- Zero.

      zero′ : Bin′
      zero′ = []

      -- A lemma relating zero′ and N.zero.

      to-ℕ′-zero′ : to-ℕ′ zero′ ≡ N.zero
      to-ℕ′-zero′ = refl _

      -- The number's successor.

      suc′ : Bin′ → Bin′
      suc′ []          = true ∷ˢ []
      suc′ (false ∷ n) = true ∷ˢ n
      suc′ (true  ∷ n) = false ∷ˢ suc′ n

      private

        -- The successor of the smart cons constructor applied to
        -- false and n is the smart cons constructor applied to true
        -- and n.

        suc′-false-∷ˢ : ∀ n → suc′ (false ∷ˢ n) ≡ true ∷ˢ n
        suc′-false-∷ˢ []      = refl _
        suc′-false-∷ˢ (_ ∷ _) = refl _

      -- A lemma relating suc′ and N.suc.

      to-ℕ′-suc′ : ∀ bs → to-ℕ′ (suc′ bs) ≡ N.suc (to-ℕ′ bs)
      to-ℕ′-suc′ []             = refl _
      to-ℕ′-suc′ n@(false ∷ n′) =
        to-ℕ′ (suc′ n)      ≡⟨⟩
        to-ℕ′ (true ∷ˢ n′)  ≡⟨ to-ℕ′-∷ˢ true n′ ⟩
        1 ⊕ 2 ⊛ to-ℕ′ n′    ≡⟨⟩
        N.suc (to-ℕ′ n)     ∎
      to-ℕ′-suc′ n@(true ∷ n′) =
        to-ℕ′ (suc′ n)            ≡⟨⟩
        to-ℕ′ (false ∷ˢ suc′ n′)  ≡⟨ to-ℕ′-∷ˢ false (suc′ n′) ⟩
        2 ⊛ to-ℕ′ (suc′ n′)       ≡⟨ cong (2 ⊛_) (to-ℕ′-suc′ n′) ⟩
        2 ⊛ N.suc (to-ℕ′ n′)      ≡⟨ solve 1 (λ n → con 2 :* (con 1 :+ n) := con 2 :+ con 2 :* n) (refl _) _ ⟩
        2 ⊕ 2 ⊛ to-ℕ′ n′          ≡⟨⟩
        N.suc (to-ℕ′ n)           ∎

      private

        -- Converts from ℕ to Bin′.

        from-ℕ′ : ℕ → Bin′
        from-ℕ′ zero      = []
        from-ℕ′ (N.suc n) = suc′ (from-ℕ′ n)

        -- The function from-ℕ′ commutes with "multiplication by two".

        from-ℕ′-2-⊛ : ∀ n → from-ℕ′ (2 ⊛ n) ≡ false ∷ˢ from-ℕ′ n
        from-ℕ′-2-⊛ zero      = refl _
        from-ℕ′-2-⊛ (N.suc n) =
          from-ℕ′ (2 ⊛ N.suc n)               ≡⟨⟩
          suc′ (from-ℕ′ (n ⊕ N.suc (n ⊕ 0)))  ≡⟨ cong (suc′ ∘ from-ℕ′) $ sym $ N.suc+≡+suc n ⟩
          suc′ (from-ℕ′ (N.suc (2 ⊛ n)))      ≡⟨⟩
          suc′ (suc′ (from-ℕ′ (2 ⊛ n)))       ≡⟨ cong (suc′ ∘ suc′) (from-ℕ′-2-⊛ n) ⟩
          suc′ (suc′ (false ∷ˢ from-ℕ′ n))    ≡⟨ cong suc′ (suc′-false-∷ˢ (from-ℕ′ n)) ⟩
          suc′ (true ∷ˢ from-ℕ′ n)            ≡⟨⟩
          false ∷ˢ suc′ (from-ℕ′ n)           ≡⟨⟩
          false ∷ˢ from-ℕ′ (N.suc n)          ∎

    -- There is a bijection from Bin′ to ℕ.

    Bin′↔ℕ : Bin′ ↔ ℕ
    Bin′↔ℕ = record
      { surjection = record
        { logical-equivalence = record
          { to   = to-ℕ′
          ; from = from-ℕ′
          }
        ; right-inverse-of = to-ℕ′∘from-ℕ′
        }
      ; left-inverse-of = from-ℕ′∘to-ℕ′
      }
      where

      abstract

        to-ℕ′∘from-ℕ′ : ∀ n → to-ℕ′ (from-ℕ′ n) ≡ n
        to-ℕ′∘from-ℕ′ zero      = refl _
        to-ℕ′∘from-ℕ′ (N.suc n) =
          to-ℕ′ (from-ℕ′ (N.suc n))  ≡⟨⟩
          to-ℕ′ (suc′ (from-ℕ′ n))   ≡⟨ to-ℕ′-suc′ (from-ℕ′ n) ⟩
          N.suc (to-ℕ′ (from-ℕ′ n))  ≡⟨ cong N.suc (to-ℕ′∘from-ℕ′ n) ⟩∎
          N.suc n                    ∎

        from-ℕ′∘to-ℕ′ : ∀ n → from-ℕ′ (to-ℕ′ n) ≡ n
        from-ℕ′∘to-ℕ′ [] = refl _

        from-ℕ′∘to-ℕ′ n@(true ∷ n′) =
          from-ℕ′ (to-ℕ′ n)                   ≡⟨⟩
          from-ℕ′ (1 ⊕ 2 ⊛ to-ℕ′ n′)          ≡⟨⟩
          suc′ (from-ℕ′ (2 ⊛ to-ℕ′ n′))       ≡⟨ cong suc′ (from-ℕ′-2-⊛ (to-ℕ′ n′)) ⟩
          suc′ (false ∷ˢ from-ℕ′ (to-ℕ′ n′))  ≡⟨ cong (suc′ ∘ (false ∷ˢ_)) (from-ℕ′∘to-ℕ′ n′) ⟩
          suc′ (false ∷ˢ n′)                  ≡⟨ suc′-false-∷ˢ n′ ⟩
          true ∷ˢ n′                          ≡⟨⟩
          n                                   ∎

        from-ℕ′∘to-ℕ′ n@(false ∷ n′@(_ ∷ _)) =
          from-ℕ′ (to-ℕ′ n)            ≡⟨⟩
          from-ℕ′ (2 ⊛ to-ℕ′ n′)       ≡⟨ from-ℕ′-2-⊛ (to-ℕ′ n′) ⟩
          false ∷ˢ from-ℕ′ (to-ℕ′ n′)  ≡⟨ cong (false ∷ˢ_) (from-ℕ′∘to-ℕ′ n′) ⟩
          false ∷ˢ n′                  ≡⟨⟩
          n                            ∎

    abstract

      private

        -- Helper functions used to implement addition.

        add-with-carryᴮ : Bool → Bool → Bool → Bool × Bool
        add-with-carryᴮ false false false = false , false
        add-with-carryᴮ false false true  = true  , false
        add-with-carryᴮ false true  false = true  , false
        add-with-carryᴮ false true  true  = false , true
        add-with-carryᴮ true  false false = true  , false
        add-with-carryᴮ true  false true  = false , true
        add-with-carryᴮ true  true  false = false , true
        add-with-carryᴮ true  true  true  = true  , true

        add-with-carry₁ : Bool → Bin′ → Bin′
        add-with-carry₁ false = id
        add-with-carry₁ true  = suc′

        add-with-carry₂ : Bool → Bin′ → Bin′ → Bin′
        add-with-carry₂ b []        n  = add-with-carry₁ b n
        add-with-carry₂ b m@(_ ∷ _) [] = add-with-carry₁ b m

        add-with-carry₂ b (c ∷ m) (d ∷ n) =
          case add-with-carryᴮ b c d of λ where
            (e , f) → e ∷ˢ add-with-carry₂ f m n

        to-ℕ′-add-with-carry₁ :
          ∀ b cs →
          to-ℕ′ (add-with-carry₁ b cs) ≡
          from-Bool b ⊕ to-ℕ′ cs
        to-ℕ′-add-with-carry₁ false n = refl _
        to-ℕ′-add-with-carry₁ true  n = to-ℕ′-suc′ n

        to-ℕ′-add-with-carry₂ :
          ∀ b m n →
          to-ℕ′ (add-with-carry₂ b m n) ≡
          from-Bool b ⊕ (to-ℕ′ m ⊕ to-ℕ′ n)
        to-ℕ′-add-with-carry₂ b [] n = to-ℕ′-add-with-carry₁ b n

        to-ℕ′-add-with-carry₂ b m@(_ ∷ _) [] =
          to-ℕ′ (add-with-carry₁ b m)         ≡⟨ to-ℕ′-add-with-carry₁ b m ⟩
          from-Bool b ⊕ to-ℕ′ m               ≡⟨ solve 2 (λ b c → b :+ c := b :+ (c :+ con 0)) (refl _) (from-Bool b) _ ⟩
          from-Bool b ⊕ (to-ℕ′ m ⊕ 0)         ≡⟨⟩
          from-Bool b ⊕ (to-ℕ′ m ⊕ to-ℕ′ [])  ∎

        to-ℕ′-add-with-carry₂ false m@(false ∷ m′) n@(false ∷ n′) =
          to-ℕ′ (false ∷ˢ add-with-carry₂ false m′ n′)  ≡⟨ to-ℕ′-∷ˢ false (add-with-carry₂ false m′ n′) ⟩
          2 ⊛ to-ℕ′ (add-with-carry₂ false m′ n′)       ≡⟨ cong (2 ⊛_) (to-ℕ′-add-with-carry₂ false m′ n′) ⟩
          2 ⊛ (to-ℕ′ m′ ⊕ to-ℕ′ n′)                     ≡⟨ solve 2 (λ c d → con 2 :* (c :+ d) :=
                                                                            con 2 :* c :+ con 2 :* d)
                                                                 (refl _) (to-ℕ′ m′) _ ⟩
          2 ⊛ to-ℕ′ m′ ⊕ 2 ⊛ to-ℕ′ n′                   ≡⟨⟩
          to-ℕ′ m ⊕ to-ℕ′ n       ∎

        to-ℕ′-add-with-carry₂ false m@(false ∷ m′) n@(true  ∷ n′) =
          to-ℕ′ (true ∷ˢ add-with-carry₂ false m′ n′)  ≡⟨ to-ℕ′-∷ˢ true (add-with-carry₂ false m′ n′) ⟩
          1 ⊕ 2 ⊛ to-ℕ′ (add-with-carry₂ false m′ n′)  ≡⟨ cong ((1 ⊕_) ∘ (2 ⊛_)) (to-ℕ′-add-with-carry₂ false m′ n′) ⟩
          1 ⊕ 2 ⊛ (to-ℕ′ m′ ⊕ to-ℕ′ n′)                ≡⟨ solve 2 (λ c d → con 1 :+ con 2 :* (c :+ d) :=
                                                                           con 2 :* c :+ (con 1 :+ con 2 :* d))
                                                                (refl _) (to-ℕ′ m′) _ ⟩
          2 ⊛ to-ℕ′ m′ ⊕ (1 ⊕ 2 ⊛ to-ℕ′ n′)            ≡⟨⟩
          to-ℕ′ m ⊕ to-ℕ′ n       ∎

        to-ℕ′-add-with-carry₂ false m@(true  ∷ m′) n@(false ∷ n′) =
          to-ℕ′ (true ∷ˢ add-with-carry₂ false m′ n′)  ≡⟨ to-ℕ′-∷ˢ true (add-with-carry₂ false m′ n′) ⟩
          1 ⊕ 2 ⊛ to-ℕ′ (add-with-carry₂ false m′ n′)  ≡⟨ cong ((1 ⊕_) ∘ (2 ⊛_)) (to-ℕ′-add-with-carry₂ false m′ n′) ⟩
          1 ⊕ 2 ⊛ (to-ℕ′ m′ ⊕ to-ℕ′ n′)                ≡⟨ solve 2 (λ c d → con 1 :+ con 2 :* (c :+ d) :=
                                                                           con 1 :+ con 2 :* c :+ con 2 :* d)
                                                                (refl _) (to-ℕ′ m′) _ ⟩
          1 ⊕ 2 ⊛ to-ℕ′ m′ ⊕ 2 ⊛ to-ℕ′ n′              ≡⟨⟩
          to-ℕ′ m ⊕ to-ℕ′ n                            ∎

        to-ℕ′-add-with-carry₂ false m@(true ∷ m′) n@(true ∷ n′) =
          to-ℕ′ (false ∷ˢ add-with-carry₂ true m′ n′)  ≡⟨ to-ℕ′-∷ˢ false (add-with-carry₂ true m′ n′) ⟩
          2 ⊛ to-ℕ′ (add-with-carry₂ true m′ n′)       ≡⟨ cong (2 ⊛_) (to-ℕ′-add-with-carry₂ true m′ n′) ⟩
          2 ⊛ (1 ⊕ to-ℕ′ m′ ⊕ to-ℕ′ n′)                ≡⟨ solve 2 (λ c d → con 2 :* (con 1 :+ c :+ d) :=
                                                                           con 1 :+ con 2 :* c :+ (con 1 :+ con 2 :* d))
                                                                (refl _) (to-ℕ′ m′) _ ⟩
          1 ⊕ 2 ⊛ to-ℕ′ m′ ⊕ (1 ⊕ 2 ⊛ to-ℕ′ n′)        ≡⟨⟩
          to-ℕ′ m ⊕ to-ℕ′ n                            ∎

        to-ℕ′-add-with-carry₂ true m@(false ∷ m′) n@(false ∷ n′) =
          to-ℕ′ (true ∷ˢ add-with-carry₂ false m′ n′)  ≡⟨ to-ℕ′-∷ˢ true (add-with-carry₂ false m′ n′) ⟩
          1 ⊕ 2 ⊛ to-ℕ′ (add-with-carry₂ false m′ n′)  ≡⟨ cong ((1 ⊕_) ∘ (2 ⊛_)) (to-ℕ′-add-with-carry₂ false m′ n′) ⟩
          1 ⊕ 2 ⊛ (to-ℕ′ m′ ⊕ to-ℕ′ n′)                ≡⟨ solve 2 (λ c d → con 1 :+ con 2 :* (c :+ d) :=
                                                                           con 1 :+ con 2 :* c :+ con 2 :* d)
                                                                (refl _) (to-ℕ′ m′) _ ⟩
          1 ⊕ 2 ⊛ to-ℕ′ m′ ⊕ 2 ⊛ to-ℕ′ n′              ≡⟨⟩
          1 ⊕ to-ℕ′ m ⊕ to-ℕ′ n                        ∎

        to-ℕ′-add-with-carry₂ true m@(false ∷ m′) n@(true  ∷ n′) =
          to-ℕ′ (false ∷ˢ add-with-carry₂ true m′ n′)  ≡⟨ to-ℕ′-∷ˢ false (add-with-carry₂ true m′ n′) ⟩
          2 ⊛ to-ℕ′ (add-with-carry₂ true m′ n′)       ≡⟨ cong (2 ⊛_) (to-ℕ′-add-with-carry₂ true m′ n′) ⟩
          2 ⊛ (1 ⊕ to-ℕ′ m′ ⊕ to-ℕ′ n′)                ≡⟨ solve 2 (λ c d → con 2 :* (con 1 :+ c :+ d) :=
                                                                           con 1 :+ con 2 :* c :+ (con 1 :+ con 2 :* d))
                                                                (refl _) (to-ℕ′ m′) _ ⟩
          1 ⊕ 2 ⊛ to-ℕ′ m′ ⊕ (1 ⊕ 2 ⊛ to-ℕ′ n′)        ≡⟨⟩
          1 ⊕ to-ℕ′ m ⊕ to-ℕ′ n                        ∎

        to-ℕ′-add-with-carry₂ true m@(true  ∷ m′) n@(false ∷ n′) =
          to-ℕ′ (false ∷ˢ add-with-carry₂ true m′ n′)  ≡⟨ to-ℕ′-∷ˢ false (add-with-carry₂ true m′ n′) ⟩
          2 ⊛ to-ℕ′ (add-with-carry₂ true m′ n′)       ≡⟨ cong (2 ⊛_) (to-ℕ′-add-with-carry₂ true m′ n′) ⟩
          2 ⊛ (1 ⊕ to-ℕ′ m′ ⊕ to-ℕ′ n′)                ≡⟨ solve 2 (λ c d → con 2 :* (con 1 :+ c :+ d) :=
                                                                           con 2 :+ con 2 :* c :+ con 2 :* d)
                                                                (refl _) (to-ℕ′ m′) _ ⟩
          2 ⊕ 2 ⊛ to-ℕ′ m′ ⊕ 2 ⊛ to-ℕ′ n′              ≡⟨⟩
          1 ⊕ to-ℕ′ m ⊕ to-ℕ′ n                        ∎

        to-ℕ′-add-with-carry₂ true m@(true ∷ m′) n@(true ∷ n′) =
          to-ℕ′ (true ∷ˢ add-with-carry₂ true m′ n′)  ≡⟨ to-ℕ′-∷ˢ true (add-with-carry₂ true m′ n′) ⟩
          1 ⊕ 2 ⊛ to-ℕ′ (add-with-carry₂ true m′ n′)  ≡⟨ cong ((1 ⊕_) ∘ (2 ⊛_)) (to-ℕ′-add-with-carry₂ true m′ n′) ⟩
          1 ⊕ 2 ⊛ (1 ⊕ to-ℕ′ m′ ⊕ to-ℕ′ n′)           ≡⟨ solve 2 (λ c d → con 1 :+ con 2 :* (con 1 :+ c :+ d) :=
                                                                          con 2 :+ con 2 :* c :+ (con 1 :+ con 2 :* d))
                                                               (refl _) (to-ℕ′ m′) _ ⟩
          2 ⊕ 2 ⊛ to-ℕ′ m′ ⊕ (1 ⊕ 2 ⊛ to-ℕ′ n′)       ≡⟨⟩
          1 ⊕ to-ℕ′ m ⊕ to-ℕ′ n                       ∎

      -- Addition.

      add-with-carry : Bin′ → Bin′ → Bin′
      add-with-carry = add-with-carry₂ false

      to-ℕ′-add-with-carry :
        ∀ m n →
        to-ℕ′ (add-with-carry m n) ≡
        to-ℕ′ m ⊕ to-ℕ′ n
      to-ℕ′-add-with-carry = to-ℕ′-add-with-carry₂ false

      -- Division by two, rounded downwards.

      ⌊_/2⌋ : Bin′ → Bin′
      ⌊ []    /2⌋ = []
      ⌊ _ ∷ n /2⌋ = n

      to-ℕ′-⌊/2⌋ : ∀ n → to-ℕ′ ⌊ n /2⌋ ≡ N.⌊ to-ℕ′ n /2⌋
      to-ℕ′-⌊/2⌋ []          = refl _
      to-ℕ′-⌊/2⌋ (false ∷ n) =
        to-ℕ′ n              ≡⟨ sym $ N.⌊2*/2⌋≡ _ ⟩∎
        N.⌊ 2 ⊛ to-ℕ′ n /2⌋  ∎

      to-ℕ′-⌊/2⌋ (true ∷ n) =
        to-ℕ′ n                  ≡⟨ sym $ N.⌊1+2*/2⌋≡ _ ⟩∎
        N.⌊ 1 ⊕ 2 ⊛ to-ℕ′ n /2⌋  ∎

      -- Division by two, rounded upwards.

      ⌈_/2⌉ : Bin′ → Bin′
      ⌈ []        /2⌉ = []
      ⌈ false ∷ n /2⌉ = n
      ⌈ true  ∷ n /2⌉ = suc′ n

      to-ℕ′-⌈/2⌉ : ∀ n → to-ℕ′ ⌈ n /2⌉ ≡ N.⌈ to-ℕ′ n /2⌉
      to-ℕ′-⌈/2⌉ []          = refl _
      to-ℕ′-⌈/2⌉ (false ∷ n) =
        to-ℕ′ n              ≡⟨ sym $ N.⌈2*/2⌉≡ _ ⟩∎
        N.⌈ 2 ⊛ to-ℕ′ n /2⌉  ∎

      to-ℕ′-⌈/2⌉ (true ∷ n) =
        to-ℕ′ (suc′ n)           ≡⟨ to-ℕ′-suc′ n ⟩
        1 ⊕ to-ℕ′ n              ≡⟨ sym $ N.⌈1+2*/2⌉≡ _ ⟩∎
        N.⌈ 1 ⊕ 2 ⊛ to-ℕ′ n /2⌉  ∎

      -- Multiplication.

      infixl 7 _*_

      _*_ : Bin′ → Bin′ → Bin′
      []      * n = zero′
      (b ∷ m) * n =
        (if b then add-with-carry n else id)
          (false ∷ˢ m * n)

      to-ℕ′-* : ∀ m n → to-ℕ′ (m * n) ≡ to-ℕ′ m ⊛ to-ℕ′ n
      to-ℕ′-* []                  n = refl _
      to-ℕ′-* (false ∷ m ⟨ inv ⟩) n =
        to-ℕ′ (false ∷ˢ m * n)               ≡⟨ to-ℕ′-∷ˢ false (m * n) ⟩
        2 ⊛ to-ℕ′ (m * n)                    ≡⟨ cong (2 ⊛_) (to-ℕ′-* m _) ⟩
        2 ⊛ (to-ℕ′ m ⊛ to-ℕ′ n)              ≡⟨ N.*-assoc 2 {n = to-ℕ′ m} ⟩
        (2 ⊛ to-ℕ′ m) ⊛ to-ℕ′ n              ≡⟨⟩
        to-ℕ′ (false ∷ m ⟨ inv ⟩) ⊛ to-ℕ′ n  ∎
      to-ℕ′-* (true ∷ m) n =
        to-ℕ′ (add-with-carry n (false ∷ˢ m * n))  ≡⟨ to-ℕ′-add-with-carry n _ ⟩
        to-ℕ′ n ⊕ to-ℕ′ (false ∷ˢ m * n)           ≡⟨ cong (to-ℕ′ n ⊕_) (to-ℕ′-∷ˢ false (m * n)) ⟩
        to-ℕ′ n ⊕ 2 ⊛ to-ℕ′ (m * n)                ≡⟨ cong (λ x → to-ℕ′ n ⊕ 2 ⊛ x) (to-ℕ′-* m _) ⟩
        to-ℕ′ n ⊕ 2 ⊛ (to-ℕ′ m ⊛ to-ℕ′ n)          ≡⟨ solve 2 (λ m n → n :+ con 2 :* (m :* n) :=
                                                                       (con 1 :+ con 2 :* m) :* n)
                                                            (refl _) (to-ℕ′ m) _ ⟩
        (1 ⊕ 2 ⊛ to-ℕ′ m) ⊛ to-ℕ′ n                ≡⟨⟩
        to-ℕ′ (true ∷ m) ⊛ to-ℕ′ n                 ∎

      -- Exponentiation.

      infixr 8 _^_

      _^_ : Bin′ → Bin′ → Bin′
      m ^ []      = suc′ zero′
      m ^ (b ∷ n) =
        (if b then (m *_) else id)
          ((m * m) ^ n)

      to-ℕ′-^ : ∀ m n → to-ℕ′ (m ^ n) ≡ to-ℕ′ m N.^ to-ℕ′ n
      to-ℕ′-^ m []                  = refl _
      to-ℕ′-^ m (false ∷ n ⟨ inv ⟩) =
        to-ℕ′ (m ^ (false ∷ n ⟨ inv ⟩))        ≡⟨⟩
        to-ℕ′ ((m * m) ^ n)                    ≡⟨ to-ℕ′-^ (m * m) n ⟩
        to-ℕ′ (m * m) N.^ to-ℕ′ n              ≡⟨ cong (N._^ to-ℕ′ n) (to-ℕ′-* m m) ⟩
        (to-ℕ′ m ⊛ to-ℕ′ m) N.^ to-ℕ′ n        ≡⟨ cong (λ x → (to-ℕ′ m ⊛ x) N.^ to-ℕ′ n) (sym (N.*-right-identity (to-ℕ′ m))) ⟩
        (to-ℕ′ m N.^ 2) N.^ to-ℕ′ n            ≡⟨ N.^^≡^* 2 {k = to-ℕ′ n} ⟩
        to-ℕ′ m N.^ (2 ⊛ to-ℕ′ n)              ≡⟨⟩
        to-ℕ′ m N.^ to-ℕ′ (false ∷ n ⟨ inv ⟩)  ∎
      to-ℕ′-^ m (true ∷ n) =
        to-ℕ′ (m ^ (true ∷ n))                     ≡⟨⟩
        to-ℕ′ (m * (m * m) ^ n)                    ≡⟨ to-ℕ′-* m ((m * m) ^ n) ⟩
        to-ℕ′ m ⊛ to-ℕ′ ((m * m) ^ n)              ≡⟨ cong (to-ℕ′ m ⊛_) (to-ℕ′-^ (m * m) n) ⟩
        to-ℕ′ m ⊛ to-ℕ′ (m * m) N.^ to-ℕ′ n        ≡⟨ cong (λ x → to-ℕ′ m ⊛ x N.^ to-ℕ′ n) (to-ℕ′-* m m) ⟩
        to-ℕ′ m ⊛ (to-ℕ′ m ⊛ to-ℕ′ m) N.^ to-ℕ′ n  ≡⟨ cong (λ x → to-ℕ′ m ⊛ (to-ℕ′ m ⊛ x) N.^ to-ℕ′ n) (sym (N.*-right-identity (to-ℕ′ m))) ⟩
        to-ℕ′ m ⊛ (to-ℕ′ m N.^ 2) N.^ to-ℕ′ n      ≡⟨ cong₂ _⊛_ (sym (N.^-right-identity {n = to-ℕ′ m})) (N.^^≡^* 2 {k = to-ℕ′ n}) ⟩
        to-ℕ′ m N.^ 1 ⊛ to-ℕ′ m N.^ (2 ⊛ to-ℕ′ n)  ≡⟨ sym $ N.^+≡^*^ {m = to-ℕ′ m} 1 {k = 2 ⊛ to-ℕ′ n} ⟩
        to-ℕ′ m N.^ (1 ⊕ 2 ⊛ to-ℕ′ n)              ≡⟨⟩
        to-ℕ′ m N.^ to-ℕ′ (true ∷ n)               ∎

      -- "Left shift".

      infixl 8 _*2^_

      _*2^_ : Bin′ → ℕ → Bin′
      m *2^ zero    = m
      m *2^ N.suc n = (false ∷ˢ m) *2^ n

      to-ℕ′-*2^ :
        ∀ m n →
        to-ℕ′ (m *2^ n) ≡
        to-ℕ′ m ⊛ 2 N.^ n
      to-ℕ′-*2^ m zero =
        to-ℕ′ m      ≡⟨ sym $ N.*-right-identity _ ⟩∎
        to-ℕ′ m ⊛ 1  ∎
      to-ℕ′-*2^ m (N.suc n) =
        to-ℕ′ ((false ∷ˢ m) *2^ n)    ≡⟨ to-ℕ′-*2^ (false ∷ˢ m) n ⟩
        to-ℕ′ (false ∷ˢ m) ⊛ 2 N.^ n  ≡⟨ cong (_⊛ _) $ to-ℕ′-∷ˢ false m ⟩
        2 ⊛ to-ℕ′ m ⊛ 2 N.^ n         ≡⟨ cong (_⊛ (2 N.^ n)) $ N.*-comm 2 {n = to-ℕ′ m} ⟩
        to-ℕ′ m ⊛ 2 ⊛ 2 N.^ n         ≡⟨ sym $ N.*-assoc (to-ℕ′ m) ⟩∎
        to-ℕ′ m ⊛ 2 N.^ N.suc n       ∎

      private

        -- The empty list is not equal to any non-empty list.

        []≢∷ : []′ ≢ b ∷ n ⟨ inv ⟩′
        []≢∷ {b = b} {n = n} =
          [] ≡ b ∷ n          ↝⟨ cong to-List ⟩
          [] ≡ b ∷ to-List n  ↝⟨ List.[]≢∷ ⟩□
          ⊥                   □

        -- Equality is decidable for Bin′.
        --
        -- This definition uses Dec-Erased instead of Dec ∘ Erased
        -- because I thought this made the code a little less
        -- complicated.

        equal? : (m n : Bin′) → Dec-Erased (m ≡ n)
        equal? [] [] = yes [ refl _ ]

        equal? [] (b ∷ n) = no [ []≢∷ ]

        equal? (b ∷ n) [] = no [ []≢∷ ∘ sym ]

        equal? (b₁ ∷ n₁) (b₂ ∷ n₂) =
          helper₁ _ _ (b₁ Bool.≟ b₂)
          where
          helper₂ :
            ∀ n₁ n₂
            (@0 inv₁ : Invariant b₁ n₁) (@0 inv₂ : Invariant b₂ n₂) →
            b₁ ≡ b₂ →
            Dec-Erased (n₁ ≡ n₂) →
            Dec-Erased ((b₁ ∷ n₁ ⟨ inv₁ ⟩′) ≡ (b₂ ∷ n₂ ⟨ inv₂ ⟩′))
          helper₂ n₁ n₂ _ _ _ (no [ n₁≢n₂ ]) = no [
            (b₁ ∷ n₁ ⟨ _ ⟩) ≡ (b₂ ∷ n₂ ⟨ _ ⟩)  ↝⟨ cong to-List ⟩
            b₁ ∷ to-List n₁ ≡ b₂ ∷ to-List n₂  ↝⟨ List.cancel-∷-tail ⟩
            to-List n₁ ≡ to-List n₂            ↝⟨ cong List-to-ℕ ⟩
            to-ℕ′ n₁ ≡ to-ℕ′ n₂                ↝⟨ _↔_.injective Bin′↔ℕ ⟩
            n₁ ≡ n₂                            ↝⟨ n₁≢n₂ ⟩□
            ⊥                                  □ ]

          helper₂ n₁ n₂ inv₁ inv₂ b₁≡b₂ (yes [ n₁≡n₂ ]) = yes [  $⟨ b₁≡b₂ , n₁≡n₂ ⟩
            b₁ ≡ b₂ × n₁ ≡ n₂                                    ↝⟨ Σ-map id (cong to-List) ⟩
            b₁ ≡ b₂ × to-List n₁ ≡ to-List n₂                    ↔⟨ inverse ∷≡∷↔≡×≡ ⟩
            b₁ ∷ to-List n₁ ≡ b₂ ∷ to-List n₂                    ↝⟨ cong List-to-ℕ ⟩
            to-ℕ′ (b₁ ∷ n₁ ⟨ inv₁ ⟩) ≡ to-ℕ′ (b₂ ∷ n₂ ⟨ inv₂ ⟩)  ↝⟨ _↔_.injective Bin′↔ℕ ⟩□
            b₁ ∷ n₁ ≡ b₂ ∷ n₂                                    □ ]

          helper₁ :
            ∀ n₁ n₂
              {@0 inv₁ : Invariant b₁ n₁} {@0 inv₂ : Invariant b₂ n₂} →
            Dec (b₁ ≡ b₂) →
            Dec-Erased ((b₁ ∷ n₁ ⟨ inv₁ ⟩′) ≡ (b₂ ∷ n₂ ⟨ inv₂ ⟩′))
          helper₁ n₁ n₂ (yes b₁≡b₂) =
            helper₂ _ _ _ _ b₁≡b₂ (equal? n₁ n₂)

          helper₁ n₁ n₂ (no b₁≢b₂) = no [
            b₁ ∷ n₁ ≡ b₂ ∷ n₂                  ↝⟨ cong to-List ⟩
            b₁ ∷ to-List n₁ ≡ b₂ ∷ to-List n₂  ↝⟨ List.cancel-∷-head ⟩
            b₁ ≡ b₂                            ↝⟨ b₁≢b₂ ⟩□
            ⊥                                  □ ]

      -- An equality test.

      infix 4 _≟_

      _≟_ : (m n : Bin′) → Dec (Erased (to-ℕ′ m ≡ to-ℕ′ n))
      m ≟ n =                             $⟨ equal? m n ⟩
        Dec-Erased (m ≡ n)                ↝⟨ Dec-Erased-map lemma ⟩
        Dec-Erased (to-ℕ′ m ≡ to-ℕ′ n)    ↝⟨ Dec-Erased↔Dec-Erased _ ⟩□
        Dec (Erased (to-ℕ′ m ≡ to-ℕ′ n))  □
        where
        lemma : m ≡ n ⇔ to-ℕ′ m ≡ to-ℕ′ n
        lemma = record { to = cong to-ℕ′; from = _↔_.injective Bin′↔ℕ }

      private

        -- A lemma used to prove that from-bits and to-bits are
        -- correct.

        to-ℕ′-foldr-∷ˢ-[] :
          ∀ bs →
          to-ℕ′ (foldr _∷ˢ_ []′ bs) ≡
          foldr (λ b n → from-Bool b ⊕ 2 ⊛ n) 0 bs
        to-ℕ′-foldr-∷ˢ-[] []       = refl _
        to-ℕ′-foldr-∷ˢ-[] (b ∷ bs) =
          to-ℕ′ (foldr _∷ˢ_ [] (b ∷ bs))                              ≡⟨⟩
          to-ℕ′ (b ∷ˢ foldr _∷ˢ_ [] bs)                               ≡⟨ to-ℕ′-∷ˢ b _ ⟩
          from-Bool b ⊕ 2 ⊛ to-ℕ′ (foldr _∷ˢ_ [] bs)                  ≡⟨ cong (λ n → from-Bool b ⊕ 2 ⊛ n) (to-ℕ′-foldr-∷ˢ-[] bs) ⟩
          from-Bool b ⊕ 2 ⊛ foldr (λ b n → from-Bool b ⊕ 2 ⊛ n) 0 bs  ≡⟨⟩
          foldr (λ b n → from-Bool b ⊕ 2 ⊛ n) 0 (b ∷ bs)              ∎

      -- Converts from lists of bits. (The most significant bit comes
      -- first.)

      from-bits : List Bool → Bin′
      from-bits = foldr _∷ˢ_ [] ∘ reverse

      to-ℕ′-from-bits :
        ∀ bs →
        to-ℕ′ (from-bits bs) ≡
        foldl (λ n b → (if b then 1 else 0) ⊕ 2 ⊛ n) 0 bs
      to-ℕ′-from-bits bs =
        to-ℕ′ (from-bits bs)                                ≡⟨⟩
        to-ℕ′ (foldr _∷ˢ_ [] (reverse bs))                  ≡⟨ to-ℕ′-foldr-∷ˢ-[] (reverse bs) ⟩
        foldr (λ b n → from-Bool b ⊕ 2 ⊛ n) 0 (reverse bs)  ≡⟨ foldr-reverse bs ⟩∎
        foldl (λ n b → from-Bool b ⊕ 2 ⊛ n) 0 bs            ∎

      -- Converts to lists of bits. (The most significant bit comes
      -- first.)

      to-bits : Bin′ → List Bool
      to-bits = reverse ∘ to-List

      to-ℕ′-from-bits-to-bits :
        ∀ n → to-ℕ′ (from-bits (to-bits n)) ≡ to-ℕ′ n
      to-ℕ′-from-bits-to-bits n =
        to-ℕ′ (foldr _∷ˢ_ [] (reverse (reverse (to-List n))))  ≡⟨ cong (to-ℕ′ ∘ foldr _∷ˢ_ []) (reverse-reverse (to-List n)) ⟩
        to-ℕ′ (foldr _∷ˢ_ [] (to-List n))                      ≡⟨ to-ℕ′-foldr-∷ˢ-[] (to-List n) ⟩
        foldr (λ b n → from-Bool b ⊕ 2 ⊛ n) 0 (to-List n)      ≡⟨⟩
        to-ℕ′ n                                                ∎

------------------------------------------------------------------------
-- Binary natural numbers

private

  module Bin-wrapper = Wrapper Bin′.Bin′ Bin′.Bin′↔ℕ
  open Bin-wrapper using (Operations)

-- Some definitions from Nat.Wrapper are reexported.

open Bin-wrapper public
  using (⌊_⌋; ⌈_⌉; ≡⌊⌋;
         nullary-[]; nullary; nullary-correct;
         unary-[]; unary; unary-correct;
         binary-[]; binary; binary-correct;
         n-ary-[]; n-ary; n-ary-correct)
  renaming
    ( Nat-[_] to Bin-[_]
    ; Nat to Bin
    ; Nat-[]↔Σℕ to Bin-[]↔Σℕ
    )

open Bin-wrapper.[]-cong ax public
  using (≡-for-indices↔≡)
  renaming
    ( Nat-[]-propositional to Bin-[]-propositional
    ; Nat↔ℕ to Bin↔ℕ
    )

private

  -- An implementation of some operations for Bin′.

  Operations-for-Bin′ : Operations
  Operations-for-Bin′ = λ where
    .Operations.zero                   → Bin′.zero′
    .Operations.to-ℕ-zero              → Bin′.to-ℕ′-zero′
    .Operations.suc                    → Bin′.suc′
    .Operations.to-ℕ-suc               → Bin′.to-ℕ′-suc′
    .Operations._+_                    → Bin′.add-with-carry
    .Operations.to-ℕ-+                 → Bin′.to-ℕ′-add-with-carry
    .Operations._*_                    → Bin′._*_
    .Operations.to-ℕ-*                 → Bin′.to-ℕ′-*
    .Operations._^_                    → Bin′._^_
    .Operations.to-ℕ-^                 → Bin′.to-ℕ′-^
    .Operations.⌊_/2⌋                  → Bin′.⌊_/2⌋
    .Operations.to-ℕ-⌊/2⌋              → Bin′.to-ℕ′-⌊/2⌋
    .Operations.⌈_/2⌉                  → Bin′.⌈_/2⌉
    .Operations.to-ℕ-⌈/2⌉              → Bin′.to-ℕ′-⌈/2⌉
    .Operations._*2^_                  → Bin′._*2^_
    .Operations.to-ℕ-*2^               → Bin′.to-ℕ′-*2^
    .Operations._≟_                    → Bin′._≟_
    .Operations.from-bits              → Bin′.from-bits
    .Operations.to-ℕ-from-bits         → Bin′.to-ℕ′-from-bits
    .Operations.to-bits                → Bin′.to-bits
    .Operations.to-ℕ-from-bits-to-bits → Bin′.to-ℕ′-from-bits-to-bits

-- Operations for Bin-[_].

module Operations-for-Bin-[] =
  Bin-wrapper.Operations-for-Nat-[] Operations-for-Bin′

-- Operations for Bin.

module Operations-for-Bin =
  Bin-wrapper.Operations-for-Nat Operations-for-Bin′

------------------------------------------------------------------------
-- Some examples

private

  module Bin-[]-examples where

    open Operations-for-Bin-[]

    -- Converts unary natural numbers to binary natural numbers.

    from-ℕ : ∀ n → Bin-[ n ]
    from-ℕ = proj₂ ∘ _↔_.from Bin↔ℕ

    -- Bin n is a proposition, so it is easy to prove that two values
    -- of this type are equal.

    example₁ : from-ℕ 4 + ⌊ from-ℕ 12 /2⌋ ≡ from-ℕ 10
    example₁ = Bin-[]-propositional _ _

    -- However, stating that two values of type Bin m and Bin n are
    -- equal, for equal natural numbers m and n, can be awkward.

    @0 example₂ :
      {@0 m n : ℕ}
      (b : Bin-[ m ]) (c : Bin-[ n ]) →
      subst (λ n → Bin-[ n ]) (N.+-comm m) (b + c) ≡ c + b
    example₂ _ _ = Bin-[]-propositional _ _

  module Bin-examples where

    open Operations-for-Bin

    -- If Bin is used instead of Bin-[_], then it can be easier to
    -- state that two values are equal.

    example₁ : ⌈ 4 ⌉ + ⌊ ⌈ 12 ⌉ /2⌋ ≡ ⌈ 10 ⌉
    example₁ = _↔_.to ≡-for-indices↔≡ [ refl _ ]

    example₂ : ∀ m n → m + n ≡ n + m
    example₂ m n = _↔_.to ≡-for-indices↔≡
      [ ⌊ m ⌋ ⊕ ⌊ n ⌋  ≡⟨ N.+-comm ⌊ m ⌋ ⟩∎
        ⌊ n ⌋ ⊕ ⌊ m ⌋  ∎
      ]

    -- One can construct a proof showing that ⌈ 5 ⌉ is either equal or
    -- not equal to ⌈ 2 ⌉ + ⌈ 3 ⌉, but the proof does not compute to
    -- "inj₁ something" at compile-time.

    example₃ : Dec (⌈ 5 ⌉ ≡ ⌈ 2 ⌉ + ⌈ 3 ⌉)
    example₃ =
      Dec-map (_↔_.logical-equivalence ≡-for-indices↔≡)
        (⌈ 5 ⌉ ≟ ⌈ 2 ⌉ + ⌈ 3 ⌉)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality