text:
------------------------------------------------------------------------
-- Lemmas related to application of substitutions
------------------------------------------------------------------------

-- The record below allows the application operation to be
-- "heterogeneous", applying substitutions containing one kind of term
-- to another kind of term. TODO: This results in some extra
-- complication—is it worth it?

open import Data.Universe.Indexed

module deBruijn.Substitution.Data.Application.Application21
  {i u e} {Uni : IndexedUniverse i u e} where

import deBruijn.Context; open deBruijn.Context Uni
open import deBruijn.Substitution.Data.Application.Application
open import deBruijn.Substitution.Data.Basics
open import deBruijn.Substitution.Data.Map
open import deBruijn.Substitution.Data.Simple
open import Function using (_$_)
open import Level using (_⊔_)
import Relation.Binary.PropositionalEquality as P

open P.≡-Reasoning

-- Lemmas and definitions related to application.

record Application₂₁
  {t₁} {T₁ : Term-like t₁}
  {t₂} {T₂ : Term-like t₂}

  -- Simple substitutions for the first kind of terms.
  (simple₁ : Simple T₁)

  -- Simple substitutions for the second kind of terms.
  (simple₂ : Simple T₂)

  -- A translation from the first to the second kind of terms.
  (trans : [ T₁ ⟶⁼ T₂ ])
  : Set (i ⊔ u ⊔ e ⊔ t₁ ⊔ t₂) where

  open Term-like T₁ using () renaming (_⊢_ to _⊢₁_; _≅-⊢_ to _≅-⊢₁_)
  open Term-like T₂ using ([_]) renaming (_⊢_ to _⊢₂_; _≅-⊢_ to _≅-⊢₂_)
  open Simple simple₁
    using ()
    renaming ( id to id₁; sub to sub₁; var to var₁
             ; weaken[_] to weaken₁[_]; wk to wk₁
             ; wk-subst to wk-subst₁; wk-subst[_] to wk-subst₁[_]
             ; _↑ to _↑₁; _↑_ to _↑₁_; _↑⁺_ to _↑⁺₁_; _↑₊_ to _↑₊₁_
             ; _↑⋆_ to _↑⋆₁_; _↑⁺⋆_ to _↑⁺⋆₁_; _↑₊⋆_ to _↑₊⋆₁_
             )
  open Simple simple₂
    using ()
    renaming ( id to id₂; id[_] to id₂[_]; var to var₂
             ; weaken to weaken₂; weaken[_] to weaken₂[_]; wk to wk₂
             ; wk-subst to wk-subst₂; wk-subst[_] to wk-subst₂[_]
             ; _↑ to _↑₂; _↑_ to _↑₂_
             )

  field
    application : Application T₁ T₂

  open Application application

  field
    -- The two weakening functions coincide.
    trans-weaken : ∀ {Γ σ τ} (t : Γ ⊢₁ τ) →
                   trans · (weaken₁[ σ ] · t) ≅-⊢₂
                   weaken₂[ σ ] · (trans · t)

    -- The two variable inclusion functions coincide.
    trans-var : ∀ {Γ σ} (x : Γ ∋ σ) → trans · (var₁ · x) ≅-⊢₂ var₂ · x

    -- _/⊢_ and _/∋₁_ coincide for variables.
    var-/⊢ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ ∋ σ) (ρ : Sub T₁ ρ̂) →
             var₂ · x /⊢ ρ ≅-⊢₂ trans · (x /∋ ρ)

  -- Application of multiple substitutions to variables.
  --
  -- TODO: Remove?

  app∋⋆ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Subs T₁ ρ̂ → [ Var ⟶ T₂ ] ρ̂
  app∋⋆ ε        = var₂
  app∋⋆ (ε ▻ ρ)  = trans [∘] app∋ ρ
  app∋⋆ (ρs ▻ ρ) = app ρ [∘] app∋⋆ ρs

  infixl 8 _/∋⋆_

  _/∋⋆_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} → Γ ∋ σ → Subs T₁ ρ̂ → Δ ⊢₂ σ /̂ ρ̂
  x /∋⋆ ρs = app∋⋆ ρs · x

  -- Composition of multiple substitutions.
  --
  -- TODO: Remove?

  ∘⋆ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Subs T₁ ρ̂ → Sub T₂ ρ̂
  ∘⋆ ε        = id₂
  ∘⋆ (ρs ▻ ρ) = ∘⋆ ρs ∘ ρ

  -- Some congruence lemmas.

  trans-cong : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢₁ σ₁}
                 {Γ₂ σ₂} {t₂ : Γ₂ ⊢₁ σ₂} →
               t₁ ≅-⊢₁ t₂ → trans · t₁ ≅-⊢₂ trans · t₂
  trans-cong P.refl = P.refl

  app∋⋆-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρs₁ : Subs T₁ ρ̂₁}
                 {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρs₂ : Subs T₁ ρ̂₂} →
               ρs₁ ≅-⇨⋆ ρs₂ → app∋⋆ ρs₁ ≅-⟶ app∋⋆ ρs₂
  app∋⋆-cong P.refl = [ P.refl ]

  /∋⋆-cong :
    ∀ {Γ₁ Δ₁ σ₁} {x₁ : Γ₁ ∋ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρs₁ : Subs T₁ ρ̂₁}
      {Γ₂ Δ₂ σ₂} {x₂ : Γ₂ ∋ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρs₂ : Subs T₁ ρ̂₂} →
    x₁ ≅-∋ x₂ → ρs₁ ≅-⇨⋆ ρs₂ → x₁ /∋⋆ ρs₁ ≅-⊢₂ x₂ /∋⋆ ρs₂
  /∋⋆-cong P.refl P.refl = P.refl

  ∘⋆-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρs₁ : Subs T₁ ρ̂₁}
              {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρs₂ : Subs T₁ ρ̂₂} →
            ρs₁ ≅-⇨⋆ ρs₂ → ∘⋆ ρs₁ ≅-⇨ ∘⋆ ρs₂
  ∘⋆-cong P.refl = P.refl

  abstract

    -- Applying a composed substitution to a variable is equivalent to
    -- applying all the substitutions one after another.
    --
    -- TODO: Remove this lemma?

    /∋-∘⋆ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ ∋ σ) (ρs : Subs T₁ ρ̂) →
            x /∋ ∘⋆ ρs ≅-⊢₂ var₂ · x /⊢⋆ ρs
    /∋-∘⋆ x ε = begin
      [ x /∋ id₂ ]  ≡⟨ Simple./∋-id simple₂ x ⟩
      [ var₂ · x ]  ∎
    /∋-∘⋆ x (ρs ▻ ρ) = begin
      [ x /∋ ∘⋆ ρs ∘ ρ       ]  ≡⟨ /∋-∘ x (∘⋆ ρs) ρ ⟩
      [ x /∋ ∘⋆ ρs /⊢ ρ      ]  ≡⟨ /⊢-cong (/∋-∘⋆ x ρs) P.refl ⟩
      [ var₂ · x /⊢⋆ ρs /⊢ ρ ]  ∎

    -- x /∋⋆ ρs is synonymous with var₂ · x /⊢⋆ ρs.
    --
    -- TODO: Remove?

    var-/⊢⋆ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ ∋ σ) (ρs : Subs T₁ ρ̂) →
              var₂ · x /⊢⋆ ρs ≅-⊢₂ x /∋⋆ ρs
    var-/⊢⋆ x ε       = P.refl
    var-/⊢⋆ x (ε ▻ ρ) = begin
      [ var₂ · x /⊢ ρ    ]  ≡⟨ var-/⊢ x ρ ⟩
      [ trans · (x /∋ ρ) ]  ∎
    var-/⊢⋆ x (ρs ▻ ρ₁ ▻ ρ₂) = begin
      [ var₂ · x /⊢⋆ (ρs ▻ ρ₁) /⊢ ρ₂ ]  ≡⟨ /⊢-cong (var-/⊢⋆ x (ρs ▻ ρ₁)) P.refl ⟩
      [ x /∋⋆ (ρs ▻ ρ₁) /⊢ ρ₂        ]  ∎

    -- A helper lemma.

    /∋-≅-⊢-var : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ}
                 (x : Γ ∋ σ) (ρ : Sub T₁ ρ̂) {y : Δ ∋ σ / ρ} →
                 x /∋ ρ ≅-⊢₁ var₁ · y →
                 var₂ · x /⊢ ρ ≅-⊢₂ var₂ · y
    /∋-≅-⊢-var x ρ {y} hyp = begin
      [ var₂ · x /⊢ ρ      ]  ≡⟨ var-/⊢ x ρ ⟩
      [ trans · (x /∋ ρ)   ]  ≡⟨ trans-cong hyp ⟩
      [ trans · (var₁ · y) ]  ≡⟨ trans-var y ⟩
      [ var₂ · y           ]  ∎

    -- A variant of /∋-id.

    var-/⊢-id : ∀ {Γ σ} (x : Γ ∋ σ) → var₂ · x /⊢ id₁ ≅-⊢₂ var₂ · x
    var-/⊢-id x = /∋-≅-⊢-var x id₁ (Simple./∋-id simple₁ x)

    -- A variant of /∋-wk-↑⁺.

    var-/⊢-wk-↑⁺ : ∀ {Γ σ} Γ⁺ {τ} (x : Γ ++⁺ Γ⁺ ∋ τ) →
                   var₂ · x /⊢ wk₁ {σ = σ} ↑⁺₁ Γ⁺ ≅-⊢₂
                   var₂ · (lift weaken∋[ σ ] Γ⁺ · x)
    var-/⊢-wk-↑⁺ Γ⁺ x =
      /∋-≅-⊢-var x (wk₁ ↑⁺₁ Γ⁺) (Simple./∋-wk-↑⁺ simple₁ Γ⁺ x)

    -- A variant of /∋-wk-↑⁺-↑⁺.

    var-/⊢-wk-↑⁺-↑⁺ : ∀ {Γ σ} Γ⁺ Γ⁺⁺ {τ} (x : Γ ++⁺ Γ⁺ ++⁺ Γ⁺⁺ ∋ τ) →
                      var₂ · x /⊢ wk₁ {σ = σ} ↑⁺₁ Γ⁺ ↑⁺₁ Γ⁺⁺ ≅-⊢₂
                      var₂ · (lift (lift weaken∋[ σ ] Γ⁺) Γ⁺⁺ · x)
    var-/⊢-wk-↑⁺-↑⁺ Γ⁺ Γ⁺⁺ x =
      /∋-≅-⊢-var x (wk₁ ↑⁺₁ Γ⁺ ↑⁺₁ Γ⁺⁺)
                 (Simple./∋-wk-↑⁺-↑⁺ simple₁ Γ⁺ Γ⁺⁺ x)

    -- Variants of zero-/∋-↑.

    zero-/⊢-↑ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} σ (ρ : Sub T₁ ρ̂) →
                var₂ · zero /⊢ ρ ↑₁ σ ≅-⊢₂ var₂ · zero[ σ / ρ ]
    zero-/⊢-↑ σ ρ =
      /∋-≅-⊢-var zero (ρ ↑₁ σ) (Simple.zero-/∋-↑ simple₁ σ ρ)

    zero-/⊢⋆-↑⋆ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} σ (ρs : Subs T₁ ρ̂) →
                  var₂ · zero /⊢⋆ ρs ↑⋆₁ σ ≅-⊢₂
                  var₂ · zero[ σ /⋆ ρs ]
    zero-/⊢⋆-↑⋆ σ ε        = P.refl
    zero-/⊢⋆-↑⋆ σ (ρs ▻ ρ) = begin
      [ var₂ · zero /⊢⋆ ρs ↑⋆₁ σ /⊢ ρ ↑₁ ]  ≡⟨ /⊢-cong (zero-/⊢⋆-↑⋆ σ ρs) (P.refl {x = [ ρ ↑₁ (σ /⋆ ρs) ]}) ⟩
      [ var₂ · zero /⊢ ρ ↑₁ (σ /⋆ ρs)    ]  ≡⟨ zero-/⊢-↑ (σ /⋆ ρs) ρ ⟩
      [ var₂ · zero                      ]  ∎

    -- Corollaries of ε-↑⁺⋆ and ε-↑₊⋆.

    /⊢⋆-ε-↑⁺⋆ : ∀ {Γ} Γ⁺ {σ} (t : Γ ++⁺ Γ⁺ ⊢₂ σ) →
                t /⊢⋆ ε ↑⁺⋆₁ Γ⁺ ≅-⊢₂ t
    /⊢⋆-ε-↑⁺⋆ Γ⁺ t = begin
      [ t /⊢⋆ ε ↑⁺⋆₁ Γ⁺ ]  ≡⟨ /⊢⋆-cong (P.refl {x = [ t ]}) (Simple.ε-↑⁺⋆ simple₁ Γ⁺) ⟩
      [ t /⊢⋆ ε         ]  ≡⟨ P.refl ⟩
      [ t               ]  ∎

    /⊢⋆-ε-↑₊⋆ : ∀ {Γ} Γ₊ {σ} (t : Γ ++₊ Γ₊ ⊢₂ σ) →
                t /⊢⋆ ε ↑₊⋆₁ Γ₊ ≅-⊢₂ t
    /⊢⋆-ε-↑₊⋆ Γ₊ t = begin
      [ t /⊢⋆ ε ↑₊⋆₁ Γ₊ ]  ≡⟨ /⊢⋆-cong (P.refl {x = [ t ]}) (Simple.ε-↑₊⋆ simple₁ Γ₊) ⟩
      [ t /⊢⋆ ε         ]  ≡⟨ P.refl ⟩
      [ t               ]  ∎

    -- Corollaries of ▻-↑⁺⋆ and ▻-↑₊⋆.

    /⊢⋆-▻-↑⁺⋆ :
      ∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} Γ⁺ {σ}
      (t : Γ ++⁺ Γ⁺ ⊢₂ σ) (ρs : Subs T₁ ρ̂₁) (ρ : Sub T₁ ρ̂₂) →
      t /⊢⋆ (ρs ▻ ρ) ↑⁺⋆₁ Γ⁺ ≅-⊢₂ t /⊢⋆ ρs ↑⁺⋆₁ Γ⁺ /⊢ ρ ↑⁺₁ (Γ⁺ /⁺⋆ ρs)
    /⊢⋆-▻-↑⁺⋆ Γ⁺ t ρs ρ =
      /⊢⋆-cong (P.refl {x = [ t ]}) (Simple.▻-↑⁺⋆ simple₁ ρs ρ Γ⁺)

    /⊢⋆-▻-↑₊⋆ :
      ∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} Γ₊ {σ}
      (t : Γ ++₊ Γ₊ ⊢₂ σ) (ρs : Subs T₁ ρ̂₁) (ρ : Sub T₁ ρ̂₂) →
      t /⊢⋆ (ρs ▻ ρ) ↑₊⋆₁ Γ₊ ≅-⊢₂ t /⊢⋆ ρs ↑₊⋆₁ Γ₊ /⊢ ρ ↑₊₁ (Γ₊ /₊⋆ ρs)
    /⊢⋆-▻-↑₊⋆ Γ₊ t ρs ρ =
      /⊢⋆-cong (P.refl {x = [ t ]}) (Simple.▻-↑₊⋆ simple₁ ρs ρ Γ₊)

    -- Corollaries of ε-↑⁺⋆/ε-↑₊⋆ and ▻-↑⁺⋆/▻-↑₊⋆.

    /⊢⋆-ε-▻-↑⁺⋆ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} Γ⁺ {σ}
                  (t : Γ ++⁺ Γ⁺ ⊢₂ σ) (ρ : Sub T₁ ρ̂) →
                  t /⊢⋆ (ε ▻ ρ) ↑⁺⋆₁ Γ⁺ ≅-⊢₂ t /⊢ ρ ↑⁺₁ Γ⁺
    /⊢⋆-ε-▻-↑⁺⋆ Γ⁺ t ρ = begin
      [ t /⊢⋆ (ε ▻ ρ) ↑⁺⋆₁ Γ⁺               ]  ≡⟨ /⊢⋆-cong (P.refl {x = [ t ]}) (Simple.▻-↑⁺⋆ simple₁ ε ρ Γ⁺) ⟩
      [ t /⊢⋆ ε ↑⁺⋆₁ Γ⁺ /⊢ ρ ↑⁺₁ (Γ⁺ /̂⁺ îd) ]  ≡⟨ /⊢-cong (/⊢⋆-ε-↑⁺⋆ Γ⁺ t) (Simple.↑⁺-cong simple₁ P.refl (/̂⁺-îd Γ⁺)) ⟩
      [ t               /⊢ ρ ↑⁺₁ Γ⁺         ]  ∎

    /⊢⋆-ε-▻-▻-↑⁺⋆ :
      ∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} Γ⁺ {σ}
      (t : Γ ++⁺ Γ⁺ ⊢₂ σ) (ρ₁ : Sub T₁ ρ̂₁) (ρ₂ : Sub T₁ ρ̂₂) →
      t /⊢⋆ (ε ▻ ρ₁ ▻ ρ₂) ↑⁺⋆₁ Γ⁺ ≅-⊢₂
      t /⊢ ρ₁ ↑⁺₁ Γ⁺ /⊢ ρ₂ ↑⁺₁ (Γ⁺ /⁺ ρ₁)
    /⊢⋆-ε-▻-▻-↑⁺⋆ Γ⁺ t ρ₁ ρ₂ = begin
      [ t /⊢⋆ (ε ▻ ρ₁ ▻ ρ₂) ↑⁺⋆₁ Γ⁺                 ]  ≡⟨ /⊢⋆-cong (P.refl {x = [ t ]}) (Simple.▻-↑⁺⋆ simple₁ (ε ▻ ρ₁) ρ₂ Γ⁺) ⟩
      [ t /⊢⋆ (ε ▻ ρ₁) ↑⁺⋆₁ Γ⁺ /⊢ ρ₂ ↑⁺₁ (Γ⁺ /⁺ ρ₁) ]  ≡⟨ /⊢-cong (/⊢⋆-ε-▻-↑⁺⋆ Γ⁺ t ρ₁) P.refl ⟩
      [ t /⊢ ρ₁ ↑⁺₁ Γ⁺ /⊢ ρ₂ ↑⁺₁ (Γ⁺ /⁺ ρ₁)         ]  ∎

    /⊢⋆-ε-▻-↑₊⋆ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} Γ₊ {σ}
                  (t : Γ ++₊ Γ₊ ⊢₂ σ) (ρ : Sub T₁ ρ̂) →
                  t /⊢⋆ (ε ▻ ρ) ↑₊⋆₁ Γ₊ ≅-⊢₂ t /⊢ ρ ↑₊₁ Γ₊
    /⊢⋆-ε-▻-↑₊⋆ Γ₊ t ρ = begin
      [ t /⊢⋆ (ε ▻ ρ) ↑₊⋆₁ Γ₊               ]  ≡⟨ /⊢⋆-cong (P.refl {x = [ t ]}) (Simple.▻-↑₊⋆ simple₁ ε ρ Γ₊) ⟩
      [ t /⊢⋆ ε ↑₊⋆₁ Γ₊ /⊢ ρ ↑₊₁ (Γ₊ /̂₊ îd) ]  ≡⟨ /⊢-cong (/⊢⋆-ε-↑₊⋆ Γ₊ t) (Simple.↑₊-cong simple₁ P.refl (/̂₊-îd Γ₊)) ⟩
      [ t               /⊢ ρ ↑₊₁ Γ₊         ]  ∎

    /⊢⋆-ε-▻-▻-↑₊⋆ :
      ∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} Γ₊ {σ}
      (t : Γ ++₊ Γ₊ ⊢₂ σ) (ρ₁ : Sub T₁ ρ̂₁) (ρ₂ : Sub T₁ ρ̂₂) →
      t /⊢⋆ (ε ▻ ρ₁ ▻ ρ₂) ↑₊⋆₁ Γ₊ ≅-⊢₂
      t /⊢ ρ₁ ↑₊₁ Γ₊ /⊢ ρ₂ ↑₊₁ (Γ₊ /₊ ρ₁)
    /⊢⋆-ε-▻-▻-↑₊⋆ Γ₊ t ρ₁ ρ₂ = begin
      [ t /⊢⋆ (ε ▻ ρ₁ ▻ ρ₂) ↑₊⋆₁ Γ₊                 ]  ≡⟨ /⊢⋆-cong (P.refl {x = [ t ]}) (Simple.▻-↑₊⋆ simple₁ (ε ▻ ρ₁) ρ₂ Γ₊) ⟩
      [ t /⊢⋆ (ε ▻ ρ₁) ↑₊⋆₁ Γ₊ /⊢ ρ₂ ↑₊₁ (Γ₊ /₊ ρ₁) ]  ≡⟨ /⊢-cong (/⊢⋆-ε-▻-↑₊⋆ Γ₊ t ρ₁) P.refl ⟩
      [ t /⊢ ρ₁ ↑₊₁ Γ₊ /⊢ ρ₂ ↑₊₁ (Γ₊ /₊ ρ₁)         ]  ∎

    -- Application of sub cancels one occurrence of suc.

    suc-/⊢-sub : ∀ {Γ σ τ} (x : Γ ∋ σ) (t : Γ ⊢₁ τ) →
                 var₂ · suc x /⊢ sub₁ t ≅-⊢₂ var₂ · x
    suc-/⊢-sub x t = begin
      [ var₂ · suc x /⊢ sub₁ t    ]  ≡⟨ var-/⊢ (suc x) (sub₁ t) ⟩
      [ trans · (suc x /∋ sub₁ t) ]  ≡⟨ P.refl ⟩
      [ trans · (x /∋ id₁)        ]  ≡⟨ trans-cong (Simple./∋-id simple₁ x) ⟩
      [ trans · (var₁ · x)        ]  ≡⟨ trans-var x ⟩
      [ var₂ · x                  ]  ∎

    -- First weakening and then substituting something for the first
    -- variable is equivalent to doing nothing.

    wk-∘-sub : ∀ {Γ σ} (t : Γ ⊢₁ σ) → wk₂ ∘ sub₁ t ≅-⇨ id₂[ Γ ]
    wk-∘-sub t = extensionality P.refl λ x → begin
      [ x /∋ wk₂ ∘ sub₁ t      ]  ≡⟨ /∋-∘ x wk₂ (sub₁ t) ⟩
      [ x /∋ wk₂ /⊢ sub₁ t     ]  ≡⟨ /⊢-cong (Simple./∋-wk simple₂ x) P.refl ⟩
      [ var₂ · suc x /⊢ sub₁ t ]  ≡⟨ suc-/⊢-sub x t ⟩
      [ var₂ · x               ]  ≡⟨ P.sym $ Simple./∋-id simple₂ x ⟩
      [ x /∋ id₂               ]  ∎

    -- id is a left identity of _∘_ (more or less).

    id-∘ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T₁ ρ̂) → id₂ ∘ ρ ≅-⇨ map trans ρ
    id-∘ ρ = extensionality P.refl λ x → begin
      [ x /∋ id₂ ∘ ρ     ]  ≡⟨ /∋-∘ x id₂ ρ ⟩
      [ x /∋ id₂ /⊢ ρ    ]  ≡⟨ /⊢-cong (Simple./∋-id simple₂ x) (P.refl {x = [ ρ ]}) ⟩
      [ var₂ · x /⊢ ρ    ]  ≡⟨ var-/⊢ x ρ ⟩
      [ trans · (x /∋ ρ) ]  ≡⟨ P.sym $ /∋-map x trans ρ ⟩
      [ x /∋ map trans ρ ]  ∎

    -- One can translate a substitution either before or after
    -- weakening it.

    map-trans-wk-subst : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T₁ ρ̂) →
                         map trans (wk-subst₁[ σ ] ρ) ≅-⇨
                         wk-subst₂[ σ ] (map trans ρ)
    map-trans-wk-subst {σ = σ} ρ = begin
      [ map trans (wk-subst₁[ σ ] ρ)   ]  ≡⟨ P.sym $ map-[∘] trans weaken₁[ σ ] ρ ⟩
      [ map (trans [∘] weaken₁[ σ ]) ρ ]  ≡⟨ map-cong-ext₁ P.refl trans-weaken (P.refl {x = [ ρ ]}) ⟩
      [ map (weaken₂ [∘] trans) ρ      ]  ≡⟨ map-[∘] weaken₂ trans ρ ⟩
      [ wk-subst₂ (map trans ρ)        ]  ∎

    -- One can translate a substitution either before or after lifting
    -- it.

    map-trans-↑ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T₁ ρ̂) →
                  map trans (ρ ↑₁ σ) ≅-⇨ map trans ρ ↑₂ σ
    map-trans-↑ {σ = σ} ρ = begin
      [ map trans (ρ ↑₁ σ)                                       ]  ≡⟨ map-cong (trans ∎-⟶) (Simple.unfold-↑ simple₁ ρ) ⟩
      [ map trans (wk-subst₁[ σ / ρ ] ρ ▻ var₁ · zero)           ]  ≡⟨ map-▻ trans (wk-subst₁ ρ) _ ⟩
      [ map trans (wk-subst₁[ σ / ρ ] ρ) ▻ trans · (var₁ · zero) ]  ≡⟨ ▻⇨-cong P.refl (map-trans-wk-subst ρ) (trans-var zero) ⟩
      [ wk-subst₂ (map trans ρ) ▻ var₂ · zero                    ]  ≡⟨ P.sym $ Simple.unfold-↑ simple₂ (map trans ρ) ⟩
      [ map trans ρ ↑₂                                           ]  ∎

  open Application application public

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
module Abstract where

data Bool : Set where
  true false : Bool

not : Bool → Bool
not true  = false
not false = true

abstract
  Answer : Set
  Answer = Bool

  yes : Answer
  yes = true

  no : Answer
  no = false

  contradict : Answer → Answer
  contradict x = not x

counter-contradict : Answer → Answer
counter-contradict x = contradict (contradict x)

no-way : Answer
no-way = contradict yes

data Answers : Set where
  one-answer   : Answer → Answers
  more-answers : Answer → Answers → Answers

yes-or-no : Answers
yes-or-no = more-answers yes (one-answer no)

ext: agda

max_stars_repo_name: dagit/agda

max_issues_repo_name: dagit/agda

max_forks_repo_name: dagit/agda


text:
------------------------------------------------------------------------
-- Excluded middle
------------------------------------------------------------------------

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

open import Equality

module Excluded-middle
  {e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where

open Derived-definitions-and-properties eq

open import Prelude

open import H-level.Closure eq

-- Excluded middle (roughly as stated in the HoTT book).

Excluded-middle : (ℓ : Level) → Type (lsuc ℓ)
Excluded-middle p = {P : Type p} → Is-proposition P → Dec P

-- Excluded middle is pointwise propositional (assuming
-- extensionality).

Excluded-middle-propositional :
  ∀ {ℓ} →
  Extensionality (lsuc ℓ) ℓ →
  Is-proposition (Excluded-middle ℓ)
Excluded-middle-propositional ext =
  implicit-Π-closure ext 1 λ _ →
  Π-closure (lower-extensionality _ lzero ext) 1 λ P-prop →
  Dec-closure-propositional (lower-extensionality _ _ ext) P-prop

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------------
-- Lists examples
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.List.Examples where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Data.List.Type

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

l₁ : List (true ∷ false ∷ [])
l₁ = lcons true (lcons false lnil)

l₂ : List (zero ∷ 1' ∷ 2' ∷ [])
l₂ = lcons zero (lcons 1' (lcons 2' lnil))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --cubical --no-import-sorts  #-}

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
import Cubical.Algebra.Semigroup as Std
open import MorePropAlgebra.Bundles

module MorePropAlgebra.Properties.Semigroup {ℓ} (assumptions : Semigroup {ℓ}) where
open Semigroup assumptions renaming (Carrier to G)

stdIsSemigroup : Std.IsSemigroup _·_
stdIsSemigroup  .Std.IsSemigroup.is-set = is-set
stdIsSemigroup  .Std.IsSemigroup.assoc  = is-assoc

stdSemigroup : Std.Semigroup {ℓ}
stdSemigroup = record { Semigroup assumptions ; isSemigroup = stdIsSemigroup }

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic ordering of lists
------------------------------------------------------------------------

-- The definition of lexicographic ordering used here is suitable if
-- the argument order is a (non-strict) partial order. The
-- lexicographic ordering itself can be either strict or non-strict,
-- depending on the value of a parameter.

module Relation.Binary.List.NonStrictLex where

open import Data.Empty
open import Function
open import Data.Unit using (⊤; tt)
open import Data.Product
open import Data.List
open import Level
open import Relation.Nullary
open import Relation.Binary

import Relation.Binary.NonStrictToStrict as Conv
import Relation.Binary.List.StrictLex as Strict

open import Relation.Binary.List.Pointwise as Pointwise using ([])

module _ {A : Set} where

  Lex : (P : Set) → (_≈_ _≤_ : Rel A zero) → Rel (List A) zero
  Lex P _≈_ _≤_ = Strict.Lex P _≈_ (Conv._<_ _≈_ _≤_)

  -- Strict lexicographic ordering.

  Lex-< : (_≈_ _≤_ : Rel A zero) → Rel (List A) zero
  Lex-< = Lex ⊥

  -- Non-strict lexicographic ordering.

  Lex-≤ : (_≈_ _≤_ : Rel A zero) → Rel (List A) zero
  Lex-≤ = Lex ⊤

  ------------------------------------------------------------------------
  -- Properties

  ≤-reflexive : ∀ _≈_ _≤_ → Pointwise.Rel _≈_ ⇒ Lex-≤ _≈_ _≤_
  ≤-reflexive _≈_ _≤_ = Strict.≤-reflexive _≈_ (Conv._<_ _≈_ _≤_)

  <-irreflexive : ∀ {_≈_ _≤_} →
                  Irreflexive (Pointwise.Rel _≈_) (Lex-< _≈_ _≤_)
  <-irreflexive {_≈_} {_≤_} =
    Strict.<-irreflexive {_<_ = Conv._<_ _≈_ _≤_} (Conv.irrefl _≈_ _≤_)

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

  antisymmetric : ∀ {P _≈_ _≤_} →
                  Symmetric _≈_ → Antisymmetric _≈_ _≤_ →
                  Antisymmetric (Pointwise.Rel _≈_) (Lex P _≈_ _≤_)
  antisymmetric {_≈_ = _≈_} {_≤_} sym antisym =
    Strict.antisymmetric sym (Conv.irrefl _≈_ _≤_)
                         (Conv.antisym⟶asym _≈_ _ antisym)

  <-asymmetric : ∀ {_≈_ _≤_} →
                 IsEquivalence _≈_ → _≤_ Respects₂ _≈_ →
                 Antisymmetric _≈_ _≤_ → Asymmetric (Lex-< _≈_ _≤_)
  <-asymmetric {_≈_} eq resp antisym  =
    Strict.<-asymmetric sym (Conv.<-resp-≈ _ _ eq resp)
                        (Conv.antisym⟶asym _≈_ _ antisym)
    where open IsEquivalence eq

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

  decidable : ∀ {P _≈_ _≤_} →
              Dec P → Decidable _≈_ → Decidable _≤_ →
              Decidable (Lex P _≈_ _≤_)
  decidable dec-P dec-≈ dec-≤ =
    Strict.decidable dec-P dec-≈ (Conv.decidable _ _ dec-≈ dec-≤)

  <-decidable :
    ∀ {_≈_ _≤_} →
    Decidable _≈_ → Decidable _≤_ → Decidable (Lex-< _≈_ _≤_)
  <-decidable = decidable (no id)

  ≤-decidable :
    ∀ {_≈_ _≤_} →
    Decidable _≈_ → Decidable _≤_ → Decidable (Lex-≤ _≈_ _≤_)
  ≤-decidable = decidable (yes tt)

  ≤-total : ∀ {_≈_ _≤_} → Symmetric _≈_ → Decidable _≈_ →
            Antisymmetric _≈_ _≤_ → Total _≤_ →
            Total (Lex-≤ _≈_ _≤_)
  ≤-total sym dec-≈ antisym tot =
    Strict.≤-total sym (Conv.trichotomous _ _ sym dec-≈ antisym tot)

  <-compare : ∀ {_≈_ _≤_} → Symmetric _≈_ → Decidable _≈_ →
              Antisymmetric _≈_ _≤_ → Total _≤_ →
              Trichotomous (Pointwise.Rel _≈_) (Lex-< _≈_ _≤_)
  <-compare sym dec-≈ antisym tot =
    Strict.<-compare sym (Conv.trichotomous _ _ sym dec-≈ antisym tot)

  -- Some collections of properties which are preserved by Lex-≤ or
  -- Lex-<.

  ≤-isPreorder : ∀ {_≈_ _≤_} →
                 IsPartialOrder _≈_ _≤_ →
                 IsPreorder (Pointwise.Rel _≈_) (Lex-≤ _≈_ _≤_)
  ≤-isPreorder po =
    Strict.≤-isPreorder
       isEquivalence (Conv.trans _ _ po)
       (Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
   where open IsPartialOrder po

  ≤-isPartialOrder : ∀ {_≈_ _≤_} →
                     IsPartialOrder _≈_ _≤_ →
                     IsPartialOrder (Pointwise.Rel _≈_) (Lex-≤ _≈_ _≤_)
  ≤-isPartialOrder po =
    Strict.≤-isPartialOrder
      (Conv.isPartialOrder⟶isStrictPartialOrder _ _ po)

  ≤-isTotalOrder : ∀ {_≈_ _≤_} →
                   Decidable _≈_ → IsTotalOrder _≈_ _≤_ →
                   IsTotalOrder (Pointwise.Rel _≈_) (Lex-≤ _≈_ _≤_)
  ≤-isTotalOrder dec tot =
    Strict.≤-isTotalOrder
      (Conv.isTotalOrder⟶isStrictTotalOrder _ _ dec tot)

  ≤-isDecTotalOrder :
    ∀ {_≈_ _≤_} →
    IsDecTotalOrder _≈_ _≤_ →
    IsDecTotalOrder (Pointwise.Rel _≈_) (Lex-≤ _≈_ _≤_)
  ≤-isDecTotalOrder dtot =
    Strict.≤-isDecTotalOrder
      (Conv.isDecTotalOrder⟶isStrictTotalOrder _ _ dtot)

  <-isStrictPartialOrder : ∀ {_≈_ _≤_} →
    IsPartialOrder _≈_ _≤_ →
    IsStrictPartialOrder (Pointwise.Rel _≈_) (Lex-< _≈_ _≤_)
  <-isStrictPartialOrder po =
    Strict.<-isStrictPartialOrder
      (Conv.isPartialOrder⟶isStrictPartialOrder _ _ po)

  <-isStrictTotalOrder : ∀ {_≈_ _≤_} →
    Decidable _≈_ → IsTotalOrder _≈_ _≤_ →
    IsStrictTotalOrder (Pointwise.Rel _≈_) (Lex-< _≈_ _≤_)
  <-isStrictTotalOrder dec tot =
    Strict.<-isStrictTotalOrder
      (Conv.isTotalOrder⟶isStrictTotalOrder _ _ dec tot)

-- "Packages" (e.g. preorders) can also be handled.

≤-preorder : Poset _ _ _ → Preorder _ _ _
≤-preorder po = record
  { isPreorder = ≤-isPreorder isPartialOrder
  } where open Poset po

≤-partialOrder : Poset _ _ _ → Poset _ _ _
≤-partialOrder po = record
  { isPartialOrder = ≤-isPartialOrder isPartialOrder
  } where open Poset po

≤-decTotalOrder : DecTotalOrder _ _ _ → DecTotalOrder _ _ _
≤-decTotalOrder dtot = record
  { isDecTotalOrder = ≤-isDecTotalOrder isDecTotalOrder
  } where open DecTotalOrder dtot

<-strictPartialOrder : Poset _ _ _ → StrictPartialOrder _ _ _
<-strictPartialOrder po = record
  { isStrictPartialOrder = <-isStrictPartialOrder isPartialOrder
  } where open Poset po

<-strictTotalOrder : DecTotalOrder _ _ _ → StrictTotalOrder _ _ _
<-strictTotalOrder dtot = record
  { isStrictTotalOrder = <-isStrictTotalOrder _≟_ isTotalOrder
  } where open IsDecTotalOrder (DecTotalOrder.isDecTotalOrder dtot)


text:
------------------------------------------------------------------------
-- Some definitions related to and properties of the Maybe type
------------------------------------------------------------------------

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

open import Equality

module Maybe
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Prelude

open import Bijection eq using (_↔_)
open Derived-definitions-and-properties eq
open import Monad eq

-- A dependent eliminator.

maybe : ∀ {a b} {A : Type a} {B : Maybe A → Type b} →
        ((x : A) → B (just x)) → B nothing → (x : Maybe A) → B x
maybe j n (just x) = j x
maybe j n nothing  = n

-- Is the value just something?

is-just : ∀ {a} {A : Type a} → Maybe A → Bool
is-just = maybe (const true) false

-- Is the value nothing?

is-nothing : ∀ {a} {A : Type a} → Maybe A → Bool
is-nothing = not ∘ is-just

-- Is-just x is a proposition that is inhabited iff x is
-- just something.

Is-just : ∀ {a} {A : Type a} → Maybe A → Type
Is-just = T ∘ is-just

-- Is-nothing x is a proposition that is inhabited iff x is nothing.

Is-nothing : ∀ {a} {A : Type a} → Maybe A → Type
Is-nothing = T ∘ is-nothing

-- Is-just and Is-nothing are mutually exclusive.

not-both-just-and-nothing :
  ∀ {a} {A : Type a} (x : Maybe A) →
  Is-just x → Is-nothing x → ⊥₀
not-both-just-and-nothing (just _) _  ()
not-both-just-and-nothing nothing  () _

-- A universe-polymorphic variant of bind.

infixl 5 _>>=′_

_>>=′_ : ∀ {a b} {A : Type a} {B : Type b} →
         Maybe A → (A → Maybe B) → Maybe B
x >>=′ f = maybe f nothing x

instance

  -- The maybe monad.

  raw-monad : ∀ {ℓ} → Raw-monad (Maybe {a = ℓ})
  Raw-monad.return raw-monad x = just x
  Raw-monad._>>=_ raw-monad    = _>>=′_

  monad : ∀ {ℓ} → Monad (Maybe {a = ℓ})
  Monad.raw-monad      monad              = raw-monad
  Monad.left-identity  monad x f          = refl (f x)
  Monad.right-identity monad nothing      = refl nothing
  Monad.right-identity monad (just x)     = refl (just x)
  Monad.associativity  monad nothing f g  = refl nothing
  Monad.associativity  monad (just x) f g = refl (f x >>= g)

-- The maybe monad transformer.

record MaybeT {d c} (M : Type d → Type c) (A : Type d) : Type c where
  constructor wrap
  field
    run : M (Maybe A)

open MaybeT public

-- Failure.

fail : ∀ {d c} {M : Type d → Type c} ⦃ is-monad : Raw-monad M ⦄ {A} →
       MaybeT M A
run fail = return nothing

-- MaybeT id is pointwise isomorphic to Maybe.

MaybeT-id↔Maybe : ∀ {a} {A : Type a} → MaybeT id A ↔ Maybe A
MaybeT-id↔Maybe = record
  { surjection = record
    { logical-equivalence = record { to = run; from = wrap }
    ; right-inverse-of    = refl
    }
  ; left-inverse-of = refl
  }

instance

  -- MaybeT is a "raw monad" transformer.

  raw-monad-transformer :
    ∀ {d c} → Raw-monad-transformer (MaybeT {d = d} {c = c})

  run (Raw-monad.return (Raw-monad-transformer.transform
                           raw-monad-transformer) x) =
    return (just x)

  run (Raw-monad._>>=_ (Raw-monad-transformer.transform
                          raw-monad-transformer) x f) =
    run x >>= maybe (run ∘ f) (return nothing)

  run (Raw-monad-transformer.liftʳ raw-monad-transformer m) =
    map just m

  transform :
    ∀ {d c} {M : Type d → Type c} ⦃ is-raw-monad : Raw-monad M ⦄ →
    Raw-monad (MaybeT M)
  transform = Raw-monad-transformer.transform raw-monad-transformer

-- MaybeT is a monad transformer (assuming extensionality).

monad-transformer :
  ∀ {d c} →
  Extensionality d c →
  Monad-transformer (MaybeT {d = d} {c = c})

Monad.raw-monad (Monad-transformer.transform (monad-transformer _)) =
  Raw-monad-transformer.transform raw-monad-transformer

Monad.left-identity
  (Monad-transformer.transform (monad-transformer _)) x f = cong wrap (
    return (just x) >>= maybe (run ∘ f) (return nothing)  ≡⟨ left-identity (just x) (maybe (run ∘ f) (return nothing)) ⟩∎
    run (f x)                                             ∎)

Monad.right-identity
  (Monad-transformer.transform (monad-transformer ext)) x = cong wrap (
    run x >>= maybe (return ∘ just) (return nothing)  ≡⟨ cong (run x >>=_) (apply-ext ext (maybe (λ _ → refl _) (refl _))) ⟩
    run x >>= return                                  ≡⟨ right-identity _ ⟩∎
    run x                                             ∎)

Monad.associativity
  (Monad-transformer.transform (monad-transformer ext)) x f g = cong wrap (
    run x >>=
      (maybe (λ x → run (f x) >>= maybe (run ∘ g) (return nothing))
             (return nothing))                                       ≡⟨ cong (run x >>=_) (apply-ext ext (maybe (λ _ → refl _) (

      return nothing                                                      ≡⟨ sym $ left-identity _ _ ⟩∎
      return nothing >>= maybe (run ∘ g) (return nothing)                 ∎))) ⟩

    run x >>= (λ x → maybe (run ∘ f) (return nothing) x >>=
                     maybe (run ∘ g) (return nothing))               ≡⟨ associativity _ _ _ ⟩∎

    (run x >>= maybe (run ∘ f) (return nothing)) >>=
      maybe (run ∘ g) (return nothing)                               ∎)

Monad-transformer.liftᵐ (monad-transformer _) = liftʳ

Monad-transformer.lift-return (monad-transformer _) x = cong wrap (
  map just (return x)  ≡⟨ map-return just x ⟩∎
  return (just x)      ∎)

Monad-transformer.lift->>= (monad-transformer ext) x f = cong wrap (
  map just (x >>= f)                                    ≡⟨ map->>= _ _ _ ⟩
  x >>= map just ∘ f                                    ≡⟨ sym $ >>=-map ext _ _ _ ⟩∎
  map just x >>= maybe (map just ∘ f) (return nothing)  ∎)


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

open import Level

module Categories.Category.Instance.SimplicialSet.Properties (o ℓ : Level) where

open import Function using (_$_)

open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
open import Data.Nat using (ℕ)
open import Data.Fin using (Fin)
open import Data.Product using (proj₁)

import Relation.Binary.PropositionalEquality as Eq

open import Categories.Category using (Category; _[_,_]; _[_∘_]; _[_≈_])
open import Categories.Category.Instance.SimplicialSet using (SimplicialSet)
open import Categories.Category.Instance.Simplex using (Δ; face; degeneracy)

open import Categories.Functor using (Functor; _∘F_)
open import Categories.Functor.Construction.Constant using (const)
open import Categories.Functor.Construction.LiftSetoids using (LiftSetoids)

open import Categories.NaturalTransformation using (ntHelper)

open import Categories.Yoneda

private
  module Y = Functor (Yoneda.embed Δ)

-- Some useful notation for a simplicial set
ΔSet : Set (suc o ⊔ suc ℓ)
ΔSet = Category.Obj (SimplicialSet o ℓ )

-- The standard n-simplex.
Δ[_] : ℕ → ΔSet
Δ[_] n = LiftSetoids o ℓ ∘F Y.F₀ n

--------------------------------------------------------------------------------
-- Boundaries of the Standard Simplicies
--
-- The basic idea here is that we will build up boundary of 'Δ[ n ]' by considering
-- all of the morphisms 'Δ[ m , n ]' that factor through some face map 'face i : Δ[ n - 1 , n ]'

-- The indexing here is a bit tricky, but this is the price we pay to avoid 'pred'
-- A 'Boundary m n' represents some set of maps into 'Δ[ ℕ.suc n ]' that factor through
-- a face map. To make this indexing more obvious, we use the suggestively named variable 'n-1'.
record Boundary (m n-1 : ℕ) : Set where
  -- To avoid the (somewhat confusion) pattern of 'ℕ.suc n-1', let's define
  -- a bit of helpful local notation.
  private
    n : ℕ
    n = ℕ.suc n-1

  field
    hom : Δ [ m , n ]
    factor : Δ [ m , n-1 ]
    factor-dim : Fin n
    factor-face : Δ [ hom ≈ Δ [ face factor-dim ∘ factor ] ]

-- Lift morphisms in Δ to maps between boundary sets on 'Δ[ n ]'
boundary-map : ∀ {x y n} → Δ [ x , y ] → Boundary y n → Boundary x n
boundary-map {n = n} f b = record
  { hom = hom b ∘ f
  ; factor = factor b ∘ f
  ; factor-dim = factor-dim b
  ; factor-face = λ x → factor-face b (proj₁ f x)
  }
  where
    open Category Δ
    open Boundary

-- The boundary of an n-simplex
∂Δ[_] : ℕ → ΔSet
∂Δ[_] ℕ.zero = const record
  { Carrier = ⊥
  ; _≈_ = λ ()
  ; isEquivalence = record
    { refl  = λ { {()} }
    ; sym   = λ { {()} }
    ; trans = λ { {()} }
    }
  }
∂Δ[_] (ℕ.suc n) = record
  { F₀ = λ m → record
    { Carrier = Lift o (Boundary m n)
    -- Unwinding the equality by hand here leads to less unsolved metavariables down the line
    ; _≈_ = λ (lift b) (lift b′) → ∀ x → Lift ℓ (proj₁ (hom b) x ≡ proj₁ (hom b′) x)
    ; isEquivalence = record
      { refl = λ x → lift refl
      ; sym = λ eq x → lift (sym (lower (eq x)))
      ; trans = λ eq₁ eq₂ x → lift (trans (lower (eq₁ x)) (lower (eq₂ x)))
      }
    }
  ; F₁ = λ f → record
    { _⟨$⟩_ = λ (lift b) → lift (boundary-map f b)
    ; cong = λ eq x → eq (proj₁ f x)
    }
  ; identity = λ eq → eq
  ; homomorphism = λ {_} {_} {_} {f} {g} eq x → eq (proj₁ f (proj₁ g x))
  ; F-resp-≈ = λ {_} {_} {f} {g} f≈g {b} {b′} eq x → lift $ begin
    proj₁ (hom (lower b)) (proj₁ f x)  ≡⟨ lower (eq (proj₁ f x)) ⟩
    proj₁ (hom (lower b′)) (proj₁ f x) ≡⟨ cong (proj₁ (hom (lower b′))) (f≈g x) ⟩
    proj₁ (hom (lower b′)) (proj₁ g x) ∎
  }
  where
    open Boundary
    open Eq
    open ≡-Reasoning

--------------------------------------------------------------------------------
-- Horns
--
-- The idea here is essentially the same as the boundaries, but we exclude the kth
-- face map as a possible factor.

record Horn (m n-1 : ℕ) (k : Fin (ℕ.suc n-1)) : Set where
  field
    horn : Boundary m n-1

  open Boundary horn public

  field
    is-horn : factor-dim Eq.≢ k

Λ[_,_] : (n : ℕ) → Fin n → ΔSet
Λ[ ℕ.suc n , k ] = record
  { F₀ = λ m → record
    { Carrier = Lift o (Horn m n k)
    ; _≈_ = λ (lift b) (lift b′) → ∀ x → Lift ℓ (proj₁ (hom b) x ≡ proj₁ (hom b′) x)
    ; isEquivalence = record
      { refl = λ x → lift refl
      ; sym = λ eq x → lift (sym (lower (eq x)))
      ; trans = λ eq₁ eq₂ x → lift (trans (lower (eq₁ x)) (lower (eq₂ x)))
      }
    }
  ; F₁ = λ f → record
    { _⟨$⟩_ = λ (lift h) → lift $ record
      { horn = boundary-map f (horn h)
      ; is-horn = is-horn h
      }
    ; cong = λ eq x → eq (proj₁ f x)
    }
  ; identity = λ eq → eq
  ; homomorphism = λ {_} {_} {_} {f} {g} eq x → eq (proj₁ f (proj₁ g x))
  ; F-resp-≈ = λ {_} {_} {f} {g} f≈g {b} {b′} eq x → lift $ begin
    proj₁ (hom (lower b)) (proj₁ f x)  ≡⟨ lower (eq (proj₁ f x)) ⟩
    proj₁ (hom (lower b′)) (proj₁ f x) ≡⟨ cong (proj₁ (hom (lower b′))) (f≈g x) ⟩
    proj₁ (hom (lower b′)) (proj₁ g x) ∎
  }
  where
    open Horn
    open Eq
    open ≡-Reasoning

--------------------------------------------------------------------------------
-- Morphims between simplicial sets

module _ where
  open Category (SimplicialSet o ℓ)

  -- Inclusion of boundaries
  ∂Δ-inj : ∀ {n} → ∂Δ[ n ] ⇒ Δ[ n ]
  ∂Δ-inj {ℕ.zero} = ntHelper record
    { η = λ X → record
      { _⟨$⟩_ = ⊥-elim
      ; cong = λ { {()} }
      }
    ; commute = λ { _ {()} _ }
    }
  ∂Δ-inj {ℕ.suc n} = ntHelper record
    { η = λ X → record
      { _⟨$⟩_ = λ (lift b) → lift (hom b)
      ; cong = λ eq → lift (λ x → lower (eq x))
      }
    ; commute = λ f eq → lift (λ x → lower (eq (proj₁ f x)))
    }
    where
      open Boundary

  -- Inclusion of n-horns into n-simplicies
  Λ-inj : ∀ {n} → (k : Fin n) → Λ[ n , k ] ⇒ Δ[ n ]
  Λ-inj {n = ℕ.suc n} k = ntHelper record
    { η = λ X → record
      { _⟨$⟩_ = λ (lift h) → lift (hom h)
      ; cong = λ eq → lift (λ x → lower (eq x))
      }
    ; commute = λ f eq → lift (λ x → lower (eq (proj₁ f x)))
    }
    where
      open Horn

max_stars_repo_name: jaykru/agda-categories

max_issues_repo_name: jaykru/agda-categories

max_forks_repo_name: jaykru/agda-categories


text:
module PLRTree.Equality.Correctness {A : Set} where

open import BTree.Equality {A}
open import PLRTree {A}
open import PLRTree.Equality {A} renaming (_≃_ to _≃'_)

lemma-≃'-≃ : {l r : PLRTree} → l ≃' r → forget l ≃ forget r
lemma-≃'-≃ ≃lf = ≃lf
lemma-≃'-≃ (≃nd x x' l≃'r l'≃'r' l≃'l') = ≃nd x x' (lemma-≃'-≃ l≃'r) (lemma-≃'-≃ l≃'l') (lemma-≃'-≃ l'≃'r')

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
-- Andreas, 2019-07-15, issue #3901, requested by msuperdock
--
-- Allow function spaces  {A} → B  and  {{A}} → B.

postulate
  A B : Set
  foo : {{A}} → B
  bar : {A} → B

-- Original feature request:

open import Agda.Builtin.Unit using (⊤; tt)

data ⊥ : Set where

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

_≤_ : Nat → Nat → Set
zero ≤ _      = ⊤
suc m ≤ zero  = ⊥
suc m ≤ suc n = m ≤ n

data SList (bound : Nat) : Set where
  []    : SList bound
  scons : (head : Nat)
        → {head ≤ bound}       -- here: anonymous binding
        → (tail : SList head)
        → SList bound

xs : SList zero
xs = scons zero []

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Jesper, 2018-11-23: Unsolved metas are turned into postulates
-- when --allow-unsolved-metas is enabled, but there was no internal
-- representation of postulated sorts.

module Issue3256 where

open import Issue3256.B

-- WAS:
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/Reduce.hs:149

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Graphs where

open import Categories.Category
  hiding (module Heterogeneous)
open import Data.Product
open import Level
open import Relation.Binary
  renaming (_⇒_ to _⊆_)
open import Relation.Binary.PropositionalEquality
  using ()
  renaming (_≡_ to _≣_; refl to ≣-refl)

open import Graphs.Graph
open import Graphs.GraphMorphism

Graphs : ∀ o ℓ e → Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
Graphs o ℓ e = record
  { Obj       = Obj
  ; _⇒_       = _⇒_
  ; _≡_       = _≈_
  ; id        = id
  ; _∘_       = _∘_
  ; equiv     = isEquivalence
  ; assoc     = λ {A}{B}{C}{D}{f}{g}{h} → assoc {A}{B}{C}{D}{f}{g}{h}
  ; identityˡ = λ {A}{B}{f : A ⇒ B} → IsEquivalence.refl (isEquivalence {A = A}{B}) {x = f}
  ; identityʳ = λ {A}{B}{f : A ⇒ B} → IsEquivalence.refl (isEquivalence {A = A}{B}) {x = f}
  ; ∘-resp-≡  = λ {_}{_}{_}{f}{h}{g}{i} → ∘-resp-≈ {F = f}{h}{g}{i}
  }
  where
    Obj : Set (suc (o ⊔ ℓ ⊔ e))
    Obj = Graph o ℓ e

    _⇒_ : Obj → Obj → Set _
    _⇒_ = GraphMorphism

    .assoc : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} → ((h ∘ g) ∘ f) ≈ (h ∘ (g ∘ f))
    assoc {f = f}{g}{h} = (λ x → ≣-refl) , (λ f → refl)
      where open Heterogeneous _

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --cubical-compatible #-}

module WithoutK1 where

-- Equality defined with one index.

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

K : {A : Set} (P : {x : A} → x ≡ x → Set) →
    (∀ x → P (refl {x = x})) →
    ∀ {x} (x≡x : x ≡ x) → P x≡x
K P p refl = p _


text:
postulate
  U V W X Y Z : Set
  u : U
  v : V
  w : W
  x : X
  y : Y
  z : Z

module Top (u : U) where
  module A (v : V) where
    module M (w : W) where
      module O (x : X) where
      postulate O : X
    postulate O : X
  module B (y : Y) where
    open A public

module Test0 where
  module C = Top.B u y
  module D = C.M.O v w x
  O₁ : X
  O₁ = C.M.O v w
  O₂ : X
  O₂ = C.O v

module Test1 where
  module C (i g n o r i n g m e : Z) = Top.B u y
  module D = C.M.O z z z z z z z z z z v w x
  O : X
  O = C.M.O z z z z z z z z z z v w

module Test2 where
  module C (y : Y) = Top.B u y
  module D = C.M.O y v w x
  O : X
  O = C.M.O y v w

module Test3 where
  module C (z : Z) = Top.B u y
  module D = C.M.O z v w x


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

{-# OPTIONS --allow-exec #-}

open import Vehicle
open import Vehicle.Data.Tensor
open import Data.Rational as ℚ using (ℚ)
open import Data.List
open import Relation.Binary.PropositionalEquality

module autoencoderError-temp-output where

postulate encode : Tensor ℚ (5 ∷ []) → Tensor ℚ (2 ∷ [])

postulate decode : Tensor ℚ (2 ∷ []) → Tensor ℚ (5 ∷ [])

abstract
  identity : ∀ (x : Tensor ℚ (5 ∷ [])) → decode (encode x) ≡ x
  identity = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

max_stars_repo_name: vehicle-lang/vehicle

max_issues_repo_name: vehicle-lang/vehicle

max_forks_repo_name: vehicle-lang/vehicle


text:
module Data.List.Kleene.Relation.Unary.All where

open import Data.List.Kleene.Base
open import Relation.Unary
open import Relation.Nullary
open import Level using (_⊔_)
open import Function

mutual
  record All⁺ {a p} {A : Set a} (P : Pred A p) (xs : A ⁺) : Set (a ⊔ p) where
    constructor P⟨_&_⟩
    inductive
    field
      P⟨head⟩ : P (head xs)
      P⟨tail⟩ : All⋆ P (tail xs)

  data All⋆ {a p} {A : Set a} (P : Pred A p) : Pred (A ⋆) (a ⊔ p) where
    P⟨[]⟩ : All⋆ P []
    P⟨∹_⟩ : ∀ {xs} → All⁺ P xs → All⋆ P (∹ xs)
open All⁺ public

module _ {a p} {A : Set a} {P : Pred A p} where
  mutual
    all⋆ : Decidable P → Decidable (All⋆ P)
    all⋆ p? [] = yes P⟨[]⟩
    all⋆ p? (∹ xs) with all⁺ p? xs
    all⋆ p? (∹ xs) | yes p = yes P⟨∹ p ⟩
    all⋆ p? (∹ xs) | no ¬p = no λ { P⟨∹ x ⟩ → ¬p x }

    all⁺ : Decidable P → Decidable (All⁺ P)
    all⁺ p? xs with p? (head xs) | all⋆ p? (tail xs)
    all⁺ p? xs | no ¬p | ys = no (¬p ∘ P⟨head⟩)
    all⁺ p? xs | yes p | yes ps = yes P⟨ p & ps ⟩
    all⁺ p? xs | yes p | no ¬p = no (¬p ∘ P⟨tail⟩)

max_stars_repo_name: oisdk/agda-kleene-lists

max_issues_repo_name: oisdk/agda-kleene-lists

max_forks_repo_name: oisdk/agda-kleene-lists


text:
open import Data.List    using (List; _∷_; [])
open import Data.Product using (_×_; _,_; Σ)
open import Data.Unit    using (⊤; tt)
open import Relation.Binary.PropositionalEquality using (_≡_)

module SystemT where

  {- de Bruijn indices are represented as proofs that
     an element is in a list -}
  data _∈_ {A : Set} : (x : A) (l : List A) → Set where -- type \in
    i0 : {x : A} {xs : List A} → x ∈ (x ∷ xs)
    iS : {x y : A} {xs : List A} → x ∈ xs → x ∈ (y ∷ xs)

  {- types of the STLC -}
  data TType : Set where
    b : TType             -- uninterpreted base type
    _⇒_ : TType → TType → TType -- type \=>

  {- contexts are lists of TType's -}
  Ctx = List
  _,,_ : ∀ {A} → Ctx A → TType → Ctx A
  Γ ,, τ = τ ∷ Γ

  infixr 10 _⇒_
  infixr 9 _,,_
  infixr 8 _⊢_ -- type \entails

  {- Γ ⊢ τ represents a term of type τ in context Γ -}
  data _⊢_ (Γ : Ctx) : TType → Set where
    c   : Γ ⊢ b -- some constant of the base type
    v   : {τ : TType} → τ ∈ Γ → Γ ⊢ τ
    lam : {τ1 τ2 : TType} → Γ ,, τ1 ⊢ τ2 → Γ ⊢ τ1 ⇒ τ2
    app : {τ1 τ2 : TType} → Γ ⊢ τ1 ⇒ τ2 → Γ ⊢ τ1 → Γ ⊢ τ2

  module Examples where
    i : [] ⊢ b ⇒ b
    i = lam (v i0) -- \ x -> x

    k : [] ⊢ b ⇒ b ⇒ b
    k = lam (lam (v (iS i0))) -- \ x -> \ y -> x

    {- TASK 1: Define a term representing  \ x -> \ y -> y -}
    k' : [] ⊢ b ⇒ b ⇒ b
    k' = {!!}

  {- The following proof is like a "0-ary" logical relation.
     It gives a semantics of the STLC in Agda.
     This shows that the STLC is sound, relative to Agda.
  -}
  module Semantics (B : Set) (elB : B) where
    -- works for any interpretation of the base type b

    -- function mapping STLC types to Agda types
    ⟦_⟧t : TType → Set  -- type \(0 and \)0
    ⟦ b ⟧t = B
    ⟦ τ1 ⇒ τ2 ⟧t = ⟦ τ1 ⟧t → ⟦ τ2 ⟧t

    -- function mapping STLC contexts to Agda types
    ⟦_⟧c : Ctx → Set
    ⟦ [] ⟧c = ⊤
    ⟦ τ ∷ Γ ⟧c = ⟦ Γ ⟧c × ⟦ τ ⟧t

    {- TASK 2 : Define the interpretation of terms -}
    ⟦_⟧ : {Γ : Ctx} {τ : TType} → Γ ⊢ τ → ⟦ Γ ⟧c → ⟦ τ ⟧t
    ⟦ e ⟧ γ = {!!}

    {- the following test should pass
    test : ⟦ Examples.k ⟧ == \ γ x y → x
    test = Refl
    -}

  {- you can ignore the implementation of this module.
     the interface for the components you need is listed below
  -}
  module RenamingAndSubstitution where

    -- renamings = variable for variable substitutions

    infix 9 _⊇_

    _⊇_ : Ctx → Ctx → Set -- type \sup=
    Γ' ⊇ [] = ⊤
    Γ' ⊇ (τ ∷ Γ) = (Γ' ⊇ Γ) × (τ ∈ Γ')

    extend⊇ : {Γ : Ctx} (Γ' : Ctx) {τ : TType} → Γ ⊇ Γ' → (Γ ,, τ) ⊇ Γ'
    extend⊇ [] ren = tt
    extend⊇ (τ ∷ Γ') (ρ , x) = extend⊇ Γ' ρ , iS x

    open import Data.List using (_++_)
    extend⊇* : {Γ : Ctx} (Γ' : Ctx) (Γ'' : Ctx) → Γ ⊇ Γ' → (Γ'' ++ Γ) ⊇ Γ'
    extend⊇* Γ' [] ρ = ρ
    extend⊇* Γ' (x ∷ Γ'') ρ = extend⊇ _ (extend⊇* Γ' Γ'' ρ)

    shift : {Γ : Ctx} {τ : TType} (Γ' : Ctx) (i : τ ∈ Γ) → τ ∈ (Γ' ++ Γ)
    shift [] i = i
    shift (τ ∷ Γ) i = iS (shift Γ i)

    ⊇-id : (Γ : Ctx) → Γ ⊇ Γ
    ⊇-id [] = tt
    ⊇-id (τ ∷ Γ) = extend⊇ Γ (⊇-id Γ) , i0

    ⊇-single : {Γ : Ctx} {τ : TType} → (Γ ,, (τ ⊇ Γ))
    ⊇-single = extend⊇ _ (⊇-id _)

    -- you can rename a term

    rename : {Γ Γ' : Ctx} {τ : TType} → Γ' ⊇ Γ → Γ ⊢ τ → Γ' ⊢ τ
    rename ρ c = c
    rename (_ , x') (v i0) = v x'
    rename (ρ , _) (v (iS x)) = rename ρ (v x)
    rename ρ (lam e) = lam (rename (extend⊇ _ ρ , i0) e)
    rename ρ (app e e') = app (rename ρ e) (rename ρ e')

    -- expression-for-variable substitutions

    _⊢c_ : Ctx → Ctx → Set
    Γ' ⊢c [] = tt
    Γ' ⊢c (τ ∷ Γ) = (Γ' ⊢c Γ) × (Γ' ⊢ τ)

    rename-subst : {Γ1 Γ2 Γ3 : Ctx} →  Γ1 ⊇ Γ2 → Γ2 ⊢c Γ3 → Γ1 ⊢c Γ3
    rename-subst {Γ1} {Γ2} {[]} ρ θ = tt
    rename-subst {Γ1} {Γ2} {τ3 ∷ Γ3} ρ (θ , e) = rename-subst ρ θ , rename ρ e

    addvar : {Γ Γ' : Ctx} {τ : TType} → Γ ⊢c Γ' → (Γ ,, τ) ⊢c (Γ' ,, τ)
    addvar θ = rename-subst ⊇-single θ , v i0

    id-subst : {Γ : Ctx} → Γ ⊢c Γ
    id-subst {[]} = tt
    id-subst {τ ∷ Γ} = rename-subst ⊇-single (id-subst {Γ}) , v i0

    subst : {Γ Γ' : Ctx}{τ : TType} → Γ ⊢c Γ' → Γ' ⊢ τ  → Γ ⊢ τ
    subst θ c = c
    subst (θ , e) (v i0) = e
    subst (θ , e) (v (iS x)) = subst θ (v x)
    subst θ (lam e) = lam (subst (addvar θ) e)
    subst θ (app e e') = app (subst θ e) (subst θ e')

    subst1 : {τ τ0 : TType} → [] ⊢ τ0 → ([] ,, τ0) ⊢ τ → [] ⊢ τ
    subst1 e0 e = subst (tt , e0) e

    -- these are not tasks (unless you really want); I didn't get to prove them; sorry!
    compose : {τ1 τ2 : TType} {Γ : Ctx} (θ : [] ⊢c Γ) (e' : [] ⊢ τ1) (e : Γ ,, τ1 ⊢ τ2)
            → subst (θ , e') e ≡ subst1 e' (subst (addvar θ) e)
    compose = {!!}

    ident : {Γ : Ctx} {τ : TType} {e : Γ ⊢ τ} → e ≡ subst (id-subst) e
    ident = {!!}

  open RenamingAndSubstitution using (subst1 ; _⊢c_ ; subst ; ident ; compose)
  {- θ : Γ ⊢c Γ' means θ is a substitution for Γ' in terms of Γ.  It is defined as follows:

    _⊢c_ : Ctx → Ctx → Set
    Γ' ⊢c [] = Unit
    Γ' ⊢c (τ ∷ Γ) = (Γ' ⊢c Γ) × (Γ' ⊢ τ)

    -- apply a substitution to a term
    subst : {Γ Γ' : Ctx}{τ : TType} → Γ ⊢c Γ' → Γ' ⊢ τ  → Γ ⊢ τ

    -- substitution for a single variable
    subst1 : {τ τ0 : TType} → [] ⊢ τ0 → ([] ,, τ0) ⊢ τ → [] ⊢ τ

    -- you will need these two properties:
    compose : {τ1 τ2 : TType} {Γ : Ctx} (θ : [] ⊢c Γ) (e' : [] ⊢ τ1) (e : Γ ,, τ1 ⊢ τ2)
            → subst (θ , e') e == subst1 e' (subst (addvar θ) e)

    ident : {Γ : Ctx} {τ : TType} {e : Γ ⊢ τ} → e == subst (id-subst) e
  -}

  module OpSem where
    -- step relation
    data _↦_ : {τ : TType} → [] ⊢ τ → [] ⊢ τ → Set where
      Step/app  :{τ1 τ2 : TType} {e e' : [] ⊢ τ1 ⇒ τ2} {e1 : [] ⊢ τ1}
             → e ↦ e'
             → (app e e1) ↦ (app e' e1)
      Step/β : {τ1 τ2 : TType} {e : [] ,, τ1 ⊢ τ2} {e1 : [] ⊢ τ1}
             → (app (lam e) e1) ↦ subst1 e1 e

    -- reflexive/transitive closure
    data _↦*_ : {τ : TType} → [] ⊢ τ → [] ⊢ τ → Set where
      Done : {τ : TType} {e : [] ⊢ τ} → e ↦* e
      Step : {τ : TType} {e1 e2 e3 : [] ⊢ τ}
           → e1 ↦ e2  →  e2 ↦* e3
           → e1 ↦* e3
  open OpSem

  {- Next, you will prove "very weak normalization".  The theorem is
     that any closed term *of base type b* evaluates to the constant c.
     No claims are made about terms of function type.
  -}
  module VeryWeakNormalization where

    WN : (τ : TType) → [] ⊢ τ → Set
    -- WN_τ(e) iff e ↦* c
    WN b e = e ↦* c
    -- WN_τ(e) iff for all e1 : τ1, if WN_τ1(e1) then WN_τ2(e e1)
    WN (τ1 ⇒ τ2) e = (e1 : [] ⊢ τ1) → WN τ1 e1 → WN τ2 (app e e1)

    -- extend WN to contexts and substitutions
    WNc : (Γ : Ctx) → [] ⊢c Γ → Set
    WNc [] θ = tt
    WNc (τ ∷ Γ) (θ , e) = WNc Γ θ × WN τ e

    {- TASK 3 : show that the relation is closed under head expansion: -}
    head-expand : (τ : TType) {e e' : [] ⊢ τ} → e ↦ e' → WN τ e' → WN τ e
    head-expand = {!!}

    {- TASK 4 : prove the fundamental theorem

    Hint: you may find it helpful to use
      transport : {A : Set} (B : A → Set) {a1 a2 : A} → a1 == a2 → (B a1 → B a2)
    to coerce by a propositional equality.
    -}
    fund : {Γ : Ctx} {τ : TType} {θ : [] ⊢c Γ}
         → (e : Γ ⊢ τ)
         → WNc Γ θ
         → WN τ (subst θ e)
    fund = {!!}

    {- TASK 5 : conclude weak normalization at base type -}
    corollary : (e : [] ⊢ b) → e ↦* c
    corollary = {!!}

  {- TASK 6 : change the definition of the logical relation so that you also can conclude normalization
              at function type.
  -}
  module WeakNormalization where

    open RenamingAndSubstitution using (addvar)
    --- you will want to use
    --    addvar : {Γ Γ' : Ctx} {τ : TType} → Γ ⊢c Γ' → (Γ ,, τ) ⊢c (Γ' ,, τ)

    -- Hint: you will need a couple of lemmas about ↦* that we didn't need above
    -- (I used three of them)

    {- TASK 6a -}
    corollary1 : (e : [] ⊢ b) → e ↦* c
    corollary1 e = {!!}

    {- TASK 6b -}
    corollary2 : {τ1 τ2 : TType} (e : [] ⊢ τ1 ⇒ τ2) → Σ \(e' : _) → e ↦* (lam e')
    corollary2 e = {!!}

max_stars_repo_name: ayberkt/system-t-normalization

max_issues_repo_name: ayberkt/system-t-normalization

max_forks_repo_name: ayberkt/system-t-normalization


text:
{-# OPTIONS --universe-polymorphism #-}
open import Categories.Category
open import Categories.Object.BinaryProducts
open import Categories.Object.Exponentiating

module Categories.Object.Exponentiating.Functor {o ℓ e}
    (C : Category o ℓ e)
    (binary : BinaryProducts C)
    (Σ : Category.Obj C)
    (exponentiating : Exponentiating C binary Σ) where

open Category C
open BinaryProducts binary
open Exponentiating exponentiating

open Equiv
open HomReasoning

import Categories.Object.Product.Morphisms
open Categories.Object.Product.Morphisms C

open import Categories.Functor
  using (Functor; Contravariant)
  renaming (_∘_ to _∘F_)

Σ↑-Functor : Contravariant C C
Σ↑-Functor = record
    { F₀            =  Σ↑_
    ; F₁            = [Σ↑_]
    ; identity      = identity
    ; homomorphism  = homomorphism
    ; F-resp-≡      = F-resp-≡
    }
    where
        .identity : ∀ {A} → [Σ↑ id {A} ] ≡ id
        identity {A} =
            begin
                λ-abs A (eval ∘ second id)
            ↓⟨ λ-cong (∘-resp-≡ refl (id⁂id product)) ⟩
                λ-abs A (eval ∘ id)
            ↓⟨ λ-cong identityʳ ⟩
                λ-abs A eval
            ↓⟨ λ-η-id ⟩
                id
            ∎

        .homomorphism : ∀ {X Y Z}
            {f : X ⇒ Y} {g : Y ⇒ Z}
            → [Σ↑ (g ∘ f) ] ≡ [Σ↑ f ] ∘ [Σ↑ g ]
        homomorphism {X}{Y}{Z}{f}{g} =
            begin
                λ-abs X (eval ∘ second (g ∘ f))
            ↑⟨ λ-cong (refl ⟩∘⟨ second∘second) ⟩
                λ-abs X (eval ∘ second g ∘ second f)
            ↑⟨ λ-cong assoc  ⟩
                λ-abs X ((eval ∘ second g) ∘ second f)
            ↓⟨ λ-distrib ⟩
                λ-abs X (eval ∘ second f)
                    ∘
                λ-abs Y (eval ∘ second g)
            ∎

        .F-resp-≡ : ∀ {A B}{f g : A ⇒ B }
            → f ≡ g → [Σ↑ f ] ≡ [Σ↑ g ]
        F-resp-≡ {A}{B}{f}{g} f≡g =
            begin
                λ-abs A (eval ∘ second f)
            ↓⟨ λ-cong (refl ⟩∘⟨ ⟨⟩-cong₂ refl (f≡g ⟩∘⟨ refl)) ⟩
                λ-abs A (eval ∘ second g)
            ∎

Σ²-Functor : Functor C C
Σ²-Functor = Σ↑-Functor ∘F Functor.op Σ↑-Functor


text:
-- Module shadowing using generated modules for records and datatypes
module Issue260c where

record R : Set where
module R where


text:
open import Structure.Setoid
open import Structure.Category
open import Type

module Structure.Category.Monad.ExtensionSystem
  {ℓₒ ℓₘ ℓₑ}
  {cat : CategoryObject{ℓₒ}{ℓₘ}{ℓₑ}}
  where

import      Data.Tuple as Tuple
import      Function.Equals
open        Function.Equals.Dependent
open import Functional.Dependent using () renaming (_∘_ to _∘ᶠⁿ_)
import      Lvl
open import Logic.Predicate
open import Structure.Category.Functor
open import Structure.Category.Functor.Functors as Functors
open import Structure.Category.Monad{cat = cat}
open import Structure.Category.NaturalTransformation
open import Structure.Category.NaturalTransformation.NaturalTransformations as NaturalTransformations
open import Structure.Category.Proofs
open import Structure.Categorical.Properties
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Syntax.Transitivity

open CategoryObject(cat)
open Category.ArrowNotation(category)
open Category(category)
open NaturalTransformations.Raw(cat)(cat)
private open module MorphismEquiv {x}{y} = Equivalence (Equiv-equivalence ⦃ morphism-equiv{x}{y} ⦄) using ()

record ExtensionSystem (T : Object → Object) : Type{Lvl.of(Type.of(cat))} where
  field
    η   : (x : Object) → (x ⟶ T(x))
    ext : ∀{x y} → (x ⟶ T(y)) → (T(x) ⟶ T(y))

  μ : (x : Object) → (T(T(x)) ⟶ T(x))
  μ(x) = ext(id{x = T(x)})

  field
    ⦃ ext-function ⦄ : ∀{x y} → Function(ext{x}{y})
    ext-inverse      : ∀{x} → (ext(η(x)) ≡ id) -- ext ∘ᶠⁿ η ⊜ idᴺᵀ
    ext-identity     : ∀{x y}{f : x ⟶ T(y)} → (ext(f) ∘ η(x) ≡ f)
    ext-distribute   : ∀{x y z}{f : y ⟶ T(z)}{g : x ⟶ T(y)} → (ext(ext(f) ∘ g) ≡ ext(f) ∘ ext(g))

  functor : Functor(category)(category)(T)
  Functor.map functor {x} {y} f = ext(η(y) ∘ f)
  Function.congruence (Functor.map-function functor) xy = congruence₁(ext) (congruence₂ᵣ(_∘_)(_) xy)
  Functor.op-preserving functor {x} {y} {z} {f} {g} =
    ext(η(z) ∘ f ∘ g)               🝖-[ congruence₁(ext) (Morphism.associativity(_∘_)) ]-sym
    ext((η(z) ∘ f) ∘ g)             🝖-[ congruence₁(ext) (congruence₂ₗ(_∘_)(g) (symmetry(_≡_) ext-identity)) ]
    ext((ext(η(z) ∘ f) ∘ η(y)) ∘ g) 🝖-[ congruence₁(ext) (Morphism.associativity(_∘_)) ]
    ext(ext(η(z) ∘ f) ∘ (η(y) ∘ g)) 🝖-[ ext-distribute ]
    ext(η(z) ∘ f) ∘ ext(η(y) ∘ g)   🝖-end
  Functor.id-preserving functor {x} =
    ext(η(x) ∘ id) 🝖-[ congruence₁(ext) (Morphism.identityᵣ(_∘_)(id)) ]
    ext(η(x))      🝖-[ ext-inverse ]
    id             🝖-end
  open Functor(functor)

  monad : Monad(T) ⦃ functor ⦄
  ∃.witness (Monad.Η monad) = η
  NaturalTransformation.natural (∃.proof (Monad.Η monad)) = symmetry(_≡_) ext-identity
  ∃.witness (Monad.Μ monad) = μ
  NaturalTransformation.natural (∃.proof (Monad.Μ monad)) {x} {y} {f} =
    μ(y) ∘ ext(η(T(y)) ∘ ext(η(y) ∘ f))      🝖[ _≡_ ]-[]
    ext(id) ∘ ext(η(T(y)) ∘ ext(η(y) ∘ f))   🝖-[ ext-distribute ]-sym
    ext(ext(id) ∘ (η(T(y)) ∘ ext(η(y) ∘ f))) 🝖-[ congruence₁(ext) (symmetry(_≡_) (Morphism.associativity(_∘_))) ]
    ext((ext(id) ∘ η(T(y))) ∘ ext(η(y) ∘ f)) 🝖-[ congruence₁(ext) (congruence₂ₗ(_∘_)(_) ext-identity) ]
    ext(id ∘ ext(η(y) ∘ f))                  🝖-[ congruence₁(ext) (Morphism.identityₗ(_∘_)(id)) ]
    ext(ext(η(y) ∘ f))                       🝖-[ congruence₁(ext) (Morphism.identityᵣ(_∘_)(id)) ]-sym
    ext(ext(η(y) ∘ f) ∘ id)                  🝖-[ ext-distribute ]
    ext(η(y) ∘ f) ∘ ext(id)                  🝖[ _≡_ ]-[]
    ext(η(y) ∘ f) ∘ μ(x)                     🝖-end
  _⊜_.proof (Monad.μ-functor-[∘]-commutativity monad) {x} = -- TODO: Same as above?
    μ(x) ∘ map(μ(x))                   🝖[ _≡_ ]-[]
    ext(id) ∘ map(ext(id))             🝖[ _≡_ ]-[]
    ext(id) ∘ ext(η(T(x)) ∘ ext(id))   🝖-[ ext-distribute ]-sym
    ext(ext(id) ∘ (η(T(x)) ∘ ext(id))) 🝖-[ congruence₁(ext) (symmetry(_≡_) (Morphism.associativity(_∘_))) ]
    ext((ext(id) ∘ η(T(x))) ∘ ext(id)) 🝖-[ congruence₁(ext) (congruence₂ₗ(_∘_)(_) ext-identity) ]
    ext(id ∘ ext(id))                  🝖-[ congruence₁(ext) (Morphism.identityₗ(_∘_)(id)) ]
    ext(ext(id))                       🝖-[ congruence₁(ext) (Morphism.identityᵣ(_∘_)(id)) ]-sym
    ext(ext(id) ∘ id)                  🝖-[ ext-distribute ]
    ext(id) ∘ ext(id)                  🝖[ _≡_ ]-[]
    μ(x) ∘ μ(T(x))                     🝖-end
  _⊜_.proof (Monad.μ-functor-[∘]-identityₗ monad) {x} =
    μ(x) ∘ ext(η(T(x)) ∘ η(x))      🝖[ _≡_ ]-[]
    ext(id) ∘ ext(η(T(x)) ∘ η(x))   🝖[ _≡_ ]-[ ext-distribute ]-sym
    ext(ext(id) ∘ (η(T(x)) ∘ η(x))) 🝖[ _≡_ ]-[ congruence₁(ext) (symmetry(_≡_) (Morphism.associativity(_∘_))) ]
    ext((ext(id) ∘ η(T(x))) ∘ η(x)) 🝖[ _≡_ ]-[ congruence₁(ext) (congruence₂ₗ(_∘_)(_) ext-identity) ]
    ext(id ∘ η(x))                  🝖[ _≡_ ]-[ congruence₁(ext) (Morphism.identityₗ(_∘_)(id)) ]
    ext(η(x))                       🝖[ _≡_ ]-[ ext-inverse ]
    id                              🝖[ _≡_ ]-end
  _⊜_.proof (Monad.μ-functor-[∘]-identityᵣ monad) {x} =
    μ(x) ∘ η(T(x))    🝖[ _≡_ ]-[]
    ext(id) ∘ η(T(x)) 🝖[ _≡_ ]-[ ext-identity ]
    id                🝖[ _≡_ ]-end

  -- Also called: Kleisli composition.
  _∘ₑₓₜ_ : ∀{x y z} → (y ⟶ T(z)) → (x ⟶ T(y)) → (x ⟶ T(z))
  f ∘ₑₓₜ g = ext(f) ∘ g

  idₑₓₜ : ∀{x} → (x ⟶ T(x))
  idₑₓₜ{x} = η(x)

  module FunctionalNames where
    -- Name sources:
    --   https://wiki.haskell.org/Lifting
    -- Also called: unit.
    lift : ∀{x} → (x ⟶ T(x))
    lift{x} = η(x)

    -- Name sources:
    --   Javascript: Array.prototype.flat
    --   Scala: scala.collection.IterableOnceOps.flatten
    flatten : ∀{x} → (T(T(x)) ⟶ T(x))
    flatten{x} = μ(x)

    -- Name sources:
    --   Javascript: Array.prototype.flatMap
    --   Java: Stream.flatMap
    --   Scala: scala.collection.IterableOnceOps.flatMap
    flatMap : ∀{x y} → (x ⟶ T(y)) → (T(x) ⟶ T(y))
    flatMap = ext

  module HaskellNames where
    return = FunctionalNames.lift
    join   = FunctionalNames.flatten
    bind   = FunctionalNames.flatMap

module _ where
  open Functor ⦃ … ⦄
  open Monad   ⦃ … ⦄

  monad-to-extensionSystem : ∀{T : Object → Object} → ⦃ functor : Functor(category)(category)(T) ⦄ → ⦃ monad : Monad(T) ⦄ → ExtensionSystem(T)
  ExtensionSystem.η   (monad-to-extensionSystem ⦃ functor ⦄ ⦃ monad ⦄) = η
  ExtensionSystem.ext (monad-to-extensionSystem ⦃ functor ⦄ ⦃ monad ⦄) = ext
  Function.congruence (ExtensionSystem.ext-function monad-to-extensionSystem  {x} {y}) {f} {g} fg =
    ((μ(y) ∘_) ∘ᶠⁿ map) f 🝖[ _≡_ ]-[]
    μ(y) ∘ map f          🝖[ _≡_ ]-[ congruence₂ᵣ(_∘_) _ (congruence₁(map) fg) ]
    μ(y) ∘ map g          🝖[ _≡_ ]-[]
    ((μ(y) ∘_) ∘ᶠⁿ map) g 🝖[ _≡_ ]-end
  ExtensionSystem.ext-inverse monad-to-extensionSystem {x} =
    ((μ(x) ∘_) ∘ᶠⁿ map)(η(x)) 🝖[ _≡_ ]-[]
    μ(x) ∘ map(η(x))          🝖[ _≡_ ]-[ _⊜_.proof μ-functor-[∘]-identityₗ ]
    id                        🝖[ _≡_ ]-end
  ExtensionSystem.ext-identity (monad-to-extensionSystem {T = T}) {x} {y} {f} =
    ((μ(y) ∘_) ∘ᶠⁿ map)(f) ∘ η(x) 🝖[ _≡_ ]-[]
    (μ(y) ∘ (map f)) ∘ η(x)       🝖[ _≡_ ]-[ Morphism.associativity(_∘_) ]
    μ(y) ∘ ((map f) ∘ η(x))       🝖[ _≡_ ]-[ congruence₂ᵣ(_∘_) _ η-natural ]-sym
    μ(y) ∘ (η(T(y)) ∘ f)          🝖[ _≡_ ]-[ Morphism.associativity(_∘_) ]-sym
    (μ(y) ∘ η(T(y))) ∘ f          🝖[ _≡_ ]-[ congruence₂ₗ(_∘_) _ (_⊜_.proof μ-functor-[∘]-identityᵣ) ]
    id ∘ f                        🝖[ _≡_ ]-[ Morphism.identityₗ(_∘_)(id) ]
    f                             🝖[ _≡_ ]-end
  ExtensionSystem.ext-distribute (monad-to-extensionSystem {T = T}) {x} {y} {z} {f} {g} =
    ((μ(z) ∘_) ∘ᶠⁿ map)(((μ(z) ∘_) ∘ᶠⁿ map)(f) ∘ g) 🝖[ _≡_ ]-[]
    μ(z) ∘ map((μ(z) ∘ (map f)) ∘ g)                🝖[ _≡_ ]-[ congruence₂ᵣ(_∘_) _ op-preserving ]
    μ(z) ∘ (map(μ(z) ∘ (map f)) ∘ (map g))          🝖[ _≡_ ]-[ congruence₂ᵣ(_∘_) _ (congruence₂ₗ(_∘_) _ op-preserving) ]
    μ(z) ∘ ((map(μ(z)) ∘ map(map f)) ∘ (map g))     🝖[ _≡_ ]-[ associate4-231-121 category ]
    (μ(z) ∘ map(μ(z))) ∘ (map(map f) ∘ (map g))     🝖[ _≡_ ]-[ congruence₂ₗ(_∘_) _ (_⊜_.proof μ-functor-[∘]-commutativity) ]
    (μ(z) ∘ μ(T(z))) ∘ (map(map f) ∘ (map g))       🝖[ _≡_ ]-[ associate4-213-121 category ]-sym
    (μ(z) ∘ (μ(T(z)) ∘ map(map f))) ∘ (map g)       🝖[ _≡_ ]-[ congruence₂ₗ(_∘_) _ (congruence₂ᵣ(_∘_) _ μ-natural) ]
    (μ(z) ∘ ((map f) ∘ μ(y))) ∘ (map g)             🝖[ _≡_ ]-[ associate4-213-121 category ]
    (μ(z) ∘ (map f)) ∘ (μ(y) ∘ (map g))             🝖[ _≡_ ]-[]
    ((μ(z) ∘_) ∘ᶠⁿ map)(f) ∘ ((μ(y) ∘_) ∘ᶠⁿ map)(g) 🝖[ _≡_ ]-end

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import Level
open import Categories.Category
open import Categories.Monad

module Categories.Monad.Idempotent {o ℓ e} {C : Category o ℓ e} (M : Monad C) where

open import Categories.NaturalTransformation
open import Categories.NaturalTransformation.Equivalence
open import Categories.Functor

private
  module M = Monad M

open NaturalTransformation

record Idempotent : Set (o ⊔ ℓ ⊔ e) where
  field
    Fη≡ηF : ∀ X → C [ η (M.F ∘ˡ M.η) X ≈ η (M.η ∘ʳ M.F) X ]

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{- Formal verification of authenticated append-only skiplists in Agda, version 1.0.

   Copyright (c) 2021 Victor C Miraldo and Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import Data.Unit.NonEta
open import Data.Empty
open import Data.Sum
open import Data.Product
open import Data.Product.Properties
open import Data.Fin hiding (_<_; _≤_)
open import Data.Fin.Properties using () renaming (_≟_ to _≟Fin_)
open import Data.Nat renaming (_≟_ to _≟ℕ_; _≤?_ to _≤?ℕ_)
open import Data.Nat.Properties
open import Data.List renaming (map to List-map)
open import Data.List.Properties using (∷-injective; length-map)
open import Data.List.Relation.Unary.Any renaming (map to Any-map)
open import Data.List.Relation.Unary.All renaming (lookup to All-lookup; map to All-map)
open import Data.List.Relation.Unary.All.Properties hiding (All-map)
open import Data.List.Relation.Unary.Any.Properties renaming (map⁺ to Any-map⁺)
open import Data.List.Relation.Binary.Pointwise using (decidable-≡)
open import Data.Bool hiding (_<_; _≤_)
open import Data.Maybe renaming (map to Maybe-map)
open import Function

open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Definitions
open import Relation.Nullary

open import AAOSL.Lemmas
open import AAOSL.Abstract.Hash
open import AAOSL.Abstract.DepRel

module AAOSL.Abstract.EvoCR
   -- A Hash function maps a bytestring into a hash.
   (hash    : ByteString → Hash)
   -- And is collision resistant
   (hash-cr : ∀{x y} → hash x ≡ hash y → Collision hash x y ⊎ x ≡ y)

   -- Indexes can be encoded in an injective way
   (encodeI     : ℕ → ByteString)
   (encodeI-inj : (m n : ℕ) → encodeI m ≡ encodeI n → m ≡ n)

   (dep  : DepRel)
 where

  open WithCryptoHash hash hash-cr
  open import AAOSL.Abstract.Advancement hash hash-cr encodeI encodeI-inj dep
  open DepRel dep

  -- Returns the last element on path a that is smaller than k
  last-bef : ∀{j i k}(a : AdvPath j i)(i<k : i < k)(k≤j : k ≤′ j) → ℕ
  last-bef {j} a i<k ≤′-refl = j
  -- TODO-1 : The same or similar proof is repeated numerous times below; refactor for clarity
  last-bef AdvDone i<k (≤′-step k≤j) = ⊥-elim (1+n≰n (≤-unstep (≤-trans i<k (≤′⇒≤ k≤j))))
  last-bef {k = k} (AdvThere d h a) i<k (≤′-step k≤j)
    with hop-tgt h ≤?ℕ k
  ...| yes th≤k = hop-tgt h
  ...| no th>k = last-bef a i<k (≤⇒≤′ (≰⇒≥ th>k))

  last-bef-correct : ∀{j i k}(a : AdvPath j i)(i<k : i < k)(k≤j : k ≤′ j)
                   → last-bef a i<k k≤j ∈AP a
  last-bef-correct {j} a i<k ≤′-refl = ∈AP-src
  last-bef-correct AdvDone i<k (≤′-step k≤j) = ⊥-elim (1+n≰n (≤-unstep (≤-trans i<k (≤′⇒≤ k≤j))))
  last-bef-correct {k = k} (AdvThere d h a) i<k (≤′-step k≤j)
    with hop-tgt h ≤?ℕ k
  ...| yes th≤k = step (<⇒≢ (hop-< h)) ∈AP-src
  ...| no th>k
    with last-bef-correct a i<k (≤⇒≤′ (≰⇒≥ th>k))
  ...| ind = step (<⇒≢ (≤-trans (s≤s (∈AP-≤ ind)) (hop-< h))) ind

  lemma5-hop : ∀{j i}(a : AdvPath j i)
             → ∀{k} → j < k
             → (h : HopFrom k) → hop-tgt h ≤ j → i ≤ hop-tgt h → hop-tgt h ∈AP a
  lemma5-hop {j} a j<k h th≤j i≤th
    with hop-tgt h ≟ℕ j
  ...| yes th≡j rewrite th≡j = ∈AP-src
  ...| no th≢j
    with a
  ...| AdvDone rewrite ≤-antisym th≤j i≤th = hereTgtDone
  ...| (AdvThere x h' a')
    with hop-tgt h' ≟ℕ hop-tgt h
  ...| yes th'≡th rewrite sym th'≡th = step (<⇒≢ (hop-< h')) ∈AP-src
  ...| no th'≢th
    with hop-tgt h' ≤?ℕ hop-tgt h
  ...| yes th'≤th = ⊥-elim (1+n≰n (≤-trans j<k (hops-nested-or-nonoverlapping (≤∧≢⇒< th'≤th th'≢th) (≤∧≢⇒< th≤j th≢j))))
  ...| no th'>th = step th≢j (lemma5-hop a' (≤-trans (hop-< h') (≤-unstep j<k)) h (≰⇒≥ th'>th) i≤th)

  lemma5 : ∀{j i k}(a : AdvPath j i)(i<k : i < k)(k≤j : k ≤′ j)
         → ∀{i₀}(b : AdvPath k i₀) → i₀ ≤ i
         → last-bef a i<k k≤j ∈AP b
  lemma5 a i<k ≤′-refl b i₀≤i = ∈AP-src
  lemma5 AdvDone i<k (≤′-step k≤j) b i₀≤i = ⊥-elim (1+n≰n (≤-unstep (≤-trans i<k (≤′⇒≤ k≤j))))
  lemma5 {k = k} (AdvThere d h a) i<k (≤′-step k≤j) b i₀≤i
       with hop-tgt h ≤?ℕ k
  ...| yes th≤k = lemma5-hop b (s≤s (≤′⇒≤ k≤j)) h th≤k (≤-trans i₀≤i (lemma1 a))
  ...| no th>k = lemma5 a i<k (≤⇒≤′ (≰⇒≥ th>k)) b i₀≤i

  -- returns the first element on path a that is greather than k
  first-aft : ∀{j i k}(a : AdvPath j i)(i≤k : i ≤′ k)(k<j : k < j) → ℕ
  first-aft {i = i} a ≤′-refl k<j = i
  first-aft AdvDone (≤′-step i≤k) k<j = ⊥-elim (1+n≰n (≤-unstep (≤-trans k<j (≤′⇒≤ i≤k))))
  first-aft {j} {i} {k} (AdvThere d h a) (≤′-step i≤k) k<j
    with hop-tgt h ≟ℕ k
  ...| yes _ = k
  ...| no th≢k
    with hop-tgt h ≤?ℕ k
  ...| yes th≤k = j
  ...| no th≥k = first-aft a (≤′-step i≤k) (≰⇒> th≥k)

  first-aft-correct : ∀{j i k}(a : AdvPath j i)(i≤k : i ≤′ k)(k<j : k < j)
                    → first-aft a i≤k k<j ∈AP a
  first-aft-correct a ≤′-refl k<j = ∈AP-tgt
  first-aft-correct AdvDone (≤′-step i≤k) k<j = ⊥-elim (1+n≰n (≤-unstep (≤-trans k<j (≤′⇒≤ i≤k))))
  first-aft-correct {j} {i} {k} (AdvThere d h a) (≤′-step i≤k) k<j
    with hop-tgt h ≟ℕ k
  ...| yes th≡k rewrite sym th≡k = step (<⇒≢ k<j) ∈AP-src
  ...| no th≢k
    with hop-tgt h ≤?ℕ k
  ...| yes th≤k = ∈AP-src
  ...| no th≥k
    with first-aft-correct a (≤′-step i≤k) (≰⇒> th≥k)
  ...| ind = step (<⇒≢ (≤-trans (s≤s (∈AP-≤ ind)) (hop-< h))) ind

  lemma5'-hop
    : ∀{j j₁ k}(h : HopFrom j)
    → hop-tgt h < k → k < j → (b : AdvPath j₁ k) → j ≤ j₁ → j ∈AP b
  lemma5'-hop {j} {j₁} h th<k k≤j b j≤j₁
    with j ≟ℕ j₁
  ...| yes refl = ∈AP-src
  ...| no j≢j₁
    with b
  ...| AdvDone = ⊥-elim (1+n≰n (≤-trans k≤j j≤j₁))
  ...| (AdvThere x hb b')
    with hop-tgt hb ≟ℕ j
  ...| yes refl = step (<⇒≢ (hop-< hb)) ∈AP-src
  ...| no tb≢j
    with hop-tgt hb ≤?ℕ j
  ...| no tb≰j = step j≢j₁ (lemma5'-hop h th<k k≤j b' (≰⇒≥ tb≰j))
  ...| yes tb≤j
    with hops-nested-or-nonoverlapping (≤-trans th<k (lemma1 b')) (≤∧≢⇒< tb≤j tb≢j)
  ...| j₁≤j rewrite ≤-antisym j≤j₁ j₁≤j = ∈AP-src

  lemma5' : ∀{j i k}(a : AdvPath j i)(i≤k : i ≤′ k)(k<j : k < j)
          → ∀{j₁}(b : AdvPath j₁ k) → j ≤ j₁
          → first-aft a i≤k k<j ∈AP b
  lemma5' a ≤′-refl k<j b j≤j₁ = ∈AP-tgt
  lemma5' AdvDone (≤′-step i≤k) k<j b j≤j₁ = ⊥-elim (1+n≰n (≤-unstep (≤-trans k<j (≤′⇒≤ i≤k))))
  lemma5' {j} {i} {k} (AdvThere d h a) (≤′-step i≤k) k<j b j≤j₁
    with hop-tgt h ≟ℕ k
  ...| yes _ = ∈AP-tgt
  ...| no th≢k
    with hop-tgt h ≤?ℕ k
  ...| yes th≤k = lemma5'-hop h (≤∧≢⇒< th≤k th≢k) k<j b j≤j₁
  ...| no th≥k = lemma5' a (≤′-step i≤k) (≰⇒> th≥k) b (≤-unstep (≤-trans (hop-< h) j≤j₁))

  ∈AP-⊕-intro-l : ∀{j k i m}
                → {a₂  : AdvPath j k}{a₁ : AdvPath k i}
                → m ∈AP a₂
                → m ∈AP (a₂ ⊕ a₁)
  ∈AP-⊕-intro-l hereTgtThere = hereTgtThere
  ∈AP-⊕-intro-l (step prog m∈a) = step prog (∈AP-⊕-intro-l m∈a)
  ∈AP-⊕-intro-l {a₁ = AdvDone} hereTgtDone = hereTgtDone
  ∈AP-⊕-intro-l {a₁ = AdvThere d h a} hereTgtDone = hereTgtThere

  ∈AP-⊕-intro-r : ∀{j k i m}
                → {a₂  : AdvPath j k}{a₁ : AdvPath k i}
                → m ∈AP a₁
                → m ∈AP (a₂ ⊕ a₁)
  ∈AP-⊕-intro-r {a₂ = AdvDone} hyp = hyp
  ∈AP-⊕-intro-r {k = k} {a₂ = AdvThere d h a} hyp =
      step (<⇒≢ (≤-trans (s≤s (∈AP-≤ hyp)) (≤-trans (s≤s (lemma1 a)) (hop-< h))))
           (∈AP-⊕-intro-r {a₂ = a} hyp)

  ∈AP-⊕-≤-r : ∀{j k i m}{a₂  : AdvPath j k}{a₁ : AdvPath k i}
            → m ∈AP (a₂ ⊕ a₁)
            → m ≤ k
            → m ∈AP a₁
  ∈AP-⊕-≤-r {a₂ = AdvDone} m∈a12 m≤k = m∈a12
  ∈AP-⊕-≤-r {a₂ = AdvThere d h a₂} hereTgtThere m≤k = ⊥-elim (1+n≰n (≤-trans (≤-trans (s≤s (lemma1 a₂)) (hop-< h)) m≤k))
  ∈AP-⊕-≤-r {a₂ = AdvThere d h a₂} (step x m∈a12) m≤k
    = ∈AP-⊕-≤-r m∈a12 m≤k

  findM : ∀ {j i₂ s₁ s₂ tgt}
          → (a₁₁ : AdvPath j s₁)
          → (a₂₁ : AdvPath j s₂)
          → (a₂₂ : AdvPath s₂ i₂)
          → (m₂ : MembershipProof s₂ tgt)
          → i₂ ≤ s₁
          → tgt ≤ s₁
          → s₁ ≤ s₂
          → ∃[ M ] (M ∈AP a₂₂ × M ∈AP mbr-proof m₂ × M ∈AP a₁₁)
  findM {s₁ = s₁} {s₂} a₁₁ a₂₁ a₂₂ m₂ i₂≤s₁ t≤s₁ s₁≤s₂
     with <-cmp s₁ s₂
  ...| tri> _ _ s₂<s₁ = ⊥-elim (<⇒≢ s₂<s₁ (sym (≤-antisym s₁≤s₂ (≤-unstep s₂<s₁))))
  ...| tri≈ _ refl _  = s₁ , ∈AP-src , ∈AP-src , ∈AP-tgt
  ...| tri< s₁<s₂ _ _ = last-bef a₁₁ s₁<s₂ (≤⇒≤′ (lemma1 a₂₁))
                      , lemma5 a₁₁ s₁<s₂ (≤⇒≤′ (lemma1 a₂₁)) a₂₂ i₂≤s₁
                      , lemma5 a₁₁ s₁<s₂ (≤⇒≤′ (lemma1 a₂₁)) (mbr-proof m₂) t≤s₁
                      , last-bef-correct a₁₁ s₁<s₂ (≤⇒≤′ (lemma1 a₂₁))

  findR : ∀{j i₁ s₁ s₂ tgt}
          → (a₁₁ : AdvPath j s₁)
          → (a₁₂ : AdvPath s₁ i₁)
          → (a₂₁ : AdvPath j s₂)
          → (m₁ : MembershipProof s₁ tgt)(m₂ : MembershipProof s₂ tgt)
          → i₁ ≤ tgt
          → tgt ≤ s₁
          → s₁ ≤ s₂ -- wlog
          → ∃[ R ] (R ∈AP mbr-proof m₁ × R ∈AP mbr-proof m₂ × R ∈AP a₁₂)
  findR {s₁ = s₁} {tgt = tgt} a₁₁ a₁₂ a₂₁ m₁ m₂ i₁≤t t≤s₁ s₁≤s₂
    with <-cmp tgt s₁
  ...| tri> _ _ s₁<t = ⊥-elim (<⇒≢ s₁<t (sym (≤-antisym t≤s₁ (≤-unstep s₁<t))))
  ...| tri≈ _ refl _ = s₁ , ∈AP-src , ∈AP-tgt , ∈AP-src
  ...| tri< t<s₁ _ _ = first-aft a₁₂ (≤⇒≤′ i₁≤t) t<s₁
                       , lemma5' a₁₂ (≤⇒≤′ i₁≤t) t<s₁ (mbr-proof m₁) ≤-refl
                       , lemma5' a₁₂ (≤⇒≤′ i₁≤t) t<s₁ (mbr-proof m₂) s₁≤s₂
                       , first-aft-correct a₁₂ (≤⇒≤′ i₁≤t) t<s₁

  -- check Figure 4 (page 12) in: https://arxiv.org/pdf/cs/0302010.pdf
  --
  -- a₁ is dashed black line
  -- a₂ is dashed gray line
  -- m₁ is thick black line
  -- m₂ is thick gray line
  -- s₁ is j
  -- s₂ is k
  -- j is n
  -- tgt is i
  evo-cr : ∀{j i₁ i₂}{t₁ t₂ : View}
          → (a₁ : AdvPath j i₁)
          → (a₂ : AdvPath j i₂)
          → rebuild a₁ t₁ j ≡ rebuild a₂ t₂ j
          → ∀{s₁ s₂ tgt}{u₁ u₂ : View}
          → (m₁ : MembershipProof s₁ tgt)(m₂ : MembershipProof s₂ tgt)
          → s₁ ∈AP a₁ → s₂ ∈AP a₂
          → s₁ ≤ s₂ -- wlog
          → i₁ ≤ tgt
          → i₂ ≤ tgt
          → rebuildMP m₁ u₁ s₁ ≡ rebuild a₁ t₁ s₁
          → rebuildMP m₂ u₂ s₂ ≡ rebuild a₂ t₂ s₂
          → HashBroke ⊎ (mbr-datum m₁ ≡ mbr-datum m₂)
  evo-cr {t₁ = t₁} {t₂} a₁ a₂ hyp {s₁} {s₂} {tgt} {u₁} {u₂}
      m₁ m₂ s₁∈a₁ s₂∈a₂ s₁≤s₂ i₁≤t i₂≤t c₁ c₂
    with ∈AP-cut a₁ s₁∈a₁ | ∈AP-cut a₂ s₂∈a₂
  ...| ((a₁₁ , a₁₂) , refl) | ((a₂₁ , a₂₂) , refl)
    with lemma1 (mbr-proof m₁)
  ...| t≤s₁
  -- The first part of the proof is find some points common to three
  -- of the provided proofs. This is given in Figure 4 of Maniatis and Baker,
  -- and they are called M and R too, to help make it at least a little clear.
  -- First we find a point that belongs in a₂, m₁ and a₁.
    with findM a₁₁ a₂₁ a₂₂ m₂ (≤-trans i₂≤t t≤s₁) t≤s₁ s₁≤s₂
  ...| M , M∈a₂₂ , M∈m₂ , M∈a₁₁
  -- Next, we find a point that belongs in m₁, m₂ and a₁.
    with findR a₁₁ a₁₂ a₂₁ m₁ m₂ i₁≤t t≤s₁ s₁≤s₂
  ...| R , R∈m₁ , R∈m₂ , R∈a₁₂
  -- Now, since a₁ and a₂ rebuild to the same hash and M belongs
  -- to both these proofs, the hash for M is the same.
    with AgreeOnCommon a₁ a₂ hyp (∈AP-⊕-intro-l M∈a₁₁) (∈AP-⊕-intro-r M∈a₂₂)
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ M-a1a2
  -- Similarly, for a₂₂ and m₂
    with AgreeOnCommon a₂₂ (mbr-proof m₂) (trans (sym (rebuild-⊕ a₂₁ a₂₂ ∈AP-src)) (sym c₂)) M∈a₂₂ M∈m₂
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ M-a22m2
  -- Which brings us to: rebuild a1 M == rebuild m2 M
    with trans (trans M-a1a2 (rebuild-⊕ a₂₁ a₂₂ M∈a₂₂)) M-a22m2
  ...| M-a1m2
  -- If a1 and m2 agree on one point, they agree on all points. In particular, they
  -- agree on R!
    with ∈AP-cut (mbr-proof m₂) M∈m₂
  ...| ((m₂₁ , m₂₂) , refl)
    with trans M-a1m2 (rebuild-⊕ m₂₁ m₂₂ ∈AP-src)
  ...| M-a1m22
    with AgreeOnCommon-∈ a₁ m₂₂ (∈AP-⊕-intro-l M∈a₁₁) M-a1m22
           (∈AP-⊕-intro-r R∈a₁₂) (∈AP-⊕-≤-r R∈m₂ (≤-trans (∈AP-≤ R∈a₁₂) (∈AP-≥ M∈a₁₁)))
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ R-a1m22
    with AgreeOnCommon a₁₂ (mbr-proof m₁) (trans (sym (rebuild-⊕ a₁₁ a₁₂ ∈AP-src)) (sym c₁)) R∈a₁₂ R∈m₁
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ R-a12m1
  -- Which finally lets us argue that m1 and m2 also agree on R. Similarly, if they agree
  -- on one point they agree on all points.
    with ∈AP-cut (mbr-proof m₁) R∈m₁
  ...| ((m₁₁ , m₁₂) , refl)
    with trans (trans (trans (sym R-a1m22) (rebuild-⊕ a₁₁ a₁₂ R∈a₁₂)) R-a12m1) (rebuild-⊕ m₁₁ m₁₂ ∈AP-src)
  ...| R-m22m12
    with AgreeOnCommon-∈ m₂₂ m₁₂ (∈AP-⊕-≤-r R∈m₂ (≤-trans (∈AP-≤ R∈a₁₂) (∈AP-≥ M∈a₁₁))) R-m22m12 ∈AP-tgt ∈AP-tgt
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ tgt-m22m12
    with trans (rebuild-⊕ m₂₁ m₂₂ ∈AP-tgt) (trans tgt-m22m12 (sym (rebuild-⊕ m₁₁ m₁₂ ∈AP-tgt)))
  ...| tgt-m1m2 with rebuild-tgt-lemma (mbr-proof m₁)
                       {u₁ ∪₁ (tgt , auth tgt (mbr-datum m₁) u₁) }
                   | rebuild-tgt-lemma (mbr-proof m₂)
                       {u₂ ∪₁ (tgt , auth tgt (mbr-datum m₂) u₂) }
  ...| l1 | l2
    with trans (sym l1) (trans (sym tgt-m1m2) l2)
  ...| auths≡
    rewrite ≟ℕ-refl tgt = auth-inj-1 {tgt} {mbr-datum m₁} {mbr-datum m₂} (mbr-not-init m₁) auths≡

max_stars_repo_name: cwjnkins/aaosl-agda

max_issues_repo_name: cwjnkins/aaosl-agda

max_forks_repo_name: cwjnkins/aaosl-agda


text:
-- | Examples for SDE.

module SDE-Example where

open import Size
import Level
open import Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P hiding ([_])
open ≡-Reasoning

open import Data.Product as Prod renaming (Σ to ⨿)
open import Data.Nat as Nat
open import Data.Sum as Sum
open import Data.Fin hiding (_+_)

open import Streams
open import SDE

-- Example: Basic operations over streams over naturals
[_] : ∀{i} → ℕ → Stream {i} ℕ
hd [ n ] = n
tl [ n ] = [ 0 ]

_⊕_ : ∀ {i} → Stream {i} ℕ → Stream {i} ℕ → Stream {i} ℕ
hd (x ⊕ y) = hd x + hd y
tl (x ⊕ y) = tl x ⊕ tl y

_⊗_ : ∀{i} → Stream {i} ℕ → Stream {i} ℕ → Stream {i} ℕ
hd (x ⊗ y)           = hd x * hd y
tl (_⊗_ {i} x y) {j} = (tl x ⊗ y) ⊕ ([ hd x ] ⊗ (tl y))

_•_ : ∀{i} → Stream {i} ℕ → Stream {i} ℕ → Stream {i} ℕ
hd (x • y) = hd x
tl (x • y) = tl y ⊗ (tl x • y)

--------- Example for syntactic SDE.
-- We define symbols iₙ (n ∈ ℕ), p and c through SDEs for streams
-- over natural numbers. Here, iₙ is the injection of the number n into streams
-- and corresponds to [n], p is stream addition, and c is the convolution
-- product. The SDEs are the usual ones:
-- (iₙ)(0) = n
-- (iₙ)'   = i₀
-- (p s t)(0) = s(0) + t(0)
-- (p s t)'   = p s' t'
-- (c s t)(0) = s(0) * t(0)
-- (c s t)'   = p (c s' t) (c i_{s(0)} t')

-- First, we define the signature, which has ℕ-many symbols for the iₙ of
-- arity 0 and two symbols (p and c) of arity 2.
Σ : Sig
Σ = record { ∥_∥ = ℕ ⊎ Fin 2 ; ar = ar-Σ }
  where
    ar-Σ : ℕ ⊎ Fin 2 → Set
    ar-Σ (inj₁ _)       = Fin 0
    ar-Σ (inj₂ zero)    = Fin 2
    ar-Σ (inj₂ (suc _)) = Fin 2

-- Short-hand notations for the symbols.

-- | Injections iₙ
i : ℕ → ∥ Σ ∥
i n = inj₁ n

-- | Plus
p : ∥ Σ ∥
p = inj₂ (# 0)

-- | Convolution product
c : ∥ Σ ∥
c = inj₂ (# 1)

-- | We are going to define the SDEs by means of two variabls, later called x
-- and y.
X : Set
X = Fin 2

open Terms Σ public
open SDE-Impl Σ X public

-- | Short-hand names for variables and the variables denoting the corresponding
-- derivatives.
x y x' y' : V
x = inj₁ (# 0)
y = inj₁ (# 1)
x' = inj₂ (# 0)
y' = inj₂ (# 1)

-- Term constructors
i₁ : ℕ → T V
i₁ n = sup (inj₁ (i n , (λ ())))

p₁ : T V → T V → T V
p₁ t s = sup (inj₁ (p , α))
   where
     α : Fin 2 → T V
     α zero    = t
     α (suc _) = s

c₁ : T V → T V → T V
c₁ t s = sup (inj₁ (c , α))
   where
     α : Fin 2 → T V
     α zero    = t
     α (suc _) = s

-- | SDEs describing iₙ, ⊕ and ⊗
E : SDE ℕ
E (inj₁ n) = (λ _ → n) , (λ _ → sup (inj₁ (i 0 , (λ ()))))
E (inj₂ zero) = out , step
  where
    out : (Fin 2 → ℕ) → ℕ
    out r = r (# 0) + r (# 1)

    step : (Fin 2 → ℕ) → T V
    step _ = p₁ (η x') (η y')
E (inj₂ (suc _)) = out , step
  where
    out : (Fin 2 → ℕ) → ℕ
    out r = r (# 0) * r (# 1)

    step : (Fin 2 → ℕ) → T V
    step o = p₁
             (c₁ (η x') (η y))
             (c₁ (i₁ (o (# 0))) (η y'))

-- | Assignment of variables to positions of the symbols of our SDEs
vars : (f : ∥ Σ ∥) → ar Σ f → X
vars (inj₁ x)       ()
vars (inj₂ zero)    x = x
vars (inj₂ (suc _)) x = x

-- | Standard variable assignment.
put : ∀ {i} → Stream {i} ℕ → Stream {i} ℕ → (X → Stream {i} ℕ)
put s t zero    = s
put s t (suc _) = t

-- | Dummy stream for unused variables
dummy : Stream ℕ
hd dummy = 0
tl dummy = dummy

-- | Define injection [_] from SDE
[_]' : ℕ → Stream ℕ
[ n ]' = ⟦ E ⟧ vars (i n) (put dummy dummy)

-- | The addition of the streams s and t can be given by the interpretation
-- of the symbol p of the SDE above with variable assignment (x ↦ s, y ↦ t).
_⊕'_ : ∀ {i} → Stream {i} ℕ → Stream {i} ℕ → Stream {i} ℕ
s ⊕' t = ⟦ E ⟧ vars p (put s t)

_⊗'_ : ∀ {i} → Stream {i} ℕ → Stream {i} ℕ → Stream {i} ℕ
s ⊗' t = ⟦ E ⟧ vars c (put s t)

------ Correctness for the examples

-- We cheat a bit for now
postulate
  ext : Extensionality Level.zero Level.zero

-- | The interpretation of the SDE for stream addition has indeed the
-- same behaviour as the direct implemenentation.
correct-⊕ : ∀ {s t} → (s ⊕ t) ~ (s ⊕' t)
correct-⊕ = ex-bisimulation→bisim is-bisim rel
  where
    -- Bisimulation relating s ⊕ t and the interpretation of p with
    -- variable assignment (x ↦ s, y ↦ t).
    _R_ : Rel (Stream ℕ) _
    x R y = ∃ λ s →
            ∃ λ t →
            x ≡ s ⊕ t ×
            y ≡ ⟦ E ⟧ vars p (put s t)

    -- Recall that we have s ⊕' t = ⟦ E ⟧ vars p (put s t), which allows
    -- us to prove the following.
    rel : ∀{s t} → (s ⊕ t) R (s ⊕' t)
    rel {s} {t} = (s , t , refl , refl)

    lem : ∀{x y} (z : X) → tl (put x y z) ≡ put (tl x) (tl y) z
    lem zero = refl
    lem (suc z) = refl

    is-bisim : Is-Bisim _R_
    is-bisim x y (s , t , x=⊕ , y=E) = hd-≡ , tl-R
      where
        hd-≡ : hd x ≡ hd y
        hd-≡ =
          begin
            hd x
          ≡⟨ cong hd x=⊕ ⟩
            hd (s ⊕ t)
          ≡⟨ refl ⟩
            hd (⟦ E ⟧ vars p (put s t))
          ≡⟨ cong hd (sym y=E) ⟩
            hd y
          ∎

        tl-R : (tl x) R (tl y)
        tl-R = (tl s , tl t , u' , v)
          where
            u' : tl x ≡ tl s ⊕ tl t
            u' =
              begin
                tl x
              ≡⟨ cong (λ x → tl x {∞}) x=⊕ ⟩
                tl (s ⊕ t)
              ≡⟨ refl ⟩
                tl s ⊕ tl t
              ∎

            -- This uses, for now, extensionality
            v : tl y ≡ ⟦ E ⟧ vars p (put (tl s) (tl t))
            v =
              begin
                tl y
              ≡⟨ cong (λ x₁ → tl x₁ {∞}) y=E ⟩
                tl (⟦ E ⟧ vars p (put s t))
              ≡⟨ refl ⟩
                ⟦ E ⟧₁ vars (p₁ (sup (inj₂ x')) (sup (inj₂ y'))) (put s t)
              ≡⟨ refl ⟩
                ⟦ E ⟧ vars p (λ x → tl ((put s t) x))
              ≡⟨ cong (⟦ E ⟧ vars p) (ext lem) ⟩
                ⟦ E ⟧ vars p (put (tl s) (tl t))
              ∎

-- Conjecture.
correct-⊗ : ∀ {s t} → (s ⊗ t) ~ (s ⊗' t)
correct-⊗ = {!!}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Tarski-style semantics with contexts as concrete worlds, and glueing for α, ▻, and □.
-- Gentzen-style syntax.

module BasicIS4.Semantics.TarskiOvergluedGentzen where

open import BasicIS4.Syntax.Common public
open import Common.Semantics public

-- Intuitionistic Tarski models.

record Model : Set₁ where
  infix 3 _⊩ᵅ_ _[⊢]_ _[⊢⋆]_
  field
    -- Forcing for atomic propositions; monotonic.
    _⊩ᵅ_   : Cx Ty → Atom → Set
    mono⊩ᵅ : ∀ {P Γ Γ′} → Γ ⊆ Γ′ → Γ ⊩ᵅ P → Γ′ ⊩ᵅ P

    -- Gentzen-style syntax representation; monotonic.
    _[⊢]_     : Cx Ty → Ty → Set
    _[⊢⋆]_    : Cx Ty → Cx Ty → Set
    mono[⊢]   : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ [⊢] A → Γ′ [⊢] A
    [var]      : ∀ {A Γ}    → A ∈ Γ → Γ [⊢] A
    [lam]      : ∀ {A B Γ}  → Γ , A [⊢] B → Γ [⊢] A ▻ B
    [app]      : ∀ {A B Γ}  → Γ [⊢] A ▻ B → Γ [⊢] A → Γ [⊢] B
    [multibox] : ∀ {A Δ Γ}  → Γ [⊢⋆] □⋆ Δ → □⋆ Δ [⊢] A → Γ [⊢] □ A
    [down]     : ∀ {A Γ}    → Γ [⊢] □ A → Γ [⊢] A
    [pair]     : ∀ {A B Γ}  → Γ [⊢] A → Γ [⊢] B → Γ [⊢] A ∧ B
    [fst]      : ∀ {A B Γ}  → Γ [⊢] A ∧ B → Γ [⊢] A
    [snd]      : ∀ {A B Γ}  → Γ [⊢] A ∧ B → Γ [⊢] B
    [unit]     : ∀ {Γ}      → Γ [⊢] ⊤

    -- TODO: Workarounds for Agda bug #2143.
    top[⊢⋆] : ∀ {Γ}     → (Γ [⊢⋆] ∅) ≡ 𝟙
    pop[⊢⋆] : ∀ {Ξ A Γ} → (Γ [⊢⋆] Ξ , A) ≡ (Γ [⊢⋆] Ξ × Γ [⊢] A)

  infix 3 _[⊢]⋆_
  _[⊢]⋆_ : Cx Ty → Cx Ty → Set
  Γ [⊢]⋆ ∅     = 𝟙
  Γ [⊢]⋆ Ξ , A = Γ [⊢]⋆ Ξ × Γ [⊢] A

  [⊢⋆]→[⊢]⋆ : ∀ {Ξ Γ} → Γ [⊢⋆] Ξ → Γ [⊢]⋆ Ξ
  [⊢⋆]→[⊢]⋆ {∅}     {Γ} ts = ∙
  [⊢⋆]→[⊢]⋆ {Ξ , A} {Γ} ts rewrite pop[⊢⋆] {Ξ} {A} {Γ} = [⊢⋆]→[⊢]⋆ (π₁ ts) , π₂ ts

  [⊢]⋆→[⊢⋆] : ∀ {Ξ Γ} → Γ [⊢]⋆ Ξ → Γ [⊢⋆] Ξ
  [⊢]⋆→[⊢⋆] {∅}     {Γ} ∙        rewrite top[⊢⋆] {Γ}         = ∙
  [⊢]⋆→[⊢⋆] {Ξ , A} {Γ} (ts , t) rewrite pop[⊢⋆] {Ξ} {A} {Γ} = [⊢]⋆→[⊢⋆] ts , t

open Model {{…}} public

-- Forcing in a particular model.

module _ {{_ : Model}} where
  infix 3 _⊩_
  _⊩_ : Cx Ty → Ty → Set
  Γ ⊩ α P   = Glue (Γ [⊢] α P) (Γ ⊩ᵅ P)
  Γ ⊩ A ▻ B = ∀ {Γ′} → Γ ⊆ Γ′ → Glue (Γ′ [⊢] A ▻ B) (Γ′ ⊩ A → Γ′ ⊩ B)
  Γ ⊩ □ A   = ∀ {Γ′} → Γ ⊆ Γ′ → Glue (Γ′ [⊢] □ A) (Γ′ ⊩ A)
  Γ ⊩ A ∧ B = Γ ⊩ A × Γ ⊩ B
  Γ ⊩ ⊤    = 𝟙

  infix 3 _⊩⋆_
  _⊩⋆_ : Cx Ty → Cx Ty → Set
  Γ ⊩⋆ ∅     = 𝟙
  Γ ⊩⋆ Ξ , A = Γ ⊩⋆ Ξ × Γ ⊩ A

-- Monotonicity with respect to context inclusion.

module _ {{_ : Model}} where
  mono⊩ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊩ A → Γ′ ⊩ A
  mono⊩ {α P}   η s = mono[⊢] η (syn s) ⅋ mono⊩ᵅ η (sem s)
  mono⊩ {A ▻ B} η s = λ η′ → s (trans⊆ η η′)
  mono⊩ {□ A}   η s = λ η′ → s (trans⊆ η η′)
  mono⊩ {A ∧ B} η s = mono⊩ {A} η (π₁ s) , mono⊩ {B} η (π₂ s)
  mono⊩ {⊤}    η s = ∙

  mono⊩⋆ : ∀ {Ξ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊩⋆ Ξ → Γ′ ⊩⋆ Ξ
  mono⊩⋆ {∅}     η ∙        = ∙
  mono⊩⋆ {Ξ , A} η (ts , t) = mono⊩⋆ {Ξ} η ts , mono⊩ {A} η t

-- Extraction of syntax representation in a particular model.

module _ {{_ : Model}} where
  reifyʳ : ∀ {A Γ} → Γ ⊩ A → Γ [⊢] A
  reifyʳ {α P}   s = syn s
  reifyʳ {A ▻ B} s = syn (s refl⊆)
  reifyʳ {□ A}   s = syn (s refl⊆)
  reifyʳ {A ∧ B} s = [pair] (reifyʳ {A} (π₁ s)) (reifyʳ {B} (π₂ s))
  reifyʳ {⊤}    s = [unit]

  reifyʳ⋆ : ∀ {Ξ Γ} → Γ ⊩⋆ Ξ → Γ [⊢]⋆ Ξ
  reifyʳ⋆ {∅}     ∙        = ∙
  reifyʳ⋆ {Ξ , A} (ts , t) = reifyʳ⋆ ts , reifyʳ t

-- Shorthand for variables.

module _ {{_ : Model}} where
  [v₀] : ∀ {A Γ} → Γ , A [⊢] A
  [v₀] = [var] i₀

  [v₁] : ∀ {A B Γ} → Γ , A , B [⊢] A
  [v₁] = [var] i₁

  [v₂] : ∀ {A B C Γ} → Γ , A , B , C [⊢] A
  [v₂] = [var] i₂

-- Useful theorems in functional form.

module _ {{_ : Model}} where
  [multicut] : ∀ {Ξ A Γ} → Γ [⊢]⋆ Ξ → Ξ [⊢] A → Γ [⊢] A
  [multicut] {∅}     ∙        u = mono[⊢] bot⊆ u
  [multicut] {Ξ , B} (ts , t) u = [app] ([multicut] ts ([lam] u)) t

  [dist] : ∀ {A B Γ} → Γ [⊢] □ (A ▻ B) → Γ [⊢] □ A → Γ [⊢] □ B
  [dist] t u = [multibox] ([⊢]⋆→[⊢⋆] ((∙ , t) , u)) ([app] ([down] [v₁]) ([down] [v₀]))

  [up] : ∀ {A Γ} → Γ [⊢] □ A → Γ [⊢] □ □ A
  [up] t = [multibox] ([⊢]⋆→[⊢⋆] ((∙ , t))) [v₀]

-- Useful theorems in combinatory form.

module _ {{_ : Model}} where
  [ci] : ∀ {A Γ} → Γ [⊢] A ▻ A
  [ci] = [lam] [v₀]

  [ck] : ∀ {A B Γ} → Γ [⊢] A ▻ B ▻ A
  [ck] = [lam] ([lam] [v₁])

  [cs] : ∀ {A B C Γ} → Γ [⊢] (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
  [cs] = [lam] ([lam] ([lam] ([app] ([app] [v₂] [v₀]) ([app] [v₁] [v₀]))))

  [cdist] : ∀ {A B Γ} → Γ [⊢] □ (A ▻ B) ▻ □ A ▻ □ B
  [cdist] = [lam] ([lam] ([dist] [v₁] [v₀]))

  [cup] : ∀ {A Γ} → Γ [⊢] □ A ▻ □ □ A
  [cup] = [lam] ([up] [v₀])

  [cdown] : ∀ {A Γ} → Γ [⊢] □ A ▻ A
  [cdown] = [lam] ([down] [v₀])

  [box] : ∀ {A Γ} → ∅ [⊢] A → Γ [⊢] □ A
  [box] t = [multibox] ([⊢]⋆→[⊢⋆] ∙) t

  [cpair] : ∀ {A B Γ} → Γ [⊢] A ▻ B ▻ A ∧ B
  [cpair] = [lam] ([lam] ([pair] [v₁] [v₀]))

  [cfst] : ∀ {A B Γ} → Γ [⊢] A ∧ B ▻ A
  [cfst] = [lam] ([fst] [v₀])

  [csnd] : ∀ {A B Γ} → Γ [⊢] A ∧ B ▻ B
  [csnd] = [lam] ([snd] [v₀])

-- Additional useful equipment.

module _ {{_ : Model}} where
  _⟪$⟫_ : ∀ {A B Γ} → Γ ⊩ A ▻ B → Γ ⊩ A → Γ ⊩ B
  s ⟪$⟫ a = sem (s refl⊆) a

  ⟪K⟫ : ∀ {A B Γ} → Γ ⊩ A → Γ ⊩ B ▻ A
  ⟪K⟫ {A} a η = let a′ = mono⊩ {A} η a
                in  [app] [ck] (reifyʳ a′) ⅋ K a′

  ⟪S⟫ : ∀ {A B C Γ} → Γ ⊩ A ▻ B ▻ C → Γ ⊩ A ▻ B → Γ ⊩ A → Γ ⊩ C
  ⟪S⟫ s₁ s₂ a = (s₁ ⟪$⟫ a) ⟪$⟫ (s₂ ⟪$⟫ a)

  ⟪S⟫′ : ∀ {A B C Γ} → Γ ⊩ A ▻ B ▻ C → Γ ⊩ (A ▻ B) ▻ A ▻ C
  ⟪S⟫′ {A} {B} {C} s₁ η = let s₁′ = mono⊩ {A ▻ B ▻ C} η s₁
                              t   = syn (s₁′ refl⊆)
                          in  [app] [cs] t ⅋ λ s₂ η′ →
                                let s₁″ = mono⊩ {A ▻ B ▻ C} (trans⊆ η η′) s₁
                                    s₂′ = mono⊩ {A ▻ B} η′ s₂
                                    t′  = syn (s₁″ refl⊆)
                                    u   = syn (s₂′ refl⊆)
                                in  [app] ([app] [cs] t′) u ⅋ ⟪S⟫ s₁″ s₂′

  _⟪D⟫_ : ∀ {A B Γ} → Γ ⊩ □ (A ▻ B) → Γ ⊩ □ A → Γ ⊩ □ B
  (s₁ ⟪D⟫ s₂) η = let t ⅋ s₁′ = s₁ η
                      u ⅋ a   = s₂ η
                  in  [app] ([app] [cdist] t) u ⅋ s₁′ ⟪$⟫ a

  _⟪D⟫′_ : ∀ {A B Γ} → Γ ⊩ □ (A ▻ B) → Γ ⊩ □ A ▻ □ B
  _⟪D⟫′_ {A} {B} s₁ η = let s₁′ = mono⊩ {□ (A ▻ B)} η s₁
                        in  [app] [cdist] (reifyʳ (λ {_} η′ → s₁′ η′ )) ⅋ _⟪D⟫_ s₁′

  ⟪↑⟫ : ∀ {A Γ} → Γ ⊩ □ A → Γ ⊩ □ □ A
  ⟪↑⟫ s η = [app] [cup] (syn (s η)) ⅋ λ η′ → s (trans⊆ η η′)

  ⟪↓⟫ : ∀ {A Γ} → Γ ⊩ □ A → Γ ⊩ A
  ⟪↓⟫ s = sem (s refl⊆)

  _⟪,⟫′_ : ∀ {A B Γ} → Γ ⊩ A → Γ ⊩ B ▻ A ∧ B
  _⟪,⟫′_ {A} a η = let a′ = mono⊩ {A} η a
                   in  [app] [cpair] (reifyʳ a′) ⅋ _,_ a′

-- Forcing in a particular world of a particular model, for sequents.

module _ {{_ : Model}} where
  infix 3 _⊩_⇒_
  _⊩_⇒_ : Cx Ty → Cx Ty → Ty → Set
  w ⊩ Γ ⇒ A = w ⊩⋆ Γ → w ⊩ A

  infix 3 _⊩_⇒⋆_
  _⊩_⇒⋆_ : Cx Ty → Cx Ty → Cx Ty → Set
  w ⊩ Γ ⇒⋆ Ξ = w ⊩⋆ Γ → w ⊩⋆ Ξ

-- Entailment, or forcing in all worlds of all models, for sequents.

infix 3 _⊨_
_⊨_ : Cx Ty → Ty → Set₁
Γ ⊨ A = ∀ {{_ : Model}} {w : Cx Ty} → w ⊩ Γ ⇒ A

infix 3 _⊨⋆_
_⊨⋆_ : Cx Ty → Cx Ty → Set₁
Γ ⊨⋆ Ξ = ∀ {{_ : Model}} {w : Cx Ty} → w ⊩ Γ ⇒⋆ Ξ

-- Additional useful equipment, for sequents.

module _ {{_ : Model}} where
  lookup : ∀ {A Γ w} → A ∈ Γ → w ⊩ Γ ⇒ A
  lookup top     (γ , a) = a
  lookup (pop i) (γ , b) = lookup i γ

  _⟦$⟧_ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A ▻ B → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ B
  (s₁ ⟦$⟧ s₂) γ = s₁ γ ⟪$⟫ s₂ γ

  ⟦K⟧ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ B ▻ A
  ⟦K⟧ {A} {B} a γ = ⟪K⟫ {A} {B} (a γ)

  ⟦S⟧ : ∀ {A B C Γ w} → w ⊩ Γ ⇒ A ▻ B ▻ C → w ⊩ Γ ⇒ A ▻ B → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ C
  ⟦S⟧ s₁ s₂ a γ = ⟪S⟫ (s₁ γ) (s₂ γ) (a γ)

  _⟦D⟧_ : ∀ {A B Γ w} → w ⊩ Γ ⇒ □ (A ▻ B) → w ⊩ Γ ⇒ □ A → w ⊩ Γ ⇒ □ B
  (s₁ ⟦D⟧ s₂) γ = (s₁ γ) ⟪D⟫ (s₂ γ)

  ⟦↑⟧ : ∀ {A Γ w} → w ⊩ Γ ⇒ □ A → w ⊩ Γ ⇒ □ □ A
  ⟦↑⟧ s γ = ⟪↑⟫ (s γ)

  ⟦↓⟧ : ∀ {A Γ w} → w ⊩ Γ ⇒ □ A → w ⊩ Γ ⇒ A
  ⟦↓⟧ s γ = ⟪↓⟫ (s γ)

  _⟦,⟧_ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ B → w ⊩ Γ ⇒ A ∧ B
  (a ⟦,⟧ b) γ = a γ , b γ

  ⟦π₁⟧ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A ∧ B → w ⊩ Γ ⇒ A
  ⟦π₁⟧ s γ = π₁ (s γ)

  ⟦π₂⟧ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A ∧ B → w ⊩ Γ ⇒ B
  ⟦π₂⟧ s γ = π₂ (s γ)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
{-# OPTIONS --cubical --without-K --safe #-}
module Cubical.Relation.Binary.Converse where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Data.Prod hiding (map)
open import Cubical.HITs.PropositionalTruncation

open import Cubical.Relation.Binary

------------------------------------------------------------------------
-- Properties

module _ {a ℓ} {A : Type a} (∼ : Rel A ℓ) where

  reflexive : Reflexive ∼ → Reflexive (flip ∼)
  reflexive r = r

  irrefl : Irreflexive ∼ → Irreflexive (flip ∼)
  irrefl i = i

  symmetric : Symmetric ∼ → Symmetric (flip ∼)
  symmetric s = s

  transitive : Transitive ∼ → Transitive (flip ∼)
  transitive t = flip t

  asym : Asymmetric ∼ → Asymmetric (flip ∼)
  asym a = a

  rawtotal : RawTotal ∼ → RawTotal (flip ∼)
  rawtotal t x y = t y x

  total : Total ∼ → Total (flip ∼)
  total t x y = t y x

  resp : ∀ {p} (P : A → hProp p) → Symmetric ∼ →
             P Respects ∼ → P Respects (flip ∼)
  resp _ sym resp ∼ = resp (sym ∼)

  max : ∀ {⊥} → Minimum ∼ ⊥ → Maximum (flip ∼) ⊥
  max min = min

  min : ∀ {⊤} → Maximum ∼ ⊤ → Minimum (flip ∼) ⊤
  min max = max

  fromEq : FromEq ∼ → FromEq (flip ∼)
  fromEq impl = impl ∘ map sym

  toNotEq : ToNotEq ∼ → ToNotEq (flip ∼)
  toNotEq tne y∼x x≡y = tne y∼x (map sym x≡y)

  antisym : Antisymmetric ∼ → Antisymmetric (flip ∼)
  antisym ans = flip ans

  compare : Trichotomous ∼ → Trichotomous (flip ∼)
  compare cmp x y with cmp x y
  ... | tri< x<y x≡y y≮x = tri> y≮x x≡y x<y
  ... | tri≡ x≮y x≡y y≮x = tri≡ y≮x x≡y x≮y
  ... | tri> x≮y x≡y y<x = tri< y<x x≡y x≮y

module _ {a ℓ₁ ℓ₂} {A : Type a} (∼₁ : Rel A ℓ₁) (∼₂ : Rel A ℓ₂) where

  resp₂ : ∼₁ Respects₂ ∼₂ → (flip ∼₁) Respects₂ ∼₂
  resp₂ (resp₁ , resp₂) = resp₂ , resp₁

module _ {a b ℓ} {A : Type a} {B : Type b} (∼ : REL A B ℓ) where

  dec : Decidable ∼ → Decidable (flip ∼)
  dec dec = flip dec

------------------------------------------------------------------------
-- Structures

module _ {a ℓ} {A : Type a} {≈ : Rel A ℓ} where

  isPartialEquivalence : IsPartialEquivalence ≈ → IsPartialEquivalence (flip ≈)
  isPartialEquivalence eq = record
    { symmetric  = symmetric  ≈ Eq.symmetric
    ; transitive = transitive ≈ Eq.transitive
    }
    where module Eq = IsPartialEquivalence eq

  isEquivalence : IsEquivalence ≈ → IsEquivalence (flip ≈)
  isEquivalence eq = record
    { isPartialEquivalence = isPartialEquivalence Eq.isPartialEquivalence
    ; reflexive            = reflexive ≈ Eq.reflexive
    }
    where module Eq = IsEquivalence eq

  isDecEquivalence : IsDecEquivalence ≈ → IsDecEquivalence (flip ≈)
  isDecEquivalence eq = record
    { isEquivalence = isEquivalence Dec.isEquivalence
    ; _≟_           = dec ≈ Dec._≟_
    }
    where module Dec = IsDecEquivalence eq

module _ {a ℓ} {A : Set a} {∼ : Rel A ℓ} where

  isPreorder : IsPreorder ∼ → IsPreorder (flip ∼)
  isPreorder O = record
    { reflexive  = reflexive ∼ O.reflexive
    ; transitive = transitive ∼ O.transitive
    }
    where module O = IsPreorder O

  isPartialOrder : IsPartialOrder ∼ → IsPartialOrder (flip ∼)
  isPartialOrder O = record
    { isPreorder = isPreorder O.isPreorder
    ; antisym    = antisym ∼ O.antisym
    }
    where module O = IsPartialOrder O

  isTotalOrder : IsTotalOrder ∼ → IsTotalOrder (flip ∼)
  isTotalOrder O = record
    { isPartialOrder = isPartialOrder O.isPartialOrder
    ; total          = total ∼ O.total
    }
    where module O = IsTotalOrder O

  isDecTotalOrder : IsDecTotalOrder ∼ → IsDecTotalOrder (flip ∼)
  isDecTotalOrder O = record
    { isTotalOrder = isTotalOrder O.isTotalOrder
    ; _≤?_         = dec ∼ O._≤?_
    }
    where module O = IsDecTotalOrder O

  isStrictPartialOrder : IsStrictPartialOrder ∼ →
                         IsStrictPartialOrder (flip ∼)
  isStrictPartialOrder O = record
    { irrefl     = irrefl ∼ O.irrefl
    ; transitive = transitive ∼ O.transitive
    }
    where module O = IsStrictPartialOrder O

  isStrictTotalOrder : IsStrictTotalOrder ∼ →
                       IsStrictTotalOrder (flip ∼)
  isStrictTotalOrder O = record
    { transitive = transitive ∼ O.transitive
    ; compare    = compare ∼ O.compare
    }
    where module O = IsStrictTotalOrder O

module _ {a ℓ} {A : Type a} where

  equivalence : Equivalence A ℓ → Equivalence A ℓ
  equivalence S = record
    { isEquivalence = isEquivalence S.isEquivalence
    }
    where module S = Equivalence S

  decEquivalence : DecEquivalence A ℓ → DecEquivalence A ℓ
  decEquivalence S = record
    { isDecEquivalence = isDecEquivalence S.isDecEquivalence
    }
    where module S = DecEquivalence S

module _ {a ℓ} {A : Type a} where

  preorder : Preorder A ℓ → Preorder A ℓ
  preorder O = record
    { isPreorder = isPreorder O.isPreorder
    }
    where module O = Preorder O

  partialOrder : PartialOrder A ℓ → PartialOrder A ℓ
  partialOrder O = record
    { isPartialOrder = isPartialOrder O.isPartialOrder
    }
    where module O = PartialOrder O

  totalOrder : TotalOrder A ℓ → TotalOrder A ℓ
  totalOrder O = record
    { isTotalOrder = isTotalOrder O.isTotalOrder
    }
    where module O = TotalOrder O

  decTotalOrder : DecTotalOrder A ℓ → DecTotalOrder A ℓ
  decTotalOrder O = record
    { isDecTotalOrder = isDecTotalOrder O.isDecTotalOrder
    }
    where module O = DecTotalOrder O

  strictPartialOrder : StrictPartialOrder A ℓ →
                       StrictPartialOrder A ℓ
  strictPartialOrder O = record
    { isStrictPartialOrder = isStrictPartialOrder O.isStrictPartialOrder
    }
    where module O = StrictPartialOrder O

  strictTotalOrder : StrictTotalOrder A ℓ →
                     StrictTotalOrder A ℓ
  strictTotalOrder O = record
    { isStrictTotalOrder = isStrictTotalOrder O.isStrictTotalOrder
    }
    where module O = StrictTotalOrder O


text:
module 4-the-natural-numbers where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; ⌊_/2⌋)

-- 4)
--sum-to-n : ℕ → ℕ
--sum-to-n n = sum (upTo (suc n))
open import Data.Nat.Properties using (*-comm; *-distribʳ-+; +-suc; +-comm; *-distribˡ-+)

1+⋯+n : ℕ → ℕ
1+⋯+n zero = zero
1+⋯+n (suc n) = suc n + 1+⋯+n n

n≡[n*2]/2 : ∀ (n : ℕ) → n ≡ ⌊ n * 2 /2⌋
n≡[n*2]/2 zero = refl
n≡[n*2]/2 (suc n) =
  begin
    suc n
  ≡⟨ cong suc (n≡[n*2]/2 n) ⟩
    suc ⌊  n * 2 /2⌋
  ≡⟨⟩
    1 + ⌊  n * 2 /2⌋
  ≡⟨⟩
    ⌊ 2 + n * 2 /2⌋
  ≡⟨⟩
    ⌊ suc n * 2 /2⌋
  ∎

data IsEven : ℕ → Set where
  even : (k : ℕ) → IsEven (k * 2)

rearrange-lemma : ∀ n → suc (suc n) * suc n ≡ suc n * 2 + suc n * n
rearrange-lemma n =
  begin
    suc (suc n) * suc n
  ≡⟨⟩
    suc (1 + n) * (1 + n)
  ≡⟨⟩
    (2 + n) * (1 + n)
  ≡⟨ *-distribʳ-+ (1 + n) 2 n ⟩
    2 * (1 + n) + n * (1 + n)
  ≡⟨ cong (2 * (1 + n) +_) (*-comm n (1 + n)) ⟩
    2 * (1 + n) + (1 + n) * n
  ≡⟨⟩
    2 * suc n + suc n * n
  ≡⟨ cong (_+ suc n * n) (*-comm 2 (suc n)) ⟩
    suc n * 2 + suc n * n
  ∎

even+even≡even : ∀ {m n : ℕ} → IsEven m → IsEven n → IsEven (m + n)
even+even≡even (even k) (even i) rewrite (sym (*-distribʳ-+ 2 k i)) = even (k + i)

[1+n]*n≡even : ∀ (n : ℕ) → IsEven (suc n * n)
[1+n]*n≡even zero = even 0
[1+n]*n≡even (suc n) rewrite rearrange-lemma n = even+even≡even (even (suc n)) ([1+n]*n≡even n)

even/2+even/2≡[even+even]/2 : ∀ {m n : ℕ} → IsEven m → IsEven n → ⌊ m /2⌋ + ⌊ n /2⌋ ≡ ⌊ m + n /2⌋
even/2+even/2≡[even+even]/2 (even k) (even i) =
  begin
    ⌊ k * 2 /2⌋ + ⌊ i * 2 /2⌋
  ≡⟨ cong (_+ ⌊ i * 2 /2⌋) (sym (n≡[n*2]/2 k)) ⟩
    k + ⌊ i * 2 /2⌋
  ≡⟨ cong (k +_) (sym (n≡[n*2]/2 i)) ⟩
    k + i
  ≡⟨ n≡[n*2]/2 (k + i) ⟩
    ⌊ (k + i) * 2 /2⌋
  ≡⟨ cong ⌊_/2⌋ (*-distribʳ-+ 2 k i) ⟩
    ⌊ k * 2 + i * 2 /2⌋
  ∎

gaussian-sum : ∀ (n : ℕ) → 1+⋯+n n ≡ ⌊ n * (n + 1) /2⌋
gaussian-sum zero = refl
gaussian-sum (suc n) =
  begin
    1+⋯+n (suc n)
  ≡⟨⟩
    suc n + 1+⋯+n n
  ≡⟨ cong (suc n +_) (gaussian-sum n)⟩
    suc n + ⌊ n * (n + 1) /2⌋
  ≡⟨ cong (_+ ⌊ n * (n + 1) /2⌋) (n≡[n*2]/2 (suc n)) ⟩
    ⌊ suc n * 2 /2⌋ + ⌊ n * (n + 1) /2⌋
  ≡⟨ cong (λ {term → ⌊ suc n * 2 /2⌋ + ⌊ n * term /2⌋}) (+-comm n 1) ⟩
    ⌊ suc n * 2 /2⌋ + ⌊ n * (1 + n) /2⌋
  ≡⟨⟩
    ⌊ suc n * 2 /2⌋ + ⌊ n * suc n /2⌋
  ≡⟨ cong (λ {term → ⌊ suc n * 2 /2⌋ + ⌊ term /2⌋}) (*-comm n (suc n)) ⟩
    ⌊ suc n * 2 /2⌋ + ⌊ suc n * n /2⌋
  ≡⟨ even/2+even/2≡[even+even]/2 (even (suc n)) ([1+n]*n≡even n) ⟩
    ⌊ suc n * 2 + suc n * n /2⌋
  ≡⟨ cong (⌊_/2⌋) (sym (*-distribˡ-+ (1 + n) 2 n)) ⟩
    ⌊ suc n * (2 + n) /2⌋
  ≡⟨ cong (λ {term → ⌊ suc n * term /2⌋}) (+-comm 2 n) ⟩
    ⌊ suc n * (n + 2) /2⌋
  ≡⟨ cong (λ {term → ⌊ suc n * term /2⌋}) (+-suc n 1) ⟩
    ⌊ suc n * (suc n + 1) /2⌋
  ∎

max_stars_repo_name: aronerben/agda-playground

max_issues_repo_name: aronerben/agda-playground

max_forks_repo_name: aronerben/agda-playground