text:
------------------------------------------------------------------------
-- Application of substitutions to terms
------------------------------------------------------------------------

import Level
open import Data.Universe

module README.DependentlyTyped.Term.Substitution
  (Uni₀ : Universe Level.zero Level.zero) where

open import Data.Product as Prod renaming (curry to c; uncurry to uc)
open import deBruijn.Substitution.Data
open import Function as F using (_$_; _ˢ_) renaming (const to k)
import README.DependentlyTyped.Term as Term; open Term Uni₀
import Relation.Binary.PropositionalEquality as P

open P.≡-Reasoning

-- Code for applying substitutions.
--
-- Note that the _↦_ record ensures that we already have access to
-- operations such as lifting.

module Apply {T : Term-like Level.zero} (T↦Tm : T ↦ Tm) where

  open _↦_ T↦Tm hiding (var)

  mutual

    infixl 8 _/⊢_ _/⊢-lemma_

    -- Applies a substitution to a term. TODO: Generalise and allow
    -- the codomain to be any suitable applicative structure?

    _/⊢_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} → Γ ⊢ σ → Sub T ρ̂ → Δ ⊢ σ /̂ ρ̂
    var x   /⊢ ρ = trans ⊙ (x /∋ ρ)
    ƛ t     /⊢ ρ = ƛ (t /⊢ ρ ↑)
    t₁ · t₂ /⊢ ρ = [ t₁ · t₂ ]/⊢ ρ

    -- The body of the last case above. (At the time of writing the
    -- termination checker complains if [ t₁ · t₂ ]/⊢ ρ is replaced by
    -- t₁ · t₂ /⊢ ρ in the type signature of ·-/⊢ below.)

    [_·_]/⊢ :
      ∀ {Γ Δ sp₁ sp₂ σ} {ρ̂ : Γ ⇨̂ Δ}
      (t₁ : Γ ⊢ π sp₁ sp₂ , σ) (t₂ : Γ ⊢ fst σ) (ρ : Sub T ρ̂) →
      Δ ⊢ snd σ /̂ ŝub ⟦ t₂ ⟧ /̂ ρ̂
    [_·_]/⊢ {σ = σ} t₁ t₂ ρ =
      P.subst (λ v → _ ⊢ snd σ /̂ ⟦ ρ ⟧⇨ ↑̂ /̂ ŝub v)
              (≅-Value-⇒-≡ $ P.sym $ t₂ /⊢-lemma ρ)
              ((t₁ /⊢ ρ) · (t₂ /⊢ ρ))

    abstract

      -- An unfolding lemma.

      ·-/⊢ : ∀ {Γ Δ sp₁ sp₂ σ} {ρ̂ : Γ ⇨̂ Δ}
             (t₁ : Γ ⊢ π sp₁ sp₂ , σ) (t₂ : Γ ⊢ fst σ) (ρ : Sub T ρ̂) →
             [ t₁ · t₂ ]/⊢ ρ ≅-⊢ (t₁ /⊢ ρ) · (t₂ /⊢ ρ)
      ·-/⊢ {σ = σ} t₁ t₂ ρ =
        drop-subst-⊢ (λ v → snd σ /̂ ⟦ ρ ⟧⇨ ↑̂ /̂ ŝub v)
                     (≅-Value-⇒-≡ $ P.sym $ t₂ /⊢-lemma ρ)

      -- The application operation is well-behaved.

      _/⊢-lemma_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (t : Γ ⊢ σ) (ρ : Sub T ρ̂) →
                   ⟦ t ⟧ /Val ρ ≅-Value ⟦ t /⊢ ρ ⟧
      var x /⊢-lemma ρ = /̂∋-⟦⟧⇨ x ρ
      ƛ t   /⊢-lemma ρ = begin
        [ c ⟦ t ⟧ /Val ρ     ]  ≡⟨ P.refl ⟩
        [ c (⟦ t ⟧ /Val ρ ↑) ]  ≡⟨ curry-cong (t /⊢-lemma (ρ ↑)) ⟩
        [ c ⟦ t /⊢ ρ ↑ ⟧     ]  ∎
      t₁ · t₂ /⊢-lemma ρ = begin
        [ ⟦ t₁ · t₂ ⟧ /Val ρ                ]  ≡⟨ P.refl ⟩
        [ (⟦ t₁ ⟧ /Val ρ) ˢ (⟦ t₂ ⟧ /Val ρ) ]  ≡⟨ ˢ-cong (t₁ /⊢-lemma ρ) (t₂ /⊢-lemma ρ) ⟩
        [ ⟦ t₁ /⊢ ρ ⟧ ˢ ⟦ t₂ /⊢ ρ ⟧         ]  ≡⟨ P.refl ⟩
        [ ⟦ (t₁ /⊢ ρ) · (t₂ /⊢ ρ) ⟧         ]  ≡⟨ ⟦⟧-cong (P.sym $ ·-/⊢ t₁ t₂ ρ) ⟩
        [ ⟦ t₁ · t₂ /⊢ ρ ⟧                  ]  ∎

  app : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → [ Tm ⟶ Tm ] ρ̂
  app ρ = record
    { function    = λ _ t → t /⊢ ρ
    ; corresponds = λ _ t → t /⊢-lemma ρ
    }

  -- Application of substitutions to syntactic types. TODO: Remove?

  infixl 8 _/⊢t_ _/⊢t⋆_

  _/⊢t_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} → Γ ⊢ σ type → Sub T ρ̂ → Δ ⊢ σ /̂ ρ̂ type
  ⋆       /⊢t ρ = ⋆
  el t    /⊢t ρ = P.subst (λ v → _ ⊢ -, k U-el ˢ v type)
                          (≅-Value-⇒-≡ $ P.sym $ t /⊢-lemma ρ) $
                    el (t /⊢ ρ)
  π σ′ τ′ /⊢t ρ = π (σ′ /⊢t ρ) (τ′ /⊢t ρ ↑)

  _/⊢t⋆_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} →
           Γ ⊢ σ type → Subs T ρ̂ → Δ ⊢ σ /̂ ρ̂ type
  σ′ /⊢t⋆ ε        = σ′
  σ′ /⊢t⋆ (ρs ▻ ρ) = σ′ /⊢t⋆ ρs /⊢t ρ

  -- Congruence lemmas.

  /⊢t-cong :
    ∀ {Γ₁ Δ₁ σ₁} {σ′₁ : Γ₁ ⊢ σ₁ type} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
      {Γ₂ Δ₂ σ₂} {σ′₂ : Γ₂ ⊢ σ₂ type} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
    σ′₁ ≅-type σ′₂ → ρ₁ ≅-⇨ ρ₂ → σ′₁ /⊢t ρ₁ ≅-type σ′₂ /⊢t ρ₂
  /⊢t-cong P.refl P.refl = P.refl

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

substitution₁ : Substitution₁ Tm
substitution₁ = record
  { var      = record { function    = λ _ → var
                      ; corresponds = λ _ _ → P.refl
                      }
  ; app′     = Apply.app
  ; app′-var = λ _ _ _ → P.refl
  }

open Substitution₁ substitution₁ hiding (var)

-- Some unfolding lemmas.

module Unfolding-lemmas
  {T : Term-like Level.zero}
  (T↦Tm : Translation-from T)
  where

  open Translation-from T↦Tm
  open Apply translation hiding (_/⊢_; app)

  abstract

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

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

    -- TODO: Remove the following lemmas?

    ⋆-/⊢t⋆ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρs : Subs T ρ̂) →
             ⋆ /⊢t⋆ ρs ≅-type ⋆ {Γ = Δ}
    ⋆-/⊢t⋆ ε        = P.refl
    ⋆-/⊢t⋆ (ρs ▻ ρ) = begin
      [ ⋆ /⊢t⋆ ρs /⊢t ρ ]  ≡⟨ /⊢t-cong (⋆-/⊢t⋆ ρs) (P.refl {x = [ ρ ]}) ⟩
      [ ⋆ /⊢t ρ         ]  ≡⟨ P.refl ⟩
      [ ⋆               ]  ∎

    el-/⊢t : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (t : Γ ⊢ -, k U-⋆) (ρ : Sub T ρ̂) →
             el t /⊢t ρ ≅-type el (t /⊢ ρ)
    el-/⊢t t ρ =
      drop-subst-⊢-type (λ v → -, k U-el ˢ v)
                        (≅-Value-⇒-≡ $ P.sym $ t /⊢-lemma ρ)

    el-/⊢t⋆ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (t : Γ ⊢ -, k U-⋆) (ρs : Subs T ρ̂) →
              el t /⊢t⋆ ρs ≅-type el (t /⊢⋆ ρs)
    el-/⊢t⋆ t ε        = P.refl
    el-/⊢t⋆ t (ρs ▻ ρ) = begin
      [ el t /⊢t⋆ ρs /⊢t ρ  ]  ≡⟨ /⊢t-cong (el-/⊢t⋆ t ρs) (P.refl {x = [ ρ ]}) ⟩
      [ el (t /⊢⋆ ρs) /⊢t ρ ]  ≡⟨ el-/⊢t (t /⊢⋆ ρs) ρ ⟩
      [ el (t /⊢⋆ ρs /⊢ ρ)  ]  ∎

    π-/⊢t⋆ : ∀ {Γ Δ σ τ} {ρ̂ : Γ ⇨̂ Δ}
             (σ′ : Γ ⊢ σ type) (τ′ : Γ ▻ σ ⊢ τ type) (ρs : Subs T ρ̂) →
             π σ′ τ′ /⊢t⋆ ρs ≅-type π (σ′ /⊢t⋆ ρs) (τ′ /⊢t⋆ ρs ↑⋆)
    π-/⊢t⋆ σ′ τ′ ε        = P.refl
    π-/⊢t⋆ σ′ τ′ (ρs ▻ ρ) = begin
      [ π σ′ τ′ /⊢t⋆ ρs /⊢t ρ                        ]  ≡⟨ /⊢t-cong (π-/⊢t⋆ σ′ τ′ ρs) (P.refl {x = [ ρ ]}) ⟩
      [ π (σ′ /⊢t⋆ ρs) (τ′ /⊢t⋆ ρs ↑⋆) /⊢t ρ         ]  ≡⟨ P.refl ⟩
      [ π (σ′ /⊢t⋆ ρs /⊢t ρ) (τ′ /⊢t⋆ ρs ↑⋆ /⊢t ρ ↑) ]  ∎

-- Another lemma.

module Apply-lemma
  {T₁ T₂ : Term-like Level.zero}
  (T₁↦T : Translation-from T₁) (T₂↦T : Translation-from T₂)
  {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρs₁ : Subs T₁ ρ̂) (ρs₂ : Subs T₂ ρ̂) where

  open Translation-from T₁↦T
    using () renaming (_↑⁺⋆_ to _↑⁺⋆₁_; _/⊢⋆_ to _/⊢⋆₁_)
  open Apply (Translation-from.translation T₁↦T)
    using () renaming (_/⊢t⋆_ to _/⊢t⋆₁_)
  open Translation-from T₂↦T
    using () renaming (_↑⁺⋆_ to _↑⁺⋆₂_; _/⊢⋆_ to _/⊢⋆₂_)
  open Apply (Translation-from.translation T₂↦T)
    using () renaming (_/⊢t⋆_ to _/⊢t⋆₂_)

  abstract

    var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆ :
      (∀ Γ⁺ {σ} (x : Γ ++⁺ Γ⁺ ∋ σ) →
         var x /⊢⋆₁ ρs₁ ↑⁺⋆₁ Γ⁺ ≅-⊢ var x /⊢⋆₂ ρs₂ ↑⁺⋆₂ Γ⁺) →
      ∀ Γ⁺ {σ} (t : Γ ++⁺ Γ⁺ ⊢ σ) →
      t /⊢⋆₁ ρs₁ ↑⁺⋆₁ Γ⁺ ≅-⊢ t /⊢⋆₂ ρs₂ ↑⁺⋆₂ Γ⁺
    var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆ hyp Γ⁺ (var x)  = hyp Γ⁺ x
    var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆ hyp Γ⁺ (ƛ {σ = σ} t) = begin
      [ ƛ t /⊢⋆₁ ρs₁ ↑⁺⋆₁ Γ⁺         ]  ≡⟨ Unfolding-lemmas.ƛ-/⊢⋆ T₁↦T t (ρs₁ ↑⁺⋆₁ Γ⁺) ⟩
      [ ƛ (t /⊢⋆₁ ρs₁ ↑⁺⋆₁ (Γ⁺ ▻ σ)) ]  ≡⟨ ƛ-cong (var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆ hyp (Γ⁺ ▻ σ) t) ⟩
      [ ƛ (t /⊢⋆₂ ρs₂ ↑⁺⋆₂ (Γ⁺ ▻ σ)) ]  ≡⟨ P.sym $ Unfolding-lemmas.ƛ-/⊢⋆ T₂↦T t (ρs₂ ↑⁺⋆₂ Γ⁺) ⟩
      [ ƛ t /⊢⋆₂ ρs₂ ↑⁺⋆₂ Γ⁺         ]  ∎
    var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆ hyp Γ⁺ (t₁ · t₂) = begin
      [ t₁ · t₂ /⊢⋆₁ ρs₁ ↑⁺⋆₁ Γ⁺                      ]  ≡⟨ Unfolding-lemmas.·-/⊢⋆ T₁↦T t₁ t₂ (ρs₁ ↑⁺⋆₁ Γ⁺) ⟩
      [ (t₁ /⊢⋆₁ ρs₁ ↑⁺⋆₁ Γ⁺) · (t₂ /⊢⋆₁ ρs₁ ↑⁺⋆₁ Γ⁺) ]  ≡⟨ ·-cong (var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆ hyp Γ⁺ t₁)
                                                                   (var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆ hyp Γ⁺ t₂) ⟩
      [ (t₁ /⊢⋆₂ ρs₂ ↑⁺⋆₂ Γ⁺) · (t₂ /⊢⋆₂ ρs₂ ↑⁺⋆₂ Γ⁺) ]  ≡⟨ P.sym $ Unfolding-lemmas.·-/⊢⋆ T₂↦T t₁ t₂ (ρs₂ ↑⁺⋆₂ Γ⁺) ⟩
      [ t₁ · t₂ /⊢⋆₂ ρs₂ ↑⁺⋆₂ Γ⁺                      ]  ∎

-- Term substitutions, along with a number of lemmas.

substitution₂ : Substitution₂ Tm
substitution₂ = record
  { substitution₁          = substitution₁
  ; var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆′ = Apply-lemma.var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆
  }

open Apply (Translation-from.translation no-translation) public
  using (·-/⊢; _/⊢t_; /⊢t-cong; _/⊢t⋆_; /⊢t⋆-cong)
open Unfolding-lemmas no-translation public
open Substitution₂ substitution₂ public hiding (var; substitution₁)

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:
------------------------------------------------------------------------
-- Coinductive definition of subtyping
------------------------------------------------------------------------

module RecursiveTypes.Subtyping.Semantic.Coinductive where

open import Codata.Musical.Notation
open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin using (Fin)
open import Function.Base
open import Data.Empty using (⊥-elim)
open import Relation.Nullary
open import Relation.Nullary.Negation hiding (stable)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import RecursiveTypes.Syntax
open import RecursiveTypes.Substitution
open import RecursiveTypes.Semantics

infixr 10 _⟶_
infix  4  _≤∞_ _≤Coind_
infix  3  _∎
infixr 2  _≤⟨_⟩_

------------------------------------------------------------------------
-- Definition

-- The obvious definition of subtyping for trees.

data _≤∞_ {n} : Tree n → Tree n → Set where
  ⊥   : ∀ {τ} → ⊥ ≤∞ τ
  ⊤   : ∀ {σ} → σ ≤∞ ⊤
  var : ∀ {x} → var x ≤∞ var x
  _⟶_ : ∀ {σ₁ σ₂ τ₁ τ₂}
        (τ₁≤σ₁ : ∞ (♭ τ₁ ≤∞ ♭ σ₁)) (σ₂≤τ₂ : ∞ (♭ σ₂ ≤∞ ♭ τ₂)) →
        σ₁ ⟶ σ₂ ≤∞ τ₁ ⟶ τ₂

-- Subtyping for recursive types is defined in terms of subtyping for
-- trees.

_≤Coind_ : ∀ {n} → Ty n → Ty n → Set
σ ≤Coind τ = ⟦ σ ⟧ ≤∞ ⟦ τ ⟧

------------------------------------------------------------------------
-- A trick used to ensure guardedness of expressions using
-- transitivity

infix 4 _≤∞P_ _≤∞W_

data _≤∞P_ {n} : Tree n → Tree n → Set where
  ⊥      : ∀ {τ} → ⊥ ≤∞P τ
  ⊤      : ∀ {σ} → σ ≤∞P ⊤
  var    : ∀ {x} → var x ≤∞P var x
  _⟶_    : ∀ {σ₁ σ₂ τ₁ τ₂}
           (τ₁≤σ₁ : ∞ (♭ τ₁ ≤∞P ♭ σ₁)) (σ₂≤τ₂ : ∞ (♭ σ₂ ≤∞P ♭ τ₂)) →
           σ₁ ⟶ σ₂ ≤∞P τ₁ ⟶ τ₂
  -- Transitivity.
  _≤⟨_⟩_ : ∀ τ₁ {τ₂ τ₃}
           (τ₁≤τ₂ : τ₁ ≤∞P τ₂) (τ₂≤τ₃ : τ₂ ≤∞P τ₃) → τ₁ ≤∞P τ₃

data _≤∞W_ {n} : Tree n → Tree n → Set where
  ⊥   : ∀ {τ} → ⊥ ≤∞W τ
  ⊤   : ∀ {σ} → σ ≤∞W ⊤
  var : ∀ {x} → var x ≤∞W var x
  _⟶_ : ∀ {σ₁ σ₂ τ₁ τ₂}
        (τ₁≤σ₁ : ♭ τ₁ ≤∞P ♭ σ₁) (σ₂≤τ₂ : ♭ σ₂ ≤∞P ♭ τ₂) →
        σ₁ ⟶ σ₂ ≤∞W τ₁ ⟶ τ₂

transW : ∀ {n} {τ₁ τ₂ τ₃ : Tree n} →
         τ₁ ≤∞W τ₂ → τ₂ ≤∞W τ₃ → τ₁ ≤∞W τ₃
transW ⊥               _               = ⊥
transW _               ⊤               = ⊤
transW var             var             = var
transW (τ₁≤σ₁ ⟶ σ₂≤τ₂) (χ₁≤τ₁ ⟶ τ₂≤χ₂) =
  (_ ≤⟨ χ₁≤τ₁ ⟩ τ₁≤σ₁) ⟶ (_ ≤⟨ σ₂≤τ₂ ⟩ τ₂≤χ₂)

whnf : ∀ {n} {σ τ : Tree n} → σ ≤∞P τ → σ ≤∞W τ
whnf ⊥                    = ⊥
whnf ⊤                    = ⊤
whnf var                  = var
whnf (τ₁≤σ₁ ⟶ σ₂≤τ₂)      = ♭ τ₁≤σ₁ ⟶ ♭ σ₂≤τ₂
whnf (σ ≤⟨ τ₁≤τ₂ ⟩ τ₂≤τ₃) = transW (whnf τ₁≤τ₂) (whnf τ₂≤τ₃)

mutual

  ⟦_⟧W : ∀ {n} {σ τ : Tree n} → σ ≤∞W τ → σ ≤∞ τ
  ⟦ ⊥             ⟧W = ⊥
  ⟦ ⊤             ⟧W = ⊤
  ⟦ var           ⟧W = var
  ⟦ τ₁≤σ₁ ⟶ σ₂≤τ₂ ⟧W = ♯ ⟦ τ₁≤σ₁ ⟧P ⟶ ♯ ⟦ σ₂≤τ₂ ⟧P

  ⟦_⟧P : ∀ {n} {σ τ : Tree n} → σ ≤∞P τ → σ ≤∞ τ
  ⟦ σ≤τ ⟧P = ⟦ whnf σ≤τ ⟧W

⌜_⌝ : ∀ {n} {σ τ : Tree n} → σ ≤∞ τ → σ ≤∞P τ
⌜ ⊥             ⌝ = ⊥
⌜ ⊤             ⌝ = ⊤
⌜ var           ⌝ = var
⌜ τ₁≤σ₁ ⟶ σ₂≤τ₂ ⌝ = ♯ ⌜ ♭ τ₁≤σ₁ ⌝ ⟶ ♯ ⌜ ♭ σ₂≤τ₂ ⌝

------------------------------------------------------------------------
-- Some lemmas

refl∞ : ∀ {n} (τ : Tree n) → τ ≤∞ τ
refl∞ ⊥       = ⊥
refl∞ ⊤       = ⊤
refl∞ (var x) = var
refl∞ (σ ⟶ τ) = ♯ refl∞ (♭ σ) ⟶ ♯ refl∞ (♭ τ)

_∎ : ∀ {n} (τ : Tree n) → τ ≤∞P τ
τ ∎ = ⌜ refl∞ τ ⌝

trans : ∀ {n} {τ₁ τ₂ τ₃ : Tree n} →
        τ₁ ≤∞ τ₂ → τ₂ ≤∞ τ₃ → τ₁ ≤∞ τ₃
trans {τ₁ = τ₁} {τ₂} {τ₃} τ₁≤τ₂ τ₂≤τ₃ =
  ⟦ τ₁ ≤⟨ ⌜ τ₁≤τ₂ ⌝ ⟩
    τ₂ ≤⟨ ⌜ τ₂≤τ₃ ⌝ ⟩
    τ₃ ∎ ⟧P

unfold : ∀ {n} {τ₁ τ₂ : Ty (suc n)} →
         μ τ₁ ⟶ τ₂ ≤Coind unfold[μ τ₁ ⟶ τ₂ ]
unfold = ♯ refl∞ _ ⟶ ♯ refl∞ _

fold : ∀ {n} {τ₁ τ₂ : Ty (suc n)} →
       unfold[μ τ₁ ⟶ τ₂ ] ≤Coind μ τ₁ ⟶ τ₂
fold = ♯ refl∞ _ ⟶ ♯ refl∞ _

var:≤∞⟶≡ : ∀ {n} {x y : Fin n} →
           var x ≤∞ var y → Ty.var x ≡ Ty.var y
var:≤∞⟶≡ var = refl

left-proj : ∀ {n} {σ₁ σ₂ τ₁ τ₂ : ∞ (Tree n)} →
            σ₁ ⟶ σ₂ ≤∞ τ₁ ⟶ τ₂ → ♭ τ₁ ≤∞ ♭ σ₁
left-proj (τ₁≤σ₁ ⟶ σ₂≤τ₂) = ♭ τ₁≤σ₁

right-proj : ∀ {n} {σ₁ σ₂ τ₁ τ₂ : ∞ (Tree n)} →
             σ₁ ⟶ σ₂ ≤∞ τ₁ ⟶ τ₂ → ♭ σ₂ ≤∞ ♭ τ₂
right-proj (τ₁≤σ₁ ⟶ σ₂≤τ₂) = ♭ σ₂≤τ₂

------------------------------------------------------------------------
-- _≤∞_ is stable under double-negation

stable : ∀ {n} (σ τ : Tree n) → Stable (σ ≤∞ τ)
stable ⊥         τ         ¬≰ = ⊥
stable σ         ⊤         ¬≰ = ⊤
stable (var x)   (var  y)  ¬≰ with var x ≡? var y
stable (var x)   (var .x)  ¬≰ | yes refl = var
stable (var x)   (var  y)  ¬≰ | no  x≠y  = ⊥-elim (¬≰ (x≠y ∘ var:≤∞⟶≡))
stable (σ₁ ⟶ σ₂) (τ₁ ⟶ τ₂) ¬≰ =
  ♯ stable (♭ τ₁) (♭ σ₁) (λ ≰ → ¬≰ (≰ ∘  left-proj)) ⟶
  ♯ stable (♭ σ₂) (♭ τ₂) (λ ≰ → ¬≰ (≰ ∘ right-proj))
stable ⊤         ⊥         ¬≰ = ⊥-elim (¬≰ (λ ()))
stable ⊤         (var x)   ¬≰ = ⊥-elim (¬≰ (λ ()))
stable ⊤         (τ₁ ⟶ τ₂) ¬≰ = ⊥-elim (¬≰ (λ ()))
stable (var x)   ⊥         ¬≰ = ⊥-elim (¬≰ (λ ()))
stable (var x)   (τ₁ ⟶ τ₂) ¬≰ = ⊥-elim (¬≰ (λ ()))
stable (σ₁ ⟶ σ₂) ⊥         ¬≰ = ⊥-elim (¬≰ (λ ()))
stable (σ₁ ⟶ σ₂) (var x)   ¬≰ = ⊥-elim (¬≰ (λ ()))

ext: agda

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
import      Lvl
open import Type

module Structure.Logic.Constructive.Predicate
  {ℓₗ}  {Formula : Type{ℓₗ}}
  {ℓₘₗ} (Proof : Formula → Type{ℓₘₗ})
  {ℓₚ}  {Predicate : Type{ℓₚ}}
  {ℓₒ}  {Domain : Type{ℓₒ}}
  (_$_ : Predicate → Domain → Formula)
  where

import      Logic.Predicate as Meta
import      Structure.Logic.Constructive.Propositional as Propositional
open import Type.Properties.Inhabited using (◊)

private variable P : Predicate
private variable X Y Q : Formula
private variable x y z : Domain

-- Rules of universal quantification (for all).
record Universal(∀ₗ : Predicate → Formula) : Type{ℓₘₗ Lvl.⊔ Lvl.of(Formula) Lvl.⊔ Lvl.of(Domain) Lvl.⊔ Lvl.of(Predicate)} where
  field
    intro : (∀{x} → Proof(P $ x)) → Proof(∀ₗ P)
    elim  : Proof(∀ₗ P) → ∀{x} → Proof(P $ x)
∀ₗ = \ ⦃(Meta.[∃]-intro ▫) : Meta.∃(Universal)⦄ → ▫
module ∀ₗ {▫} ⦃ p ⦄ = Universal {▫} p

-- Rules of existential quantification (exists).
record Existential(∃ : Predicate → Formula) : Type{ℓₘₗ Lvl.⊔ Lvl.of(Formula) Lvl.⊔ Lvl.of(Domain) Lvl.⊔ Lvl.of(Predicate)} where
  field
    intro : Proof(P $ x) → Proof(∃ P)
    elim  : (∀{x} → Proof(P $ x) → Proof(Q)) → (Proof(∃ P) → Proof(Q))
∃ = \ ⦃(Meta.[∃]-intro ▫) : Meta.∃(Existential)⦄ → ▫
module ∃ {▫} ⦃ p ⦄ = Existential {▫} p

record ExistentialWitness(∃ : Predicate → Formula) : Type{ℓₘₗ Lvl.⊔ Lvl.of(Formula) Lvl.⊔ Lvl.of(Domain) Lvl.⊔ Lvl.of(Predicate)} where
  field
    witness : Proof(∃ P) → Domain
    proof   : (p : Proof(∃ P)) → Proof(P $ witness p)

NonEmptyDomain = ◊ Domain

record Equality(_≡_ : Domain → Domain → Formula) : Type{ℓₘₗ Lvl.⊔ Lvl.of(Formula) Lvl.⊔ Lvl.of(Domain) Lvl.⊔ Lvl.of(Domain)} where
  field
    reflexivity : Proof(x ≡ x)
    substitute  : (P : Domain → Formula) → Proof(x ≡ y) → (Proof(P(x)) → Proof(P(y)))

record Logic : Type{ℓₘₗ Lvl.⊔ Lvl.of(Formula) Lvl.⊔ Lvl.of(Domain) Lvl.⊔ Lvl.of(Predicate)} where
  field
    ⦃ propositional ⦄ : Propositional.Logic(Proof)
    ⦃ universal ⦄     : Meta.∃(Universal)
    ⦃ existential ⦄   : Meta.∃(Existential)

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 --rewriting #-}

-- Set-theoretic interpretation and consistency

open import Library

module Interpretation (Base : Set) (B⦅_⦆ : Base → Set) where

import Formulas   ; open module Form = Formulas    Base
import Derivations; open module Der  = Derivations Base

T⦅_⦆ : (A : Form) → Set
T⦅ Atom P ⦆ = B⦅ P ⦆
T⦅ True ⦆ = ⊤
T⦅ False ⦆ = ⊥
T⦅ A ∨ B ⦆ = T⦅ A ⦆ ⊎ T⦅ B ⦆
T⦅ A ∧ B ⦆ = T⦅ A ⦆ × T⦅ B ⦆
T⦅ A ⇒ B ⦆ = T⦅ A ⦆ → T⦅ B ⦆

C⦅_⦆ : (Γ : Cxt) → Set
C⦅ ε ⦆ = ⊤
C⦅ Γ ∙ A ⦆ = C⦅ Γ ⦆ × T⦅ A ⦆

Fun' : (Γ : Cxt) (S : Set) → Set
Fun' Γ S = (γ : C⦅ Γ ⦆) → S

Fun : (Γ : Cxt) (A : Form) → Set
Fun Γ A = Fun' Γ T⦅ A ⦆

Mor : (Γ Δ : Cxt) → Set
Mor Γ Δ = Fun' Γ C⦅ Δ ⦆

H⦅_⦆ : ∀{Γ A} (x : Hyp A Γ) → Fun Γ A
H⦅ top   ⦆ = proj₂
H⦅ pop x ⦆ = H⦅ x ⦆ ∘ proj₁

D⦅_⦆ : ∀{Γ A} (t : Γ ⊢ A) → Fun Γ A
D⦅ hyp x ⦆      = H⦅ x ⦆
D⦅ impI t ⦆     = curry D⦅ t ⦆
D⦅ impE t u ⦆   = apply D⦅ t ⦆ D⦅ u ⦆
D⦅ andI t u ⦆   = < D⦅ t ⦆ , D⦅ u ⦆ >
D⦅ andE₁ t ⦆    = proj₁ ∘ D⦅ t ⦆
D⦅ andE₂ t ⦆    = proj₂ ∘ D⦅ t ⦆
D⦅ orI₁ t ⦆     = inj₁ ∘ D⦅ t ⦆
D⦅ orI₂ t ⦆     = inj₂ ∘ D⦅ t ⦆
D⦅ orE t u v ⦆ = caseof D⦅ t ⦆ D⦅ u ⦆ D⦅ v ⦆
D⦅ falseE t ⦆  = ⊥-elim ∘ D⦅ t ⦆
D⦅ trueI ⦆      = _

consistency : (t : ε ⊢ False) → ⊥
consistency t = D⦅ t ⦆ _

Ne⦅_⦆ : ∀{Γ A} (t : Ne Γ A) → Fun Γ A
Ne⦅_⦆ = D⦅_⦆ ∘ ne[_]

Nf⦅_⦆ : ∀{Γ A} (t : Nf Γ A) → Fun Γ A
Nf⦅_⦆ = D⦅_⦆ ∘ nf[_]

-- Functor

R⦅_⦆ : ∀{Γ Δ} (τ : Γ ≤ Δ) → Mor Γ Δ
R⦅ ε      ⦆ = _
R⦅ weak τ ⦆ = R⦅ τ ⦆ ∘ proj₁
R⦅ lift τ ⦆ = R⦅ τ ⦆ ×̇ id

R-id : ∀ Γ (γ : C⦅ Γ ⦆)→ R⦅ id≤ {Γ} ⦆ γ ≡ γ
R-id ε γ = refl
R-id (Γ ∙ A) γ = cong₂ _,_ (R-id Γ (proj₁ γ)) refl

{-# REWRITE R-id #-}

-- Kripke application

kapp : ∀ A B {Γ} (f : Fun Γ (A ⇒ B)) {Δ} (τ : Δ ≤ Γ) (a : Fun Δ A) → Fun Δ B
kapp A B f τ a δ = f (R⦅ τ ⦆ δ) (a δ)

-- Naturality

natH  : ∀{Γ Δ A} (τ : Δ ≤ Γ) (x : Hyp A Γ) → H⦅ monH τ x ⦆ ≡ H⦅ x ⦆ ∘ R⦅ τ ⦆
natH ε ()
natH (weak τ) x = cong (_∘ proj₁) (natH τ x)
natH (lift τ) top = refl
natH (lift τ) (pop x) = cong (_∘ proj₁) (natH τ x)

{-# REWRITE natH #-}

natR : ∀{Γ Δ Φ} (σ : Φ ≤ Δ) (τ : Δ ≤ Γ) → R⦅ σ • τ ⦆ ≡ R⦅ τ ⦆ ∘ R⦅ σ ⦆
natR ε        τ = refl
natR (weak σ) τ = cong (_∘ proj₁) (natR σ τ)
natR (lift σ) (weak τ) = cong (_∘ proj₁) (natR σ τ)
natR (lift σ) (lift τ) = cong (_×̇ id) (natR σ τ)

{-# REWRITE natR #-}

natD : ∀{Γ Δ A} (τ : Δ ≤ Γ) (t : Γ ⊢ A) → D⦅ monD τ t ⦆ ≡ D⦅ t ⦆ ∘ R⦅ τ ⦆
natD τ (hyp x) = natH τ x
natD τ (impI t) = cong curry (natD (lift τ) t)
natD τ (impE t u) = cong₂ apply (natD τ t) (natD τ u)
natD τ (andI t u) = cong₂ <_,_> (natD τ t) (natD τ u)
natD τ (andE₁ t) = cong (proj₁ ∘_) (natD τ t)
natD τ (andE₂ t) = cong (proj₂ ∘_) (natD τ t)
natD τ (orI₁ t) = cong (inj₁ ∘_) (natD τ t)
natD τ (orI₂ t) = cong (inj₂ ∘_) (natD τ t)
natD τ (orE t u v) = cong₃ caseof (natD τ t) (natD (lift τ) u) (natD (lift τ) v)
natD τ (falseE t) = cong (⊥-elim ∘_) (natD τ t)
natD τ trueI = funExt λ _ → refl

{-# REWRITE natD #-}

-- -}

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


text:
module Implicits.Resolution.Embedding.Lemmas where

open import Prelude
open import Data.Fin.Substitution
open import Data.Vec hiding ([_]; _∈_)
open import Data.List as List hiding ([_]; map)
open import Data.List.Properties
open import Data.List.Any hiding (map)
open Membership-≡
open import Extensions.Vec
open import Data.Vec.Properties as VP using ()
open import Relation.Binary.HeterogeneousEquality as H using ()
module HR = H.≅-Reasoning

open import Implicits.Syntax
open import SystemF.Everything as F using ()
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas
open import Implicits.Resolution.Embedding

open TypeSubst hiding (subst)
private
  module TS = TypeSubst

length-weaken-Δ : ∀ {ν} (Δ : ICtx ν) →
  (List.length (List.map ⟦_⟧tp→ (ictx-weaken Δ))) ≡ (List.length (List.map ⟦_⟧tp→ Δ))
length-weaken-Δ Δ = begin
  (List.length (List.map ⟦_⟧tp→ (List.map (λ s → s / wk) Δ)))
    ≡⟨ cong List.length (sym $ map-compose Δ) ⟩
  (List.length (List.map (⟦_⟧tp→ ∘ (λ s → s / wk)) Δ))
    ≡⟨ length-map _ Δ ⟩
  List.length Δ
    ≡⟨ sym $ length-map _ Δ ⟩
  (List.length (List.map ⟦_⟧tp→ Δ)) ∎

tp→← : ∀ {ν} (a : Type ν) → ⟦ ⟦ a ⟧tp→ ⟧tp← ≡ a
tp→← (simpl (tc x)) = refl
tp→← (simpl (tvar n)) = refl
tp→← (simpl (x →' x₁)) = cong₂ (λ u v → simpl (u →' v)) (tp→← x) (tp→← x₁)
tp→← (a ⇒ b) = cong₂ _⇒_ (tp→← a) (tp→← b)
tp→← (∀' a) = cong ∀' (tp→← a)

tp←→ : ∀ {ν} (a : F.Type ν) → ⟦ ⟦ a ⟧tp← ⟧tp→ ≡ a
tp←→ (F.tc x) = refl
tp←→ (F.tvar n) = refl
tp←→ (x F.→' x₁) = cong₂ F._→'_ (tp←→ x) (tp←→ x₁)
tp←→ (a F.⟶ b) = cong₂ F._⟶_ (tp←→ a) (tp←→ b)
tp←→ (F.∀' a) = cong F.∀' (tp←→ a)

ctx→← : ∀ {ν} (Δ : ICtx ν) → ⟦ ⟦ Δ ⟧ctx→ ⟧ctx← ≡ Δ
ctx→← [] = refl
ctx→← (x ∷ xs) = begin
  ⟦ ⟦ x ∷ xs ⟧ctx→ ⟧ctx←
    ≡⟨ refl ⟩
  toList (map ⟦_⟧tp← (fromList (List.map ⟦_⟧tp→ (x List.∷ xs))))
    ≡⟨ refl ⟩
  ⟦ ⟦ x ⟧tp→ ⟧tp← List.∷ (toList (map ⟦_⟧tp← (fromList (List.map ⟦_⟧tp→ xs))))
    ≡⟨ cong₂ List._∷_ (tp→← x) (ctx→← xs) ⟩
  (x List.∷ xs) ∎

Γ-cong₂ : ∀ {ν n n'} {x x' : F.Type ν} {xs : F.Ctx ν n} {xs' : F.Ctx ν n'} →
          n ≡ n' → x ≡ x' → xs H.≅ xs' → (x Vec.∷ xs) H.≅ (x' Vec.∷ xs')
Γ-cong₂ refl refl H.refl = H.refl

ctx←→ : ∀ {ν n} (Γ : F.Ctx ν n) → ⟦ ⟦ Γ ⟧ctx← ⟧ctx→ H.≅ Γ
ctx←→ [] = H.refl
ctx←→ {ν = ν} (x ∷ xs) = HR.begin
  ⟦ ⟦ x ∷ xs ⟧ctx← ⟧ctx→
    HR.≡⟨ refl ⟩
  ⟦ ⟦ x ⟧tp← ⟧tp→ ∷ ⟦ ⟦ xs ⟧ctx← ⟧ctx→
    HR.≅⟨ Γ-cong₂ (length-map-toList (map ⟦_⟧tp← xs)) (tp←→ x) (ctx←→ xs) ⟩
  (x ∷ xs) HR.∎

⟦a/var⟧tp← : ∀ {ν ν'} (a : F.Type ν) (s : Vec (Fin ν') ν) → ⟦ a F./Var s ⟧tp← ≡ ⟦ a ⟧tp← /Var s
⟦a/var⟧tp← (F.tc x) s = refl
⟦a/var⟧tp← (F.tvar n) s = refl
⟦a/var⟧tp← (a F.→' b) s = cong₂ _⇒_ (⟦a/var⟧tp← a s) (⟦a/var⟧tp← b s)
⟦a/var⟧tp← (a F.⟶ b) s = cong₂ (λ u v → simpl (u →' v)) (⟦a/var⟧tp← a s) (⟦a/var⟧tp← b s)
⟦a/var⟧tp← (F.∀' a) s = cong ∀' (⟦a/var⟧tp← a (s VarSubst.↑))

⟦a/var⟧tp→ : ∀ {ν ν'} (a : Type ν) (s : Vec (Fin ν') ν) → ⟦ a /Var s ⟧tp→ ≡ ⟦ a ⟧tp→ F./Var s
⟦a/var⟧tp→ (simpl (tc x)) s = refl
⟦a/var⟧tp→ (simpl (tvar n)) s = refl
⟦a/var⟧tp→ (simpl (a →' b)) s = cong₂ F._⟶_ (⟦a/var⟧tp→ a s) (⟦a/var⟧tp→ b s)
⟦a/var⟧tp→ (a ⇒ b) s = cong₂ F._→'_ (⟦a/var⟧tp→ a s) (⟦a/var⟧tp→ b s)
⟦a/var⟧tp→ (∀' a) s = cong F.∀' (⟦a/var⟧tp→ a (s VarSubst.↑))

⟦weaken⟧tp← : ∀ {ν} (a : F.Type ν) → ⟦ F.weaken a ⟧tp← ≡ weaken ⟦ a ⟧tp←
⟦weaken⟧tp← x = ⟦a/var⟧tp← x VarSubst.wk

⟦weaken⟧tp→ : ∀ {ν} (a : Type ν) → ⟦ weaken a ⟧tp→ ≡ F.weaken ⟦ a ⟧tp→
⟦weaken⟧tp→ x = ⟦a/var⟧tp→ x VarSubst.wk

-- helper lemma on mapping type-semantics over weakend substitutions
⟦⟧tps←⋆weaken : ∀ {ν n} (xs : Vec (F.Type ν) n) →
                ⟦ (map F.weaken xs) ⟧tps← ≡ (map weaken ⟦ xs ⟧tps←)
⟦⟧tps←⋆weaken xs = begin
  (map ⟦_⟧tp← ∘ map F.weaken) xs
    ≡⟨ sym $ (VP.map-∘ ⟦_⟧tp← F.weaken) xs ⟩
  map (⟦_⟧tp← ∘ F.weaken) xs
  ≡⟨ (VP.map-cong ⟦weaken⟧tp←) xs ⟩
  map (TS.weaken ∘ ⟦_⟧tp←) xs
    ≡⟨ (VP.map-∘ TS.weaken ⟦_⟧tp←) xs ⟩
  map TS.weaken (map ⟦_⟧tp← xs) ∎

-- helper lemma on mapping type-semantics over weakend substitutions
⟦⟧tps→⋆weaken : ∀ {ν n} (xs : Vec (Type ν) n) →
                ⟦ (map TS.weaken xs) ⟧tps→ ≡ (map F.weaken ⟦ xs ⟧tps→)
⟦⟧tps→⋆weaken xs = begin
  (map ⟦_⟧tp→ ∘ map TS.weaken) xs
    ≡⟨ sym $ (VP.map-∘ ⟦_⟧tp→ TS.weaken) xs ⟩
  map (⟦_⟧tp→ ∘ TS.weaken) xs
  ≡⟨ (VP.map-cong ⟦weaken⟧tp→) xs ⟩
  map (F.weaken ∘ ⟦_⟧tp→) xs
    ≡⟨ (VP.map-∘ F.weaken ⟦_⟧tp→) xs ⟩
  map F.weaken (map ⟦_⟧tp→ xs) ∎

-- the semantics of identity type-substitution is exactly
-- system-f's identity type substitution
⟦id⟧tp← : ∀ {n} → map ⟦_⟧tp← (F.id {n}) ≡ TS.id
⟦id⟧tp← {zero} = refl
⟦id⟧tp← {suc n} = begin
  map ⟦_⟧tp← (F.tvar zero ∷ map F.weaken (F.id {n}))
    ≡⟨ refl ⟩
  (simpl (tvar zero)) ∷ (map ⟦_⟧tp← (map F.weaken (F.id {n})))
    ≡⟨ cong (_∷_ (simpl (tvar zero))) (⟦⟧tps←⋆weaken (F.id {n})) ⟩
  (simpl (tvar zero)) ∷ (map TS.weaken (map ⟦_⟧tp← (F.id {n})))
    ≡⟨ cong (λ e → simpl (tvar zero) ∷ (map TS.weaken e)) ⟦id⟧tp← ⟩
  (simpl (tvar zero)) ∷ (map TS.weaken (TS.id {n}))
    ≡⟨ refl ⟩
  TS.id ∎

-- the semantics of identity type-substitution is exactly
-- system-f's identity type substitution
⟦id⟧tp→ : ∀ {n} → map ⟦_⟧tp→ (TS.id {n}) ≡ F.id
⟦id⟧tp→ {zero} = refl
⟦id⟧tp→ {suc n} = begin
  map ⟦_⟧tp→ (simpl (tvar zero) ∷ map TS.weaken (TS.id {n}))
    ≡⟨ refl ⟩
  F.tvar zero ∷ (map ⟦_⟧tp→ (map TS.weaken (TS.id {n})))
    ≡⟨ cong (_∷_ (F.tvar zero)) (⟦⟧tps→⋆weaken (TS.id {n})) ⟩
  F.tvar zero ∷ (map F.weaken (map ⟦_⟧tp→ (TS.id {n})))
    ≡⟨ cong (λ e → F.tvar zero ∷ (map F.weaken e)) ⟦id⟧tp→ ⟩
  F.tvar zero ∷ (map F.weaken (F.id {n}))
    ≡⟨ refl ⟩
  F.id ∎

-- the semantics of type weakening is exactly system-f's type weakening
⟦wk⟧tp← : ∀ {n} → map ⟦_⟧tp← (F.wk {n}) ≡ TS.wk {n}
⟦wk⟧tp← = begin
  map ⟦_⟧tp← F.wk
    ≡⟨ ⟦⟧tps←⋆weaken F.id ⟩
  map TS.weaken (map ⟦_⟧tp← F.id)
    ≡⟨ cong (map TS.weaken) ⟦id⟧tp← ⟩
  TS.wk ∎

-- the semantics of type weakening is exactly system-f's type weakening
⟦wk⟧tp→ : ∀ {n} → map ⟦_⟧tp→ (TS.wk {n}) ≡ F.wk {n}
⟦wk⟧tp→ = begin
  map ⟦_⟧tp→ TS.wk
    ≡⟨ ⟦⟧tps→⋆weaken TS.id ⟩
  map F.weaken (map ⟦_⟧tp→ TS.id)
    ≡⟨ cong (map F.weaken) ⟦id⟧tp→ ⟩
  F.wk ∎

⟦⟧tps←⋆↑ :  ∀ {ν n} (v : Vec (F.Type ν) n) → ⟦ v F.↑ ⟧tps← ≡ ⟦ v ⟧tps← TS.↑
⟦⟧tps←⋆↑ xs = begin
  (simpl (tvar zero)) ∷ (map ⟦_⟧tp← (map F.weaken xs))
    ≡⟨ cong (_∷_ (simpl (tvar zero))) (⟦⟧tps←⋆weaken xs) ⟩
  (simpl (tvar zero)) ∷ (map TS.weaken (map ⟦_⟧tp← xs))
    ≡⟨ refl ⟩
  (map ⟦_⟧tp← xs) TS.↑ ∎

⟦⟧tps→⋆↑ :  ∀ {ν n} (v : Vec (Type ν) n) → ⟦ v TS.↑ ⟧tps→ ≡ ⟦ v ⟧tps→ F.↑
⟦⟧tps→⋆↑ xs = begin
  F.tvar zero ∷ (map ⟦_⟧tp→ (map TS.weaken xs))
    ≡⟨ cong (_∷_ (F.tvar zero)) (⟦⟧tps→⋆weaken xs) ⟩
  F.tvar zero ∷ (map F.weaken (map ⟦_⟧tp→ xs))
    ≡⟨ refl ⟩
  (map ⟦_⟧tp→ xs) F.↑ ∎

-- type substitution commutes with interpreting types
/⋆⟦⟧tp← : ∀ {ν μ} (tp : F.Type ν) (σ : Sub F.Type ν μ) → ⟦ tp F./ σ ⟧tp← ≡ ⟦ tp ⟧tp← TS./ (map ⟦_⟧tp← σ)
/⋆⟦⟧tp← (F.tc c) σ = refl
/⋆⟦⟧tp← (F.tvar n) σ = begin
  ⟦ lookup n σ ⟧tp←
    ≡⟨ lookup⋆map σ ⟦_⟧tp← n ⟩
  ⟦ F.tvar n ⟧tp← TS./ (map ⟦_⟧tp← σ) ∎
/⋆⟦⟧tp← (l F.→' r) σ = cong₂ _⇒_ (/⋆⟦⟧tp← l σ) (/⋆⟦⟧tp← r σ)
/⋆⟦⟧tp← (l F.⟶ r) σ = cong₂ (λ u v → simpl (u →' v)) (/⋆⟦⟧tp← l σ) (/⋆⟦⟧tp← r σ)
/⋆⟦⟧tp← (F.∀' a) σ = begin
  ∀' ⟦ (a F./ σ F.↑) ⟧tp←
    ≡⟨ cong ∀' (/⋆⟦⟧tp← a (σ F.↑)) ⟩
  ∀' (⟦ a ⟧tp← / ⟦ σ F.↑ ⟧tps←)
    ≡⟨ cong (λ u → ∀' (⟦ a ⟧tp← TS./ u)) ((⟦⟧tps←⋆↑ σ)) ⟩
  ⟦ F.∀' a ⟧tp← / (map ⟦_⟧tp← σ) ∎

-- type substitution commutes with interpreting types
/⋆⟦⟧tp→ : ∀ {ν μ} (tp : Type ν) (σ : Sub Type ν μ) → ⟦ tp TS./ σ ⟧tp→ ≡ ⟦ tp ⟧tp→ F./ (map ⟦_⟧tp→ σ)
/⋆⟦⟧tp→ (simpl (tc c)) σ = refl
/⋆⟦⟧tp→ (simpl (tvar n)) σ = begin
  ⟦ lookup n σ ⟧tp→
    ≡⟨ lookup⋆map σ ⟦_⟧tp→ n ⟩
  ⟦ simpl (tvar n) ⟧tp→ F./ (map ⟦_⟧tp→ σ) ∎
/⋆⟦⟧tp→ (l ⇒ r) σ = cong₂ F._→'_ (/⋆⟦⟧tp→ l σ) (/⋆⟦⟧tp→ r σ)
/⋆⟦⟧tp→ (simpl (l →' r)) σ = cong₂ F._⟶_ (/⋆⟦⟧tp→ l σ) (/⋆⟦⟧tp→ r σ)
/⋆⟦⟧tp→ (∀' a) σ = begin
  F.∀' ⟦ (a TS./ σ TS.↑) ⟧tp→
    ≡⟨ cong F.∀' (/⋆⟦⟧tp→ a (σ TS.↑)) ⟩
  F.∀' (⟦ a ⟧tp→ F./ ⟦ σ TS.↑ ⟧tps→)
    ≡⟨ cong (λ u → F.∀' (⟦ a ⟧tp→ F./ u)) ((⟦⟧tps→⋆↑ σ)) ⟩
  ⟦ ∀' a ⟧tp→ F./ (map ⟦_⟧tp→ σ) ∎

⟦a/sub⟧tp← : ∀ {ν} (a : F.Type (suc ν)) b → ⟦ a F./ (F.sub b) ⟧tp← ≡ ⟦ a ⟧tp← TS./ (TS.sub ⟦ b ⟧tp←)
⟦a/sub⟧tp← a b = begin
  ⟦ a F./ (F.sub b) ⟧tp←
  ≡⟨ /⋆⟦⟧tp← a (b ∷ F.id) ⟩
  (⟦ a ⟧tp← TS./ (map ⟦_⟧tp← (b ∷ F.id)) )
  ≡⟨ refl ⟩
  (⟦ a ⟧tp← TS./ (⟦ b ⟧tp← ∷ (map ⟦_⟧tp← F.id)) )
  ≡⟨ cong (λ s → ⟦ a ⟧tp← TS./ (⟦ b ⟧tp← ∷ s)) ⟦id⟧tp← ⟩
  (⟦ a ⟧tp← TS./ (TS.sub ⟦ b ⟧tp←)) ∎

⟦a/wk⟧tp← : ∀ {ν} → (a : F.Type ν) → ⟦ a F./ F.wk ⟧tp← ≡ ⟦ a ⟧tp← / wk
⟦a/wk⟧tp← tp = begin
  ⟦ tp F./ F.wk ⟧tp←
    ≡⟨ /⋆⟦⟧tp← tp F.wk ⟩
  ⟦ tp ⟧tp← / (map ⟦_⟧tp← F.wk)
    ≡⟨ cong (λ e → ⟦ tp ⟧tp← / e) ⟦wk⟧tp← ⟩
  ⟦ tp ⟧tp← / wk ∎

⟦a/wk⟧tp→ : ∀ {ν} → (a : Type ν) → ⟦ a / wk ⟧tp→ ≡ ⟦ a ⟧tp→ F./ F.wk
⟦a/wk⟧tp→ tp = begin
  ⟦ tp TS./ TS.wk ⟧tp→
    ≡⟨ /⋆⟦⟧tp→ tp TS.wk ⟩
  ⟦ tp ⟧tp→ F./ (map ⟦_⟧tp→ TS.wk)
    ≡⟨ cong (λ e → ⟦ tp ⟧tp→ F./ e) ⟦wk⟧tp→ ⟩
  ⟦ tp ⟧tp→ F./ F.wk ∎

⟦weaken⟧ctx← : ∀ {ν n} (Γ : F.Ctx ν n) → ⟦ F.ctx-weaken Γ ⟧ctx← ≡ ictx-weaken ⟦ Γ ⟧ctx←
⟦weaken⟧ctx← [] = refl
⟦weaken⟧ctx← (x ∷ xs) = begin
  ⟦ F.ctx-weaken (x ∷ xs) ⟧ctx←
    ≡⟨ refl ⟩
  toList (map ⟦_⟧tp← (map (flip F._/_ F.wk) (x ∷ xs)))
    ≡⟨ cong toList (sym (VP.map-∘ _ _ (x ∷ xs))) ⟩
  (⟦ x F./ F.wk ⟧tp← List.∷ (toList (map (⟦_⟧tp← ∘ (flip F._/_ F.wk)) xs)))
    ≡⟨ cong (λ u → ⟦ F._/_ x F.wk ⟧tp← List.∷ toList u) (VP.map-∘ _ _ xs) ⟩
  (⟦ x F./ F.wk ⟧tp← List.∷ ⟦ F.ctx-weaken xs ⟧ctx←)
    ≡⟨ cong (λ u → ⟦ F._/_ x F.wk ⟧tp← List.∷ u) (⟦weaken⟧ctx← xs) ⟩
  (⟦ x F./ F.wk ⟧tp← List.∷ (ictx-weaken ⟦ xs ⟧ctx←))
    ≡⟨ cong (flip List._∷_ (ictx-weaken ⟦ xs ⟧ctx←)) (⟦a/wk⟧tp← x) ⟩
  ictx-weaken ⟦ x ∷ xs ⟧ctx← ∎

⟦weaken⟧ctx→ : ∀ {ν} (Δ : ICtx ν) → F.ctx-weaken ⟦ Δ ⟧ctx→ H.≅ ⟦ ictx-weaken Δ ⟧ctx→
⟦weaken⟧ctx→ List.[] = H.refl
⟦weaken⟧ctx→ (x List.∷ xs) = HR.begin
  F.ctx-weaken ⟦ x List.∷ xs ⟧ctx→
    HR.≅⟨ H.refl ⟩
  (⟦ x ⟧tp→ F./ F.wk) Vec.∷ F.ctx-weaken ⟦ xs ⟧ctx→
    HR.≅⟨ ∷-cong (sym (length-weaken-Δ xs)) (⟦weaken⟧ctx→ xs) ⟩
  (⟦ x ⟧tp→ F./ F.wk) Vec.∷ ⟦ ictx-weaken xs ⟧ctx→
    HR.≅⟨ H.cong (flip Vec._∷_ ⟦ ictx-weaken xs ⟧ctx→) (H.≡-to-≅ $ sym $ ⟦a/wk⟧tp→ x) ⟩
  ⟦ x / wk ⟧tp→ ∷ ⟦ ictx-weaken xs ⟧ctx→
    HR.≅⟨ H.cong (λ u → ⟦ x / wk ⟧tp→ Vec.∷ fromList u) (H.≡-to-≅ (sym (map-compose xs))) ⟩
  (fromList (List.map (⟦_⟧tp→ ∘ (λ s → s / wk)) (x List.∷ xs)))
    HR.≅⟨ H.cong fromList (H.≡-to-≅ (map-compose (x List.∷ xs))) ⟩
  ⟦ ictx-weaken (x List.∷ xs) ⟧ctx→ HR.∎

⟦a/sub⟧tp→ : ∀ {ν} (a : Type (suc ν)) b → ⟦ a TS./ (TS.sub b) ⟧tp→ ≡ ⟦ a ⟧tp→ F./ (F.sub ⟦ b ⟧tp→)
⟦a/sub⟧tp→ a b = begin
  ⟦ a TS./ (TS.sub b) ⟧tp→
  ≡⟨ /⋆⟦⟧tp→ a (b ∷ TS.id) ⟩
  (⟦ a ⟧tp→ F./ (map ⟦_⟧tp→ (b ∷ TS.id)) )
  ≡⟨ refl ⟩
  (⟦ a ⟧tp→ F./ (⟦ b ⟧tp→ ∷ (map ⟦_⟧tp→ TS.id)) )
  ≡⟨ cong (λ s → ⟦ a ⟧tp→ F./ (⟦ b ⟧tp→ ∷ s)) ⟦id⟧tp→ ⟩
  (⟦ a ⟧tp→ F./ (F.sub ⟦ b ⟧tp→)) ∎

⊢subst-n : ∀ {ν n n'} {Γ : F.Ctx ν n} {Γ' : F.Ctx ν n'} {t a} → (n-eq : n ≡ n') →
            Γ H.≅ Γ' → Γ F.⊢ t ∈ a →
            Γ' F.⊢ (subst (F.Term ν) n-eq t) ∈ a
⊢subst-n refl H.refl p = p

lookup-subst-n : ∀ {n n' l} {A : Set l} {v : Vec A n} {v' : Vec A n'} {i : Fin n} →
                  (n-eq : n ≡ n') →
                  (v H.≅ v') →
                  (lookup i v) ≡ (lookup (subst Fin n-eq i) v')
lookup-subst-n refl H.refl = refl

lookup⟦⟧ : ∀ {ν} (Δ : ICtx ν) {r} i → lookup i (fromList Δ) ≡ r →
            (lookup (subst Fin (sym $ length-map _ Δ) i) ⟦ Δ ⟧ctx→) ≡ ⟦ r ⟧tp→
lookup⟦⟧ Δ {r = r} i eq = begin
  (lookup (subst Fin (sym $ length-map _ Δ) i) ⟦ Δ ⟧ctx→)
    ≡⟨ refl ⟩
  (lookup (subst Fin (sym $ length-map _ Δ) i) (fromList $ (List.map ⟦_⟧tp→ Δ)))
    ≡⟨ sym $ lookup-subst-n (sym $ length-map _ Δ) (H.sym $ fromList-map _ Δ) ⟩
  (lookup i (map ⟦_⟧tp→ (fromList Δ)))
    ≡⟨ sym $ lookup⋆map (fromList Δ) ⟦_⟧tp→ i ⟩
  ⟦ lookup i (fromList Δ) ⟧tp→
    ≡⟨ cong ⟦_⟧tp→ eq ⟩
  ⟦ r ⟧tp→ ∎

lookup-∈ : ∀ {ν n} → (x : Fin n) → (v : F.Ctx ν n) → ⟦ lookup x v ⟧tp← ∈ ⟦ v ⟧ctx←
lookup-∈ zero (x ∷ xs) = here refl
lookup-∈ (suc x) (v ∷ vs) = there (lookup-∈ x vs)

⇑-subst-n : ∀ {ν n n'} {Γ : F.Ctx ν n} {Γ' : F.Ctx ν n'} {t a} → (n-eq : n ≡ n') →
            Γ H.≅ Γ' → Γ F.⊢ t ⇑ a →
            Γ' F.⊢ (subst (F.Term ν) n-eq t) ⇑ a
⇑-subst-n refl H.refl p = p

⟦base⟧tp← : ∀ {ν} {a : F.Type ν} → F.Base a → ∃ λ τ → ⟦ a ⟧tp← ≡ (simpl τ)
⟦base⟧tp← (F.tc n) = tc n , refl
⟦base⟧tp← (F.tvar n) = tvar n , refl
⟦base⟧tp← (a F.⟶ b) = ⟦ a ⟧tp← →' ⟦ b ⟧tp← , refl

⟦simpl⟧tp→ : ∀ {ν} (τ : SimpleType ν) → F.Base ⟦ simpl τ ⟧tp→
⟦simpl⟧tp→ (tc x) = F.tc x
⟦simpl⟧tp→ (tvar n) = F.tvar n
⟦simpl⟧tp→ (x →' x₁) = ⟦ x ⟧tp→ F.⟶ ⟦ x₁ ⟧tp→

open import Function.Inverse

tp-iso : ∀ {ν} → (→-to-⟶ (⟦_⟧tp→ {ν = ν})) InverseOf (→-to-⟶ (⟦_⟧tp← {ν = ν}))
tp-iso = record { left-inverse-of = tp←→ ; right-inverse-of = tp→← }


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

syntax Monoid | M

type
  * : 0-ary

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

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

module Monoid.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import Monoid.Signature
open import Monoid.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution M:Syn
open import SOAS.Metatheory.SecondOrder.Equality M:Syn

private
  variable
    α β γ τ : *T
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ M) α Γ → (𝔐 ▷ M) α Γ → Set where
  εU⊕ᴸ : ⁅ * ⁆̣             ▹ ∅ ⊢       ε ⊕ 𝔞 ≋ₐ 𝔞
  εU⊕ᴿ : ⁅ * ⁆̣             ▹ ∅ ⊢       𝔞 ⊕ ε ≋ₐ 𝔞
  ⊕A   : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (𝔞 ⊕ 𝔟) ⊕ 𝔠 ≋ₐ 𝔞 ⊕ (𝔟 ⊕ 𝔠)

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
------------------------------------------------------------------------
-- Sums of binary relations
------------------------------------------------------------------------

module Relation.Binary.Sum where

open import Data.Function
open import Data.Sum as Sum
open import Data.Product
open import Data.Unit using (⊤)
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary

infixr 1 _⊎-Rel_ _⊎-<_

------------------------------------------------------------------------
-- Sums of relations

-- Generalised sum.

data ⊎ʳ (P : Set) {a₁ : Set} (_∼₁_ : Rel a₁)
                  {a₂ : Set} (_∼₂_ : Rel a₂)
          : a₁ ⊎ a₂ → a₁ ⊎ a₂ → Set where
  ₁∼₂ : ∀ {x y} (p : P)         → ⊎ʳ P _∼₁_ _∼₂_ (inj₁ x) (inj₂ y)
  ₁∼₁ : ∀ {x y} (x∼₁y : x ∼₁ y) → ⊎ʳ P _∼₁_ _∼₂_ (inj₁ x) (inj₁ y)
  ₂∼₂ : ∀ {x y} (x∼₂y : x ∼₂ y) → ⊎ʳ P _∼₁_ _∼₂_ (inj₂ x) (inj₂ y)

-- Pointwise sum.

_⊎-Rel_ : ∀ {a₁} (_∼₁_ : Rel a₁) →
          ∀ {a₂} (_∼₂_ : Rel a₂) →
          Rel (a₁ ⊎ a₂)
_⊎-Rel_ = ⊎ʳ ⊥

-- All things to the left are smaller than (or equal to, depending on
-- the underlying equality) all things to the right.

_⊎-<_ : ∀ {a₁} (_∼₁_ : Rel a₁) →
        ∀ {a₂} (_∼₂_ : Rel a₂) →
        Rel (a₁ ⊎ a₂)
_⊎-<_ = ⊎ʳ ⊤

------------------------------------------------------------------------
-- Helpers

private

  ₁≁₂ : ∀ {a₁} {∼₁ : Rel a₁} →
        ∀ {a₂} {∼₂ : Rel a₂} →
        ∀ {x y} → ¬ (inj₁ x ⟨ ∼₁ ⊎-Rel ∼₂ ⟩₁ inj₂ y)
  ₁≁₂ (₁∼₂ ())

  drop-inj₁ : ∀ {a₁} {∼₁ : Rel a₁} →
              ∀ {a₂} {∼₂ : Rel a₂} →
              ∀ {P x y} → inj₁ x ⟨ ⊎ʳ P ∼₁ ∼₂ ⟩₁ inj₁ y → ∼₁ x y
  drop-inj₁ (₁∼₁ x∼y) = x∼y

  drop-inj₂ : ∀ {a₁} {∼₁ : Rel a₁} →
              ∀ {a₂} {∼₂ : Rel a₂} →
              ∀ {P x y} → inj₂ x ⟨ ⊎ʳ P ∼₁ ∼₂ ⟩₁ inj₂ y → ∼₂ x y
  drop-inj₂ (₂∼₂ x∼y) = x∼y

------------------------------------------------------------------------
-- Some properties which are preserved by the relation formers above

_⊎-reflexive_ : ∀ {a₁} {≈₁ ∼₁ : Rel a₁} → ≈₁ ⇒ ∼₁ →
                ∀ {a₂} {≈₂ ∼₂ : Rel a₂} → ≈₂ ⇒ ∼₂ →
                ∀ {P} → (≈₁ ⊎-Rel ≈₂) ⇒ (⊎ʳ P ∼₁ ∼₂)
refl₁ ⊎-reflexive refl₂ = refl
  where
  refl : (_ ⊎-Rel _) ⇒ (⊎ʳ _ _ _)
  refl (₁∼₁ x₁≈y₁) = ₁∼₁ (refl₁ x₁≈y₁)
  refl (₂∼₂ x₂≈y₂) = ₂∼₂ (refl₂ x₂≈y₂)
  refl (₁∼₂ ())

_⊎-refl_ : ∀ {a₁} {∼₁ : Rel a₁} → Reflexive ∼₁ →
           ∀ {a₂} {∼₂ : Rel a₂} → Reflexive ∼₂ →
           Reflexive (∼₁ ⊎-Rel ∼₂)
refl₁ ⊎-refl refl₂ = refl
  where
  refl : Reflexive (_ ⊎-Rel _)
  refl {x = inj₁ _} = ₁∼₁ refl₁
  refl {x = inj₂ _} = ₂∼₂ refl₂

_⊎-irreflexive_ : ∀ {a₁} {≈₁ <₁ : Rel a₁} → Irreflexive ≈₁ <₁ →
                  ∀ {a₂} {≈₂ <₂ : Rel a₂} → Irreflexive ≈₂ <₂ →
                  ∀ {P} → Irreflexive (≈₁ ⊎-Rel ≈₂) (⊎ʳ P <₁ <₂)
irrefl₁ ⊎-irreflexive irrefl₂ = irrefl
  where
  irrefl : Irreflexive (_ ⊎-Rel _) (⊎ʳ _ _ _)
  irrefl (₁∼₁ x₁≈y₁) (₁∼₁ x₁<y₁) = irrefl₁ x₁≈y₁ x₁<y₁
  irrefl (₂∼₂ x₂≈y₂) (₂∼₂ x₂<y₂) = irrefl₂ x₂≈y₂ x₂<y₂
  irrefl (₁∼₂ ())    _

_⊎-symmetric_ : ∀ {a₁} {∼₁ : Rel a₁} → Symmetric ∼₁ →
                ∀ {a₂} {∼₂ : Rel a₂} → Symmetric ∼₂ →
                Symmetric (∼₁ ⊎-Rel ∼₂)
sym₁ ⊎-symmetric sym₂ = sym
  where
  sym : Symmetric (_ ⊎-Rel _)
  sym (₁∼₁ x₁∼y₁) = ₁∼₁ (sym₁ x₁∼y₁)
  sym (₂∼₂ x₂∼y₂) = ₂∼₂ (sym₂ x₂∼y₂)
  sym (₁∼₂ ())

_⊎-transitive_ : ∀ {a₁} {∼₁ : Rel a₁} → Transitive ∼₁ →
                 ∀ {a₂} {∼₂ : Rel a₂} → Transitive ∼₂ →
                 ∀ {P} → Transitive (⊎ʳ P ∼₁ ∼₂)
trans₁ ⊎-transitive trans₂ = trans
  where
  trans : Transitive (⊎ʳ _ _ _)
  trans (₁∼₁ x∼y) (₁∼₁ y∼z) = ₁∼₁ (trans₁ x∼y y∼z)
  trans (₂∼₂ x∼y) (₂∼₂ y∼z) = ₂∼₂ (trans₂ x∼y y∼z)
  trans (₁∼₂ p)   (₂∼₂ _)     = ₁∼₂ p
  trans (₁∼₁ _)   (₁∼₂ p)     = ₁∼₂ p

_⊎-antisymmetric_ : ∀ {a₁} {≈₁ ≤₁ : Rel a₁} → Antisymmetric ≈₁ ≤₁ →
                    ∀ {a₂} {≈₂ ≤₂ : Rel a₂} → Antisymmetric ≈₂ ≤₂ →
                    ∀ {P} → Antisymmetric (≈₁ ⊎-Rel ≈₂) (⊎ʳ P ≤₁ ≤₂)
antisym₁ ⊎-antisymmetric antisym₂ = antisym
  where
  antisym : Antisymmetric (_ ⊎-Rel _) (⊎ʳ _ _ _)
  antisym (₁∼₁ x≤y) (₁∼₁ y≤x) = ₁∼₁ (antisym₁ x≤y y≤x)
  antisym (₂∼₂ x≤y) (₂∼₂ y≤x) = ₂∼₂ (antisym₂ x≤y y≤x)
  antisym (₁∼₂ _)   ()

_⊎-asymmetric_ : ∀ {a₁} {<₁ : Rel a₁} → Asymmetric <₁ →
                 ∀ {a₂} {<₂ : Rel a₂} → Asymmetric <₂ →
                 ∀ {P} → Asymmetric (⊎ʳ P <₁ <₂)
asym₁ ⊎-asymmetric asym₂ = asym
  where
  asym : Asymmetric (⊎ʳ _ _ _)
  asym (₁∼₁ x<y) (₁∼₁ y<x) = asym₁ x<y y<x
  asym (₂∼₂ x<y) (₂∼₂ y<x) = asym₂ x<y y<x
  asym (₁∼₂ _)   ()

_⊎-≈-respects₂_ : ∀ {a₁} {≈₁ ∼₁ : Rel a₁} → ∼₁ Respects₂ ≈₁ →
                  ∀ {a₂} {≈₂ ∼₂ : Rel a₂} → ∼₂ Respects₂ ≈₂ →
                  ∀ {P} → (⊎ʳ P ∼₁ ∼₂) Respects₂ (≈₁ ⊎-Rel ≈₂)
_⊎-≈-respects₂_ {≈₁ = ≈₁} {∼₁ = ∼₁} resp₁
                {≈₂ = ≈₂} {∼₂ = ∼₂} resp₂ {P} =
  (λ {_ _ _} → resp¹) ,
  (λ {_ _ _} → resp²)
  where
  resp¹ : ∀ {x} → ((⊎ʳ P ∼₁ ∼₂) x) Respects (≈₁ ⊎-Rel ≈₂)
  resp¹ (₁∼₁ y≈y') (₁∼₁ x∼y) = ₁∼₁ (proj₁ resp₁ y≈y' x∼y)
  resp¹ (₂∼₂ y≈y') (₂∼₂ x∼y) = ₂∼₂ (proj₁ resp₂ y≈y' x∼y)
  resp¹ (₂∼₂ y≈y') (₁∼₂ p)   = (₁∼₂ p)
  resp¹ (₁∼₂ ())   _

  resp² :  ∀ {y}
        → (flip₁ (⊎ʳ P ∼₁ ∼₂) y) Respects (≈₁ ⊎-Rel ≈₂)
  resp² (₁∼₁ x≈x') (₁∼₁ x∼y) = ₁∼₁ (proj₂ resp₁ x≈x' x∼y)
  resp² (₂∼₂ x≈x') (₂∼₂ x∼y) = ₂∼₂ (proj₂ resp₂ x≈x' x∼y)
  resp² (₁∼₁ x≈x') (₁∼₂ p)   = (₁∼₂ p)
  resp² (₁∼₂ ())   _

_⊎-substitutive_ : ∀ {a₁} {∼₁ : Rel a₁} → Substitutive ∼₁ →
                   ∀ {a₂} {∼₂ : Rel a₂} → Substitutive ∼₂ →
                   Substitutive (∼₁ ⊎-Rel ∼₂)
subst₁ ⊎-substitutive subst₂ = subst
  where
  subst : Substitutive (_ ⊎-Rel _)
  subst P (₁∼₁ x∼y) Px = subst₁ (λ z → P (inj₁ z)) x∼y Px
  subst P (₂∼₂ x∼y) Px = subst₂ (λ z → P (inj₂ z)) x∼y Px
  subst P (₁∼₂ ())  Px

⊎-decidable : ∀ {a₁} {∼₁ : Rel a₁} → Decidable ∼₁ →
              ∀ {a₂} {∼₂ : Rel a₂} → Decidable ∼₂ →
              ∀ {P} → (∀ {x y} → Dec (inj₁ x ⟨ ⊎ʳ P ∼₁ ∼₂ ⟩₁ inj₂ y)) →
              Decidable (⊎ʳ P ∼₁ ∼₂)
⊎-decidable {∼₁ = ∼₁} dec₁ {∼₂ = ∼₂} dec₂ {P} dec₁₂ = dec
  where
  dec : Decidable (⊎ʳ P ∼₁ ∼₂)
  dec (inj₁ x) (inj₁ y) with dec₁ x y
  ...                   | yes x∼y = yes (₁∼₁ x∼y)
  ...                   | no  x≁y = no (x≁y ∘ drop-inj₁)
  dec (inj₂ x) (inj₂ y) with dec₂ x y
  ...                   | yes x∼y = yes (₂∼₂ x∼y)
  ...                   | no  x≁y = no (x≁y ∘ drop-inj₂)
  dec (inj₁ x) (inj₂ y) = dec₁₂
  dec (inj₂ x) (inj₁ y) = no (λ())

_⊎-<-total_ : ∀ {a₁} {≤₁ : Rel a₁} → Total ≤₁ →
              ∀ {a₂} {≤₂ : Rel a₂} → Total ≤₂ →
              Total (≤₁ ⊎-< ≤₂)
total₁ ⊎-<-total total₂ = total
  where
  total : Total (_ ⊎-< _)
  total (inj₁ x) (inj₁ y) = Sum.map ₁∼₁ ₁∼₁ $ total₁ x y
  total (inj₂ x) (inj₂ y) = Sum.map ₂∼₂ ₂∼₂ $ total₂ x y
  total (inj₁ x) (inj₂ y) = inj₁ (₁∼₂ _)
  total (inj₂ x) (inj₁ y) = inj₂ (₁∼₂ _)

_⊎-<-trichotomous_ : ∀ {a₁} {≈₁ <₁ : Rel a₁} → Trichotomous ≈₁ <₁ →
                     ∀ {a₂} {≈₂ <₂ : Rel a₂} → Trichotomous ≈₂ <₂ →
                     Trichotomous (≈₁ ⊎-Rel ≈₂) (<₁ ⊎-< <₂)
_⊎-<-trichotomous_ {≈₁ = ≈₁} {<₁ = <₁} tri₁
                   {≈₂ = ≈₂} {<₂ = <₂} tri₂ = tri
  where
  tri : Trichotomous (≈₁ ⊎-Rel ≈₂) (<₁ ⊎-< <₂)
  tri (inj₁ x) (inj₂ y) = tri< (₁∼₂ _) ₁≁₂ (λ())
  tri (inj₂ x) (inj₁ y) = tri> (λ()) (λ()) (₁∼₂ _)
  tri (inj₁ x) (inj₁ y) with tri₁ x y
  ...                   | tri< x<y x≉y x≯y =
    tri< (₁∼₁ x<y)        (x≉y ∘ drop-inj₁) (x≯y ∘ drop-inj₁)
  ...                   | tri≈ x≮y x≈y x≯y =
    tri≈ (x≮y ∘ drop-inj₁) (₁∼₁ x≈y)    (x≯y ∘ drop-inj₁)
  ...                   | tri> x≮y x≉y x>y =
    tri> (x≮y ∘ drop-inj₁) (x≉y ∘ drop-inj₁) (₁∼₁ x>y)
  tri (inj₂ x) (inj₂ y) with tri₂ x y
  ...                   | tri< x<y x≉y x≯y =
    tri< (₂∼₂ x<y)        (x≉y ∘ drop-inj₂) (x≯y ∘ drop-inj₂)
  ...                   | tri≈ x≮y x≈y x≯y =
    tri≈ (x≮y ∘ drop-inj₂) (₂∼₂ x≈y)    (x≯y ∘ drop-inj₂)
  ...                   | tri> x≮y x≉y x>y =
    tri> (x≮y ∘ drop-inj₂) (x≉y ∘ drop-inj₂) (₂∼₂ x>y)

------------------------------------------------------------------------
-- Some collections of properties which are preserved

_⊎-isEquivalence_ : ∀ {a₁} {≈₁ : Rel a₁} → IsEquivalence ≈₁ →
                    ∀ {a₂} {≈₂ : Rel a₂} → IsEquivalence ≈₂ →
                    IsEquivalence (≈₁ ⊎-Rel ≈₂)
eq₁ ⊎-isEquivalence eq₂ = record
  { refl  = refl  eq₁ ⊎-refl        refl  eq₂
  ; sym   = sym   eq₁ ⊎-symmetric   sym   eq₂
  ; trans = trans eq₁ ⊎-transitive  trans eq₂
  }
  where open IsEquivalence

_⊎-isPreorder_ : ∀ {a₁} {≈₁ ∼₁ : Rel a₁} → IsPreorder ≈₁ ∼₁ →
                 ∀ {a₂} {≈₂ ∼₂ : Rel a₂} → IsPreorder ≈₂ ∼₂ →
                 ∀ {P} → IsPreorder (≈₁ ⊎-Rel ≈₂) (⊎ʳ P ∼₁ ∼₂)
pre₁ ⊎-isPreorder pre₂ = record
  { isEquivalence = isEquivalence pre₁ ⊎-isEquivalence
                    isEquivalence pre₂
  ; reflexive     = reflexive pre₁ ⊎-reflexive   reflexive pre₂
  ; trans         = trans     pre₁ ⊎-transitive  trans     pre₂
  ; ∼-resp-≈      = ∼-resp-≈  pre₁ ⊎-≈-respects₂ ∼-resp-≈  pre₂
  }
  where open IsPreorder

_⊎-isDecEquivalence_ : ∀ {a₁} {≈₁ : Rel a₁} → IsDecEquivalence ≈₁ →
                       ∀ {a₂} {≈₂ : Rel a₂} → IsDecEquivalence ≈₂ →
                       IsDecEquivalence (≈₁ ⊎-Rel ≈₂)
eq₁ ⊎-isDecEquivalence eq₂ = record
  { isEquivalence = isEquivalence eq₁ ⊎-isEquivalence
                    isEquivalence eq₂
  ; _≟_           = ⊎-decidable (_≟_ eq₁) (_≟_ eq₂) (no ₁≁₂)
  }
  where open IsDecEquivalence

_⊎-isPartialOrder_ : ∀ {a₁} {≈₁ ≤₁ : Rel a₁} → IsPartialOrder ≈₁ ≤₁ →
                     ∀ {a₂} {≈₂ ≤₂ : Rel a₂} → IsPartialOrder ≈₂ ≤₂ →
                     ∀ {P} → IsPartialOrder (≈₁ ⊎-Rel ≈₂) (⊎ʳ P ≤₁ ≤₂)
po₁ ⊎-isPartialOrder po₂ = record
  { isPreorder = isPreorder po₁ ⊎-isPreorder    isPreorder po₂
  ; antisym    = antisym    po₁ ⊎-antisymmetric antisym    po₂
  }
  where open IsPartialOrder

_⊎-isStrictPartialOrder_ :
  ∀ {a₁} {≈₁ <₁ : Rel a₁} → IsStrictPartialOrder ≈₁ <₁ →
  ∀ {a₂} {≈₂ <₂ : Rel a₂} → IsStrictPartialOrder ≈₂ <₂ →
  ∀ {P} → IsStrictPartialOrder (≈₁ ⊎-Rel ≈₂) (⊎ʳ P <₁ <₂)
spo₁ ⊎-isStrictPartialOrder spo₂ = record
  { isEquivalence = isEquivalence spo₁ ⊎-isEquivalence
                    isEquivalence spo₂
  ; irrefl        = irrefl   spo₁ ⊎-irreflexive irrefl   spo₂
  ; trans         = trans    spo₁ ⊎-transitive  trans    spo₂
  ; <-resp-≈      = <-resp-≈ spo₁ ⊎-≈-respects₂ <-resp-≈ spo₂
  }
  where open IsStrictPartialOrder

_⊎-<-isTotalOrder_ : ∀ {a₁} {≈₁ ≤₁ : Rel a₁} → IsTotalOrder ≈₁ ≤₁ →
                     ∀ {a₂} {≈₂ ≤₂ : Rel a₂} → IsTotalOrder ≈₂ ≤₂ →
                     IsTotalOrder (≈₁ ⊎-Rel ≈₂) (≤₁ ⊎-< ≤₂)
to₁ ⊎-<-isTotalOrder to₂ = record
  { isPartialOrder = isPartialOrder to₁ ⊎-isPartialOrder
                     isPartialOrder to₂
  ; total          = total to₁ ⊎-<-total total to₂
  }
  where open IsTotalOrder

_⊎-<-isDecTotalOrder_ :
  ∀ {a₁} {≈₁ ≤₁ : Rel a₁} → IsDecTotalOrder ≈₁ ≤₁ →
  ∀ {a₂} {≈₂ ≤₂ : Rel a₂} → IsDecTotalOrder ≈₂ ≤₂ →
  IsDecTotalOrder (≈₁ ⊎-Rel ≈₂) (≤₁ ⊎-< ≤₂)
to₁ ⊎-<-isDecTotalOrder to₂ = record
  { isTotalOrder = isTotalOrder to₁ ⊎-<-isTotalOrder isTotalOrder to₂
  ; _≟_          = ⊎-decidable (_≟_  to₁) (_≟_  to₂) (no ₁≁₂)
  ; _≤?_         = ⊎-decidable (_≤?_ to₁) (_≤?_ to₂) (yes (₁∼₂ _))
  }
  where open IsDecTotalOrder

------------------------------------------------------------------------
-- The game can be taken even further...

_⊎-setoid_ : Setoid → Setoid → Setoid
s₁ ⊎-setoid s₂ = record
  { isEquivalence = isEquivalence s₁ ⊎-isEquivalence isEquivalence s₂
  } where open Setoid

_⊎-preorder_ : Preorder → Preorder → Preorder
p₁ ⊎-preorder p₂ = record
  { _∼_          = _∼_        p₁ ⊎-Rel        _∼_        p₂
  ; isPreorder   = isPreorder p₁ ⊎-isPreorder isPreorder p₂
  } where open Preorder

_⊎-decSetoid_ : DecSetoid → DecSetoid → DecSetoid
ds₁ ⊎-decSetoid ds₂ = record
  { isDecEquivalence = isDecEquivalence ds₁ ⊎-isDecEquivalence
                       isDecEquivalence ds₂
  } where open DecSetoid

_⊎-poset_ : Poset → Poset → Poset
po₁ ⊎-poset po₂ = record
  { _≤_            = _≤_ po₁ ⊎-Rel _≤_ po₂
  ; isPartialOrder = isPartialOrder po₁ ⊎-isPartialOrder
                     isPartialOrder po₂
  } where open Poset

_⊎-<-poset_ : Poset → Poset → Poset
po₁ ⊎-<-poset po₂ = record
  { _≤_            = _≤_ po₁ ⊎-< _≤_ po₂
  ; isPartialOrder = isPartialOrder po₁ ⊎-isPartialOrder
                     isPartialOrder po₂
  } where open Poset

_⊎-<-strictPartialOrder_ :
  StrictPartialOrder → StrictPartialOrder → StrictPartialOrder
spo₁ ⊎-<-strictPartialOrder spo₂ = record
  { _<_                  = _<_ spo₁ ⊎-< _<_ spo₂
  ; isStrictPartialOrder = isStrictPartialOrder spo₁
                             ⊎-isStrictPartialOrder
                           isStrictPartialOrder spo₂
  } where open StrictPartialOrder

_⊎-<-totalOrder_ : TotalOrder → TotalOrder → TotalOrder
to₁ ⊎-<-totalOrder to₂ = record
  { isTotalOrder = isTotalOrder to₁ ⊎-<-isTotalOrder isTotalOrder to₂
  } where open TotalOrder

_⊎-<-decTotalOrder_ : DecTotalOrder → DecTotalOrder → DecTotalOrder
to₁ ⊎-<-decTotalOrder to₂ = record
  { isDecTotalOrder = isDecTotalOrder to₁ ⊎-<-isDecTotalOrder
                      isDecTotalOrder to₂
  } where open DecTotalOrder

max_issues_repo_name: larrytheliquid/Lemmachine


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

module FinVec where

-- This is the second step in building a representation of
-- permutations. We use permutations expressed as equivalences (in
-- FinVec) to construct one-line notation for permutations. We have
-- enough structure to model a commutative semiring EXCEPT for
-- symmetry. This will be addressed in ConcretePermutation.

import Level using (zero)

open import Data.Nat using (ℕ; _+_; _*_)
open import Data.Fin using (Fin)
open import Data.Sum
   using (_⊎_; inj₁; inj₂)
   renaming (map to map⊎)
open import Data.Product using (_×_; proj₁; proj₂; _,′_)

open import Data.Vec
  using (Vec; allFin; tabulate; _>>=_)
  renaming (_++_ to _++V_; map to mapV)

open import Algebra using (CommutativeSemiring)
open import Algebra.Structures using
  (IsSemigroup; IsCommutativeMonoid; IsCommutativeSemiring)

open import Relation.Binary using (IsEquivalence)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; cong; cong₂; module ≡-Reasoning)
open import Function using (_∘_; id)

--

open import Equiv using (_∼_; p∘!p≡id)
open import TypeEquiv using (swap₊)
open import FinEquivPlusTimes using (module Plus; module Times)
open import FinEquivTypeEquiv using (module PlusE; module TimesE; module PlusTimesE)

open import Proofs using (
  -- FiniteFunctions
      finext;
  -- VectorLemmas
      _!!_; tabulate-split
     )

------------------------------------------------------------------------------
-- The main goal is to represent permutations in the one-line notation
-- and to develop all the infrastructure to get a commutative
-- semiring, e.g., we can take unions and products of such one-line
-- notations of permutations, etc.

-- This is the type representing permutations in the one-line
-- notation. We will show that it is a commutative semiring

FinVec : ℕ → ℕ → Set
FinVec m n = Vec (Fin m) n

-- The additive and multiplicative units are trivial

1C : {n : ℕ} → FinVec n n
1C {n} = allFin n

-- corresponds to ⊥ ≃ ⊥ × A and other impossibilities but don't use
-- it, as it is abstract and will confuse external proofs!

abstract

  0C : FinVec 0 0
  0C = 1C {0}

-- sequential composition (transitivity)

_∘̂_ : {n₀ n₁ n₂ : ℕ} → Vec (Fin n₁) n₀ → Vec (Fin n₂) n₁ → Vec (Fin n₂) n₀
π₁ ∘̂ π₂ = tabulate (_!!_ π₂ ∘ _!!_ π₁)

------------------------------------------------------------------------------
-- Additive monoid

private

  _⊎v_ : ∀ {m n} {A B : Set} → Vec A m → Vec B n → Vec (A ⊎ B) (m + n)
  α ⊎v β = tabulate (inj₁ ∘ _!!_ α) ++V tabulate (inj₂ ∘ _!!_ β)

-- Parallel additive composition
-- conceptually, what we want is

_⊎c'_ : ∀ {m₁ n₁ m₂ n₂} → FinVec m₁ m₂ → FinVec n₁ n₂ →
        FinVec (m₁ + n₁) (m₂ + n₂)
_⊎c'_ α β = mapV Plus.fwd (α ⊎v β)

-- but the above is tedious to work with.  Instead, inline a bit to get

_⊎c_ : ∀ {m₁ n₁ m₂ n₂} → FinVec m₁ m₂ → FinVec n₁ n₂ →
       FinVec (m₁ + n₁) (m₂ + n₂)
_⊎c_ {m₁} α β = tabulate (Plus.fwd ∘ inj₁ ∘ _!!_ α) ++V
                tabulate (Plus.fwd {m₁} ∘ inj₂ ∘ _!!_ β)

-- see ⊎c≡⊎c' lemma below

_⊎fv_ : ∀ {m₁ n₁ m₂ n₂} → FinVec m₁ m₂ → FinVec n₁ n₂ →
        FinVec (m₁ + n₁) (m₂ + n₂)
_⊎fv_ {m₁} α β =
  tabulate (λ j → Plus.fwd (map⊎ (_!!_ α) (_!!_ β) (Plus.bwd j)))

⊎-equiv : ∀ {m₁ n₁ m₂ n₂} → (α : FinVec m₁ m₂) → (β : FinVec n₁ n₂) →
          α ⊎c β ≡ α ⊎fv β
⊎-equiv {m₁} {n₁} {m₂} {n₂} α β =
  let mm s = map⊎ (_!!_ α) (_!!_ β) s in
  let g = Plus.fwd ∘ mm ∘ Plus.bwd in
  begin (
  tabulate (λ j → Plus.fwd (inj₁ (α !! j))) ++V
  tabulate (λ j → Plus.fwd {m₁} (inj₂ (β !! j)))
    ≡⟨ refl ⟩ -- map⊎ evaluates on inj₁/inj₂
  tabulate (Plus.fwd ∘ mm ∘ inj₁) ++V tabulate (Plus.fwd ∘ mm ∘ inj₂)
    ≡⟨ cong₂ _++V_
         (finext (λ i → cong (Plus.fwd ∘ mm)
                          (sym (Plus.bwd∘fwd~id (inj₁ i)))))
         (finext (λ i → cong (Plus.fwd ∘ mm)
                          (sym (Plus.bwd∘fwd~id (inj₂ i))))) ⟩
  tabulate {m₂} (g ∘ Plus.fwd ∘ inj₁) ++V
  tabulate {n₂} (g ∘ Plus.fwd {m₂} ∘ inj₂)
    ≡⟨ sym (tabulate-split {m₂} {n₂} {f = g}) ⟩
  tabulate g ∎)
  where
    open ≡-Reasoning

-- additive units

unite+ : {m : ℕ} → FinVec m (0 + m)
unite+ {m} = tabulate (proj₁ (PlusE.unite+ {m}))

uniti+ : {m : ℕ} → FinVec (0 + m) m
uniti+ {m} = tabulate (proj₁ (PlusE.uniti+ {m}))

unite+r : {m : ℕ} → FinVec m (m + 0)
unite+r {m} = tabulate (proj₁ (PlusE.unite+r {m}))

-- unite+r' : {m : ℕ} → FinVec m (m + 0)
-- unite+r' {m} = tabulate (proj₁ (PlusE.unite+r' {m}))

uniti+r : {m : ℕ} → FinVec (m + 0) m
uniti+r {m} = tabulate (proj₁ (PlusE.uniti+r {m}))

-- commutativity

-- swap the first m elements with the last n elements
-- [ v₀ , v₁   , v₂   , ... , vm-1 ,     vm , vm₊₁ , ... , vm+n-1 ]
-- ==>
-- [ vm , vm₊₁ , ... , vm+n-1 ,     v₀ , v₁   , v₂   , ... , vm-1 ]

-- swap+cauchy : (m n : ℕ) → FinVec (n + m) (m + n)
-- swap+cauchy m n = tabulate (Plus.swapper m n)

-- associativity

assocl+ : {m n o : ℕ} → FinVec  ((m + n) + o) (m + (n + o))
assocl+ {m} {n} {o} = tabulate (proj₁ (PlusE.assocl+ {m} {n} {o}))

assocr+ : {m n o : ℕ} → FinVec  (m + (n + o)) (m + n + o)
assocr+ {m} {n} {o} = tabulate (proj₁ (PlusE.assocr+ {m} {n} {o}))

------------------------------------------------------------------------------
-- Multiplicative monoid

private

  _×v_ : ∀ {m n} {A B : Set} → Vec A m → Vec B n → Vec (A × B) (m * n)
  α ×v β = α >>= (λ b → mapV (_,′_ b) β)

-- Tensor multiplicative composition
-- Transpositions in α correspond to swapping entire rows
-- Transpositions in β correspond to swapping entire columns

_×c_ : ∀ {m₁ n₁ m₂ n₂} → FinVec m₁ m₂ → FinVec n₁ n₂ →
       FinVec (m₁ * n₁) (m₂ * n₂)
α ×c β = mapV Times.fwd (α ×v β)

-- multiplicative units

unite* : {m : ℕ} → FinVec m (1 * m)
unite* {m} = tabulate (proj₁ (TimesE.unite* {m}))

uniti* : {m : ℕ} → FinVec (1 * m) m
uniti* {m} = tabulate (proj₁ (TimesE.uniti* {m}))

unite*r : {m : ℕ} → FinVec m (m * 1)
unite*r {m} = tabulate (proj₁ (TimesE.unite*r {m}))

uniti*r : {m : ℕ} → FinVec (m * 1) m
uniti*r {m} = tabulate (proj₁ (TimesE.uniti*r {m}))

-- commutativity

-- swap⋆
--
-- This is essentially the classical problem of in-place matrix transpose:
-- "http://en.wikipedia.org/wiki/In-place_matrix_transposition"
-- Given m and n, the desired permutation in Cauchy representation is:
-- P(i) = m*n-1 if i=m*n-1
--      = m*i mod m*n-1 otherwise

-- transposeIndex : {m n : ℕ} → Fin m × Fin n → Fin (n * m)
-- transposeIndex = Times.fwd ∘ swap
-- inject≤ (fromℕ (toℕ d * m + toℕ b)) (i*n+k≤m*n d b)

-- swap⋆cauchy : (m n : ℕ) → FinVec (n * m) (m * n)
-- swap⋆cauchy m n = tabulate (Times.swapper m n)
-- mapV transposeIndex (V.tcomp 1C 1C)

-- associativity

assocl* : {m n o : ℕ} → FinVec  ((m * n) * o) (m * (n * o))
assocl* {m} {n} {o} = tabulate (proj₁ (TimesE.assocl* {m} {n} {o}))

assocr* : {m n o : ℕ} → FinVec  (m * (n * o)) (m * n * o)
assocr* {m} {n} {o} = tabulate (proj₁ (TimesE.assocr* {m} {n} {o}))

------------------------------------------------------------------------------
-- Distributivity

dist*+ : ∀ {m n o} → FinVec (m * o + n * o) ((m + n) * o)
dist*+ {m} {n} {o} = tabulate (proj₁ (PlusTimesE.dist {m} {n} {o}))

factor*+ : ∀ {m n o} → FinVec ((m + n) * o) (m * o + n * o)
factor*+ {m} {n} {o} = tabulate (proj₁ (PlusTimesE.factor {m} {n} {o}))

distl*+ : ∀ {m n o} → FinVec (m * n + m * o) (m * (n + o))
distl*+ {m} {n} {o} = tabulate (proj₁ (PlusTimesE.distl {m} {n} {o}))

factorl*+ : ∀ {m n o} → FinVec (m * (n + o)) (m * n + m * o)
factorl*+ {m} {n} {o} = tabulate (proj₁ (PlusTimesE.factorl {m} {n} {o}))

right-zero*l : ∀ {m} → FinVec 0 (m * 0)
right-zero*l {m} = tabulate (proj₁ (PlusTimesE.distzr {m}))

right-zero*r : ∀ {m} → FinVec (m * 0) 0
right-zero*r {m} = tabulate (proj₁ (PlusTimesE.factorzr {m}))

------------------------------------------------------------------------------
-- Putting it all together, we have a commutative semiring structure
-- (modulo symmetry)

_cauchy≃_ : (m n : ℕ) → Set
m cauchy≃ n = FinVec m n

id-iso : {m : ℕ} → FinVec m m
id-iso = 1C

-- This is only here to show that we do have everything for a
-- commutative semiring structure EXCEPT for symmetry; this is
-- addressed in ConcretePermutation

postulate sym-iso : {m n : ℕ} → FinVec m n → FinVec n m

trans-iso : {m n o : ℕ} → FinVec m n → FinVec n o → FinVec m o
trans-iso c₁ c₂ = c₂ ∘̂ c₁

cauchy≃IsEquiv : IsEquivalence {Level.zero} {Level.zero} {ℕ} _cauchy≃_
cauchy≃IsEquiv = record {
  refl = id-iso ;
  sym = sym-iso ;
  trans = trans-iso
  }

cauchyPlusIsSG : IsSemigroup {Level.zero} {Level.zero} {ℕ} _cauchy≃_ _+_
cauchyPlusIsSG = record {
  isEquivalence = cauchy≃IsEquiv ;
  assoc = λ m n o → assocl+ {m} {n} {o} ;
  ∙-cong = _⊎c_
  }

cauchyTimesIsSG : IsSemigroup {Level.zero} {Level.zero} {ℕ} _cauchy≃_ _*_
cauchyTimesIsSG = record {
  isEquivalence = cauchy≃IsEquiv ;
  assoc = λ m n o → assocl* {m} {n} {o} ;
  ∙-cong = _×c_
  }

{--
cauchyPlusIsCM : IsCommutativeMonoid _cauchy≃_ _+_ 0
cauchyPlusIsCM = record {
  isSemigroup = cauchyPlusIsSG ;
  identityˡ = λ m → 1C ;
  comm = λ m n → swap+cauchy n m
  }

cauchyTimesIsCM : IsCommutativeMonoid _cauchy≃_ _*_ 1
cauchyTimesIsCM = record {
  isSemigroup = cauchyTimesIsSG ;
  identityˡ = λ m → uniti* {m} ;
  comm = λ m n → swap⋆cauchy n m
  }

cauchyIsCSR : IsCommutativeSemiring _cauchy≃_ _+_ _*_ 0 1
cauchyIsCSR = record {
  +-isCommutativeMonoid = cauchyPlusIsCM ;
  *-isCommutativeMonoid = cauchyTimesIsCM ;
  distribʳ = λ o m n → factor*+ {m} {n} {o} ;
  zeroˡ = λ m → 0C
  }

cauchyCSR : CommutativeSemiring Level.zero Level.zero
cauchyCSR = record {
  Carrier = ℕ ;
  _≈_ = _cauchy≃_ ;
  _+_ = _+_ ;
  _*_ = _*_ ;
  0# = 0 ;
  1# = 1 ;
  isCommutativeSemiring = cauchyIsCSR
  }
--}

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- List Zippers, basic types and operations
------------------------------------------------------------------------

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

module Data.List.Zipper where

open import Data.Nat.Base
open import Data.Maybe.Base as Maybe using (Maybe ; just ; nothing)
open import Data.List.Base as List using (List ; [] ; _∷_)
open import Function

-- Definition
------------------------------------------------------------------------

-- A List Zipper represents a List together with a particular sub-List
-- in focus. The user can attempt to move the focus left or right, with
-- a risk of failure if one has already reached the corresponding end.

-- To make these operations efficient, the `context` the sub List in
-- focus lives in is stored *backwards*. This is made formal by `toList`
-- which returns the List a Zipper represents.

record Zipper {a} (A : Set a) : Set a where
  constructor mkZipper
  field context : List A
        value   : List A

  toList : List A
  toList = List.reverse context List.++ value
open Zipper public

-- Embedding Lists as Zippers without any context
fromList : ∀ {a} {A : Set a} → List A → Zipper A
fromList = mkZipper []

-- Fundamental operations of a Zipper: Moving around
------------------------------------------------------------------------

module _ {a} {A : Set a} where

 left : Zipper A → Maybe (Zipper A)
 left (mkZipper []        val) = nothing
 left (mkZipper (x ∷ ctx) val) = just (mkZipper ctx (x ∷ val))

 right : Zipper A → Maybe (Zipper A)
 right (mkZipper ctx [])        = nothing
 right (mkZipper ctx (x ∷ val)) = just (mkZipper (x ∷ ctx) val)

-- Focus-respecting operations
------------------------------------------------------------------------

module _ {a} {A : Set a} where

 reverse : Zipper A → Zipper A
 reverse (mkZipper ctx val) = mkZipper val ctx

 -- If we think of a List [x₁⋯xₘ] split into a List [xₙ₊₁⋯xₘ] in focus
 -- of another list [x₁⋯xₙ] then there are 4 places (marked {k} here) in
 -- which we can insert new values: [{1}x₁⋯xₙ{2}][{3}xₙ₊₁⋯xₘ{4}]

 -- The following 4 functions implement these 4 insertions.

 -- `xs ˢ++ zp` inserts `xs` on the `s` side of the context of the Zipper `zp`
 -- `zp ++ˢ xs` insert `xs` on the `s` side of the value in focus of the Zipper `zp`

 infixr 5 _ˡ++_ _ʳ++_
 infixl 5 _++ˡ_ _++ʳ_
 -- {1}
 _ˡ++_ : List A → Zipper A → Zipper A
 xs ˡ++ mkZipper ctx val = mkZipper (ctx List.++ List.reverse xs) val

 -- {2}
 _ʳ++_ : List A → Zipper A → Zipper A
 xs ʳ++ mkZipper ctx val = mkZipper (List.reverse xs List.++ ctx) val

 -- {3}
 _++ˡ_ : Zipper A → List A → Zipper A
 mkZipper ctx val ++ˡ xs = mkZipper ctx (xs List.++ val)

 -- {4}
 _++ʳ_ : Zipper A → List A → Zipper A
 mkZipper ctx val ++ʳ xs = mkZipper ctx (val List.++ xs)

-- List-like operations
------------------------------------------------------------------------

module _ {a} {A : Set a} where

 length : Zipper A → ℕ
 length (mkZipper ctx val) = List.length ctx + List.length val

module _ {a b} {A : Set a} {B : Set b} where

 map : (A → B) → Zipper A → Zipper B
 map f (mkZipper ctx val) = (mkZipper on List.map f) ctx val

 foldr : (A → B → B) → B → Zipper A → B
 foldr c n (mkZipper ctx val) = List.foldl (flip c) (List.foldr c n val) ctx

-- Generating all the possible foci of a list
------------------------------------------------------------------------

module _ {a} {A : Set a} where

 allFociIn : List A → List A → List (Zipper A)
 allFociIn ctx []           = List.[ mkZipper ctx [] ]
 allFociIn ctx xxs@(x ∷ xs) = mkZipper ctx xxs ∷ allFociIn (x ∷ ctx) xs

 allFoci : List A → List (Zipper A)
 allFoci = allFociIn []


text:
-- AIM XXIII, Andreas, 2016-04-24
-- Overloaded projections and projection patterns

-- {-# OPTIONS -v tc.proj.amb:30 #-}
-- {-# OPTIONS -v tc.lhs.split:20 #-}

module _ where

import Common.Level
open import Common.Prelude hiding (map)
open import Common.Equality

module M (A : Set) where
  record Stream : Set where
    coinductive
    field
      head : A
      tail : Stream
open M using (Stream)
open module S = M.Stream public

-- This is a bit trickier for overloading projections
-- as it has a parameter with is of a record type
-- with the same projections.

record _≈_ {A : Set}(s t : Stream A) : Set where
  coinductive
  field
    head : head s ≡ head t
    tail : tail s ≈ tail t
open module B = _≈_ public

≈refl : ∀{A} {s : Stream A} → s ≈ s
head ≈refl = refl
tail ≈refl = ≈refl

≈sym : ∀{A} {s t : Stream A} → s ≈ t → t ≈ s
head (≈sym p) = sym (head p)
tail (≈sym p) = ≈sym (tail p)

module N (A : Set) (s : Stream A) where
  open module SS = Stream s public

  myhead : A
  myhead = SS.head  -- cannot use ambiguous head here

map : {A B : Set} → (A → B) → Stream A → Stream B
head (map f s) = f (head s)
tail (map f s) = map f (tail s)

map_id : {A : Set}(s : Stream A) → map (λ x → x) s ≈ s
head (map_id s) = refl
tail (map_id s) = map_id (tail s)

repeat : {A : Set}(a : A) → Stream A
head (repeat a) = a
tail (repeat a) = repeat a

repeat₂ : {A : Set}(a₁ a₂ : A) → Stream A
(     (head (repeat₂ a₁ a₂))) = a₁
(head (tail (repeat₂ a₁ a₂))) = a₂
(tail (tail (repeat₂ a₁ a₂))) = repeat₂ a₁ a₂

repeat≈repeat₂ : {A : Set}(a : A) → repeat a ≈ repeat₂ a a
(     (head (repeat≈repeat₂ a))) = refl
(head (tail (repeat≈repeat₂ a))) = refl
(tail (tail (repeat≈repeat₂ a))) = repeat≈repeat₂ a

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

open import Agda.Primitive
open import Prelude
import GSeTT.Typed-Syntax
import Globular-TT.Syntax

{- Structure of CwF of a globular type theory : Cut admissibility is significantly harder and has to be proved together with it -}
module Globular-TT.CwF-Structure {l} (index : Set l) (rule : index → GSeTT.Typed-Syntax.Ctx × (Globular-TT.Syntax.Pre-Ty index)) where
  open import Globular-TT.Syntax index
  open import Globular-TT.Rules index rule

  A∈Γ→Γ⊢A : ∀ {Γ x A} →  Γ ⊢C → x # A ∈ Γ → Γ ⊢T A
  A∈Γ→Γ⊢A Γ+⊢@(cc Γ⊢ Γ⊢B idp) (inl A∈Γ) = wkT (A∈Γ→Γ⊢A Γ⊢ A∈Γ) Γ+⊢
  A∈Γ→Γ⊢A Γ+⊢@(cc Γ⊢ Γ⊢A idp) (inr (idp , idp)) = wkT Γ⊢A Γ+⊢

  {- cut-admissibility -}
  -- notational shortcut : if A = B a term of type A is also of type B
  trT : ∀ {Γ A B t} → A == B → Γ ⊢t t # A → Γ ⊢t t # B
  trT idp Γ⊢t:A = Γ⊢t:A

  {- action on weakened types and terms -}
  n∉Γ : ∀ {Γ A n} → Γ ⊢C → (C-length Γ ≤ n) → ¬ (n # A ∈ Γ)
  n∉Γ (cc Γ⊢ _ idp) l+1≤n (inl n∈Γ) = n∉Γ Γ⊢ (Sn≤m→n≤m l+1≤n) n∈Γ
  n∉Γ (cc Γ⊢ _ idp) Sn≤n (inr (idp , idp)) = Sn≰n _ Sn≤n

  lΓ∉Γ : ∀ {Γ A} → Γ ⊢C → ¬ ((C-length Γ) # A ∈ Γ)
  lΓ∉Γ Γ⊢ = n∉Γ Γ⊢ (n≤n _)

  wk[]T : ∀ {Γ Δ γ x u A B} → Γ ⊢T A → Δ ⊢S < γ , x ↦ u > > (Γ ∙ x # B) → (A [ < γ , x ↦ u > ]Pre-Ty) == (A [ γ ]Pre-Ty)
  wk[]t : ∀ {Γ Δ γ x u A t B} → Γ ⊢t t # A → Δ ⊢S < γ , x ↦ u > > (Γ ∙ x # B) → (t [ < γ , x ↦ u > ]Pre-Tm) == (t [ γ ]Pre-Tm)
  wk[]S : ∀ {Γ Δ γ x u B Θ θ} → Γ ⊢S θ > Θ → Δ ⊢S < γ , x ↦ u > > (Γ ∙ x # B) → (θ ∘ < γ , x ↦ u >) == (θ ∘ γ)
  []T : ∀ {Γ A Δ γ} → Γ ⊢T A → Δ ⊢S γ > Γ → Δ ⊢T (A [ γ ]Pre-Ty)
  []t : ∀ {Γ A t Δ γ} → Γ ⊢t t # A → Δ ⊢S γ > Γ → Δ ⊢t (t [ γ ]Pre-Tm) # (A [ γ ]Pre-Ty)
  [∘]T : ∀ {Γ Δ Θ A γ δ} → Γ ⊢T A → Δ ⊢S γ > Γ → Θ ⊢S δ > Δ → ((A [ γ ]Pre-Ty) [ δ ]Pre-Ty) == (A [ γ ∘ δ ]Pre-Ty)
  [∘]t : ∀ {Γ Δ Θ A t γ δ} → Γ ⊢t t # A → Δ ⊢S γ > Γ → Θ ⊢S δ > Δ → ((t [ γ ]Pre-Tm) [ δ ]Pre-Tm) == (t [ γ ∘ δ ]Pre-Tm)
  ∘-admissibility : ∀ {Γ Δ Θ γ δ} → Δ ⊢S γ > Γ → Θ ⊢S δ > Δ → Θ ⊢S (γ ∘ δ) > Γ
  ∘-associativity : ∀ {Γ Δ Θ Ξ γ δ θ} → Δ ⊢S γ > Γ → Θ ⊢S δ > Δ → Ξ ⊢S θ > Θ → ((γ ∘ δ) ∘ θ) == (γ ∘ (δ ∘ θ))

  wk[]T (ob Γ⊢) _ = idp
  wk[]T (ar Γ⊢A Γ⊢t:A Γ⊢u:A) Δ⊢γ+:Γ+ = ⇒= (wk[]T Γ⊢A Δ⊢γ+:Γ+) (wk[]t Γ⊢t:A Δ⊢γ+:Γ+) (wk[]t Γ⊢u:A Δ⊢γ+:Γ+)
  wk[]t {x = x} (var {x = y} Γ⊢ y∈Γ) Δ⊢γ+:Γ+             with (eqdecℕ y x)
  ...                                                    | inr _ = idp
  wk[]t (var Γ⊢ l∈Γ) (sc Δ⊢γ:Γ (cc _ _ idp) _ _) | inl idp = ⊥-elim (lΓ∉Γ Γ⊢ l∈Γ)
  wk[]t (tm _ Γ⊢θ:Θ idp) Δ⊢γ+:Γ+ = Tm-constructor= idp (wk[]S Γ⊢θ:Θ Δ⊢γ+:Γ+)
  wk[]S (es _) _ = idp
  wk[]S (sc Γ⊢θ:Θ _ Γ⊢t:A[θ] idp) Δ⊢γ+:Γ+ = <,>= (wk[]S Γ⊢θ:Θ Δ⊢γ+:Γ+) idp (wk[]t Γ⊢t:A[θ] Δ⊢γ+:Γ+)

  []T (ob Γ⊢) Δ⊢γ:Γ = ob (Δ⊢γ:Γ→Δ⊢ Δ⊢γ:Γ)
  []T (ar Γ⊢A Γ⊢t:A Γ⊢u:A) Δ⊢γ:Γ = ar ([]T Γ⊢A Δ⊢γ:Γ) ([]t Γ⊢t:A Δ⊢γ:Γ) ([]t Γ⊢u:A Δ⊢γ:Γ)
  []t {t = Tm-constructor i _} (tm Ci⊢Ti x idp) Δ⊢γ:Γ = trT ([∘]T Ci⊢Ti x Δ⊢γ:Γ ^) (tm Ci⊢Ti (∘-admissibility x Δ⊢γ:Γ) idp)
  []t {Γ = (Γ ∙ _ # _)} {t = Var x} (var Γ+⊢@(cc Γ⊢ _ idp) (inl x∈Γ)) Δ⊢γ+:Γ+@(sc Δ⊢γ:Γ _ _ idp) with (eqdecℕ x (C-length Γ))
  ...                                                                                | inl idp = ⊥-elim (lΓ∉Γ Γ⊢ x∈Γ)
  ...                                                                                | inr _ = trT (wk[]T (A∈Γ→Γ⊢A Γ⊢ x∈Γ) Δ⊢γ+:Γ+ ^) ([]t (var Γ⊢ x∈Γ) Δ⊢γ:Γ)
  []t {Γ = (Γ ∙ _ # _)} {t = Var x} (var Γ+⊢@(cc Γ⊢ Γ⊢A idp) (inr (idp , idp))) Δ⊢γ+:Γ+@(sc Δ⊢γ:Γ x₁ Δ⊢t:A[γ] idp) with (eqdecℕ x (C-length Γ))
  ...                                                                                | inl p = trT (wk[]T Γ⊢A Δ⊢γ+:Γ+ ^) Δ⊢t:A[γ]
  ...                                                                                | inr x≠x = ⊥-elim (x≠x idp)

  [∘]T (ob _) _ _ = idp
  [∘]T (ar Γ⊢A Γ⊢t:A Γ⊢u:A) Δ⊢γ:Γ Θ⊢δ:Δ = ⇒= ([∘]T Γ⊢A Δ⊢γ:Γ Θ⊢δ:Δ) ([∘]t Γ⊢t:A Δ⊢γ:Γ Θ⊢δ:Δ) ([∘]t Γ⊢u:A Δ⊢γ:Γ Θ⊢δ:Δ)
  [∘]t (tm Ci⊢Ti x idp) Δ⊢γ:Γ Θ⊢δ:Δ = Tm-constructor= idp (∘-associativity x Δ⊢γ:Γ Θ⊢δ:Δ )
  [∘]t (var {x = x} Γ,y:A⊢ x∈Γ+) (sc {x = y} Δ⊢γ:Γ _ Δ⊢t:A[γ] idp) Θ⊢δ:Δ with (eqdecℕ x y )
  ...                                                                | inl idp = idp
  [∘]t (var Γ,y:A⊢ (inr (idp , idp))) (sc Δ⊢γ:Γ _ Δ⊢t:A[γ] idp) Θ⊢δ:Δ | inr x≠x = ⊥-elim (x≠x idp)
  [∘]t (var (cc Γ⊢ _ idp) (inl x∈Γ)) (sc Δ⊢γ:Γ _ Δ⊢t:A[γ] idp) Θ⊢δ:Δ | inr _ = [∘]t (var Γ⊢ x∈Γ) Δ⊢γ:Γ Θ⊢δ:Δ

  ∘-admissibility (es Δ⊢) Θ⊢δ:Δ = es (Δ⊢γ:Γ→Δ⊢ Θ⊢δ:Δ)
  ∘-admissibility (sc Δ⊢γ:Γ Γ,x:A⊢@(cc _ Γ⊢A idp) Δ⊢t:A[γ] idp) Θ⊢δ:Δ = sc (∘-admissibility Δ⊢γ:Γ Θ⊢δ:Δ) Γ,x:A⊢ (trT ([∘]T Γ⊢A Δ⊢γ:Γ Θ⊢δ:Δ) ([]t Δ⊢t:A[γ] Θ⊢δ:Δ)) idp

  ∘-associativity (es _) _ _ = idp
  ∘-associativity (sc Δ⊢γ:Γ _ Δ⊢t:A[γ] idp) Θ⊢δ:Δ Ξ⊢θ:Θ = <,>= (∘-associativity Δ⊢γ:Γ Θ⊢δ:Δ Ξ⊢θ:Θ) idp ([∘]t Δ⊢t:A[γ] Θ⊢δ:Δ Ξ⊢θ:Θ)

  Γ⊢t:A→Γ⊢A : ∀ {Γ A t} → Γ ⊢t t # A → Γ ⊢T A
  Γ⊢t:A→Γ⊢A (var Γ,x:A⊢@(cc Γ⊢ Γ⊢A idp) (inl y∈Γ)) = wkT (Γ⊢t:A→Γ⊢A (var Γ⊢ y∈Γ)) Γ,x:A⊢
  Γ⊢t:A→Γ⊢A (var Γ,x:A⊢@(cc _ _ idp) (inr (idp , idp))) = Γ,x:A⊢→Γ,x:A⊢A Γ,x:A⊢
  Γ⊢t:A→Γ⊢A (tm Ci⊢Ti Γ⊢γ:Δ idp) = []T Ci⊢Ti Γ⊢γ:Δ

  {- action of identity on types terms and substitutions is trivial (true on syntax) -}
  [id]T : ∀ Γ A → (A [ Pre-id Γ ]Pre-Ty) == A
  [id]t : ∀ Γ t → (t [ Pre-id Γ ]Pre-Tm) == t
  ∘-right-unit : ∀ {Δ γ} →  (γ ∘ Pre-id Δ) == γ

  [id]T Γ ∗ = idp
  [id]T Γ (⇒ A t u) = ⇒= ([id]T Γ A) ([id]t Γ t) ([id]t Γ u)
  [id]t Γ (Tm-constructor i γ) = Tm-constructor= idp ∘-right-unit
  [id]t ⊘ (Var x) = idp
  [id]t (Γ ∙ y # B) (Var x) with (eqdecℕ x y)
  ...                              | inl x=y = Var= (x=y ^)
  ...                              | inr _ = [id]t Γ (Var x)
  ∘-right-unit {Δ} {<>} = idp
  ∘-right-unit {Δ} {< γ , y ↦ t >} = <,>= ∘-right-unit idp ([id]t Δ t) -- ::= ∘-right-unit (×= idp ([id]t Δ t))

  {- identity is well-formed -}
  Γ⊢id:Γ : ∀ {Γ} → Γ ⊢C → Γ ⊢S Pre-id Γ > Γ
  Γ⊢id:Γ ec = es ec
  Γ⊢id:Γ Γ,x:A⊢@(cc Γ⊢ Γ⊢A idp) = sc (wkS (Γ⊢id:Γ Γ⊢) Γ,x:A⊢) Γ,x:A⊢ (var Γ,x:A⊢ (inr (idp , [id]T _ _))) idp

  {- composition is associative -}

  ∘-left-unit : ∀{Γ Δ γ} → Δ ⊢S γ > Γ → (Pre-id Γ ∘ γ) == γ
  ∘-left-unit (es _) = idp
  ∘-left-unit Δ⊢γ+:Γ+@(sc {x = x} Δ⊢γ:Γ (cc Γ⊢ _ idp) _ idp) with (eqdecℕ x x)
  ...                                                  | inl p = <,>= (wk[]S (Γ⊢id:Γ Γ⊢) Δ⊢γ+:Γ+ >> ∘-left-unit Δ⊢γ:Γ) idp idp
  ...                                                  | inr x≠x = ⊥-elim (x≠x idp)

  {- Structure of CwF -}

  Γ,x:A⊢π:Γ : ∀ {Γ x A} → (Γ ∙ x # A) ⊢C → (Γ ∙ x # A) ⊢S Pre-π Γ x A > Γ
  Γ,x:A⊢π:Γ Γ,x:A⊢@(cc Γ⊢ _ idp) = wkS (Γ⊢id:Γ Γ⊢) Γ,x:A⊢
  -- TODO : finish

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


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

module Properties where

import Properties.Contradiction
import Properties.Dec
import Properties.Equality
import Properties.Remember
import Properties.Step
import Properties.StrictMode
import Properties.TypeCheck

max_stars_repo_name: gideros/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
------------------------------------------------------------------------
-- A simple tactic for proving equality of equality proofs
------------------------------------------------------------------------

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

open import Equality

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

open Derived-definitions-and-properties eq
open import Prelude hiding (Level; lift; lower)

private
  variable
    a       : Prelude.Level
    A B     : Type a
    ℓ x y z : A
    x≡y y≡z : x ≡ y

------------------------------------------------------------------------
-- Equality expressions

-- Equality expressions.
--
-- Note that the presence of the Refl constructor means that Eq is a
-- definition of equality with a concrete, evaluating eliminator.

data Eq {A : Type a} : A → A → Type (lsuc a) where
  Lift  : (x≡y : x ≡ y) → Eq x y
  Refl  : Eq x x
  Sym   : (x≈y : Eq x y) → Eq y x
  Trans : (x≈y : Eq x y) (y≈z : Eq y z) → Eq x z
  Cong  : ∀ {B : Type a} {x y}
          (f : B → A) (x≈y : Eq x y) → Eq (f x) (f y)

-- Semantics.

⟦_⟧ : Eq x y → x ≡ y
⟦ Lift x≡y      ⟧ = x≡y
⟦ Refl          ⟧ = refl _
⟦ Sym x≈y       ⟧ = sym ⟦ x≈y ⟧
⟦ Trans x≈y y≈z ⟧ = trans ⟦ x≈y ⟧ ⟦ y≈z ⟧
⟦ Cong f x≈y    ⟧ = cong f ⟦ x≈y ⟧

-- A derived combinator.

Cong₂ : {A B C : Type a} (f : A → B → C) {x y : A} {u v : B} →
        Eq x y → Eq u v → Eq (f x u) (f y v)
Cong₂ f {y = y} {u} x≈y u≈v =
  Trans (Cong (flip f u) x≈y) (Cong (f y) u≈v)

private

  Cong₂-correct :
    {A B C : Type a} (f : A → B → C) {x y : A} {u v : B}
    (x≈y : Eq x y) (u≈v : Eq u v) →
    ⟦ Cong₂ f x≈y u≈v ⟧ ≡ cong₂ f ⟦ x≈y ⟧ ⟦ u≈v ⟧
  Cong₂-correct f x≈y u≈v = refl _

------------------------------------------------------------------------
-- Simplified expressions

private

  -- The simplified expressions are stratified into three levels.

  data Level : Type where
    upper middle lower : Level

  data EqS {A : Type a} : Level → A → A → Type (lsuc a) where

    -- Bottom layer: a single use of congruence applied to an actual
    -- equality.

    Cong : {B : Type a} {x y : B} (f : B → A) (x≡y : x ≡ y) →
           EqS lower (f x) (f y)

    -- Middle layer: at most one use of symmetry.

    No-Sym : (x≈y : EqS lower x y) → EqS middle x y
    Sym    : (x≈y : EqS lower x y) → EqS middle y x

    -- Uppermost layer: a sequence of equalities, combined using
    -- transitivity and a single use of reflexivity.

    Refl : EqS upper x x
    Cons : (x≈y : EqS middle x y) (y≈z : EqS upper y z) →
           EqS upper x z

  -- Semantics of simplified expressions.

  ⟦_⟧S : EqS ℓ x y → x ≡ y
  ⟦ Cong f x≡y   ⟧S = cong f x≡y
  ⟦ No-Sym x≈y   ⟧S =     ⟦ x≈y ⟧S
  ⟦ Sym    x≈y   ⟧S = sym ⟦ x≈y ⟧S
  ⟦ Refl         ⟧S = refl _
  ⟦ Cons x≈y y≈z ⟧S = trans ⟦ x≈y ⟧S ⟦ y≈z ⟧S

------------------------------------------------------------------------
-- Manipulation of expressions

private

  lift : x ≡ y → EqS upper x y
  lift x≡y = Cons (No-Sym (Cong id x≡y)) Refl

  abstract

    lift-correct : (x≡y : x ≡ y) → x≡y ≡ ⟦ lift x≡y ⟧S
    lift-correct x≡y =
      x≡y                           ≡⟨ cong-id _ ⟩
      cong id x≡y                   ≡⟨ sym (trans-reflʳ _) ⟩∎
      trans (cong id x≡y) (refl _)  ∎

  snoc : EqS upper x y → EqS middle y z → EqS upper x z
  snoc Refl           y≈z = Cons y≈z Refl
  snoc (Cons x≈y y≈z) z≈u = Cons x≈y (snoc y≈z z≈u)

  abstract

    snoc-correct :
      (z≈y : EqS upper z y) (y≈x : EqS middle y x) →
      sym y≡z ≡ ⟦ z≈y ⟧S → sym x≡y ≡ ⟦ y≈x ⟧S →
      sym (trans x≡y y≡z) ≡ ⟦ snoc z≈y y≈x ⟧S
    snoc-correct {y≡z = y≡z} {x≡y = x≡y} Refl y≈z h₁ h₂ =
      sym (trans x≡y y≡z)        ≡⟨ sym-trans _ _ ⟩
      trans (sym y≡z) (sym x≡y)  ≡⟨ cong₂ trans h₁ h₂ ⟩
      trans (refl _) ⟦ y≈z ⟧S    ≡⟨ trans-reflˡ _ ⟩
      ⟦ y≈z ⟧S                   ≡⟨ sym (trans-reflʳ _) ⟩∎
      trans ⟦ y≈z ⟧S (refl _)    ∎
    snoc-correct {y≡z = y≡z} {x≡y = x≡y} (Cons x≈y y≈z) z≈u h₁ h₂ =
      sym (trans x≡y y≡z)                                    ≡⟨ sym-trans _ _ ⟩
      trans (sym y≡z) (sym x≡y)                              ≡⟨ cong₂ trans h₁ (refl (sym x≡y)) ⟩
      trans (trans ⟦ x≈y ⟧S ⟦ y≈z ⟧S) (sym x≡y)              ≡⟨ trans-assoc _ _ _ ⟩
      trans ⟦ x≈y ⟧S (trans ⟦ y≈z ⟧S (sym x≡y))              ≡⟨ cong (trans ⟦ x≈y ⟧S) $
                                                                  cong₂ trans (sym (sym-sym ⟦ y≈z ⟧S)) (refl (sym x≡y)) ⟩
      trans ⟦ x≈y ⟧S (trans (sym (sym ⟦ y≈z ⟧S)) (sym x≡y))  ≡⟨ cong (trans _) $ sym (sym-trans x≡y (sym ⟦ y≈z ⟧S)) ⟩
      trans ⟦ x≈y ⟧S (sym (trans x≡y (sym ⟦ y≈z ⟧S)))        ≡⟨ cong (trans _) $ snoc-correct y≈z z≈u (sym-sym _) h₂ ⟩∎
      trans ⟦ x≈y ⟧S ⟦ snoc y≈z z≈u ⟧S                       ∎

  append : EqS upper x y → EqS upper y z → EqS upper x z
  append Refl           x≈y = x≈y
  append (Cons x≈y y≈z) z≈u = Cons x≈y (append y≈z z≈u)

  abstract

    append-correct :
      (x≈y : EqS upper x y) (y≈z : EqS upper y z) →
      x≡y ≡ ⟦ x≈y ⟧S → y≡z ≡ ⟦ y≈z ⟧S →
      trans x≡y y≡z ≡ ⟦ append x≈y y≈z ⟧S
    append-correct {x≡y = x≡y} {y≡z} Refl x≈y h₁ h₂ =
      trans x≡y y≡z            ≡⟨ cong₂ trans h₁ h₂ ⟩
      trans (refl _) ⟦ x≈y ⟧S  ≡⟨ trans-reflˡ _ ⟩∎
      ⟦ x≈y ⟧S                 ∎
    append-correct {x≡y = x≡z} {z≡u} (Cons x≈y y≈z) z≈u h₁ h₂ =
      trans x≡z z≡u                        ≡⟨ cong₂ trans h₁ (refl z≡u) ⟩
      trans (trans ⟦ x≈y ⟧S ⟦ y≈z ⟧S) z≡u  ≡⟨ trans-assoc _ _ _ ⟩
      trans ⟦ x≈y ⟧S (trans ⟦ y≈z ⟧S z≡u)  ≡⟨ cong (trans _) $ append-correct y≈z z≈u (refl _) h₂ ⟩∎
      trans ⟦ x≈y ⟧S ⟦ append y≈z z≈u ⟧S   ∎

  map-sym : EqS middle x y → EqS middle y x
  map-sym (No-Sym x≈y) = Sym    x≈y
  map-sym (Sym    x≈y) = No-Sym x≈y

  abstract

    map-sym-correct :
      (x≈y : EqS middle x y) →
      x≡y ≡ ⟦ x≈y ⟧S → sym x≡y ≡ ⟦ map-sym x≈y ⟧S
    map-sym-correct {x≡y = x≡y} (No-Sym x≈y) h =
      sym x≡y       ≡⟨ cong sym h ⟩∎
      sym ⟦ x≈y ⟧S  ∎
    map-sym-correct {x≡y = x≡y} (Sym x≈y) h =
      sym x≡y             ≡⟨ cong sym h ⟩
      sym (sym ⟦ x≈y ⟧S)  ≡⟨ sym-sym _ ⟩∎
      ⟦ x≈y ⟧S            ∎

  reverse : EqS upper x y → EqS upper y x
  reverse Refl           = Refl
  reverse (Cons x≈y y≈z) = snoc (reverse y≈z) (map-sym x≈y)

  abstract

    reverse-correct :
      (x≈y : EqS upper x y) →
      x≡y ≡ ⟦ x≈y ⟧S → sym x≡y ≡ ⟦ reverse x≈y ⟧S
    reverse-correct {x≡y = x≡y} Refl h =
      sym x≡y       ≡⟨ cong sym h ⟩
      sym (refl _)  ≡⟨ sym-refl ⟩∎
      refl _        ∎
    reverse-correct {x≡y = x≡y} (Cons x≈y y≈z) h =
      sym x≡y                                ≡⟨ cong sym h ⟩
      sym (trans ⟦ x≈y ⟧S ⟦ y≈z ⟧S)          ≡⟨ snoc-correct (reverse y≈z) _
                                                             (reverse-correct y≈z (refl _))
                                                             (map-sym-correct x≈y (refl _)) ⟩∎
      ⟦ snoc (reverse y≈z) (map-sym x≈y) ⟧S  ∎

  map-cong : {A B : Type a} {x y : A} (f : A → B) →
             EqS ℓ x y → EqS ℓ (f x) (f y)
  map-cong {ℓ = lower}  f (Cong g x≡y)   = Cong (f ∘ g) x≡y
  map-cong {ℓ = middle} f (No-Sym x≈y)   = No-Sym (map-cong f x≈y)
  map-cong {ℓ = middle} f (Sym    y≈x)   = Sym (map-cong f y≈x)
  map-cong {ℓ = upper}  f Refl           = Refl
  map-cong {ℓ = upper}  f (Cons x≈y y≈z) =
    Cons (map-cong f x≈y) (map-cong f y≈z)

  abstract

    map-cong-correct :
      (f : A → B) (x≈y : EqS ℓ x y) →
      x≡y ≡ ⟦ x≈y ⟧S → cong f x≡y ≡ ⟦ map-cong f x≈y ⟧S
    map-cong-correct {ℓ = lower} {x≡y = gx≡gy} f (Cong g x≡y) h =
      cong f gx≡gy         ≡⟨ cong (cong f) h ⟩
      cong f (cong g x≡y)  ≡⟨ cong-∘ f g _ ⟩∎
      cong (f ∘ g) x≡y     ∎
    map-cong-correct {ℓ = middle} {x≡y = x≡y} f (No-Sym x≈y) h =
      cong f x≡y           ≡⟨ map-cong-correct f x≈y h ⟩∎
      ⟦ map-cong f x≈y ⟧S  ∎
    map-cong-correct {ℓ = middle} {x≡y = x≡y} f (Sym y≈x) h =
      cong f x≡y               ≡⟨ cong (cong f) h ⟩
      cong f (sym ⟦ y≈x ⟧S)    ≡⟨ cong-sym f _ ⟩
      sym (cong f ⟦ y≈x ⟧S)    ≡⟨ cong sym (map-cong-correct f y≈x (refl _)) ⟩∎
      sym ⟦ map-cong f y≈x ⟧S  ∎
    map-cong-correct {ℓ = upper} {x≡y = x≡y} f Refl h =
      cong f x≡y       ≡⟨ cong (cong f) h ⟩
      cong f (refl _)  ≡⟨ cong-refl f ⟩∎
      refl _           ∎
    map-cong-correct {ℓ = upper} {x≡y = x≡y} f (Cons x≈y y≈z) h =
      cong f x≡y                                     ≡⟨ cong (cong f) h ⟩
      cong f (trans ⟦ x≈y ⟧S ⟦ y≈z ⟧S)               ≡⟨ cong-trans f _ _ ⟩
      trans (cong f ⟦ x≈y ⟧S) (cong f ⟦ y≈z ⟧S)      ≡⟨ cong₂ trans (map-cong-correct f x≈y (refl _))
                                                                    (map-cong-correct f y≈z (refl _)) ⟩∎
      trans ⟦ map-cong f x≈y ⟧S ⟦ map-cong f y≈z ⟧S  ∎

-- Equality-preserving simplifier.

simplify : Eq x y → EqS upper x y
simplify (Lift x≡y)      = lift x≡y
simplify Refl            = Refl
simplify (Sym x≡y)       = reverse (simplify x≡y)
simplify (Trans x≡y y≡z) = append (simplify x≡y) (simplify y≡z)
simplify (Cong f x≡y)    = map-cong f (simplify x≡y)

abstract

  simplify-correct :
    (x≈y : Eq x y) → ⟦ x≈y ⟧ ≡ ⟦ simplify x≈y ⟧S
  simplify-correct (Lift x≡y)      = lift-correct x≡y
  simplify-correct Refl            = refl _
  simplify-correct (Sym x≈y)       = reverse-correct (simplify x≈y)
                                       (simplify-correct x≈y)
  simplify-correct (Trans x≈y y≈z) = append-correct (simplify x≈y) _
                                       (simplify-correct x≈y)
                                       (simplify-correct y≈z)
  simplify-correct (Cong f x≈y)    = map-cong-correct f (simplify x≈y)
                                       (simplify-correct x≈y)

------------------------------------------------------------------------
-- Tactic

abstract

  -- Simple tactic for proving equality of equality proofs.

  prove : (x≡y x≡y′ : Eq x y) →
          ⟦ simplify x≡y ⟧S ≡ ⟦ simplify x≡y′ ⟧S →
          ⟦ x≡y ⟧ ≡ ⟦ x≡y′ ⟧
  prove x≡y x≡y′ hyp =
    ⟦ x≡y ⟧             ≡⟨ simplify-correct x≡y ⟩
    ⟦ simplify x≡y  ⟧S  ≡⟨ hyp ⟩
    ⟦ simplify x≡y′ ⟧S  ≡⟨ sym (simplify-correct x≡y′) ⟩∎
    ⟦ x≡y′ ⟧            ∎

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

private
  module Examples (x≡y : x ≡ y) where

    ex₁ : trans (refl x) (sym (sym x≡y)) ≡ x≡y
    ex₁ = prove (Trans Refl (Sym (Sym (Lift x≡y)))) (Lift x≡y) (refl _)

    ex₂ : cong proj₂ (sym (cong (_,_ x) x≡y)) ≡ sym x≡y
    ex₂ = prove (Cong proj₂ (Sym (Cong (_,_ x) (Lift x≡y))))
                (Sym (Lift x≡y))
                (refl _)

-- Non-examples: The tactic cannot prove trans-symˡ or trans-symʳ.

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module HelloWorld where

open import IO
open import Data.String
open import Data.Unit
open import Level using (0ℓ)

main = run {0ℓ} (putStrLn "Hello World!")

max_stars_repo_name: guilhermehas/agda

max_issues_repo_name: guilhermehas/agda

max_forks_repo_name: guilhermehas/agda


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

open import Level
open import Data.Empty
open import Data.Sum
open import Relation.Binary.Core

open import Categories.Category

module _ {a a′ ℓ ℓ′} {A : Set a} (_∼_ : Rel A ℓ) where
  lift-∼ : Rel (Lift {ℓ = a′} A) (ℓ ⊔ ℓ′)
  lift-∼ (lift x) (lift y) = Lift {ℓ = ℓ′} (x ∼ y)

  lift-equiv : IsEquivalence _∼_ → IsEquivalence lift-∼
  lift-equiv record { refl = refl-∼ ; sym = sym-∼ ; trans = trans-∼ } =
    record { refl = lift refl-∼
           ; sym = λ { {lift x} {lift y} {lift x∼y} → lift (sym-∼ x∼y) }
           ; trans = λ { {lift x} {lift y} {lift z} {lift x∼y} {lift y∼z} → lift (trans-∼ x∼y y∼z) }
           }

Coproduct : ∀ {o ℓ e o′ ℓ′ e′} (C : Category o ℓ e) (D : Category o′ ℓ′ e′) → Category (o ⊔ o′) (ℓ ⊔ ℓ′) (e ⊔ e′)
Coproduct {o} {ℓ} {e} {o′} {ℓ′} {e′} C D = record
  { Obj = C.Obj ⊎ D.Obj
  ; _⇒_ = λ { (inj₁ c₁) (inj₁ c₂) → Lift {ℓ = ℓ′} (C._⇒_ c₁ c₂)
             ; (inj₁ _)  (inj₂ _)  → Lift ⊥
             ; (inj₂ _)  (inj₁ _)  → Lift ⊥
             ; (inj₂ d₁) (inj₂ d₂) → Lift {ℓ = ℓ} (D._⇒_ d₁ d₂)
             }
  ; _≡_ = λ { {inj₁ _} {inj₁ _} → lift-∼ {ℓ′ = e′} C._≡_
            ; {inj₁ _} {inj₂ _} (lift ()) (lift ())
            ; {inj₂ _} {inj₁ _} (lift ()) (lift ())
            ; {inj₂ _} {inj₂ _} → lift-∼ {ℓ′ = e} D._≡_
            }
  ; _∘_ = λ { {inj₁ _} {inj₁ _} {inj₁ _} (lift f) (lift g) → lift (C._∘_ f g)
            ; {inj₁ _} {inj₁ _} {inj₂ _} (lift ()) _
            ; {inj₁ _} {inj₂ _} {inj₁ _} _ (lift ())
            ; {inj₁ _} {inj₂ _} {inj₂ _} _ (lift ())
            ; {inj₂ _} {inj₁ _} {inj₁ _} _ (lift ())
            ; {inj₂ _} {inj₁ _} {inj₂ _} (lift ()) _
            ; {inj₂ _} {inj₂ _} {inj₁ _} (lift ()) _
            ; {inj₂ _} {inj₂ _} {inj₂ _} (lift f) (lift g) → lift (D._∘_ f g)
            }
  ; id = λ { {inj₁ _} → lift C.id ; {inj₂ _} → lift D.id }
  ; assoc = λ { {inj₁ _} {inj₁ _} {inj₁ _} {inj₁ _} → lift C.assoc
              ; {inj₁ _} {inj₁ _} {inj₁ _} {inj₂ _} {_} {_} {lift ()}
              ; {inj₁ _} {inj₁ _} {inj₂ _} {inj₁ _} {_} {lift ()} {_}
              ; {inj₁ _} {inj₁ _} {inj₂ _} {inj₂ _} {_} {lift ()} {_}
              ; {inj₁ _} {inj₂ _} {inj₁ _} {inj₁ _} {lift ()} {_} {_}
              ; {inj₁ _} {inj₂ _} {inj₁ _} {inj₂ _} {lift ()} {_} {_}
              ; {inj₁ _} {inj₂ _} {inj₂ _} {inj₁ _} {lift ()} {_} {_}
              ; {inj₁ _} {inj₂ _} {inj₂ _} {inj₂ _} {lift ()} {_} {_}
              ; {inj₂ _} {inj₁ _} {inj₁ _} {inj₁ _} {lift ()} {_} {_}
              ; {inj₂ _} {inj₁ _} {inj₁ _} {inj₂ _} {lift ()} {_} {_}
              ; {inj₂ _} {inj₁ _} {inj₂ _} {inj₁ _} {lift ()} {_} {_}
              ; {inj₂ _} {inj₁ _} {inj₂ _} {inj₂ _} {lift ()} {_} {_}
              ; {inj₂ _} {inj₂ _} {inj₁ _} {inj₁ _} {_} {lift ()} {_}
              ; {inj₂ _} {inj₂ _} {inj₁ _} {inj₂ _} {_} {lift ()} {_}
              ; {inj₂ _} {inj₂ _} {inj₂ _} {inj₁ _} {_} {_} {lift ()}
              ; {inj₂ _} {inj₂ _} {inj₂ _} {inj₂ _} → lift D.assoc
              }
  ; identityˡ = λ { {inj₁ _} {inj₁ _} → lift C.identityˡ
                  ; {inj₁ _} {inj₂ _} {lift ()}
                  ; {inj₂ _} {inj₁ _} {lift ()}
                  ; {inj₂ _} {inj₂ _} → lift D.identityˡ
                  }
  ; identityʳ = λ { {inj₁ _} {inj₁ _} → lift C.identityʳ
                  ; {inj₁ _} {inj₂ _} {lift ()}
                  ; {inj₂ _} {inj₁ _} {lift ()}
                  ; {inj₂ _} {inj₂ _} → lift D.identityʳ
                  }
  ; equiv = λ { {inj₁ _} {inj₁ _} → lift-equiv _ C.equiv
              ; {inj₁ _} {inj₂ _} → record { refl = λ { {lift ()} }
                                           ; sym = λ { {lift ()} }
                                           ; trans = λ { {lift ()} }
                                           }
              ; {inj₂ _} {inj₁ _} → record { refl = λ { {lift ()} }
                                           ; sym = λ { {lift ()} }
                                           ; trans = λ { {lift ()} }
                                           }
              ; {inj₂ _} {inj₂ _} → lift-equiv _ D.equiv
              }
  ; ∘-resp-≡ = λ { {inj₁ _} {inj₁ _} {inj₁ _} → λ { (lift f) (lift g) → lift (C.∘-resp-≡ f g) }
                 ; {inj₁ _} {inj₁ _} {inj₂ _} {lift ()} {_} {_}
                 ; {inj₁ _} {inj₂ _} {inj₁ _} {lift ()} {_} {_}
                 ; {inj₁ _} {inj₂ _} {inj₂ _} {_} {_} {lift ()}
                 ; {inj₂ _} {inj₁ _} {inj₁ _} {_} {_} {lift ()}
                 ; {inj₂ _} {inj₁ _} {inj₂ _} {lift ()} {_} {_}
                 ; {inj₂ _} {inj₂ _} {inj₁ _} {lift ()} {_} {_}
                 ; {inj₂ _} {inj₂ _} {inj₂ _} → λ { (lift f) (lift g) → lift (D.∘-resp-≡ f g) }
                 }
  }
  where
  module C = Category C
  module D = Category D

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: copumpkin/categories

max_forks_repo_name: copumpkin/categories


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Data.Queue.Untruncated2List where

open import Cubical.Foundations.Everything

open import Cubical.Foundations.SIP
open import Cubical.Structures.Queue

open import Cubical.Data.Maybe
open import Cubical.Data.List
open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation

open import Cubical.Data.Queue.1List

module Untruncated2List {ℓ} (A : Type ℓ) (Aset : isSet A) where
 open Queues-on A Aset

 -- Untruncated 2Lists
 data Q : Type ℓ where
   Q⟨_,_⟩ : (xs ys : List A) → Q
   tilt : ∀ xs ys z → Q⟨ xs ++ [ z ] , ys ⟩ ≡ Q⟨ xs , ys ++ [ z ] ⟩

  -- enq into the first list, deq from the second if possible

 flushEq' : (xs ys : List A) → Q⟨ xs ++ ys , [] ⟩ ≡ Q⟨ xs , rev ys ⟩
 flushEq' xs [] = cong Q⟨_, [] ⟩ (++-unit-r xs)
 flushEq' xs (z ∷ ys) j =
   hcomp
     (λ i → λ
       { (j = i0) → Q⟨ ++-assoc xs [ z ] ys i , [] ⟩
       ; (j = i1) → tilt xs (rev ys) z i
       })
     (flushEq' (xs ++ [ z ]) ys j)

 flushEq : (xs ys : List A) → Q⟨ xs ++ rev ys , [] ⟩ ≡ Q⟨ xs , ys ⟩
 flushEq xs ys = flushEq' xs (rev ys) ∙ cong Q⟨ xs ,_⟩ (rev-rev ys)

 emp : Q
 emp = Q⟨ [] , [] ⟩

 enq : A → Q → Q
 enq a Q⟨ xs , ys ⟩ = Q⟨ a ∷ xs , ys ⟩
 enq a (tilt xs ys z i) = tilt (a ∷ xs) ys z i

 deqFlush : List A → Maybe (Q × A)
 deqFlush [] = nothing
 deqFlush (x ∷ xs) = just (Q⟨ [] , xs ⟩ , x)

 deq : Q → Maybe (Q × A)
 deq Q⟨ xs , [] ⟩ = deqFlush (rev xs)
 deq Q⟨ xs , y ∷ ys ⟩ = just (Q⟨ xs , ys ⟩ , y)
 deq (tilt xs [] z i) = path i
   where
   path : deqFlush (rev (xs ++ [ z ])) ≡ just (Q⟨ xs , [] ⟩ , z)
   path =
     cong deqFlush (rev-snoc xs z)
     ∙ cong (λ q → just (q , z)) (sym (flushEq' [] xs))
 deq (tilt xs (y ∷ ys) z i) = just (tilt xs ys z i , y)

 Raw : RawQueue
 Raw = (Q , emp , enq , deq)

 -- We construct an equivalence Q₁≃Q and prove that this is an equivalence of queue structures

 private
   module One = 1List A Aset
   open One renaming (Q to Q₁; emp to emp₁; enq to enq₁; deq to deq₁) using ()

 quot : Q₁ → Q
 quot xs = Q⟨ xs , [] ⟩

 eval : Q → Q₁
 eval Q⟨ xs , ys ⟩ = xs ++ rev ys
 eval (tilt xs ys z i) =
   hcomp
     (λ j → λ
       { (i = i0) → (xs ++ [ z ]) ++ rev ys
       ; (i = i1) → xs ++ rev-snoc ys z (~ j)
       })
     (++-assoc xs [ z ] (rev ys) i)

 quot∘eval : ∀ q → quot (eval q) ≡ q
 quot∘eval Q⟨ xs , ys ⟩ = flushEq xs ys
 quot∘eval (tilt xs ys z i) j =
   hcomp
     (λ k → λ
       { (i = i0) →
         compPath-filler (flushEq' (xs ++ [ z ]) (rev ys)) (cong Q⟨ xs ++ [ z ] ,_⟩ (rev-rev ys)) k j
       ; (i = i1) → helper k
       ; (j = i0) →
         Q⟨ compPath-filler (++-assoc xs [ z ] (rev ys)) (cong (xs ++_) (sym (rev-snoc ys z))) k i , [] ⟩
       ; (j = i1) → tilt xs (rev-rev ys k) z i
       })
     flushEq'-filler
   where
   flushEq'-filler : Q
   flushEq'-filler =
     hfill
       (λ i → λ
         { (j = i0) → Q⟨ ++-assoc xs [ z ] (rev ys) i , [] ⟩
         ; (j = i1) → tilt xs (rev (rev ys)) z i
         })
       (inS (flushEq' (xs ++ [ z ]) (rev ys) j))
       i

   helper : I → Q
   helper k =
     hcomp
       (λ l → λ
         { (j = i0) → Q⟨ xs ++ rev-snoc ys z (l ∧ ~ k) , [] ⟩
         ; (j = i1) → Q⟨ xs , rev-rev-snoc ys z l k ⟩
         ; (k = i0) → flushEq' xs (rev-snoc ys z l) j
         ; (k = i1) → flushEq xs (ys ++ [ z ]) j
         })
       (compPath-filler (flushEq' xs (rev (ys ++ [ z ]))) (cong Q⟨ xs ,_⟩ (rev-rev (ys ++ [ z ]))) k j)

 eval∘quot : ∀ xs → eval (quot xs) ≡ xs
 eval∘quot = ++-unit-r

 -- We get our desired equivalence
 quotEquiv : Q₁ ≃ Q
 quotEquiv = isoToEquiv (iso quot eval quot∘eval eval∘quot)

 -- Now it only remains to prove that this is an equivalence of queue structures
 quot∘emp : quot emp₁ ≡ emp
 quot∘emp = refl

 quot∘enq : ∀ x xs → quot (enq₁ x xs) ≡ enq x (quot xs)
 quot∘enq x xs = refl

 quot∘deq : ∀ xs → deqMap quot (deq₁ xs) ≡ deq (quot xs)
 quot∘deq [] = refl
 quot∘deq (x ∷ []) = refl
 quot∘deq (x ∷ x' ∷ xs) =
   deqMap-∘ quot (enq₁ x) (deq₁ (x' ∷ xs))
   ∙ sym (deqMap-∘ (enq x) quot (deq₁ (x' ∷ xs)))
   ∙ cong (deqMap (enq x)) (quot∘deq (x' ∷ xs))
   ∙ lemma x x' (rev xs)
   where
   lemma : ∀ x x' ys
     → deqMap (enq x) (deqFlush (ys ++ [ x' ]))
       ≡ deqFlush ((ys ++ [ x' ]) ++ [ x ])
   lemma x x' [] i = just (tilt [] [] x i , x')
   lemma x x' (y ∷ ys) i = just (tilt [] (ys ++ [ x' ]) x i , y)

 quotEquivHasQueueEquivStr : RawQueueEquivStr One.Raw Raw quotEquiv
 quotEquivHasQueueEquivStr = quot∘emp , quot∘enq , quot∘deq

 -- And we get a path between the raw 1Lists and 2Lists
 Raw-1≡2 : One.Raw ≡ Raw
 Raw-1≡2 = sip rawQueueUnivalentStr _ _ (quotEquiv , quotEquivHasQueueEquivStr)

 -- We derive the axioms for 2List from those for 1List
 WithLaws : Queue
 WithLaws = Q , str Raw , subst (uncurry QueueAxioms) Raw-1≡2 (snd (str One.WithLaws))

 -- In particular, the untruncated queue type is a set
 isSetQ : isSet Q
 isSetQ = str WithLaws .snd .fst

 WithLaws-1≡2 : One.WithLaws ≡ WithLaws
 WithLaws-1≡2 = sip queueUnivalentStr _ _ (quotEquiv , quotEquivHasQueueEquivStr)

 Finite : FiniteQueue
 Finite = Q , str WithLaws , subst (uncurry FiniteQueueAxioms) WithLaws-1≡2 (snd (str One.Finite))

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed binary relations
------------------------------------------------------------------------

-- The contents of this module should be accessed via
-- `Relation.Binary.Indexed.Heterogeneous`.

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

module Relation.Binary.Indexed.Heterogeneous.Core where

open import Level
import Relation.Binary.Core as B
import Relation.Binary.Definitions as B
import Relation.Binary.PropositionalEquality.Core as P

------------------------------------------------------------------------
-- Indexed binary relations

-- Heterogeneous types

IREL : ∀ {i₁ i₂ a₁ a₂} {I₁ : Set i₁} {I₂ : Set i₂} →
      (I₁ → Set a₁) → (I₂ → Set a₂) → (ℓ : Level) → Set _
IREL A₁ A₂ ℓ = ∀ {i₁ i₂} → A₁ i₁ → A₂ i₂ → Set ℓ

-- Homogeneous types

IRel : ∀ {i a} {I : Set i} → (I → Set a) → (ℓ : Level) → Set _
IRel A ℓ = IREL A A ℓ

------------------------------------------------------------------------
-- Generalised implication.

infixr 4 _=[_]⇒_

_=[_]⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : A → Set b} →
          B.Rel A ℓ₁ → ((x : A) → B x) → IRel B ℓ₂ → Set _
P =[ f ]⇒ Q = ∀ {i j} → P i j → Q (f i) (f j)


text:
-- Andreas, 2017-10-04, ignore irrelevant arguments during with-abstraction
-- Feature request by xekoukou

{-# OPTIONS --allow-unsolved-metas --show-irrelevant #-}

-- {-# OPTIONS -v tc.abstract:100 #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Bool

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

but : Bool → .(Bool → Bool) → Bool
but true  f = false
but false f = true

test : (x : Bool) → but x not ≡ true
test x with but x not' where
  not' : Bool → Bool
  not' true  = false
  not' false = true
test x | true = refl
test x | false = _  -- unsolved meta ok

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import HoTT

module homotopy.ConstantToSetExtendsToProp {i j}
  {A : Type i} {B : Type j} (B-is-set : is-set B)
  (f : A → B) (f-is-const : ∀ a₁ a₂ → f a₁ == f a₂) where

  private
    Skel = SetQuot {A = A} (λ _ _ → Unit)

    abstract
      Skel-has-all-paths : has-all-paths Skel
      Skel-has-all-paths =
        SetQuot-elim (λ _ → Π-is-set λ _ → =-preserves-set SetQuot-is-set)
          (λ a₁ →
            SetQuot-elim {P = λ s₂ → q[ a₁ ] == s₂}
              (λ _ → =-preserves-set SetQuot-is-set)
              (λ _ → quot-rel _)
              (λ _ → prop-has-all-paths-↓ (SetQuot-is-set _ _)))
          (λ {a₁ a₂} _ → ↓-Π-cst-app-in λ s₂ →
              prop-has-all-paths-↓ (SetQuot-is-set _ _))

    Skel-is-prop : is-prop Skel
    Skel-is-prop = all-paths-is-prop Skel-has-all-paths

    Skel-lift : Skel → B
    Skel-lift = SetQuot-rec B-is-set f (λ {a₁ a₂} _ → f-is-const a₁ a₂)

  ext : Trunc -1 A → B
  ext = Skel-lift ∘ Trunc-rec Skel-is-prop q[_]

  abstract
    ext-is-const : ∀ a₁ a₂ → ext a₁ == ext a₂
    ext-is-const = Trunc-elim
      (λ a₁ → Π-is-prop λ a₂ → B-is-set _ _)
      (λ a₁ → Trunc-elim (λ a₂ → B-is-set _ _)
        (λ a₂ → f-is-const a₁ a₂))

  private
    abstract
      -- The beta rule.
      -- This is definitionally true, so you don't need it.
      β : ext ∘ [_] == f
      β = idp

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.AssocList where

open import Cubical.HITs.AssocList.Base public
open import Cubical.HITs.AssocList.Properties public


text:
-- Andreas, 2015-09-18 Andreas, issue reported by Gillaume Brunerie

{- Problem WAS

The following code doesn’t typecheck but it should. I have no idea what’s going on.

Replacing the definition of PathOver-rewr by a question mark and
asking for full normalisation of the goal (C-u C-u C-c C-t), I obtain
HetEq idp u v == (u == v), so it seems that the term PathOver (λ _ →
B) p u v) is rewritten as HetEq idp u v using ap-cst (as expected),
but then for some reason HetEq idp u v isn’t reduced to u == v. -}

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

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

ap : ∀ {i j} {A : Set i} {B : Set j} (f : A → B) {x y : A}
  → x == y → f x == f y
ap f idp = idp

ap-cst : {A B : Set} (b : B) {x y : A} (p : x == y)
  → ap (λ _ → b) p == idp
ap-cst b idp = idp
{-# REWRITE ap-cst #-}

HetEq : {A B : Set} (e : A == B) (a : A) (b : B) → Set
HetEq idp a b = (a == b)

PathOver : {A : Set} (B : A → Set)
  {x y : A} (p : x == y) (u : B x) (v : B y) → Set
PathOver B p u v = HetEq (ap B p) u v

PathOver-rewr : {A B : Set} {x y : A} (p : x == y) (u v : B)
  → (PathOver (λ _ → B) p u v) == (u == v)
PathOver-rewr p u v = idp


text:
--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems

{-# OPTIONS --sized-types #-}

module is-lib.SInfSys {𝓁} where
  open import is-lib.InfSys.Base {𝓁} public
  open import is-lib.InfSys.Induction {𝓁} public
  open import is-lib.InfSys.SCoinduction {𝓁} public
  open import is-lib.InfSys.FlexSCoinduction {𝓁} public
  open MetaRule public
  open FinMetaRule public
  open IS public

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
module Q where
import AlonzoPrelude
open AlonzoPrelude -- , using(Bool,False,True,String,showBool)
import PreludeNat
open PreludeNat
import PreludeBool
open PreludeBool
import PreludeShow
open PreludeShow

pred : Nat -> Nat
pred (zero) = zero
pred (suc n) = n

mplus : Nat -> Nat -> Nat
mplus zero y = y
mplus (suc n) y = suc (mplus n  y )

Q : Bool -> Set
Q true = Nat
Q false = Bool

f : (b : Bool) -> Q b
f true = pred 3
f false = true

mid : {A : Set} -> A -> A
mid x = x

mainS : String
mainS = showBool (f (const false true))

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module TooManyArgumentsInLHS where

F : Set -> Set
F X Y = Y

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --postfix-projections #-}

module StateSizedIO.cellStateDependent where

open import Data.Product
open import Data.String.Base

{-
open import SizedIO.Object
open import SizedIO.ConsoleObject
-}

open import SizedIO.Console hiding (main)

open import SizedIO.Base

open import NativeIO

open import StateSizedIO.Object
open import StateSizedIO.IOObject

open import Size

data CellStateˢ  : Set where
  empty full  : CellStateˢ

data CellMethodEmpty A : Set where
    put : A → CellMethodEmpty A

data CellMethodFull A : Set where
    get : CellMethodFull A
    put : A → CellMethodFull A

CellMethodˢ : (A : Set) → CellStateˢ → Set
CellMethodˢ A empty = CellMethodEmpty A
CellMethodˢ A full = CellMethodFull A

putGen : {A : Set} → {i : CellStateˢ} → A → CellMethodˢ A i
putGen {i = empty} = put
putGen {i = full} = put

CellResultFull : ∀{A} → CellMethodFull A → Set
CellResultFull {A} get = A
CellResultFull (put _) = Unit

CellResultEmpty : ∀{A} → CellMethodEmpty A → Set
CellResultEmpty (put _) = Unit

CellResultˢ : (A : Set) → (s : CellStateˢ) → CellMethodˢ A s → Set
CellResultˢ A empty = CellResultEmpty{A}
CellResultˢ A full = CellResultFull{A}

nˢ : ∀{A} → (s : CellStateˢ) → (c : CellMethodˢ A s) → (CellResultˢ A s c) → CellStateˢ
nˢ _ _ _ = full

CellInterfaceˢ : (A : Set) → Interfaceˢ
Stateˢ (CellInterfaceˢ A)  = CellStateˢ
Methodˢ (CellInterfaceˢ A)  = CellMethodˢ A
Resultˢ (CellInterfaceˢ A)  = CellResultˢ A
nextˢ (CellInterfaceˢ A)  = nˢ

mutual
   cellPempty : (i : Size) → IOObjectˢ consoleI (CellInterfaceˢ String) i empty
   method (cellPempty i) {j} (put str) = do (putStrLn ("put (" ++ str ++ ")")) λ _ →
                                         return (unit , cellPfull j str)

   cellPfull : (i : Size) → (str : String) → IOObjectˢ consoleI (CellInterfaceˢ String) i full
   method (cellPfull i str) {j} get        = do (putStrLn ("get (" ++ str ++ ")")) λ _ →
                                             return (str , cellPfull j str)
   method (cellPfull i str) {j} (put str') = do (putStrLn ("put (" ++ str' ++ ")")) λ _ →
                                             return (unit , cellPfull j str')

-- UNSIZED Version, without IO
mutual
   cellPempty' : ∀{A} → Objectˢ (CellInterfaceˢ A) empty
   cellPempty' .objectMethod (put a)     =  (_ , cellPfull' a)

   cellPfull' : ∀{A} → A → Objectˢ (CellInterfaceˢ A) full
   cellPfull' a .objectMethod get         = (a , cellPfull' a)
   cellPfull' a .objectMethod (put a')  = (_ , cellPfull' a')

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui