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

import Categories.Category
import Categories.Functor
import Categories.Category.Instance.Setoids
import Categories.Monad.Relative
import Categories.Category.Equivalence
import Categories.Category.Cocartesian

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

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

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

  -- substitution

  infix 4 _⊕_⇒ˢ_

  _⊕_⇒ˢ_ : ∀ (Θ : MContext) (Γ Δ : VContext) → Set ℓ
  Θ ⊕ Γ ⇒ˢ Δ = ∀ {A} (x : A ∈ Γ) → Term Θ Δ A

  -- syntactic equality of substitutions

  infix 5 _≈ˢ_

  _≈ˢ_ : ∀ {Θ} {Γ Δ} (σ τ : Θ ⊕ Γ ⇒ˢ Δ) → Set ℓ
  _≈ˢ_ {Θ} {Γ} σ τ = ∀ {A} (x : A ∈ Γ) → σ x ≈ τ x

  -- equality of substitutions form a setoid
  ≈ˢ-refl : ∀ {Θ Γ Δ} {σ : Θ ⊕ Γ ⇒ˢ Δ}
          → σ ≈ˢ σ
  ≈ˢ-refl x = ≈-refl

  ≈ˢ-sym : ∀ {Θ Γ Δ} {σ τ : Θ ⊕ Γ ⇒ˢ Δ}
          → σ ≈ˢ τ
          → τ ≈ˢ σ
  ≈ˢ-sym eq x = ≈-sym (eq x)

  ≈ˢ-trans : ∀ {Θ Γ Δ} {σ τ μ : Θ ⊕ Γ ⇒ˢ Δ}
           → σ ≈ˢ τ → τ ≈ˢ μ
           → σ ≈ˢ μ
  ≈ˢ-trans eq1 eq2 x = ≈-trans (eq1 x) (eq2 x)

  substitution-setoid : ∀ (Γ Δ : VContext) (Θ : MContext) → Setoid ℓ ℓ
  substitution-setoid Γ Δ Θ =
    record
      { Carrier = Θ ⊕ Γ ⇒ˢ Δ
      ;  _≈_ = λ σ τ → σ ≈ˢ τ
      ; isEquivalence =
                      record
                        { refl = λ {σ} x → ≈ˢ-refl {σ = σ} x
                        ; sym = ≈ˢ-sym
                        ; trans = ≈ˢ-trans
                        }
      }

  congˢ : ∀ {Θ} {Γ Δ} {A} {σ τ : Θ ⊕ Γ ⇒ˢ Δ} {x : A ∈ Γ} → σ ≈ˢ τ → σ x ≈ τ x
  congˢ {x = x} eq = eq x

  congˢ-var :  ∀ {Θ} {Γ Δ} {A} {σ : Θ ⊕ Γ ⇒ˢ Δ} {x y : A ∈ Γ} → x ≡ y → σ x ≈ σ y
  congˢ-var refl = ≈-refl

  -- extension of a substitution

  ⇑ˢ : ∀ {Θ Γ Δ Ξ} → Θ ⊕ Γ ⇒ˢ Δ → Θ ⊕ (Γ ,, Ξ) ⇒ˢ (Δ ,, Ξ)
  ⇑ˢ σ (var-inl x) = [ var-inl ]ᵛ σ x
  ⇑ˢ σ (var-inr y) = tm-var (var-inr y)

  -- extension respects equality of substitutions

  ⇑ˢ-resp-≈ˢ : ∀ {Θ Γ Δ Ξ} {σ τ : Θ ⊕ Γ ⇒ˢ Δ} → σ ≈ˢ τ → ⇑ˢ {Ξ = Ξ} σ ≈ˢ ⇑ˢ {Ξ = Ξ} τ
  ⇑ˢ-resp-≈ˢ ξ (var-inl x) = []ᵛ-resp-≈ (ξ x)
  ⇑ˢ-resp-≈ˢ ξ (var-inr y) = ≈-refl

  -- the action of a renaming on a substitution

  infixr 6 _ᵛ∘ˢ_

  _ᵛ∘ˢ_ : ∀ {Θ} {Γ Δ Ξ} (ρ : Δ ⇒ᵛ Ξ) (σ : Θ ⊕ Γ ⇒ˢ Δ) → Θ ⊕ Γ ⇒ˢ Ξ
  (ρ ᵛ∘ˢ σ) x =  [ ρ ]ᵛ (σ x)

  infixl 6 _ˢ∘ᵛ_

  _ˢ∘ᵛ_ : ∀ {Θ} {Γ Δ Ξ} (σ : Θ ⊕ Δ ⇒ˢ Ξ) (ρ : Γ ⇒ᵛ Δ)  → Θ ⊕ Γ ⇒ˢ Ξ
  (σ ˢ∘ᵛ ρ) x =  σ (ρ x)

  -- extension commutes with renaming action

  ⇑ˢ-resp-ˢ∘ᵛ : ∀ {Θ} {Γ Δ Ξ Ψ} {ρ : Γ ⇒ᵛ Δ} {σ : Θ ⊕ Δ ⇒ˢ Ξ} → ⇑ˢ {Ξ = Ψ} (σ ˢ∘ᵛ ρ) ≈ˢ ⇑ˢ σ ˢ∘ᵛ ⇑ᵛ ρ
  ⇑ˢ-resp-ˢ∘ᵛ (var-inl x) = ≈-refl
  ⇑ˢ-resp-ˢ∘ᵛ (var-inr x) = ≈-refl

  -- the action of a substitution on a term

  infix 6 [_]ˢ_

  [_]ˢ_ : ∀ {Θ Γ Δ A} → Θ ⊕ Γ ⇒ˢ Δ → Term Θ Γ A → Term Θ Δ A
  [ σ ]ˢ (tm-var x) = σ x
  [ σ ]ˢ (tm-meta M ts) = tm-meta M (λ i → [ σ ]ˢ ts i)
  [ σ ]ˢ (tm-oper f es) = tm-oper f (λ i → [ ⇑ˢ σ ]ˢ es i)

  -- composition of substitutions

  infixl 7 _∘ˢ_
  _∘ˢ_ : ∀ {Θ} {Γ Δ Ξ} → Θ ⊕ Δ ⇒ˢ Ξ → Θ ⊕ Γ ⇒ˢ Δ → Θ ⊕ Γ ⇒ˢ Ξ
  (σ ∘ˢ τ) x = [ σ ]ˢ τ x

  -- substitution action respects equality of terms

  []ˢ-resp-≈ : ∀ {Θ} {Γ Δ} {A} (σ : Θ ⊕ Γ ⇒ˢ Δ) {t u : Term Θ Γ A} → t ≈ u → [ σ ]ˢ t ≈  [ σ ]ˢ u
  []ˢ-resp-≈ σ (≈-≡ refl) = ≈-refl
  []ˢ-resp-≈ σ (≈-meta ξ) = ≈-meta (λ i → []ˢ-resp-≈ σ (ξ i))
  []ˢ-resp-≈ σ (≈-oper ξ) = ≈-oper (λ i → []ˢ-resp-≈ (⇑ˢ σ) (ξ i))

  -- substitution action respects equality of substitutions

  []ˢ-resp-≈ˢ : ∀ {Θ} {Γ Δ} {A} {σ τ : Θ ⊕ Γ ⇒ˢ Δ} (t : Term Θ Γ A) → σ ≈ˢ τ → [ σ ]ˢ t ≈ [ τ ]ˢ t
  []ˢ-resp-≈ˢ (tm-var x) ξ = ξ x
  []ˢ-resp-≈ˢ (tm-meta M ts) ξ = ≈-meta (λ i → []ˢ-resp-≈ˢ (ts i) ξ)
  []ˢ-resp-≈ˢ (tm-oper f es) ξ = ≈-oper (λ i → []ˢ-resp-≈ˢ (es i) (⇑ˢ-resp-≈ˢ ξ))

  -- substitution actions respects both equalities

  []ˢ-resp-≈ˢ-≈ : ∀ {Θ} {Γ Δ} {A} {σ τ : Θ ⊕ Γ ⇒ˢ Δ} {t u : Term Θ Γ A} → σ ≈ˢ τ → t ≈ u → [ σ ]ˢ t ≈ [ τ ]ˢ u
  []ˢ-resp-≈ˢ-≈ {τ = τ} {t = t} ζ ξ = ≈-trans ([]ˢ-resp-≈ˢ t ζ) ([]ˢ-resp-≈ τ ξ)

  -- identity substitution

  idˢ : ∀ {Θ Γ} → Θ ⊕ Γ ⇒ˢ Γ
  idˢ = tm-var

  -- extension preserves identity

  ⇑ˢ-resp-idˢ : ∀ {Θ} {Γ Δ} → ⇑ˢ idˢ ≈ˢ idˢ {Θ = Θ} {Γ = Γ ,, Δ}
  ⇑ˢ-resp-idˢ (var-inl x) = ≈-refl
  ⇑ˢ-resp-idˢ (var-inr y) = ≈-refl

  -- the identity substution acts trivially

  [idˢ] : ∀ {Θ} {Γ} {A} {t : Term Θ Γ A} → [ idˢ ]ˢ t ≈ t
  [idˢ] {t = tm-var x} = ≈-refl
  [idˢ] {t = tm-meta M ts} = ≈-meta (λ i → [idˢ])
  [idˢ] {t = tm-oper f es} = ≈-oper (λ i → ≈-trans ([]ˢ-resp-≈ˢ (es i) ⇑ˢ-resp-idˢ) [idˢ])

  -- the identity substitution preserves equality of terms
  [idˢ]-resp-≈ : ∀ {Θ} {Γ} {A} {t s : Term Θ Γ A} → t ≈ s → [ idˢ ]ˢ t ≈ s
  [idˢ]-resp-≈ t≈s = ≈-trans ([]ˢ-resp-≈ idˢ t≈s) [idˢ]

  -- if a substiution is equal to the identity then it acts trivially
  ≈ˢ-idˢ-[]ˢ : ∀ {Θ} {Γ} {A} {σ : Θ ⊕ Γ ⇒ˢ Γ} {t : Term Θ Γ A} → σ ≈ˢ idˢ → [ σ ]ˢ t ≈ t
  ≈ˢ-idˢ-[]ˢ {t = t} ξ = ≈-trans ([]ˢ-resp-≈ˢ t ξ) [idˢ]

  -- interaction of extension and right renaming action

  [⇑ˢ∘ᵛ] : ∀ {Θ} {A} {Γ Δ Ξ Ψ} {σ : Θ ⊕ Δ ⇒ˢ Ξ} {ρ : Γ ⇒ᵛ Δ} (t : Term Θ (Γ ,, Ψ) A) →
         [ ⇑ˢ (σ ˢ∘ᵛ ρ) ]ˢ t ≈ [ ⇑ˢ σ ]ˢ [ ⇑ᵛ ρ ]ᵛ t
  [⇑ˢ∘ᵛ] (tm-var (var-inl x)) = ≈-refl
  [⇑ˢ∘ᵛ] (tm-var (var-inr x)) = ≈-refl
  [⇑ˢ∘ᵛ] (tm-meta M ts) = ≈-meta (λ i → [⇑ˢ∘ᵛ] (ts i))
  [⇑ˢ∘ᵛ] (tm-oper f es) = ≈-oper (λ i → ≈-trans ([]ˢ-resp-≈ˢ (es i) (⇑ˢ-resp-≈ˢ ⇑ˢ-resp-ˢ∘ᵛ)) ([⇑ˢ∘ᵛ] (es i)))

  -- interaction of extension and left renaming action

  ⇑ˢ-resp-ᵛ∘ˢ : ∀ {Θ} {Γ Δ Ξ Ψ} {σ : Θ ⊕ Γ ⇒ˢ Δ} {ρ : Δ ⇒ᵛ Ξ} →
           ⇑ˢ {Ξ = Ψ} (ρ ᵛ∘ˢ σ) ≈ˢ ⇑ᵛ ρ ᵛ∘ˢ ⇑ˢ σ
  ⇑ˢ-resp-ᵛ∘ˢ (var-inl x) = ≈-trans (≈-sym [∘ᵛ]) (≈-trans ([]ᵛ-resp-≡ᵛ (λ _ → refl)) [∘ᵛ])
  ⇑ˢ-resp-ᵛ∘ˢ (var-inr y) = ≈-refl

  [⇑ᵛ∘ˢ] : ∀ {Θ} {A} {Γ Δ Ξ Ψ} {σ : Θ ⊕ Γ ⇒ˢ Δ} {ρ : Δ ⇒ᵛ Ξ} (t : Term Θ (Γ ,, Ψ) A) →
         [ ⇑ˢ (ρ ᵛ∘ˢ σ) ]ˢ t ≈ [ ⇑ᵛ ρ ]ᵛ ([ ⇑ˢ σ ]ˢ t)
  [⇑ᵛ∘ˢ] (tm-var x) = ⇑ˢ-resp-ᵛ∘ˢ x
  [⇑ᵛ∘ˢ] (tm-meta M ts) = ≈-meta (λ i → [⇑ᵛ∘ˢ] (ts i))
  [⇑ᵛ∘ˢ] (tm-oper f es) = ≈-oper (λ i → ≈-trans ([]ˢ-resp-≈ˢ (es i) (⇑ˢ-resp-≈ˢ ⇑ˢ-resp-ᵛ∘ˢ)) ([⇑ᵛ∘ˢ] (es i)))

  -- functoriality of left renaming action

  [ᵛ∘ˢ] : ∀ {Θ} {A} {Γ Δ Ξ} {ρ : Δ ⇒ᵛ Ξ} {σ : Θ ⊕ Γ ⇒ˢ Δ} (t : Term Θ Γ A) →
           [ ρ ᵛ∘ˢ σ ]ˢ t ≈ [ ρ ]ᵛ [ σ ]ˢ t
  [ᵛ∘ˢ] (tm-var x) = ≈-refl
  [ᵛ∘ˢ] (tm-meta M ts) = ≈-meta (λ i → [ᵛ∘ˢ] (ts i))
  [ᵛ∘ˢ] (tm-oper f es) = ≈-oper (λ i → [⇑ᵛ∘ˢ] (es i))

  -- functoriality of right renaming action

  [ˢ∘ᵛ] : ∀ {Θ} {A} {Γ Δ Ξ} {σ : Θ ⊕ Δ ⇒ˢ Ξ} {ρ : Γ ⇒ᵛ Δ} (t : Term Θ Γ A) →
           [ σ ˢ∘ᵛ ρ ]ˢ t ≈ [ σ ]ˢ [ ρ ]ᵛ t
  [ˢ∘ᵛ] (tm-var x) = ≈-refl
  [ˢ∘ᵛ] (tm-meta M ts) = ≈-meta (λ i → [ˢ∘ᵛ] (ts i))
  [ˢ∘ᵛ] (tm-oper f es) = ≈-oper (λ i → [⇑ˢ∘ᵛ] (es i))

  -- composition commutes with extension

  ⇑ˢ-resp-∘ˢ : ∀ {Θ} {Γ Δ Ξ Ψ} {σ : Θ ⊕ Γ ⇒ˢ Δ} {τ : Θ ⊕ Δ ⇒ˢ Ξ} →
          ⇑ˢ {Ξ = Ψ} (τ ∘ˢ σ) ≈ˢ ⇑ˢ τ ∘ˢ ⇑ˢ σ
  ⇑ˢ-resp-∘ˢ {σ = σ} {τ = τ} (var-inl x) =  ≈-trans (≈-sym ([ᵛ∘ˢ] (σ x))) ([ˢ∘ᵛ] (σ x))
  ⇑ˢ-resp-∘ˢ (var-inr y) = ≈-refl

  -- substitition action is functorial

  [∘ˢ] : ∀ {Θ} {Γ Δ Ξ} {A} {σ : Θ ⊕ Γ ⇒ˢ Δ} {τ : Θ ⊕ Δ ⇒ˢ Ξ} (t : Term Θ Γ A) →
         [ τ ∘ˢ σ ]ˢ t ≈ [ τ ]ˢ ([ σ ]ˢ t)
  [∘ˢ] (tm-var x) = ≈-refl
  [∘ˢ] (tm-meta M ts) = ≈-meta (λ i → [∘ˢ] (ts i))
  [∘ˢ] (tm-oper f es) = ≈-oper (λ i → ≈-trans ([]ˢ-resp-≈ˢ (es i) ⇑ˢ-resp-∘ˢ) ([∘ˢ] (es i)))

  -- Terms form a relative monad

  module _ where
    open Categories.Category
    open Categories.Functor using (Functor)
    open Categories.Category.Instance.Setoids
    open Categories.Monad.Relative
    open Function.Equality using () renaming (setoid to Π-setoid)
    open Categories.Category.Equivalence using (StrongEquivalence)
    open import SecondOrder.IndexedCategory
    open import SecondOrder.RelativeKleisli

    -- The embedding of contexts into setoids indexed by sorts

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

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

    -- The relative monad of terms over contexts

    Term-Monad : Monad slots
    Term-Monad =
      let open Function.Equality using (_⟨$⟩_) renaming (cong to func-cong) in
      record
        { F₀ = Term-setoid Θ
        ; unit = λ A → record { _⟨$⟩_ = idˢ ; cong = λ ξ → ≈-≡ (cong idˢ ξ) }
        ; extend = λ σ A → record { _⟨$⟩_ =  [ (σ _ ⟨$⟩_) ]ˢ_ ; cong = []ˢ-resp-≈ (σ _ ⟨$⟩_)}
        ; identityʳ = λ {_} {_} {σ} A {_} {_} ξ → func-cong (σ A) ξ
        ; identityˡ = λ A → ≈-trans [idˢ]
        ; assoc = λ {_} {_} {_} {σ} {ρ} A {_} {t} ξ → ≈-trans ([]ˢ-resp-≈ _ ξ) ([∘ˢ] t)
        ; extend-≈ = λ {Γ} {Δ} {σ} {ρ} ζ B {s} {t} ξ → []ˢ-resp-≈ˢ-≈ (λ x → ζ _ refl) ξ
        }

    -- the category of contexts and substitutions

    -- we show below that the category of contexts and substitiions is equivalent
    -- to the Kleisli category for the Term relative monad. However, we define
    -- the category of contexts and substitutions directly, as that it is easier
    -- to work with it

    Terms : Category ℓ ℓ ℓ
    Terms =
      record
        { Obj = VContext
        ; _⇒_ = Θ ⊕_⇒ˢ_
        ; _≈_ =  _≈ˢ_
        ; id = idˢ
        ; _∘_ = _∘ˢ_
        ; assoc = λ {Γ} {Δ} {Ξ} {Ψ} {σ} {τ} {ψ} {A} x → [∘ˢ] (σ x)
        ; sym-assoc = λ {Γ} {Δ} {Ξ} {Ψ} {σ} {τ} {ψ} {A} x → ≈-sym ([∘ˢ] (σ x))
        ; identityˡ = λ x → [idˢ]
        ; identityʳ = λ x → ≈-refl
        ; identity² = λ x → ≈-refl
        ; equiv = record { refl = λ {σ} {A} → ≈ˢ-refl {σ = σ} ; sym = ≈ˢ-sym ; trans = ≈ˢ-trans }
        ; ∘-resp-≈ = λ f≈ˢg g≈ˢi x → []ˢ-resp-≈ˢ-≈ f≈ˢg (g≈ˢi x)
        }

    Terms-is-Kleisli : StrongEquivalence Terms (Kleisli Term-Monad)
    Terms-is-Kleisli =
      record
      { F = record
              { F₀ = λ Γ → Γ
              ; F₁ = λ σ A → record { _⟨$⟩_ = λ x → σ x ; cong = λ i≡j → ≈-≡ (cong σ i≡j) }
              ; identity = λ A eq → ≈-≡ (cong idˢ eq)
              ; homomorphism = λ {Γ} {Δ} {Ξ} {σ} {τ} A eq → ≈-≡ (cong (λ x → [ τ ]ˢ σ x) eq)
              ; F-resp-≈ = λ {Γ} {Δ} {σ} {τ} hom_eq A eq
                         → ≈-trans (congˢ hom_eq) (≈-≡ (cong τ eq))
              }
      ; G =
          let open Function.Equality using (_⟨$⟩_) renaming (cong to func-cong) in
          record
              { F₀ = λ Γ → Γ
              ; F₁ = λ {Γ} {Δ} σ {A} → λ x → σ A ⟨$⟩ x
              ; identity = λ x → ≈-refl
              ; homomorphism = λ x → ≈-refl
              ; F-resp-≈ = λ {Γ} {Δ} {σ} {τ} σ≈τ {A} x → σ≈τ A refl
              }
      ; weak-inverse =
          let open Function.Equality using (_⟨$⟩_) renaming (cong to func-cong) in
          record
          { F∘G≈id =
                   record
                   { F⇒G =
                         record
                         { η = λ Γ A → record { _⟨$⟩_ = idˢ
                                               ; cong = λ i≡j → ≈-≡ (cong idˢ i≡j)
                                               }
                         ; commute = λ σ A x≡y → [idˢ]-resp-≈ (≈-≡ (cong (λ x → σ A ⟨$⟩ x) x≡y))
                         ; sym-commute = λ σ A x≡y
                                       → ≈-sym ([idˢ]-resp-≈ (≈-≡ (cong (λ x → σ A ⟨$⟩ x ) (sym x≡y))))
                         }
                   ; F⇐G =
                         record
                         { η = λ Γ A → record { _⟨$⟩_ = idˢ
                                               ; cong = λ i≡j → ≈-≡ (cong idˢ i≡j)
                                               }
                         ; commute = λ σ A x≡y → [idˢ]-resp-≈ (≈-≡ (cong (λ x → σ A ⟨$⟩ x) x≡y))
                         ; sym-commute = λ σ A x≡y
                                       → ≈-sym ([idˢ]-resp-≈ (≈-≡ (cong (λ x → σ A ⟨$⟩ x ) (sym x≡y))))
                         }
                   ; iso = λ Γ → record { isoˡ = λ A x≡y → ≈-≡ (cong tm-var x≡y)
                                         ; isoʳ = λ A x≡y → ≈-≡ (cong tm-var x≡y)
                                         }
                   }
          ; G∘F≈id =
                   record
                   { F⇒G =
                         record
                         { η = λ Γ x → tm-var x
                         ; commute = λ σ x → [idˢ]
                         ; sym-commute = λ σ x → ≈-sym [idˢ]
                         }
                   ; F⇐G =
                         record
                         { η = λ Γ x → tm-var x
                         ; commute = λ σ x → [idˢ]
                         ; sym-commute = λ σ x → ≈-sym [idˢ]
                         }
                   ; iso = λ Γ → record { isoˡ = λ x → ≈-refl
                                         ; isoʳ = λ x → ≈-refl
                                         }
                   }
          }
      }

    -- the binary coproduct structure on Terms

    infixl 7 [_,_]ˢ

    [_,_]ˢ : ∀ {Γ Δ Ξ} (σ : Θ ⊕ Γ ⇒ˢ Ξ) (τ : Θ ⊕ Δ ⇒ˢ Ξ) → Θ ⊕ (Γ ,, Δ) ⇒ˢ Ξ
    [ σ , τ ]ˢ (var-inl x) = σ x
    [ σ , τ ]ˢ (var-inr y) = τ y

    inlˢ : ∀ {Γ Δ} → Θ ⊕ Γ ⇒ˢ Γ ,, Δ
    inlˢ x = tm-var (var-inl x)

    inrˢ : ∀ {Γ Δ} → Θ ⊕ Δ ⇒ˢ Γ ,, Δ
    inrˢ y = tm-var (var-inr y)

    [,]ˢ-resp-≈ˢ : ∀ {Γ Δ Ξ} {σ₁ σ₂ : Θ ⊕ Γ ⇒ˢ Ξ} {τ₁ τ₂ : Θ ⊕ Δ ⇒ˢ Ξ} →
                   σ₁ ≈ˢ σ₂ → τ₁ ≈ˢ τ₂ → [ σ₁ , τ₁ ]ˢ ≈ˢ [ σ₂ , τ₂ ]ˢ
    [,]ˢ-resp-≈ˢ ζ ξ (var-inl x) = ζ x
    [,]ˢ-resp-≈ˢ ζ ξ (var-inr y) = ξ y

    uniqueˢ : ∀ {Γ Δ Ξ} {τ : Θ ⊕ Γ ,, Δ ⇒ˢ Ξ} {ρ : Θ ⊕ Γ ⇒ˢ Ξ} {σ : Θ ⊕ Δ ⇒ˢ Ξ}
              → τ ∘ˢ inlˢ ≈ˢ ρ
              → τ ∘ˢ inrˢ ≈ˢ σ
              → [ ρ , σ ]ˢ ≈ˢ τ
    uniqueˢ ξ ζ (var-inl x) = ≈-sym (ξ x)
    uniqueˢ ξ ζ (var-inr y) = ≈-sym (ζ y)

    Terms-Coproduct : Categories.Category.Cocartesian.BinaryCoproducts Terms
    Terms-Coproduct =
      let open Function.Equality using (_⟨$⟩_) renaming (cong to func-cong) in
      record {
        coproduct =
          λ {Γ Δ} →
          record
            { A+B = Γ ,, Δ
            ; i₁ = inlˢ
            ; i₂ = inrˢ
            ; [_,_] = [_,_]ˢ
            ; inject₁ = λ x → ≈-≡ refl
            ; inject₂ = λ x → ≈-≡ refl
            ; unique = λ {Ξ} {h} p₁ p₂ → uniqueˢ {τ = h} p₁ p₂
            }
      }

    open Categories.Category.Cocartesian.BinaryCoproducts Terms-Coproduct

    -- the sum of subsitutions

    infixl 6 _+ˢ_

    _+ˢ_ : ∀ {Γ₁ Γ₂ Δ₁ Δ₂} (σ : Θ ⊕ Γ₁ ⇒ˢ Δ₁) (τ : Θ ⊕ Γ₂ ⇒ˢ Δ₂) → Θ ⊕ Γ₁ ,, Γ₂ ⇒ˢ Δ₁ ,, Δ₂
    σ +ˢ τ = σ +₁ τ

    -- reassociations of context sums

    assoc-l : ∀ {Γ Δ Ξ} → Θ ⊕ (Γ ,, Δ) ,, Ξ ⇒ˢ Γ ,, (Δ ,, Ξ)
    assoc-l (var-inl (var-inl x)) = tm-var (var-inl x)
    assoc-l (var-inl (var-inr y)) = tm-var (var-inr (var-inl y))
    assoc-l (var-inr z) = tm-var (var-inr (var-inr z))

    assoc-r : ∀ {Γ Δ Ξ} → Θ ⊕ Γ ,, (Δ ,, Ξ) ⇒ˢ (Γ ,, Δ) ,, Ξ
    assoc-r (var-inl x) = tm-var (var-inl (var-inl x))
    assoc-r (var-inr (var-inl y)) = tm-var (var-inl (var-inr y))
    assoc-r (var-inr (var-inr z)) = tm-var (var-inr z)

    assoc-lr : ∀ {Γ Δ Ξ} → assoc-l {Γ = Γ} {Δ = Δ} {Ξ = Ξ} ∘ˢ assoc-r {Γ = Γ} {Δ = Δ} {Ξ = Ξ} ≈ˢ idˢ
    assoc-lr (var-inl x) = ≈-refl
    assoc-lr (var-inr (var-inl y)) = ≈-refl
    assoc-lr (var-inr (var-inr y)) = ≈-refl

    assoc-rl : ∀ {Γ Δ Ξ} → assoc-r {Γ = Γ} {Δ = Δ} {Ξ = Ξ} ∘ˢ assoc-l {Γ = Γ} {Δ = Δ} {Ξ = Ξ} ≈ˢ idˢ
    assoc-rl (var-inl (var-inl x)) = ≈-refl
    assoc-rl (var-inl (var-inr x)) = ≈-refl
    assoc-rl (var-inr z) = ≈-refl

    -- summing with the empty context is the unit

    sum-ctx-empty-r : ∀ {Γ} → Θ ⊕ Γ ,, ctx-empty ⇒ˢ Γ
    sum-ctx-empty-r (var-inl x) = tm-var x

    sum-ctx-empty-l : ∀ {Γ} → Θ ⊕ ctx-empty ,, Γ ⇒ˢ Γ
    sum-ctx-empty-l (var-inr x) = tm-var x

max_stars_repo_name: andrejbauer/formal

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import Functions.Definition
open import Numbers.Naturals.Semiring
open import Sets.Cardinality.Finite.Definition

module Sets.Cardinality.Countable.Definition where

record CountablyInfiniteSet {a : _} (A : Set a) : Set a where
  field
    counting : A → ℕ
    countingIsBij : Bijection counting

data Countable {a : _} (A : Set a) : Set a where
  finite : FiniteSet A → Countable A
  infinite : CountablyInfiniteSet A → Countable A

ext: agda


text:
module L.Base.Unit where

-- Reexport definitions
open import L.Base.Unit.Core public

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


text:
{-# OPTIONS --sized-types #-}
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
module flcagl
   (A : Set)
   ( _≟_ :  (a b : A) → Dec ( a ≡ b ) ) where

open import Data.Bool hiding ( _≟_ )
-- open import Data.Maybe
open import Level renaming ( zero to Zero ; suc to succ )
open import Size

module List where

        data List (i : Size) (A : Set) : Set where
          [] : List i A
          _∷_ : {j : Size< i} (x : A) (xs : List j A) → List i A

        map : ∀{i A B} → (A → B) → List i A → List i B
        map f [] = []
        map f ( x ∷ xs)= f x ∷ map f xs

        foldr : ∀{i} {A B : Set} → (A → B → B) → B → List i A → B
        foldr c n [] = n
        foldr c n (x ∷ xs) = c x (foldr c n xs)

        any : ∀{i A} → (A → Bool) → List i A → Bool
        any p xs = foldr _∨_ false (map p xs)

module Lang where

        open List

        record  Lang (i : Size)  : Set  where
           coinductive
           field
              ν : Bool
              δ : ∀{j : Size< i} → A → Lang j

        open Lang

        _∋_ : ∀{i} → Lang i → List i A → Bool
        l ∋ [] = ν l
        l ∋ ( a ∷ as ) = δ l a ∋ as

        trie : ∀{i}  (f : List i A → Bool) → Lang i
        ν (trie f) = f []
        δ (trie f) a = trie (λ as → f (a ∷ as))

        ∅ : ∀{i} → Lang i
        ν ∅ = false
        δ ∅ x = ∅

        ε : ∀{i} → Lang i
        ν ε = true
        δ ε x = ∅

        open import Relation.Nullary.Decidable

        char : ∀{i}  (a : A) → Lang i
        ν (char a) = false
        δ (char a) x = if ⌊ a ≟ x ⌋ then ε else ∅

        compl : ∀{i}  (l : Lang i) → Lang i
        ν (compl l) = not (ν l)
        δ (compl l) x = compl (δ l x)

        _∪_ : ∀{i} (k l : Lang i) → Lang i
        ν (k ∪ l) = ν k ∨ ν l
        δ (k ∪ l) x = δ k x ∪ δ l x

        _·_ : ∀{i}  (k l : Lang i) → Lang i
        ν (k · l) = ν k ∧ ν l
        δ (k · l) x = let k′l =  δ k x  · l in if ν k then k′l ∪ δ l x else k′l

        _*_ : ∀{i} (k l : Lang i )  → Lang i
        ν (k * l) = ν k ∧ ν l
        δ (_*_ {i} k  l) {j} x =
            let
                k′l : Lang j
                k′l  = _*_ {j} (δ k {j} x) l
            in  if ν k then _∪_ {j}  k′l (δ l {j} x) else k′l

        _* : ∀{i} (l : Lang i) → Lang i
        ν (l *) = true
        δ (l *) x = δ l x · (l *)

        record _≅⟨_⟩≅_ (l : Lang ∞ ) i (k : Lang ∞) : Set  where
           coinductive
           field ≅ν : ν l ≡ ν k
                 ≅δ : ∀ {j : Size< i } (a : A ) → δ l a ≅⟨ j ⟩≅ δ k a

        open _≅⟨_⟩≅_

        ≅refl : ∀{i} {l : Lang ∞} → l ≅⟨ i ⟩≅ l
        ≅ν ≅refl = refl
        ≅δ ≅refl a = ≅refl

        ≅sym : ∀{i} {k l : Lang ∞} (p : l ≅⟨ i ⟩≅ k) → k ≅⟨ i ⟩≅ l
        ≅ν (≅sym p) = sym (≅ν p)
        ≅δ (≅sym p) a = ≅sym (≅δ p a)

        ≅trans : ∀{i} {k l m : Lang ∞}
           ( p : k ≅⟨ i ⟩≅ l ) ( q : l ≅⟨ i ⟩≅ m ) → k ≅⟨ i ⟩≅ m
        ≅ν (≅trans p q) = trans (≅ν p) (≅ν q)
        ≅δ (≅trans p q) a = ≅trans (≅δ p a) (≅δ q a)

        open import Relation.Binary

        ≅isEquivalence : ∀(i : Size) → IsEquivalence _≅⟨ i ⟩≅_
        ≅isEquivalence i = record { refl = ≅refl; sym = ≅sym; trans = ≅trans }

        Bis : ∀(i : Size) → Setoid _ _
        Setoid.Carrier (Bis i) = Lang ∞
        Setoid._≈_ (Bis i) = _≅⟨ i ⟩≅_
        Setoid.isEquivalence (Bis i) = ≅isEquivalence i

        -- import Relation.Binary.EqReasoning as EqR
        import Relation.Binary.Reasoning.Setoid as EqR

        ≅trans′ : ∀ i (k l m : Lang ∞)
           ( p : k ≅⟨ i ⟩≅ l ) ( q : l ≅⟨ i ⟩≅ m ) → k ≅⟨ i ⟩≅ m
        ≅trans′ i k l m p q = begin
                k ≈⟨ p ⟩
                l ≈⟨ q ⟩
                m ∎ where open EqR (Bis i)

        open import Data.Bool.Properties

        union-assoc : ∀{i} (k {l m} : Lang ∞) → ((k ∪ l) ∪ m ) ≅⟨ i ⟩≅ ( k ∪ (l ∪ m) )
        ≅ν (union-assoc k) = ∨-assoc (ν k) _ _
        ≅δ (union-assoc k) a = union-assoc (δ k a)
        union-comm : ∀{i} (l k : Lang ∞) → (l ∪ k ) ≅⟨ i ⟩≅ ( k ∪ l )
        ≅ν (union-comm l k) = ∨-comm (ν l) _
        ≅δ (union-comm l k) a = union-comm (δ l a) (δ k a)
        union-idem : ∀{i} (l : Lang ∞) → (l ∪ l ) ≅⟨ i ⟩≅ l
        ≅ν (union-idem l) = ∨-idem _
        ≅δ (union-idem l) a = union-idem (δ l a)
        union-emptyl : ∀{i}{l : Lang ∞} → (∅ ∪ l ) ≅⟨ i ⟩≅ l
        ≅ν union-emptyl = refl
        ≅δ union-emptyl a = union-emptyl

        union-cong : ∀{i}{k k′ l l′ : Lang ∞}
             (p : k ≅⟨ i ⟩≅ k′) (q : l ≅⟨ i ⟩≅ l′ ) → ( k ∪ l ) ≅⟨ i ⟩≅ ( k′ ∪ l′ )
        ≅ν (union-cong p q) = cong₂ _∨_ (≅ν p) (≅ν q)
        ≅δ (union-cong p q) a = union-cong (≅δ p a) (≅δ q a)

        withExample : (P : Bool → Set) (p : P true) (q : P false) →
           {A : Set} (g : A → Bool) (x : A) → P (g x)
        withExample P p q g x with g x
        ... | true = p
        ... | false = q

        rewriteExample : {A : Set} {P : A → Set} {x : A} (p : P x)
            {g : A → A} (e : g x ≡ x) → P (g x)
        rewriteExample p e rewrite e = p

        infixr 6 _∪_
        infixr 7 _·_
        infix 5 _≅⟨_⟩≅_

        union-congl : ∀{i}{k k′ l : Lang ∞}
             (p : k ≅⟨ i ⟩≅ k′) → ( k ∪ l ) ≅⟨ i ⟩≅ ( k′ ∪ l )
        union-congl eq = union-cong eq ≅refl

        union-congr : ∀{i}{k l l′ : Lang ∞}
             (p : l ≅⟨ i ⟩≅ l′) → ( k ∪ l ) ≅⟨ i ⟩≅ ( k ∪ l′ )
        union-congr eq = union-cong ≅refl eq

        union-swap24 :   ∀{i} ({x y z w} : Lang ∞)  →  (x ∪ y) ∪ z ∪  w
                                              ≅⟨ i ⟩≅ (x ∪ z) ∪ y ∪ w
        union-swap24 {_} {x} {y} {z} {w} = begin
              (x ∪ y) ∪ z ∪ w
           ≈⟨ union-assoc x ⟩
               x ∪ y ∪ z ∪ w
           ≈⟨ union-congr (≅sym ( union-assoc y)) ⟩
              x ∪ ((y ∪ z) ∪ w)
           ≈⟨ ≅sym ( union-assoc x ) ⟩
              (x ∪ ( y ∪ z)) ∪ w
           ≈⟨ union-congl (union-congr (union-comm y z )) ⟩
              ( x ∪ (z ∪ y)) ∪ w
           ≈⟨  union-congl (≅sym ( union-assoc x )) ⟩
              ((x ∪ z) ∪ y) ∪ w
           ≈⟨ union-assoc (x ∪ z) ⟩
              (x ∪ z) ∪ y ∪ w
           ∎
               where open EqR (Bis _)

        concat-union-distribr : ∀{i} (k {l m} : Lang ∞) → k · ( l ∪ m ) ≅⟨ i ⟩≅ ( k · l ) ∪ ( k · m )
        ≅ν (concat-union-distribr k) =  ∧-distribˡ-∨ (ν k) _ _
        ≅δ (concat-union-distribr k) a with ν k
        ≅δ (concat-union-distribr k {l} {m}) a | true = begin
              δ k a · (l ∪ m) ∪ (δ l a ∪ δ m a)
           ≈⟨ union-congl (concat-union-distribr _) ⟩
              (δ k a · l ∪ δ k a · m) ∪ (δ l a ∪ δ m a)
           ≈⟨ union-swap24 ⟩
              (δ k a · l ∪ δ l a) ∪ (δ k a · m ∪ δ m a)
           ∎
               where open EqR (Bis _)
        ≅δ (concat-union-distribr k) a | false = concat-union-distribr (δ k a)

        concat-union-distribl : ∀{i} (k {l m} : Lang ∞) → ( k ∪ l ) · m ≅⟨ i ⟩≅ ( k · m ) ∪ ( l · m )
        ≅ν (concat-union-distribl k {l} {m}) = ∧-distribʳ-∨ _ (ν k) _
        ≅δ (concat-union-distribl k {l} {m}) a with ν k |  ν l
        ≅δ (concat-union-distribl k {l} {m}) a | false | false = concat-union-distribl (δ k a)
        ≅δ (concat-union-distribl k {l} {m}) a | false | true = begin
              (if false ∨ true then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m)
           ≈⟨ ≅refl ⟩
              ((δ k a ∪ δ l a) · m ) ∪ δ m a
           ≈⟨ union-congl (concat-union-distribl _) ⟩
               (δ k a · m ∪ δ l a · m) ∪ δ m a
           ≈⟨ union-assoc _ ⟩
              (δ k a · m) ∪ ( δ l a · m ∪ δ m a )
           ≈⟨ ≅refl ⟩
              (if false then δ k a · m ∪ δ m a else δ k a · m) ∪ (if true then δ l a · m ∪ δ m a else δ l a · m)
           ∎
               where open EqR (Bis _)
        ≅δ (concat-union-distribl k {l} {m}) a | true | false = begin
               (if true ∨ false then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) ≈⟨ ≅refl ⟩
               ((δ k a ∪ δ l a) · m ) ∪ δ m a ≈⟨ union-congl (concat-union-distribl _) ⟩
               (δ k a · m ∪ δ l a · m) ∪ δ m a ≈⟨  union-assoc _ ⟩
                δ k a · m ∪ ( δ l a · m ∪ δ m a ) ≈⟨  union-congr ( union-comm   _ _) ⟩
                δ k a · m ∪ δ m a ∪ δ l a · m ≈⟨ ≅sym ( union-assoc  _  ) ⟩
               (δ k a · m ∪ δ m a) ∪ δ l a · m ≈⟨ ≅refl ⟩
               ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if false then δ l a · m ∪ δ m a else δ l a · m))
           ∎
               where open EqR (Bis _)
        ≅δ (concat-union-distribl k {l} {m}) a | true | true = begin
               (if true ∨ true then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) ≈⟨ ≅refl ⟩
               (δ k a ∪ δ l a) · m ∪ δ m a ≈⟨ union-congl ( concat-union-distribl _ ) ⟩
               (δ k a · m ∪ δ l a · m) ∪ δ m a ≈⟨  union-assoc _ ⟩
                δ k a · m ∪ ( δ l a · m ∪ δ m a ) ≈⟨ ≅sym ( union-congr ( union-congr (  union-idem _ ) ) ) ⟩
                δ k a · m ∪ ( δ l a · m ∪ (δ m a  ∪ δ m a) ) ≈⟨  ≅sym ( union-congr ( union-assoc _ )) ⟩
                δ k a · m ∪ ( (δ l a · m ∪ δ m a  ) ∪ δ m a ) ≈⟨   union-congr (  union-congl  ( union-comm _  _) )   ⟩
                δ k a · m ∪ ( (δ m a  ∪ δ l a · m ) ∪ δ m a ) ≈⟨  ≅sym ( union-assoc  _  ) ⟩
               ( δ k a · m ∪  (δ m a  ∪ δ l a · m )) ∪ δ m a ≈⟨  ≅sym ( union-congl ( union-assoc _  ) ) ⟩
               ((δ k a · m ∪ δ m a) ∪ δ l a · m) ∪ δ m a ≈⟨  union-assoc _  ⟩
               (δ k a · m ∪ δ m a) ∪ δ l a · m ∪ δ m a ≈⟨ ≅refl ⟩
               ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if true then δ l a · m ∪ δ m a else δ l a · m))
           ∎
               where open EqR (Bis _)

        postulate
                concat-emptyl : ∀{i} l → ∅ · l ≅⟨ i ⟩≅ ∅
                concat-emptyr : ∀{i} l → l · ∅ ≅⟨ i ⟩≅ ∅
                concat-unitl : ∀{i} l → ε · l ≅⟨ i ⟩≅ l
                concat-unitr : ∀{i} l → l · ε ≅⟨ i ⟩≅ l
                star-empty : ∀{i} → ∅ * ≅⟨ i ⟩≅ ε

        concat-congl : ∀{i} {m l k : Lang ∞} → l ≅⟨ i ⟩≅ k → l · m ≅⟨ i ⟩≅ k · m
        ≅ν (concat-congl {i} {m} p ) =  cong (λ x →  x ∧  ( ν m ))  ( ≅ν p )
        ≅δ (concat-congl {i} {m} {l} {k} p ) a with ν k | ν l | ≅ν p
        ≅δ (concat-congl {i} {m} {l} {k} p) a | false | false | refl = concat-congl (≅δ p a)
        ≅δ (concat-congl {i} {m} {l} {k} p) a | true | true | refl = union-congl (concat-congl (≅δ p a))

        concat-congr : ∀{i} {m l k : Lang ∞} → l ≅⟨ i ⟩≅ k → m · l ≅⟨ i ⟩≅ m · k
        ≅ν (concat-congr {i} {m} {_} {k} p ) =  cong (λ x →  ( ν m ) ∧ x )  ( ≅ν p )
        ≅δ (concat-congr {i} {m} {l} {k} p ) a with ν m | ν k | ν l | ≅ν p
        ≅δ (concat-congr {i} {m} {l} {k} p) a | false | x | .x | refl = concat-congr p
        ≅δ (concat-congr {i} {m} {l} {k} p) a | true | x | .x | refl = union-cong (concat-congr p ) ( ≅δ p a )

        concat-assoc : ∀{i} (k {l m} : Lang ∞) → (k · l) · m ≅⟨ i ⟩≅ k · (l · m)
        ≅ν (concat-assoc {i} k {l} {m} ) =  ∧-assoc ( ν k ) ( ν l ) ( ν m )
        ≅δ (concat-assoc {i} k {l} {m} ) a with  ν k
        ≅δ (concat-assoc {i} k {l} {m}) a | false  = concat-assoc _
        ≅δ (concat-assoc {i} k {l} {m}) a | true  with ν l
        ≅δ (concat-assoc {i} k {l} {m}) a | true | false =  begin
             ( if false then (δ k a · l ∪ δ l a) · m ∪ δ m a else (δ k a · l ∪ δ l a) · m )
          ≈⟨ ≅refl  ⟩
            (δ k a · l ∪ δ l a) · m
          ≈⟨ concat-union-distribl _ ⟩
            ((δ k a · l) · m ) ∪ ( δ l a · m )
          ≈⟨ union-congl (concat-assoc _) ⟩
             (δ k a · l · m ) ∪ ( δ l a · m )
          ≈⟨ ≅refl  ⟩
             δ k a · l · m ∪ (if false then δ l a · m ∪ δ m a else δ l a · m)
           ∎ where open EqR (Bis _)
        ≅δ (concat-assoc {i} k {l} {m}) a | true | true = begin
             (if true then (δ k a · l ∪ δ l a) · m ∪ δ m a else (δ k a · l ∪ δ l a) · m)
          ≈⟨ ≅refl  ⟩
             ((( δ k a · l ) ∪ δ l a) · m ) ∪ δ m a
          ≈⟨ union-congl (concat-union-distribl _   ) ⟩
             ((δ k a · l) · m   ∪ ( δ l a · m )) ∪ δ m a
          ≈⟨  union-congl (  union-congl (concat-assoc _))   ⟩
             (( δ k a · l · m ) ∪ ( δ l a · m )) ∪ δ m a
          ≈⟨ union-assoc _ ⟩
             ( δ k a · l · m ) ∪ ( ( δ l a · m ) ∪ δ m a )
          ≈⟨ ≅refl  ⟩
             δ k a · l · m ∪ (if true then δ l a · m ∪ δ m a else δ l a · m)
           ∎ where open EqR (Bis _)

        star-concat-idem : ∀{i} (l : Lang ∞) → l * · l * ≅⟨ i ⟩≅ l *
        ≅ν (star-concat-idem l) = refl
        ≅δ (star-concat-idem l) a = begin
               δ ((l *) · (l *)) a ≈⟨ union-congl (concat-assoc _) ⟩
               δ l a · (l * · l *) ∪ δ l a · l * ≈⟨ union-congl (concat-congr (star-concat-idem _)) ⟩
               δ l a · l * ∪ δ l a · l * ≈⟨ union-idem _ ⟩
               δ (l *) a ∎ where open EqR (Bis _)

        star-idem : ∀{i} (l : Lang ∞) → (l *) * ≅⟨ i ⟩≅ l *
        ≅ν (star-idem l) = refl
        ≅δ (star-idem l) a = begin
                  δ ((l *) *) a  ≈⟨ concat-assoc (δ l a)  ⟩
                  δ l a · ((l *) · ((l *) *)) ≈⟨ concat-congr ( concat-congr (star-idem l )) ⟩
                  δ l a · ((l *) · (l *)) ≈⟨  concat-congr (star-concat-idem l ) ⟩
                  δ l a · l *
                ∎ where open EqR (Bis _)

        postulate
           star-rec : ∀{i} (l : Lang ∞) → l * ≅⟨ i ⟩≅ ε ∪ (l · l *)

        star-from-rec : ∀{i} (k {l m} : Lang ∞)
                → ν k ≡ false
                → l ≅⟨ i ⟩≅ k · l ∪ m
                → l ≅⟨ i ⟩≅ k * · m
        ≅ν (star-from-rec k n p) with ≅ν p
        ... | b rewrite n = b
        ≅δ (star-from-rec k {l} {m} n p) a with ≅δ p a
        ... | q rewrite n = begin
                   (δ l a)
                ≈⟨ q ⟩
                   δ k a · l ∪ δ m a
                ≈⟨ union-congl (concat-congr (star-from-rec k {l} {m} n p))  ⟩
                   (δ k a · (k * · m) ∪ δ m a)
                ≈⟨ union-congl (≅sym (concat-assoc _)) ⟩
                    (δ k a · (k *)) · m ∪ δ m a
                ∎ where open EqR (Bis _)

open List

record DA (S : Set) : Set where
    field ν : (s : S) → Bool
          δ : (s : S)(a : A) → S
    νs : ∀{i} (ss : List.List i S) → Bool
    νs ss = List.any ν ss
    δs : ∀{i} (ss : List.List i S) (a : A) → List.List i S
    δs ss a = List.map (λ s → δ s a) ss

open Lang

lang : ∀{i} {S} (da : DA S) (s : S) → Lang i
Lang.ν (lang da s) = DA.ν da s
Lang.δ (lang da s) a = lang da (DA.δ da s a)

open import Data.Unit hiding ( _≟_ )

open DA

∅A : DA ⊤
ν ∅A s = false
δ ∅A s a = s

εA : DA Bool
ν εA b  = b
δ εA b a = false

open import Relation.Nullary.Decidable

data 3States : Set where
   init acc err : 3States

charA : (a : A) → DA 3States
ν (charA a) init = false
ν (charA a) acc = true
ν (charA a) err = false
δ (charA a) init x =
  if ⌊ a ≟  x ⌋ then acc else err
δ (charA a) acc x = err
δ (charA a) err x = err

complA : ∀{S} (da : DA S) → DA S
ν (complA da) s = not (ν da s)
δ (complA da) s a = δ da s a

open import Data.Product

_⊕_ : ∀{S1 S2} (da1 : DA S1) (da2 : DA S2) → DA (S1 × S2)
ν (da1 ⊕ da2) (s1 , s2) = ν da1 s1 ∨ ν da2 s2
δ (da1 ⊕ da2) (s1 , s2) a = δ da1 s1 a , δ da2 s2 a

powA : ∀{S} (da : DA S) → DA (List ∞ S)
ν (powA da) ss = νs da ss
δ (powA da) ss a = δs da ss a

open _≅⟨_⟩≅_

powA-nil : ∀{i S} (da : DA S) → lang (powA da) [] ≅⟨ i ⟩≅ ∅
≅ν (powA-nil da) = refl
≅δ (powA-nil da) a = powA-nil da

powA-cons : ∀{i S} (da : DA S) {s : S} {ss : List ∞ S} →
        lang (powA da) (s ∷ ss) ≅⟨ i ⟩≅ lang da s ∪ lang (powA da) ss
≅ν (powA-cons da) = refl
≅δ (powA-cons da) a = powA-cons da

composeA : ∀{S1 S2} (da1 : DA S1)(s2 : S2)(da2 : DA S2) → DA (S1 × List ∞ S2)
ν (composeA da1 s2 da2) (s1 , ss2) = (ν da1 s1 ∧ ν da2 s2) ∨ νs da2 ss2
δ (composeA da1 s2 da2) (s1 , ss2) a =
        δ da1 s1 a , δs da2 (if ν da1 s1 then s2 ∷ ss2 else ss2) a

-- import Relation.Binary.EqReasoning as EqR
import Relation.Binary.Reasoning.Setoid as EqR

composeA-gen : ∀{i S1 S2} (da1 : DA S1) (da2 : DA S2) → ∀(s1 : S1)(s2 : S2)(ss : List ∞ S2) →
        lang (composeA da1 s2 da2) (s1 , ss) ≅⟨ i ⟩≅ lang da1 s1 · lang da2 s2 ∪ lang (powA da2) ss
≅ν (composeA-gen da1 da2 s1 s2 ss) = refl
≅δ (composeA-gen da1 da2 s1 s2 ss) a with ν da1 s1
... | false = composeA-gen da1 da2 (δ da1 s1 a) s2 (δs da2 ss a)
... | true = begin
       lang (composeA da1 s2 da2) (δ da1 s1 a , δ da2 s2 a ∷ δs da2 ss a)
   ≈⟨ composeA-gen da1 da2 (δ da1 s1 a) s2 (δs da2 (s2 ∷ ss) a) ⟩
       lang da1 (δ da1 s1 a) · lang da2 s2 ∪ lang (powA da2) (δs da2 (s2 ∷ ss) a)
   ≈⟨ union-congr (powA-cons da2)  ⟩
       lang da1 (δ da1 s1 a) · lang da2 s2 ∪
          (lang da2 (δ da2 s2 a) ∪ lang (powA da2) (δs da2 ss a))
   ≈⟨ ≅sym  (union-assoc _)  ⟩
       (lang da1 (δ da1 s1 a) · lang da2 s2 ∪ lang da2 (δ da2 s2 a)) ∪ lang (powA da2) (δs da2 ss a)
   ∎ where open EqR (Bis _)

postulate
  composeA-correct : ∀{i S1 S2} (da1 : DA S1) (da2 : DA S2) s1 s2 →
     lang (composeA da1 s2 da2) (s1 , []) ≅⟨ i ⟩≅ lang da1 s1 · lang da2 s2

open import Data.Maybe

acceptingInitial : ∀{S} (s0 : S) (da : DA S) → DA (Maybe S)
ν (acceptingInitial s0 da) (just s) = ν da s
δ (acceptingInitial s0 da) (just s) a = just (δ da s a)
ν (acceptingInitial s0 da) nothing = true
δ (acceptingInitial s0 da) nothing a = just (δ da s0 a)

finalToInitial : ∀{S} (da : DA (Maybe S)) → DA (List ∞ (Maybe S))
ν (finalToInitial da) ss = νs da ss
δ (finalToInitial da) ss a =
        let ss′ = δs da ss a
        in if νs da ss then δ da nothing a ∷ ss′ else ss′

starA : ∀{S}(s0 : S)(da : DA S) → DA (List ∞(Maybe S))
starA s0 da = finalToInitial (acceptingInitial s0 da)

postulate
 acceptingInitial-just : ∀{i S} (s0 : S) (da : DA S) {s : S} →
   lang (acceptingInitial s0 da) (just s) ≅⟨ i ⟩≅ lang da s
 acceptingInitial-nothing : ∀{i S} (s0 : S) (da : DA S) →
        lang (acceptingInitial s0 da) nothing ≅⟨ i ⟩≅ ε ∪ lang da s0
 starA-lemma : ∀{i S}(da : DA S)(s0 : S)(ss : List ∞ (Maybe S))→
        lang (starA s0 da) ss ≅⟨ i ⟩≅
                lang (powA (acceptingInitial s0 da)) ss · (lang da s0) *
 starA-correct : ∀{i S} (da : DA S) (s0 : S) →
   lang (starA s0 da) (nothing ∷ []) ≅⟨ i ⟩≅ (lang da s0) *

record NAutomaton ( Q : Set ) ( Σ : Set  )
           : Set  where
        field
              Nδ : Q → Σ → Q → Bool
              Nstart : Q → Bool
              Nend  :  Q → Bool

postulate
   exists : { S : Set} → ( S → Bool ) → Bool

nlang : ∀{i} {S} (nfa : NAutomaton S A ) (s : S → Bool ) → Lang i
Lang.ν (nlang nfa s) = exists ( λ x → (s x ∧ NAutomaton.Nend nfa x ))
Lang.δ (nlang nfa s) a = nlang nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x)

nlang1 : ∀{i} {S} (nfa : NAutomaton S A ) (s : S → Bool ) → Lang i
Lang.ν (nlang1 nfa s) = NAutomaton.Nend nfa  {!!}
Lang.δ (nlang1 nfa s) a = nlang1 nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x)

-- nlang' : ∀{i} {S} (nfa : DA (S → Bool) ) (s : S → Bool ) → Lang i
-- Lang.ν (nlang' nfa s) = DA.ν nfa  s
-- Lang.δ (nlang' nfa s) a = nlang' nfa (DA.δ nfa s a)

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
-- {-# OPTIONS -v tc.cover.cover:10 -v tc.cover.strategy:20 -v tc.cover.splittree:100 #-}
-- Andreas, 2013-05-15 Reported by jesper.cockx
module Issue849 where

data Bool : Set where
  true false : Bool

¬ : Bool → Bool
¬ true = false
¬ false = true

data D : Bool → Set where
  d1 : (x : Bool) → D x
  d2 : (x : Bool) → D (¬ x)

data ⊥ : Set where

data Test : (x : Bool) → (y : D x) → Set where
  c1 : (x : Bool)   → Test x (d1 x)
  c2 : (y : D true) → Test true y

-- WAS: The following function passes the coverage checker
-- even though the case for "f false (d2 true)" is not covered.
f : (x : Bool) → (y : D x) → Test x y
f x      (d1 .x) = c1 x
f true   y       = c2 y

impossible : Test false (d2 true) → ⊥
impossible ()

error : ⊥
error = impossible (f false (d2 true))

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.ZCohomology.Groups.Wedge where

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.MayerVietorisUnreduced
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.HITs.Wedge
open import Cubical.HITs.SetTruncation renaming (elim to sElim ; elim2 to sElim2)
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec ; ∣_∣ to ∣_∣₁)
open import Cubical.Data.Nat
open import Cubical.Data.Prod
open import Cubical.Data.Unit
open import Cubical.Algebra.Group

open import Cubical.ZCohomology.Groups.Unit
open import Cubical.ZCohomology.Groups.Sn

open import Cubical.HITs.Pushout

--- This module contains a proof that Hⁿ(A ⋁ B) ≅ Hⁿ(A) × Hⁿ(B), n ≥ 1

module _ {ℓ ℓ'} (A : Pointed ℓ) (B : Pointed ℓ') where
  module I = MV (typ A) (typ B) Unit (λ _ → pt A) (λ _ → pt B)

  Hⁿ-⋁ : (n : ℕ) → GroupEquiv (coHomGr (suc n) (A ⋁ B)) (×coHomGr (suc n) (typ A) (typ B))
  Hⁿ-⋁ zero =
    BijectionIsoToGroupEquiv
      (bij-iso
        (grouphom
          (GroupHom.fun (I.i 1))
          (sElim2 (λ _ _ → isOfHLevelPath 2 (isOfHLevelΣ 2 setTruncIsSet λ _ → setTruncIsSet) _ _)
                  λ a b → GroupHom.isHom (I.i 1) ∣ a ∣₂ ∣ b ∣₂))
        (sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                λ f inker → helper ∣ f ∣₂ (I.Ker-i⊂Im-d 0 ∣ f ∣₂ inker))
        (sigmaElim (λ _ → isOfHLevelSuc 1 propTruncIsProp)
                   λ f g → I.Ker-Δ⊂Im-i 1 (∣ f ∣₂ , g) (isOfHLevelSuc 0 (isContrHⁿ-Unit 0) _ _)))
    where
    surj-helper : (x : coHom 0 Unit)
            → isInIm _ _ (I.Δ 0) x
    surj-helper =
      sElim (λ _ → isOfHLevelSuc 1 propTruncIsProp)
            λ f → ∣ (∣ (λ _ → f tt) ∣₂ , 0ₕ) , cong ∣_∣₂ (funExt (λ _ → cong ((f tt) +ₖ_) -0ₖ ∙ rUnitₖ (f tt))) ∣₁

    helper : (x : coHom 1 (A ⋁ B)) → isInIm _ _ (I.d 0) x
                  → x ≡ 0ₕ
    helper x inim =
      pRec (setTruncIsSet _ _)
           (λ p → sym (snd p) ∙
                       MV.Im-Δ⊂Ker-d _ _ Unit (λ _ → pt A) (λ _ → pt B) 0 (fst p) (surj-helper (fst p)))
             inim
  Hⁿ-⋁ (suc n) =
    vSES→GroupEquiv _ _
      (ses (isOfHLevelSuc 0 (isContrHⁿ-Unit n))
           (isOfHLevelSuc 0 (isContrHⁿ-Unit (suc n)))
           (I.d (suc n))
           (I.Δ (suc (suc n)))
           (I.i (suc (suc n)))
           (I.Ker-i⊂Im-d (suc n))
           (I.Ker-Δ⊂Im-i (suc (suc n))))

  open import Cubical.Foundations.Isomorphism
  wedgeConnected : ((x : typ A) → ∥ pt A ≡ x ∥) → ((x : typ B) → ∥ pt B ≡ x ∥) → (x : A ⋁ B) → ∥ (inl (pt A)) ≡ x ∥
  wedgeConnected conA conB =
    PushoutToProp (λ _ → propTruncIsProp)
                  (λ a → pRec propTruncIsProp (λ p → ∣ cong inl p ∣₁) (conA a))
                  λ b → pRec propTruncIsProp (λ p → ∣ push tt ∙ cong inr p ∣₁) (conB b)

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


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

module Properties.FunctionTypes where

open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
open import Luau.FunctionTypes using (srcⁿ; src; tgt)
open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_)
open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; skalar)
open import Properties.Contradiction using (CONTRADICTION; ¬; ⊥)
open import Properties.Functions using (_∘_)
open import Properties.Subtyping using (<:-refl; ≮:-refl; <:-trans-≮:; skalar-scalar; <:-impl-⊇; skalar-function-ok; language-comp)
open import Properties.TypeNormalization using (FunType; Normal; never; unknown; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:)

-- Properties of src
function-err-srcⁿ : ∀ {T t} → (FunType T) → (¬Language (srcⁿ T) t) → Language T (function-err t)
function-err-srcⁿ (S ⇒ T) p = function-err p
function-err-srcⁿ (S ∩ T) (p₁ , p₂) = (function-err-srcⁿ S p₁ , function-err-srcⁿ T p₂)

¬function-err-srcᶠ : ∀ {T t} → (FunType T) → (Language (srcⁿ T) t) → ¬Language T (function-err t)
¬function-err-srcᶠ (S ⇒ T) p = function-err p
¬function-err-srcᶠ (S ∩ T) (left p) = left (¬function-err-srcᶠ S p)
¬function-err-srcᶠ (S ∩ T) (right p) = right (¬function-err-srcᶠ T p)

¬function-err-srcⁿ : ∀ {T t} → (Normal T) → (Language (srcⁿ T) t) → ¬Language T (function-err t)
¬function-err-srcⁿ never p = never
¬function-err-srcⁿ unknown (scalar ())
¬function-err-srcⁿ (S ⇒ T) p = function-err p
¬function-err-srcⁿ (S ∩ T) (left p) = left (¬function-err-srcᶠ S p)
¬function-err-srcⁿ (S ∩ T) (right p) = right (¬function-err-srcᶠ T p)
¬function-err-srcⁿ (S ∪ T) (scalar ())

¬function-err-src : ∀ {T t} → (Language (src T) t) → ¬Language T (function-err t)
¬function-err-src {T = S ⇒ T} p = function-err p
¬function-err-src {T = nil} p = scalar-function-err nil
¬function-err-src {T = never} p = never
¬function-err-src {T = unknown} (scalar ())
¬function-err-src {T = boolean} p = scalar-function-err boolean
¬function-err-src {T = number} p = scalar-function-err number
¬function-err-src {T = string} p = scalar-function-err string
¬function-err-src {T = S ∪ T} p = <:-impl-⊇ (<:-normalize (S ∪ T)) _ (¬function-err-srcⁿ (normal (S ∪ T)) p)
¬function-err-src {T = S ∩ T} p = <:-impl-⊇ (<:-normalize (S ∩ T)) _ (¬function-err-srcⁿ (normal (S ∩ T)) p)

src-¬function-errᶠ : ∀ {T t} → (FunType T) → Language T (function-err t) → (¬Language (srcⁿ T) t)
src-¬function-errᶠ (S ⇒ T) (function-err p) = p
src-¬function-errᶠ (S ∩ T) (p₁ , p₂) = (src-¬function-errᶠ S p₁ , src-¬function-errᶠ T p₂)

src-¬function-errⁿ : ∀ {T t} → (Normal T) → Language T (function-err t) → (¬Language (srcⁿ T) t)
src-¬function-errⁿ unknown p = never
src-¬function-errⁿ (S ⇒ T) (function-err p) = p
src-¬function-errⁿ (S ∩ T) (p₁ , p₂) = (src-¬function-errᶠ S p₁ , src-¬function-errᶠ T p₂)
src-¬function-errⁿ (S ∪ T) p = never

src-¬function-err : ∀ {T t} → Language T (function-err t) → (¬Language (src T) t)
src-¬function-err {T = S ⇒ T} (function-err p) = p
src-¬function-err {T = unknown} p = never
src-¬function-err {T = S ∪ T} p = src-¬function-errⁿ (normal (S ∪ T)) (<:-normalize (S ∪ T) _ p)
src-¬function-err {T = S ∩ T} p = src-¬function-errⁿ (normal (S ∩ T)) (<:-normalize (S ∩ T) _ p)

fun-¬scalar : ∀ {S T} (s : Scalar S) → FunType T → ¬Language T (scalar s)
fun-¬scalar s (S ⇒ T) = function-scalar s
fun-¬scalar s (S ∩ T) = left (fun-¬scalar s S)

¬fun-scalar : ∀ {S T t} (s : Scalar S) → FunType T → Language T t → ¬Language S t
¬fun-scalar s (S ⇒ T) function = scalar-function s
¬fun-scalar s (S ⇒ T) (function-ok p) = scalar-function-ok s
¬fun-scalar s (S ⇒ T) (function-err p) = scalar-function-err s
¬fun-scalar s (S ∩ T) (p₁ , p₂) = ¬fun-scalar s T p₂

fun-function : ∀ {T} → FunType T → Language T function
fun-function (S ⇒ T) = function
fun-function (S ∩ T) = (fun-function S , fun-function T)

srcⁿ-¬scalar : ∀ {S T t} (s : Scalar S) → Normal T → Language T (scalar s) → (¬Language (srcⁿ T) t)
srcⁿ-¬scalar s never (scalar ())
srcⁿ-¬scalar s unknown p = never
srcⁿ-¬scalar s (S ⇒ T) (scalar ())
srcⁿ-¬scalar s (S ∩ T) (p₁ , p₂) = CONTRADICTION (language-comp (scalar s) (fun-¬scalar s S) p₁)
srcⁿ-¬scalar s (S ∪ T) p = never

src-¬scalar : ∀ {S T t} (s : Scalar S) → Language T (scalar s) → (¬Language (src T) t)
src-¬scalar {T = nil} s p = never
src-¬scalar {T = T ⇒ U} s (scalar ())
src-¬scalar {T = never} s (scalar ())
src-¬scalar {T = unknown} s p = never
src-¬scalar {T = boolean} s p = never
src-¬scalar {T = number} s p = never
src-¬scalar {T = string} s p = never
src-¬scalar {T = T ∪ U} s p = srcⁿ-¬scalar s (normal (T ∪ U)) (<:-normalize (T ∪ U) (scalar s) p)
src-¬scalar {T = T ∩ U} s p = srcⁿ-¬scalar s (normal (T ∩ U)) (<:-normalize (T ∩ U) (scalar s) p)

srcⁿ-unknown-≮: : ∀ {T U} → (Normal U) → (T ≮: srcⁿ U) → (U ≮: (T ⇒ unknown))
srcⁿ-unknown-≮: never (witness t p q) = CONTRADICTION (language-comp t q unknown)
srcⁿ-unknown-≮: unknown (witness t p q) = witness (function-err t) unknown (function-err p)
srcⁿ-unknown-≮: (U ⇒ V) (witness t p q) = witness (function-err t) (function-err q) (function-err p)
srcⁿ-unknown-≮: (U ∩ V) (witness t p q) = witness (function-err t) (function-err-srcⁿ (U ∩ V) q) (function-err p)
srcⁿ-unknown-≮: (U ∪ V) (witness t p q) = witness (scalar V) (right (scalar V)) (function-scalar V)

src-unknown-≮: : ∀ {T U} → (T ≮: src U) → (U ≮: (T ⇒ unknown))
src-unknown-≮: {U = nil} (witness t p q) = witness (scalar nil) (scalar nil) (function-scalar nil)
src-unknown-≮: {U = T ⇒ U} (witness t p q) = witness (function-err t) (function-err q) (function-err p)
src-unknown-≮: {U = never} (witness t p q) = CONTRADICTION (language-comp t q unknown)
src-unknown-≮: {U = unknown} (witness t p q) = witness (function-err t) unknown (function-err p)
src-unknown-≮: {U = boolean} (witness t p q) = witness (scalar boolean) (scalar boolean) (function-scalar boolean)
src-unknown-≮: {U = number} (witness t p q) = witness (scalar number) (scalar number) (function-scalar number)
src-unknown-≮: {U = string} (witness t p q) = witness (scalar string) (scalar string) (function-scalar string)
src-unknown-≮: {U = T ∪ U} p = <:-trans-≮: (normalize-<: (T ∪ U)) (srcⁿ-unknown-≮: (normal (T ∪ U)) p)
src-unknown-≮: {U = T ∩ U} p = <:-trans-≮: (normalize-<: (T ∩ U)) (srcⁿ-unknown-≮: (normal (T ∩ U)) p)

unknown-src-≮: : ∀ {S T U} → (U ≮: S) → (T ≮: (U ⇒ unknown)) → (U ≮: src T)
unknown-src-≮: (witness t x x₁) (witness (scalar s) p (function-scalar s)) = witness t x (src-¬scalar s p)
unknown-src-≮: r (witness (function-ok (scalar s)) p (function-ok (scalar-scalar s () q)))
unknown-src-≮: r (witness (function-ok (function-ok _)) p (function-ok (scalar-function-ok ())))
unknown-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p)

-- Properties of tgt
tgt-function-ok : ∀ {T t} → (Language (tgt T) t) → Language T (function-ok t)
tgt-function-ok {T = nil} (scalar ())
tgt-function-ok {T = T₁ ⇒ T₂} p = function-ok p
tgt-function-ok {T = never} (scalar ())
tgt-function-ok {T = unknown} p = unknown
tgt-function-ok {T = boolean} (scalar ())
tgt-function-ok {T = number} (scalar ())
tgt-function-ok {T = string} (scalar ())
tgt-function-ok {T = T₁ ∪ T₂} (left p) = left (tgt-function-ok p)
tgt-function-ok {T = T₁ ∪ T₂} (right p) = right (tgt-function-ok p)
tgt-function-ok {T = T₁ ∩ T₂} (p₁ , p₂) = (tgt-function-ok p₁ , tgt-function-ok p₂)

function-ok-tgt : ∀ {T t} → Language T (function-ok t) → (Language (tgt T) t)
function-ok-tgt (function-ok p) = p
function-ok-tgt (left p) = left (function-ok-tgt p)
function-ok-tgt (right p) = right (function-ok-tgt p)
function-ok-tgt (p₁ , p₂) = (function-ok-tgt p₁ , function-ok-tgt p₂)
function-ok-tgt unknown = unknown

tgt-never-≮: : ∀ {T U} → (tgt T ≮: U) → (T ≮: (skalar ∪ (never ⇒ U)))
tgt-never-≮: (witness t p q) = witness (function-ok t) (tgt-function-ok p) (skalar-function-ok , function-ok q)

never-tgt-≮: : ∀ {T U} → (T ≮: (skalar ∪ (never ⇒ U))) → (tgt T ≮: U)
never-tgt-≮: (witness (scalar s) p (q₁ , q₂)) = CONTRADICTION (≮:-refl (witness (scalar s) (skalar-scalar s) q₁))
never-tgt-≮: (witness function p (q₁ , scalar-function ()))
never-tgt-≮: (witness (function-ok t) p (q₁ , function-ok q₂)) = witness t (function-ok-tgt p) q₂
never-tgt-≮: (witness (function-err (scalar s)) p (q₁ , function-err (scalar ())))

src-tgtᶠ-<: : ∀ {T U V} → (FunType T) → (U <: src T) → (tgt T <: V) → (T <: (U ⇒ V))
src-tgtᶠ-<: T p q (scalar s) r = CONTRADICTION (language-comp (scalar s) (fun-¬scalar s T) r)
src-tgtᶠ-<: T p q function r = function
src-tgtᶠ-<: T p q (function-ok s) r = function-ok (q s (function-ok-tgt r))
src-tgtᶠ-<: T p q (function-err s) r = function-err (<:-impl-⊇ p s (src-¬function-err r))

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: TheGreatSageEqualToHeaven/luau

max_forks_repo_name: TheGreatSageEqualToHeaven/luau


text:
{-# OPTIONS --universe-polymorphism #-}

-- Proof that 'Free' is a functor
module Categories.Free.Functor where

open import Categories.Support.PropositionalEquality

open import Categories.Categories
open import Categories.Category
  renaming (_[_∼_] to _[_~C_])
open import Categories.Free.Core
open import Categories.Functor
  using (Functor)
  renaming (_≡_ to _≡F_; _∘_ to _∘F_)
open import Categories.Graphs
open import Data.Product
open import Graphs.Graph
  renaming (_[_~_] to _[_~G_]; module Heterogeneous to HeterogeneousG)
open import Graphs.GraphMorphism
  renaming (_∘_ to _∘G_)
open import Data.Star
open import Data.Star.Properties
  using (gmap-◅◅; gmap-id)
open import Categories.Support.StarEquality
open import Level using (_⊔_)

ε∼ε : ∀{o₁ ℓ₁ e₁}{X : Graph o₁ ℓ₁ e₁}
       {o₂ ℓ₂ e₂}{Y : Graph o₂ ℓ₂ e₂}
  → (F G : GraphMorphism X Y)
  → F ≈ G
  → {x : Graph.Obj X}
  → Free₀ Y [ ε {x = GraphMorphism.F₀ F x} ~C ε {x = GraphMorphism.F₀ G x} ]
ε∼ε {Y = Y} F G (F≈G₀ , F≈G₁) {x} = ≣-subst (λ z → Free₀ Y [ ε {x = GraphMorphism.F₀ F x} ~C ε {x = z} ]) (F≈G₀ x) (Heterogeneous.refl (Free₀ Y))
-- the below should probably work, but there's an agda bug
-- XXX bug id?  mokus?  anybody?  bueller?
{-
ε∼ε {Y = Y} F G F≈G {x} rewrite proj₁ F≈G x = refl
  where open Heterogeneous (Free₀ Y)
-}

_◅~◅_ :
  ∀ {o ℓ e}{G : Graph o ℓ e}
    {a₀ a₁ b₀ b₁ c₀ c₁ : Graph.Obj G}
    {f  :       G [ a₀ ↝ b₀ ]}
    {g  :       G [ a₁ ↝ b₁ ]}
    {fs : Free₀ G [ b₀ , c₀ ]}
    {gs : Free₀ G [ b₁ , c₁ ]}
  →       G [ f  ~G g  ]
  → Free₀ G [ fs ~C gs ]
  → Free₀ G [ (f ◅ fs) ~C (g ◅ gs) ]
_◅~◅_ {G = G} (HeterogeneousG.≈⇒~ hd) (Heterogeneous.≡⇒∼ tl)
  = ≡⇒∼ (hd ◅-cong tl)
  where
    open Heterogeneous (Free₀ G)
    open PathEquality G

Free : ∀ {o ℓ e} → Functor (Graphs o ℓ e) (Categories o (o ⊔ ℓ) (o ⊔ ℓ ⊔ e))
Free {o}{ℓ}{e} = record
  { F₀            = Free₀
  ; F₁            = Free₁
  ; identity      = λ {A} f → Heterogeneous.reflexive (Free₀ A) (gmap-id f)
  ; homomorphism  = λ {X}{Y}{Z}{f}{g} → homomorphism {X}{Y}{Z}{f}{g}
  ; F-resp-≡      = λ {X}{Y}{F G : GraphMorphism X Y} → Free₁-resp-≡ {X}{Y}{F}{G}
  }
  where
    module Graphs     = Category (Graphs o ℓ e)
    module Categories = Category (Categories o (o ⊔ ℓ) (o ⊔ ℓ ⊔ e))

    .homomorphism : ∀ {X Y Z} {f : GraphMorphism X Y} {g : GraphMorphism Y Z}
                  → Free₁ (g ∘G f) ≡F (Free₁ g ∘F Free₁ f)
    homomorphism ε = Heterogeneous.refl _
    homomorphism {X}{Y}{Z}{f}{g}{S}{U} (_◅_ {.S}{T}{.U} h hs) =
      HeterogeneousG.refl Z ◅~◅ homomorphism {X}{Y}{Z}{f}{g}{T}{U} hs

    .Free₁-resp-≡ : ∀ {X Y} {F G : GraphMorphism X Y}
      → F ≈ G
      → Free₁ F ≡F Free₁ G
    Free₁-resp-≡ {X}{Y}{F}{G} F≈G {S}{.S} ε = ε∼ε F G F≈G
    Free₁-resp-≡ {X}{Y}{F}{G} F≈G {S}{U} (_◅_ {.S}{T}{.U} h hs)
      = proj₂ F≈G h ◅~◅ Free₁-resp-≡ {X}{Y}{F}{G} F≈G {T}{U} hs

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

open import HoTT
open import homotopy.LoopSpaceCircle
open import homotopy.PinSn

module homotopy.SphereEndomorphism where

  Sphere-endo : ∀ n → Type₀
  Sphere-endo n = Sphere n → Sphere n

  ⊙Sphere-endo : ∀ n → Type₀
  ⊙Sphere-endo n = ⊙Sphere n ⊙→ ⊙Sphere n

{-
  ⊙LiftSphere-endo : ∀ {i} n → Type i
  ⊙LiftSphere-endo {i} n = ⊙Lift {j = i} (⊙Sphere n) ⊙→ ⊙Lift {j = i} (⊙Sphere n)
-}

  Trunc-Sphere-endo : ∀ n → Type₀
  Trunc-Sphere-endo = Trunc 0 ∘ Sphere-endo

  Trunc-⊙Sphere-endo : ∀ n → Type₀
  Trunc-⊙Sphere-endo = Trunc 0 ∘ ⊙Sphere-endo

{-
  Trunc-⊙LiftSphere-endo : ∀ {i} n → Type i
  Trunc-⊙LiftSphere-endo {i} = Trunc 0 ∘ ⊙LiftSphere-endo {i}
-}

  {- Part 0: pointedness is free -}

  Trunc-⊙Sphere-endo-out : ∀ n
    → Trunc-⊙Sphere-endo n → Trunc-Sphere-endo n
  Trunc-⊙Sphere-endo-out n = Trunc-fmap fst

  -- For [S¹], the pointedness is free because of the commutativity of its loop space.

  -- favonia: maybe one can simplify the proofs through
  --          an intermediate type [Σ S¹ (λ x → x == x)]?

  private
    ⊙S¹-endo-in' : (base* : S¹) (loop* : base* == base*) → (⊙S¹ ⊙→ ⊙S¹)
    ⊙S¹-endo-in' = S¹-elim
      (λ loop* → S¹-rec base loop* , idp)
      (↓-app→cst-in λ r → ap (λ loop* → (S¹-rec base loop* , idp)) (lemma₀ r)) where
      abstract
        lemma₀ : ∀ {loop₁ loop₂}
          → loop₁ == loop₂ [ (λ x → x == x) ↓ loop ]
          → loop₁ == loop₂
        lemma₀ {loop₁} {loop₂} p = anti-whisker-right loop $
          loop₁ ∙ loop
            =⟨ ↓-idf=idf-out' p ⟩
          loop ∙' loop₂
            =⟨ ∙'=∙ loop loop₂ ⟩
          loop ∙ loop₂
            =⟨ ΩS¹-is-abelian loop loop₂ ⟩
          loop₂ ∙ loop
            =∎

    ⊙S¹-endo-in : (S¹ → S¹) → (⊙S¹ ⊙→ ⊙S¹)
    ⊙S¹-endo-in f = ⊙S¹-endo-in' (f base) (ap f loop)

  Trunc-⊙S¹-endo-in : Trunc 0 (S¹ → S¹) → Trunc 0 (⊙S¹ ⊙→ ⊙S¹)
  Trunc-⊙S¹-endo-in = Trunc-fmap ⊙S¹-endo-in

  abstract
    Trunc-⊙S¹-endo-in-η : ∀ f → Trunc-⊙S¹-endo-in (Trunc-⊙Sphere-endo-out 1 f) == f
    Trunc-⊙S¹-endo-in-η = Trunc-elim
      λ{(f , pt) → ap [_] $
        ⊙S¹-endo-in'-shifted pt (ap f loop) ∙ ⊙λ= (S¹-rec-η f , idp)}
      where
      -- free one end to apply identification elimination
      ⊙S¹-endo-in'-shifted : {base* : S¹}
        (shift : base* == base) (loop* : base* == base*)
        → ⊙S¹-endo-in' base* loop* == (S¹-rec base* loop* , shift)
      ⊙S¹-endo-in'-shifted idp _ = idp

    Trunc-⊙S¹-endo-out-β : ∀ f → Trunc-⊙Sphere-endo-out 1 (Trunc-⊙S¹-endo-in f) == f
    Trunc-⊙S¹-endo-out-β = Trunc-elim
      λ f → ! (ap (λ f → [ fst (⊙S¹-endo-in f) ]) (λ= $ S¹-rec-η f))
          ∙ ⊙S¹-endo-out-β (f base) (ap f loop)
          ∙ ap [_] (λ= $ S¹-rec-η f)
      where
        -- free [base*] to apply circle elimination
        ⊙S¹-endo-out-β : (base* : S¹) (loop* : base* == base*)
          →  [ fst (⊙S¹-endo-in (S¹-rec base* loop*)) ]
          == [ S¹-rec base* loop* ] :> Trunc 0 (S¹ → S¹)
        ⊙S¹-endo-out-β = S¹-elim
          (λ loop* → ap (λ loop* → [ S¹-rec base loop* ]) (S¹Rec.loop-β base loop*))
          prop-has-all-paths-↓

  Trunc-⊙S¹-endo-out-is-equiv : is-equiv (Trunc-⊙Sphere-endo-out 1)
  Trunc-⊙S¹-endo-out-is-equiv = is-eq _ Trunc-⊙S¹-endo-in Trunc-⊙S¹-endo-out-β Trunc-⊙S¹-endo-in-η

  -- For [Sphere (S (S n))], the pointedness is free because of its connectivity.

  private
    SphereSS-conn : ∀ n → is-connected 1 (Sphere (S (S n)))
    SphereSS-conn n = connected-≤T (≤T-+2+-l 1 (-2≤T ⟨ n ⟩₋₂))

    SphereSS-conn-path : ∀ n (x y : Sphere (S (S n))) → is-connected 0 (x == y)
    SphereSS-conn-path n x y = path-conn (SphereSS-conn n)

    SphereSS-has-all-trunc-paths : ∀ n (x y : Sphere (S (S n))) → Trunc 0 (x == y)
    SphereSS-has-all-trunc-paths n x y = –> (Trunc=-equiv [ x ] [ y ])
      (contr-has-all-paths {{SphereSS-conn n}} [ x ] [ y ])

  Trunc-⊙SphereSS-endo-in : ∀ n
    → Trunc-Sphere-endo (S (S n)) → Trunc-⊙Sphere-endo (S (S n))
  Trunc-⊙SphereSS-endo-in n = Trunc-rec λ f →
    Trunc-rec (λ pt → [ f , pt ])
      (SphereSS-has-all-trunc-paths n (f north) north)

  abstract
    Trunc-⊙SphereSS-endo-in-η : ∀ n f → Trunc-⊙SphereSS-endo-in n (Trunc-⊙Sphere-endo-out (S (S n)) f) == f
    Trunc-⊙SphereSS-endo-in-η n = Trunc-elim
      λ{(f , pt) → ap (Trunc-rec (λ pt → [ f , pt ]))
        (contr-has-all-paths {{SphereSS-conn-path n (f north) north}}
          (SphereSS-has-all-trunc-paths n (f north) north) [ pt ])}

    Trunc-⊙SphereSS-endo-out-β : ∀ n f → Trunc-⊙Sphere-endo-out (S (S n)) (Trunc-⊙SphereSS-endo-in n f) == f
    Trunc-⊙SphereSS-endo-out-β n = Trunc-elim
      λ f → Trunc-elim
        {P = λ pt → Trunc-⊙Sphere-endo-out (S (S n)) (Trunc-rec (λ pt → [ f , pt ]) pt) == [ f ]}
        (λ pt → idp) (SphereSS-has-all-trunc-paths n (f north) north)

  Trunc-⊙SphereSS-endo-out-is-equiv : ∀ n → is-equiv (Trunc-⊙Sphere-endo-out (S (S n)))
  Trunc-⊙SphereSS-endo-out-is-equiv n = is-eq
    (Trunc-⊙Sphere-endo-out (S (S n))) (Trunc-⊙SphereSS-endo-in n)
    (Trunc-⊙SphereSS-endo-out-β n) (Trunc-⊙SphereSS-endo-in-η n)

  -- the unified interface

  Trunc-⊙SphereS-endo-out-is-equiv : ∀ n → is-equiv (Trunc-⊙Sphere-endo-out (S n))
  Trunc-⊙SphereS-endo-out-is-equiv 0 = Trunc-⊙S¹-endo-out-is-equiv
  Trunc-⊙SphereS-endo-out-is-equiv (S n) = Trunc-⊙SphereSS-endo-out-is-equiv n

  Trunc-⊙SphereS-endo-in : ∀ n
    → Trunc-Sphere-endo (S n) → Trunc-⊙Sphere-endo (S n)
  Trunc-⊙SphereS-endo-in n = is-equiv.g (Trunc-⊙SphereS-endo-out-is-equiv n)

  {- Part 1: suspension is an isomorphism -}

  private
    open import homotopy.Freudenthal

    SSSSk≤SSk+2+SSk : ∀ k → S (S (S (S k))) ≤T S (S k) +2+ S (S k)
    SSSSk≤SSk+2+SSk k = ≤T-+2+-l 0 $ ≤T-+2+-r (S (S k)) $ -2≤T k

    SSn≤n+2+n : ∀ n → S (S ⟨ n ⟩) ≤T ⟨ n ⟩ +2+ ⟨ n ⟩
    SSn≤n+2+n n = SSSSk≤SSk+2+SSk ⟨ n ⟩₋₂

    module F n = FreudenthalEquiv
      ⟨ n ⟩₋₁ _ (SSn≤n+2+n n) (⊙Sphere (S (S n))) {{Sphere-conn (S (S n))}}

    import homotopy.TruncationLoopLadder as TLL
    import homotopy.SuspAdjointLoop as SAL
    import homotopy.SuspAdjointLoopLadder as SALL
    import homotopy.CircleHSpace as CHS
    import homotopy.Pi2HSusp as Pi2

    ⊙up : ∀ n → ⊙Sphere n ⊙→ ⊙Ω (⊙Sphere (S n))
    ⊙up n = SAL.η (⊙Sphere n)

    Ω^'S-Trunc-up-is-equiv : ∀ n → is-equiv (Ω^'-fmap (S n) (⊙Trunc-fmap {n = ⟨ S n ⟩} (⊙up (S n))))
    Ω^'S-Trunc-up-is-equiv O = snd (Ω-emap (Pi2.⊙eq⁻¹ CHS.⊙S¹-hSpace))
    Ω^'S-Trunc-up-is-equiv (S n) = snd (Ω^'-emap (S (S n)) (F.⊙eq n))

    Trunc-Ω^'S-up-is-equiv : ∀ n → is-equiv (Trunc-fmap {n = 0} (Ω^'-fmap (S n) (⊙up (S n))))
    Trunc-Ω^'S-up-is-equiv n = ⊙CommSquareEquiv-preserves-equiv (TLL.ladder (S n) (⊙up (S n))) (Ω^'S-Trunc-up-is-equiv n)

    Trunc-post⊙∘-Ω^'S-up-is-equiv : ∀ n →
      is-equiv (Trunc-fmap {n = 0} ((⊙Ω^'-fmap (S n) (⊙up (S n)) ⊙∘_) :> (_ → ⊙Bool ⊙→ _)))
    Trunc-post⊙∘-Ω^'S-up-is-equiv n = CommSquareEquiv-preserves'-equiv
      (Trunc-csemap (⊙Bool→-equiv-idf-nat (⊙Ω^'-fmap (S n) (⊙up (S n)))))
      (Trunc-Ω^'S-up-is-equiv n)

    Trunc-post⊙∘-upS-is-equiv : ∀ n →
      is-equiv (Trunc-fmap {n = 0} ((⊙up (S n) ⊙∘_) :> (_ → ⊙Sphere (S n) ⊙→ _)))
    Trunc-post⊙∘-upS-is-equiv n = CommSquareEquiv-preserves'-equiv
      (Trunc-csemap (SALL.ladder (S n) (⊙up (S n))))
      (Trunc-post⊙∘-Ω^'S-up-is-equiv n)

    final-fix : ∀ n →
      CommSquareEquiv
        (⊙Susp-fmap :> (⊙Sphere-endo (S n) → _))
        (SAL.η _ ⊙∘_)
        (idf _)
        (–> (SAL.eq _ _))
    final-fix n = comm-sqr (λ f → ! (SAL.η-natural f)) , idf-is-equiv _ , snd (SAL.eq _ _)

  Trunc-⊙SphereS-endo-Susp-is-equiv : ∀ n →
    is-equiv (Trunc-fmap ⊙Susp-fmap :> (Trunc-⊙Sphere-endo (S n) → _))
  Trunc-⊙SphereS-endo-Susp-is-equiv n =
    CommSquareEquiv-preserves'-equiv
      (Trunc-csemap (final-fix n))
      (Trunc-post⊙∘-upS-is-equiv n)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
-- The debug output should include the text "Termination checking
-- mutual block MutId 0" once, not three times.

{-# OPTIONS -vterm.mutual.id:40 #-}

record R : Set₁ where
  constructor c
  field
    A : Set

  _ : A → A
  _ = λ x → x

  _ : A → A
  _ = λ x → x

  _ : A → A
  _ = λ x → x

-- Included in order to make the code fail to type-check.

Bad : Set
Bad = Set


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Decidable equality over lists parameterised by some setoid
------------------------------------------------------------------------

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

open import Relation.Binary

module Data.List.Relation.Binary.Equality.DecSetoid
  {a ℓ} (DS : DecSetoid a ℓ) where

import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
import Data.List.Relation.Binary.Pointwise as PW
open import Level
open import Relation.Binary using (Decidable)
open DecSetoid DS

------------------------------------------------------------------------
-- Make all definitions from setoid equality available

open SetoidEquality setoid public

------------------------------------------------------------------------
-- Additional properties

infix 4 _≋?_

_≋?_ : Decidable _≋_
_≋?_ = PW.decidable _≟_

≋-isDecEquivalence : IsDecEquivalence _≋_
≋-isDecEquivalence = PW.isDecEquivalence isDecEquivalence

≋-decSetoid : DecSetoid a (a ⊔ ℓ)
≋-decSetoid = PW.decSetoid DS


text:
module Everything where

import Relation.Ternary.Separation

-- The syntax and interpreter of LTLC
import Typed.LTLC

-- The syntax and interpreter of LTLC with strong updatable references
import Typed.LTLCRef

-- The syntax of a session typed language
import Sessions.Syntax

-- ... and its semantics
import Sessions.Semantics.Runtime
import Sessions.Semantics.Commands
import Sessions.Semantics.Expr
import Sessions.Semantics.Communication
import Sessions.Semantics.Process

-- the paper's session-typed program example
import Examples


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Functions.Definition
open import Lists.Definition
open import Lists.Monad
open import Boolean.Definition

module Lists.Filter.AllTrue where

allTrue : {a b : _} {A : Set a} (f : A → Set b) (l : List A) → Set b
allTrue f [] = True'
allTrue f (x :: l) = f x && allTrue f l

allTrueConcat : {a b : _} {A : Set a} (f : A → Set b) (l m : List A) → allTrue f l → allTrue f m → allTrue f (l ++ m)
allTrueConcat f [] m fl fm = fm
allTrueConcat f (x :: l) m (fst ,, snd) fm = fst ,, allTrueConcat f l m snd fm

allTrueFlatten : {a b : _} {A : Set a} (f : A → Set b) (l : List (List A)) → allTrue (λ i → allTrue f i) l → allTrue f (flatten l)
allTrueFlatten f [] pr = record {}
allTrueFlatten f ([] :: ls) pr = allTrueFlatten f ls (_&&_.snd pr)
allTrueFlatten f ((x :: l) :: ls) ((fx ,, fl) ,, snd) = fx ,, allTrueConcat f l (flatten ls) fl (allTrueFlatten f ls snd)

allTrueMap : {a b c : _} {A : Set a} {B : Set b} (pred : B → Set c) (f : A → B) (l : List A) → allTrue (pred ∘ f) l → allTrue pred (map f l)
allTrueMap pred f [] pr = record {}
allTrueMap pred f (x :: l) pr = _&&_.fst pr ,, allTrueMap pred f l (_&&_.snd pr)

allTrueExtension : {a b : _} {A : Set a} (f g : A → Set b) (l : List A) → ({x : A} → f x → g x) → allTrue f l → allTrue g l
allTrueExtension f g [] pred t = record {}
allTrueExtension f g (x :: l) pred (fg ,, snd) = pred {x} fg ,, allTrueExtension f g l pred snd

allTrueTail : {a b : _} {A : Set a} (pred : A → Set b) (x : A) (l : List A) → allTrue pred (x :: l) → allTrue pred l
allTrueTail pred x l (fst ,, snd) = snd

filter : {a : _} {A : Set a} (l : List A) (f : A → Bool) → List A
filter [] f = []
filter (x :: l) f with f x
filter (x :: l) f | BoolTrue = x :: filter l f
filter (x :: l) f | BoolFalse = filter l f


text:
module _ (A : Set) where

record R : Set where
  field f : A

test : R → R
test r = {!r!}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda