text:
module Text.Greek.SBLGNT.2Thess where

open import Data.List
open import Text.Greek.Bible
open import Text.Greek.Script
open import Text.Greek.Script.Unicode

ΠΡΟΣ-ΘΕΣΣΑΛΟΝΙΚΕΙΣ-Β : List (Word)
ΠΡΟΣ-ΘΕΣΣΑΛΟΝΙΚΕΙΣ-Β =
    word (Π ∷ α ∷ ῦ ∷ ∙λ ∷ ο ∷ ς ∷ []) "2Thess.1.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.1.1"
  ∷ word (Σ ∷ ι ∷ ∙λ ∷ ο ∷ υ ∷ α ∷ ν ∷ ὸ ∷ ς ∷ []) "2Thess.1.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.1.1"
  ∷ word (Τ ∷ ι ∷ μ ∷ ό ∷ θ ∷ ε ∷ ο ∷ ς ∷ []) "2Thess.1.1"
  ∷ word (τ ∷ ῇ ∷ []) "2Thess.1.1"
  ∷ word (ἐ ∷ κ ∷ κ ∷ ∙λ ∷ η ∷ σ ∷ ί ∷ ᾳ ∷ []) "2Thess.1.1"
  ∷ word (Θ ∷ ε ∷ σ ∷ σ ∷ α ∷ ∙λ ∷ ο ∷ ν ∷ ι ∷ κ ∷ έ ∷ ω ∷ ν ∷ []) "2Thess.1.1"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.1.1"
  ∷ word (θ ∷ ε ∷ ῷ ∷ []) "2Thess.1.1"
  ∷ word (π ∷ α ∷ τ ∷ ρ ∷ ὶ ∷ []) "2Thess.1.1"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.1.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.1.1"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ῳ ∷ []) "2Thess.1.1"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Thess.1.1"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ῷ ∷ []) "2Thess.1.1"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ ς ∷ []) "2Thess.1.2"
  ∷ word (ὑ ∷ μ ∷ ῖ ∷ ν ∷ []) "2Thess.1.2"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.1.2"
  ∷ word (ε ∷ ἰ ∷ ρ ∷ ή ∷ ν ∷ η ∷ []) "2Thess.1.2"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "2Thess.1.2"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "2Thess.1.2"
  ∷ word (π ∷ α ∷ τ ∷ ρ ∷ ὸ ∷ ς ∷ []) "2Thess.1.2"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.1.2"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Thess.1.2"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Thess.1.2"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Thess.1.2"
  ∷ word (Ε ∷ ὐ ∷ χ ∷ α ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ε ∷ ῖ ∷ ν ∷ []) "2Thess.1.3"
  ∷ word (ὀ ∷ φ ∷ ε ∷ ί ∷ ∙λ ∷ ο ∷ μ ∷ ε ∷ ν ∷ []) "2Thess.1.3"
  ∷ word (τ ∷ ῷ ∷ []) "2Thess.1.3"
  ∷ word (θ ∷ ε ∷ ῷ ∷ []) "2Thess.1.3"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ο ∷ τ ∷ ε ∷ []) "2Thess.1.3"
  ∷ word (π ∷ ε ∷ ρ ∷ ὶ ∷ []) "2Thess.1.3"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.1.3"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ ο ∷ ί ∷ []) "2Thess.1.3"
  ∷ word (κ ∷ α ∷ θ ∷ ὼ ∷ ς ∷ []) "2Thess.1.3"
  ∷ word (ἄ ∷ ξ ∷ ι ∷ ό ∷ ν ∷ []) "2Thess.1.3"
  ∷ word (ἐ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "2Thess.1.3"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2Thess.1.3"
  ∷ word (ὑ ∷ π ∷ ε ∷ ρ ∷ α ∷ υ ∷ ξ ∷ ά ∷ ν ∷ ε ∷ ι ∷ []) "2Thess.1.3"
  ∷ word (ἡ ∷ []) "2Thess.1.3"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ι ∷ ς ∷ []) "2Thess.1.3"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.1.3"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.1.3"
  ∷ word (π ∷ ∙λ ∷ ε ∷ ο ∷ ν ∷ ά ∷ ζ ∷ ε ∷ ι ∷ []) "2Thess.1.3"
  ∷ word (ἡ ∷ []) "2Thess.1.3"
  ∷ word (ἀ ∷ γ ∷ ά ∷ π ∷ η ∷ []) "2Thess.1.3"
  ∷ word (ἑ ∷ ν ∷ ὸ ∷ ς ∷ []) "2Thess.1.3"
  ∷ word (ἑ ∷ κ ∷ ά ∷ σ ∷ τ ∷ ο ∷ υ ∷ []) "2Thess.1.3"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ω ∷ ν ∷ []) "2Thess.1.3"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.1.3"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Thess.1.3"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ή ∷ ∙λ ∷ ο ∷ υ ∷ ς ∷ []) "2Thess.1.3"
  ∷ word (ὥ ∷ σ ∷ τ ∷ ε ∷ []) "2Thess.1.4"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ὺ ∷ ς ∷ []) "2Thess.1.4"
  ∷ word (ἡ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.1.4"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.1.4"
  ∷ word (ὑ ∷ μ ∷ ῖ ∷ ν ∷ []) "2Thess.1.4"
  ∷ word (ἐ ∷ γ ∷ κ ∷ α ∷ υ ∷ χ ∷ ᾶ ∷ σ ∷ θ ∷ α ∷ ι ∷ []) "2Thess.1.4"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.1.4"
  ∷ word (τ ∷ α ∷ ῖ ∷ ς ∷ []) "2Thess.1.4"
  ∷ word (ἐ ∷ κ ∷ κ ∷ ∙λ ∷ η ∷ σ ∷ ί ∷ α ∷ ι ∷ ς ∷ []) "2Thess.1.4"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.1.4"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "2Thess.1.4"
  ∷ word (ὑ ∷ π ∷ ὲ ∷ ρ ∷ []) "2Thess.1.4"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Thess.1.4"
  ∷ word (ὑ ∷ π ∷ ο ∷ μ ∷ ο ∷ ν ∷ ῆ ∷ ς ∷ []) "2Thess.1.4"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.1.4"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.1.4"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ε ∷ ω ∷ ς ∷ []) "2Thess.1.4"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.1.4"
  ∷ word (π ∷ ᾶ ∷ σ ∷ ι ∷ ν ∷ []) "2Thess.1.4"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Thess.1.4"
  ∷ word (δ ∷ ι ∷ ω ∷ γ ∷ μ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Thess.1.4"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.1.4"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.1.4"
  ∷ word (τ ∷ α ∷ ῖ ∷ ς ∷ []) "2Thess.1.4"
  ∷ word (θ ∷ ∙λ ∷ ί ∷ ψ ∷ ε ∷ σ ∷ ι ∷ ν ∷ []) "2Thess.1.4"
  ∷ word (α ∷ ἷ ∷ ς ∷ []) "2Thess.1.4"
  ∷ word (ἀ ∷ ν ∷ έ ∷ χ ∷ ε ∷ σ ∷ θ ∷ ε ∷ []) "2Thess.1.4"
  ∷ word (ἔ ∷ ν ∷ δ ∷ ε ∷ ι ∷ γ ∷ μ ∷ α ∷ []) "2Thess.1.5"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Thess.1.5"
  ∷ word (δ ∷ ι ∷ κ ∷ α ∷ ί ∷ α ∷ ς ∷ []) "2Thess.1.5"
  ∷ word (κ ∷ ρ ∷ ί ∷ σ ∷ ε ∷ ω ∷ ς ∷ []) "2Thess.1.5"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.1.5"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "2Thess.1.5"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Thess.1.5"
  ∷ word (τ ∷ ὸ ∷ []) "2Thess.1.5"
  ∷ word (κ ∷ α ∷ τ ∷ α ∷ ξ ∷ ι ∷ ω ∷ θ ∷ ῆ ∷ ν ∷ α ∷ ι ∷ []) "2Thess.1.5"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.1.5"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Thess.1.5"
  ∷ word (β ∷ α ∷ σ ∷ ι ∷ ∙λ ∷ ε ∷ ί ∷ α ∷ ς ∷ []) "2Thess.1.5"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.1.5"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "2Thess.1.5"
  ∷ word (ὑ ∷ π ∷ ὲ ∷ ρ ∷ []) "2Thess.1.5"
  ∷ word (ἧ ∷ ς ∷ []) "2Thess.1.5"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.1.5"
  ∷ word (π ∷ ά ∷ σ ∷ χ ∷ ε ∷ τ ∷ ε ∷ []) "2Thess.1.5"
  ∷ word (ε ∷ ἴ ∷ π ∷ ε ∷ ρ ∷ []) "2Thess.1.6"
  ∷ word (δ ∷ ί ∷ κ ∷ α ∷ ι ∷ ο ∷ ν ∷ []) "2Thess.1.6"
  ∷ word (π ∷ α ∷ ρ ∷ ὰ ∷ []) "2Thess.1.6"
  ∷ word (θ ∷ ε ∷ ῷ ∷ []) "2Thess.1.6"
  ∷ word (ἀ ∷ ν ∷ τ ∷ α ∷ π ∷ ο ∷ δ ∷ ο ∷ ῦ ∷ ν ∷ α ∷ ι ∷ []) "2Thess.1.6"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Thess.1.6"
  ∷ word (θ ∷ ∙λ ∷ ί ∷ β ∷ ο ∷ υ ∷ σ ∷ ι ∷ ν ∷ []) "2Thess.1.6"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.1.6"
  ∷ word (θ ∷ ∙λ ∷ ῖ ∷ ψ ∷ ι ∷ ν ∷ []) "2Thess.1.6"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.1.7"
  ∷ word (ὑ ∷ μ ∷ ῖ ∷ ν ∷ []) "2Thess.1.7"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Thess.1.7"
  ∷ word (θ ∷ ∙λ ∷ ι ∷ β ∷ ο ∷ μ ∷ έ ∷ ν ∷ ο ∷ ι ∷ ς ∷ []) "2Thess.1.7"
  ∷ word (ἄ ∷ ν ∷ ε ∷ σ ∷ ι ∷ ν ∷ []) "2Thess.1.7"
  ∷ word (μ ∷ ε ∷ θ ∷ []) "2Thess.1.7"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.1.7"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.1.7"
  ∷ word (τ ∷ ῇ ∷ []) "2Thess.1.7"
  ∷ word (ἀ ∷ π ∷ ο ∷ κ ∷ α ∷ ∙λ ∷ ύ ∷ ψ ∷ ε ∷ ι ∷ []) "2Thess.1.7"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.1.7"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Thess.1.7"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Thess.1.7"
  ∷ word (ἀ ∷ π ∷ []) "2Thess.1.7"
  ∷ word (ο ∷ ὐ ∷ ρ ∷ α ∷ ν ∷ ο ∷ ῦ ∷ []) "2Thess.1.7"
  ∷ word (μ ∷ ε ∷ τ ∷ []) "2Thess.1.7"
  ∷ word (ἀ ∷ γ ∷ γ ∷ έ ∷ ∙λ ∷ ω ∷ ν ∷ []) "2Thess.1.7"
  ∷ word (δ ∷ υ ∷ ν ∷ ά ∷ μ ∷ ε ∷ ω ∷ ς ∷ []) "2Thess.1.7"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Thess.1.7"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.1.8"
  ∷ word (φ ∷ ∙λ ∷ ο ∷ γ ∷ ὶ ∷ []) "2Thess.1.8"
  ∷ word (π ∷ υ ∷ ρ ∷ ό ∷ ς ∷ []) "2Thess.1.8"
  ∷ word (δ ∷ ι ∷ δ ∷ ό ∷ ν ∷ τ ∷ ο ∷ ς ∷ []) "2Thess.1.8"
  ∷ word (ἐ ∷ κ ∷ δ ∷ ί ∷ κ ∷ η ∷ σ ∷ ι ∷ ν ∷ []) "2Thess.1.8"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Thess.1.8"
  ∷ word (μ ∷ ὴ ∷ []) "2Thess.1.8"
  ∷ word (ε ∷ ἰ ∷ δ ∷ ό ∷ σ ∷ ι ∷ []) "2Thess.1.8"
  ∷ word (θ ∷ ε ∷ ὸ ∷ ν ∷ []) "2Thess.1.8"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.1.8"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Thess.1.8"
  ∷ word (μ ∷ ὴ ∷ []) "2Thess.1.8"
  ∷ word (ὑ ∷ π ∷ α ∷ κ ∷ ο ∷ ύ ∷ ο ∷ υ ∷ σ ∷ ι ∷ ν ∷ []) "2Thess.1.8"
  ∷ word (τ ∷ ῷ ∷ []) "2Thess.1.8"
  ∷ word (ε ∷ ὐ ∷ α ∷ γ ∷ γ ∷ ε ∷ ∙λ ∷ ί ∷ ῳ ∷ []) "2Thess.1.8"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.1.8"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Thess.1.8"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.1.8"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Thess.1.8"
  ∷ word (ο ∷ ἵ ∷ τ ∷ ι ∷ ν ∷ ε ∷ ς ∷ []) "2Thess.1.9"
  ∷ word (δ ∷ ί ∷ κ ∷ η ∷ ν ∷ []) "2Thess.1.9"
  ∷ word (τ ∷ ί ∷ σ ∷ ο ∷ υ ∷ σ ∷ ι ∷ ν ∷ []) "2Thess.1.9"
  ∷ word (ὄ ∷ ∙λ ∷ ε ∷ θ ∷ ρ ∷ ο ∷ ν ∷ []) "2Thess.1.9"
  ∷ word (α ∷ ἰ ∷ ώ ∷ ν ∷ ι ∷ ο ∷ ν ∷ []) "2Thess.1.9"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "2Thess.1.9"
  ∷ word (π ∷ ρ ∷ ο ∷ σ ∷ ώ ∷ π ∷ ο ∷ υ ∷ []) "2Thess.1.9"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.1.9"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Thess.1.9"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.1.9"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "2Thess.1.9"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Thess.1.9"
  ∷ word (δ ∷ ό ∷ ξ ∷ η ∷ ς ∷ []) "2Thess.1.9"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Thess.1.9"
  ∷ word (ἰ ∷ σ ∷ χ ∷ ύ ∷ ο ∷ ς ∷ []) "2Thess.1.9"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Thess.1.9"
  ∷ word (ὅ ∷ τ ∷ α ∷ ν ∷ []) "2Thess.1.10"
  ∷ word (ἔ ∷ ∙λ ∷ θ ∷ ῃ ∷ []) "2Thess.1.10"
  ∷ word (ἐ ∷ ν ∷ δ ∷ ο ∷ ξ ∷ α ∷ σ ∷ θ ∷ ῆ ∷ ν ∷ α ∷ ι ∷ []) "2Thess.1.10"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.1.10"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Thess.1.10"
  ∷ word (ἁ ∷ γ ∷ ί ∷ ο ∷ ι ∷ ς ∷ []) "2Thess.1.10"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Thess.1.10"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.1.10"
  ∷ word (θ ∷ α ∷ υ ∷ μ ∷ α ∷ σ ∷ θ ∷ ῆ ∷ ν ∷ α ∷ ι ∷ []) "2Thess.1.10"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.1.10"
  ∷ word (π ∷ ᾶ ∷ σ ∷ ι ∷ ν ∷ []) "2Thess.1.10"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Thess.1.10"
  ∷ word (π ∷ ι ∷ σ ∷ τ ∷ ε ∷ ύ ∷ σ ∷ α ∷ σ ∷ ι ∷ ν ∷ []) "2Thess.1.10"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2Thess.1.10"
  ∷ word (ἐ ∷ π ∷ ι ∷ σ ∷ τ ∷ ε ∷ ύ ∷ θ ∷ η ∷ []) "2Thess.1.10"
  ∷ word (τ ∷ ὸ ∷ []) "2Thess.1.10"
  ∷ word (μ ∷ α ∷ ρ ∷ τ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ν ∷ []) "2Thess.1.10"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.1.10"
  ∷ word (ἐ ∷ φ ∷ []) "2Thess.1.10"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.1.10"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.1.10"
  ∷ word (τ ∷ ῇ ∷ []) "2Thess.1.10"
  ∷ word (ἡ ∷ μ ∷ έ ∷ ρ ∷ ᾳ ∷ []) "2Thess.1.10"
  ∷ word (ἐ ∷ κ ∷ ε ∷ ί ∷ ν ∷ ῃ ∷ []) "2Thess.1.10"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Thess.1.11"
  ∷ word (ὃ ∷ []) "2Thess.1.11"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.1.11"
  ∷ word (π ∷ ρ ∷ ο ∷ σ ∷ ε ∷ υ ∷ χ ∷ ό ∷ μ ∷ ε ∷ θ ∷ α ∷ []) "2Thess.1.11"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ο ∷ τ ∷ ε ∷ []) "2Thess.1.11"
  ∷ word (π ∷ ε ∷ ρ ∷ ὶ ∷ []) "2Thess.1.11"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.1.11"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "2Thess.1.11"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.1.11"
  ∷ word (ἀ ∷ ξ ∷ ι ∷ ώ ∷ σ ∷ ῃ ∷ []) "2Thess.1.11"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Thess.1.11"
  ∷ word (κ ∷ ∙λ ∷ ή ∷ σ ∷ ε ∷ ω ∷ ς ∷ []) "2Thess.1.11"
  ∷ word (ὁ ∷ []) "2Thess.1.11"
  ∷ word (θ ∷ ε ∷ ὸ ∷ ς ∷ []) "2Thess.1.11"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.1.11"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.1.11"
  ∷ word (π ∷ ∙λ ∷ η ∷ ρ ∷ ώ ∷ σ ∷ ῃ ∷ []) "2Thess.1.11"
  ∷ word (π ∷ ᾶ ∷ σ ∷ α ∷ ν ∷ []) "2Thess.1.11"
  ∷ word (ε ∷ ὐ ∷ δ ∷ ο ∷ κ ∷ ί ∷ α ∷ ν ∷ []) "2Thess.1.11"
  ∷ word (ἀ ∷ γ ∷ α ∷ θ ∷ ω ∷ σ ∷ ύ ∷ ν ∷ η ∷ ς ∷ []) "2Thess.1.11"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.1.11"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ ο ∷ ν ∷ []) "2Thess.1.11"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ε ∷ ω ∷ ς ∷ []) "2Thess.1.11"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.1.11"
  ∷ word (δ ∷ υ ∷ ν ∷ ά ∷ μ ∷ ε ∷ ι ∷ []) "2Thess.1.11"
  ∷ word (ὅ ∷ π ∷ ω ∷ ς ∷ []) "2Thess.1.12"
  ∷ word (ἐ ∷ ν ∷ δ ∷ ο ∷ ξ ∷ α ∷ σ ∷ θ ∷ ῇ ∷ []) "2Thess.1.12"
  ∷ word (τ ∷ ὸ ∷ []) "2Thess.1.12"
  ∷ word (ὄ ∷ ν ∷ ο ∷ μ ∷ α ∷ []) "2Thess.1.12"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.1.12"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Thess.1.12"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.1.12"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Thess.1.12"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.1.12"
  ∷ word (ὑ ∷ μ ∷ ῖ ∷ ν ∷ []) "2Thess.1.12"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.1.12"
  ∷ word (ὑ ∷ μ ∷ ε ∷ ῖ ∷ ς ∷ []) "2Thess.1.12"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.1.12"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῷ ∷ []) "2Thess.1.12"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "2Thess.1.12"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Thess.1.12"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ ν ∷ []) "2Thess.1.12"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.1.12"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "2Thess.1.12"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.1.12"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.1.12"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Thess.1.12"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Thess.1.12"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Thess.1.12"
  ∷ word (Ἐ ∷ ρ ∷ ω ∷ τ ∷ ῶ ∷ μ ∷ ε ∷ ν ∷ []) "2Thess.2.1"
  ∷ word (δ ∷ ὲ ∷ []) "2Thess.2.1"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.2.1"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ ο ∷ ί ∷ []) "2Thess.2.1"
  ∷ word (ὑ ∷ π ∷ ὲ ∷ ρ ∷ []) "2Thess.2.1"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Thess.2.1"
  ∷ word (π ∷ α ∷ ρ ∷ ο ∷ υ ∷ σ ∷ ί ∷ α ∷ ς ∷ []) "2Thess.2.1"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.2.1"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Thess.2.1"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.2.1"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Thess.2.1"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Thess.2.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.2.1"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.2.1"
  ∷ word (ἐ ∷ π ∷ ι ∷ σ ∷ υ ∷ ν ∷ α ∷ γ ∷ ω ∷ γ ∷ ῆ ∷ ς ∷ []) "2Thess.2.1"
  ∷ word (ἐ ∷ π ∷ []) "2Thess.2.1"
  ∷ word (α ∷ ὐ ∷ τ ∷ ό ∷ ν ∷ []) "2Thess.2.1"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Thess.2.2"
  ∷ word (τ ∷ ὸ ∷ []) "2Thess.2.2"
  ∷ word (μ ∷ ὴ ∷ []) "2Thess.2.2"
  ∷ word (τ ∷ α ∷ χ ∷ έ ∷ ω ∷ ς ∷ []) "2Thess.2.2"
  ∷ word (σ ∷ α ∷ ∙λ ∷ ε ∷ υ ∷ θ ∷ ῆ ∷ ν ∷ α ∷ ι ∷ []) "2Thess.2.2"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.2.2"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "2Thess.2.2"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.2.2"
  ∷ word (ν ∷ ο ∷ ὸ ∷ ς ∷ []) "2Thess.2.2"
  ∷ word (μ ∷ η ∷ δ ∷ ὲ ∷ []) "2Thess.2.2"
  ∷ word (θ ∷ ρ ∷ ο ∷ ε ∷ ῖ ∷ σ ∷ θ ∷ α ∷ ι ∷ []) "2Thess.2.2"
  ∷ word (μ ∷ ή ∷ τ ∷ ε ∷ []) "2Thess.2.2"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "2Thess.2.2"
  ∷ word (π ∷ ν ∷ ε ∷ ύ ∷ μ ∷ α ∷ τ ∷ ο ∷ ς ∷ []) "2Thess.2.2"
  ∷ word (μ ∷ ή ∷ τ ∷ ε ∷ []) "2Thess.2.2"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "2Thess.2.2"
  ∷ word (∙λ ∷ ό ∷ γ ∷ ο ∷ υ ∷ []) "2Thess.2.2"
  ∷ word (μ ∷ ή ∷ τ ∷ ε ∷ []) "2Thess.2.2"
  ∷ word (δ ∷ ι ∷ []) "2Thess.2.2"
  ∷ word (ἐ ∷ π ∷ ι ∷ σ ∷ τ ∷ ο ∷ ∙λ ∷ ῆ ∷ ς ∷ []) "2Thess.2.2"
  ∷ word (ὡ ∷ ς ∷ []) "2Thess.2.2"
  ∷ word (δ ∷ ι ∷ []) "2Thess.2.2"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.2.2"
  ∷ word (ὡ ∷ ς ∷ []) "2Thess.2.2"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2Thess.2.2"
  ∷ word (ἐ ∷ ν ∷ έ ∷ σ ∷ τ ∷ η ∷ κ ∷ ε ∷ ν ∷ []) "2Thess.2.2"
  ∷ word (ἡ ∷ []) "2Thess.2.2"
  ∷ word (ἡ ∷ μ ∷ έ ∷ ρ ∷ α ∷ []) "2Thess.2.2"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.2.2"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Thess.2.2"
  ∷ word (μ ∷ ή ∷ []) "2Thess.2.3"
  ∷ word (τ ∷ ι ∷ ς ∷ []) "2Thess.2.3"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.2.3"
  ∷ word (ἐ ∷ ξ ∷ α ∷ π ∷ α ∷ τ ∷ ή ∷ σ ∷ ῃ ∷ []) "2Thess.2.3"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "2Thess.2.3"
  ∷ word (μ ∷ η ∷ δ ∷ έ ∷ ν ∷ α ∷ []) "2Thess.2.3"
  ∷ word (τ ∷ ρ ∷ ό ∷ π ∷ ο ∷ ν ∷ []) "2Thess.2.3"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2Thess.2.3"
  ∷ word (ἐ ∷ ὰ ∷ ν ∷ []) "2Thess.2.3"
  ∷ word (μ ∷ ὴ ∷ []) "2Thess.2.3"
  ∷ word (ἔ ∷ ∙λ ∷ θ ∷ ῃ ∷ []) "2Thess.2.3"
  ∷ word (ἡ ∷ []) "2Thess.2.3"
  ∷ word (ἀ ∷ π ∷ ο ∷ σ ∷ τ ∷ α ∷ σ ∷ ί ∷ α ∷ []) "2Thess.2.3"
  ∷ word (π ∷ ρ ∷ ῶ ∷ τ ∷ ο ∷ ν ∷ []) "2Thess.2.3"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.2.3"
  ∷ word (ἀ ∷ π ∷ ο ∷ κ ∷ α ∷ ∙λ ∷ υ ∷ φ ∷ θ ∷ ῇ ∷ []) "2Thess.2.3"
  ∷ word (ὁ ∷ []) "2Thess.2.3"
  ∷ word (ἄ ∷ ν ∷ θ ∷ ρ ∷ ω ∷ π ∷ ο ∷ ς ∷ []) "2Thess.2.3"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Thess.2.3"
  ∷ word (ἀ ∷ ν ∷ ο ∷ μ ∷ ί ∷ α ∷ ς ∷ []) "2Thess.2.3"
  ∷ word (ὁ ∷ []) "2Thess.2.3"
  ∷ word (υ ∷ ἱ ∷ ὸ ∷ ς ∷ []) "2Thess.2.3"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Thess.2.3"
  ∷ word (ἀ ∷ π ∷ ω ∷ ∙λ ∷ ε ∷ ί ∷ α ∷ ς ∷ []) "2Thess.2.3"
  ∷ word (ὁ ∷ []) "2Thess.2.4"
  ∷ word (ἀ ∷ ν ∷ τ ∷ ι ∷ κ ∷ ε ∷ ί ∷ μ ∷ ε ∷ ν ∷ ο ∷ ς ∷ []) "2Thess.2.4"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.2.4"
  ∷ word (ὑ ∷ π ∷ ε ∷ ρ ∷ α ∷ ι ∷ ρ ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ς ∷ []) "2Thess.2.4"
  ∷ word (ἐ ∷ π ∷ ὶ ∷ []) "2Thess.2.4"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ α ∷ []) "2Thess.2.4"
  ∷ word (∙λ ∷ ε ∷ γ ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ν ∷ []) "2Thess.2.4"
  ∷ word (θ ∷ ε ∷ ὸ ∷ ν ∷ []) "2Thess.2.4"
  ∷ word (ἢ ∷ []) "2Thess.2.4"
  ∷ word (σ ∷ έ ∷ β ∷ α ∷ σ ∷ μ ∷ α ∷ []) "2Thess.2.4"
  ∷ word (ὥ ∷ σ ∷ τ ∷ ε ∷ []) "2Thess.2.4"
  ∷ word (α ∷ ὐ ∷ τ ∷ ὸ ∷ ν ∷ []) "2Thess.2.4"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Thess.2.4"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "2Thess.2.4"
  ∷ word (ν ∷ α ∷ ὸ ∷ ν ∷ []) "2Thess.2.4"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.2.4"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "2Thess.2.4"
  ∷ word (κ ∷ α ∷ θ ∷ ί ∷ σ ∷ α ∷ ι ∷ []) "2Thess.2.4"
  ∷ word (ἀ ∷ π ∷ ο ∷ δ ∷ ε ∷ ι ∷ κ ∷ ν ∷ ύ ∷ ν ∷ τ ∷ α ∷ []) "2Thess.2.4"
  ∷ word (ἑ ∷ α ∷ υ ∷ τ ∷ ὸ ∷ ν ∷ []) "2Thess.2.4"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2Thess.2.4"
  ∷ word (ἔ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "2Thess.2.4"
  ∷ word (θ ∷ ε ∷ ό ∷ ς ∷ []) "2Thess.2.4"
  ∷ word (ο ∷ ὐ ∷ []) "2Thess.2.5"
  ∷ word (μ ∷ ν ∷ η ∷ μ ∷ ο ∷ ν ∷ ε ∷ ύ ∷ ε ∷ τ ∷ ε ∷ []) "2Thess.2.5"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2Thess.2.5"
  ∷ word (ἔ ∷ τ ∷ ι ∷ []) "2Thess.2.5"
  ∷ word (ὢ ∷ ν ∷ []) "2Thess.2.5"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "2Thess.2.5"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.2.5"
  ∷ word (τ ∷ α ∷ ῦ ∷ τ ∷ α ∷ []) "2Thess.2.5"
  ∷ word (ἔ ∷ ∙λ ∷ ε ∷ γ ∷ ο ∷ ν ∷ []) "2Thess.2.5"
  ∷ word (ὑ ∷ μ ∷ ῖ ∷ ν ∷ []) "2Thess.2.5"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.2.6"
  ∷ word (ν ∷ ῦ ∷ ν ∷ []) "2Thess.2.6"
  ∷ word (τ ∷ ὸ ∷ []) "2Thess.2.6"
  ∷ word (κ ∷ α ∷ τ ∷ έ ∷ χ ∷ ο ∷ ν ∷ []) "2Thess.2.6"
  ∷ word (ο ∷ ἴ ∷ δ ∷ α ∷ τ ∷ ε ∷ []) "2Thess.2.6"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Thess.2.6"
  ∷ word (τ ∷ ὸ ∷ []) "2Thess.2.6"
  ∷ word (ἀ ∷ π ∷ ο ∷ κ ∷ α ∷ ∙λ ∷ υ ∷ φ ∷ θ ∷ ῆ ∷ ν ∷ α ∷ ι ∷ []) "2Thess.2.6"
  ∷ word (α ∷ ὐ ∷ τ ∷ ὸ ∷ ν ∷ []) "2Thess.2.6"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.2.6"
  ∷ word (τ ∷ ῷ ∷ []) "2Thess.2.6"
  ∷ word (ἑ ∷ α ∷ υ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Thess.2.6"
  ∷ word (κ ∷ α ∷ ι ∷ ρ ∷ ῷ ∷ []) "2Thess.2.6"
  ∷ word (τ ∷ ὸ ∷ []) "2Thess.2.7"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "2Thess.2.7"
  ∷ word (μ ∷ υ ∷ σ ∷ τ ∷ ή ∷ ρ ∷ ι ∷ ο ∷ ν ∷ []) "2Thess.2.7"
  ∷ word (ἤ ∷ δ ∷ η ∷ []) "2Thess.2.7"
  ∷ word (ἐ ∷ ν ∷ ε ∷ ρ ∷ γ ∷ ε ∷ ῖ ∷ τ ∷ α ∷ ι ∷ []) "2Thess.2.7"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Thess.2.7"
  ∷ word (ἀ ∷ ν ∷ ο ∷ μ ∷ ί ∷ α ∷ ς ∷ []) "2Thess.2.7"
  ∷ word (μ ∷ ό ∷ ν ∷ ο ∷ ν ∷ []) "2Thess.2.7"
  ∷ word (ὁ ∷ []) "2Thess.2.7"
  ∷ word (κ ∷ α ∷ τ ∷ έ ∷ χ ∷ ω ∷ ν ∷ []) "2Thess.2.7"
  ∷ word (ἄ ∷ ρ ∷ τ ∷ ι ∷ []) "2Thess.2.7"
  ∷ word (ἕ ∷ ω ∷ ς ∷ []) "2Thess.2.7"
  ∷ word (ἐ ∷ κ ∷ []) "2Thess.2.7"
  ∷ word (μ ∷ έ ∷ σ ∷ ο ∷ υ ∷ []) "2Thess.2.7"
  ∷ word (γ ∷ έ ∷ ν ∷ η ∷ τ ∷ α ∷ ι ∷ []) "2Thess.2.7"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.2.8"
  ∷ word (τ ∷ ό ∷ τ ∷ ε ∷ []) "2Thess.2.8"
  ∷ word (ἀ ∷ π ∷ ο ∷ κ ∷ α ∷ ∙λ ∷ υ ∷ φ ∷ θ ∷ ή ∷ σ ∷ ε ∷ τ ∷ α ∷ ι ∷ []) "2Thess.2.8"
  ∷ word (ὁ ∷ []) "2Thess.2.8"
  ∷ word (ἄ ∷ ν ∷ ο ∷ μ ∷ ο ∷ ς ∷ []) "2Thess.2.8"
  ∷ word (ὃ ∷ ν ∷ []) "2Thess.2.8"
  ∷ word (ὁ ∷ []) "2Thess.2.8"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ς ∷ []) "2Thess.2.8"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ ς ∷ []) "2Thess.2.8"
  ∷ word (ἀ ∷ ν ∷ ε ∷ ∙λ ∷ ε ∷ ῖ ∷ []) "2Thess.2.8"
  ∷ word (τ ∷ ῷ ∷ []) "2Thess.2.8"
  ∷ word (π ∷ ν ∷ ε ∷ ύ ∷ μ ∷ α ∷ τ ∷ ι ∷ []) "2Thess.2.8"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.2.8"
  ∷ word (σ ∷ τ ∷ ό ∷ μ ∷ α ∷ τ ∷ ο ∷ ς ∷ []) "2Thess.2.8"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Thess.2.8"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.2.8"
  ∷ word (κ ∷ α ∷ τ ∷ α ∷ ρ ∷ γ ∷ ή ∷ σ ∷ ε ∷ ι ∷ []) "2Thess.2.8"
  ∷ word (τ ∷ ῇ ∷ []) "2Thess.2.8"
  ∷ word (ἐ ∷ π ∷ ι ∷ φ ∷ α ∷ ν ∷ ε ∷ ί ∷ ᾳ ∷ []) "2Thess.2.8"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Thess.2.8"
  ∷ word (π ∷ α ∷ ρ ∷ ο ∷ υ ∷ σ ∷ ί ∷ α ∷ ς ∷ []) "2Thess.2.8"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Thess.2.8"
  ∷ word (ο ∷ ὗ ∷ []) "2Thess.2.9"
  ∷ word (ἐ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "2Thess.2.9"
  ∷ word (ἡ ∷ []) "2Thess.2.9"
  ∷ word (π ∷ α ∷ ρ ∷ ο ∷ υ ∷ σ ∷ ί ∷ α ∷ []) "2Thess.2.9"
  ∷ word (κ ∷ α ∷ τ ∷ []) "2Thess.2.9"
  ∷ word (ἐ ∷ ν ∷ έ ∷ ρ ∷ γ ∷ ε ∷ ι ∷ α ∷ ν ∷ []) "2Thess.2.9"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.2.9"
  ∷ word (Σ ∷ α ∷ τ ∷ α ∷ ν ∷ ᾶ ∷ []) "2Thess.2.9"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.2.9"
  ∷ word (π ∷ ά ∷ σ ∷ ῃ ∷ []) "2Thess.2.9"
  ∷ word (δ ∷ υ ∷ ν ∷ ά ∷ μ ∷ ε ∷ ι ∷ []) "2Thess.2.9"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.2.9"
  ∷ word (σ ∷ η ∷ μ ∷ ε ∷ ί ∷ ο ∷ ι ∷ ς ∷ []) "2Thess.2.9"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.2.9"
  ∷ word (τ ∷ έ ∷ ρ ∷ α ∷ σ ∷ ι ∷ ν ∷ []) "2Thess.2.9"
  ∷ word (ψ ∷ ε ∷ ύ ∷ δ ∷ ο ∷ υ ∷ ς ∷ []) "2Thess.2.9"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.2.10"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.2.10"
  ∷ word (π ∷ ά ∷ σ ∷ ῃ ∷ []) "2Thess.2.10"
  ∷ word (ἀ ∷ π ∷ ά ∷ τ ∷ ῃ ∷ []) "2Thess.2.10"
  ∷ word (ἀ ∷ δ ∷ ι ∷ κ ∷ ί ∷ α ∷ ς ∷ []) "2Thess.2.10"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Thess.2.10"
  ∷ word (ἀ ∷ π ∷ ο ∷ ∙λ ∷ ∙λ ∷ υ ∷ μ ∷ έ ∷ ν ∷ ο ∷ ι ∷ ς ∷ []) "2Thess.2.10"
  ∷ word (ἀ ∷ ν ∷ θ ∷ []) "2Thess.2.10"
  ∷ word (ὧ ∷ ν ∷ []) "2Thess.2.10"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Thess.2.10"
  ∷ word (ἀ ∷ γ ∷ ά ∷ π ∷ η ∷ ν ∷ []) "2Thess.2.10"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Thess.2.10"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ε ∷ ί ∷ α ∷ ς ∷ []) "2Thess.2.10"
  ∷ word (ο ∷ ὐ ∷ κ ∷ []) "2Thess.2.10"
  ∷ word (ἐ ∷ δ ∷ έ ∷ ξ ∷ α ∷ ν ∷ τ ∷ ο ∷ []) "2Thess.2.10"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Thess.2.10"
  ∷ word (τ ∷ ὸ ∷ []) "2Thess.2.10"
  ∷ word (σ ∷ ω ∷ θ ∷ ῆ ∷ ν ∷ α ∷ ι ∷ []) "2Thess.2.10"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ύ ∷ ς ∷ []) "2Thess.2.10"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.2.11"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "2Thess.2.11"
  ∷ word (τ ∷ ο ∷ ῦ ∷ τ ∷ ο ∷ []) "2Thess.2.11"
  ∷ word (π ∷ έ ∷ μ ∷ π ∷ ε ∷ ι ∷ []) "2Thess.2.11"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Thess.2.11"
  ∷ word (ὁ ∷ []) "2Thess.2.11"
  ∷ word (θ ∷ ε ∷ ὸ ∷ ς ∷ []) "2Thess.2.11"
  ∷ word (ἐ ∷ ν ∷ έ ∷ ρ ∷ γ ∷ ε ∷ ι ∷ α ∷ ν ∷ []) "2Thess.2.11"
  ∷ word (π ∷ ∙λ ∷ ά ∷ ν ∷ η ∷ ς ∷ []) "2Thess.2.11"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Thess.2.11"
  ∷ word (τ ∷ ὸ ∷ []) "2Thess.2.11"
  ∷ word (π ∷ ι ∷ σ ∷ τ ∷ ε ∷ ῦ ∷ σ ∷ α ∷ ι ∷ []) "2Thess.2.11"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ὺ ∷ ς ∷ []) "2Thess.2.11"
  ∷ word (τ ∷ ῷ ∷ []) "2Thess.2.11"
  ∷ word (ψ ∷ ε ∷ ύ ∷ δ ∷ ε ∷ ι ∷ []) "2Thess.2.11"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "2Thess.2.12"
  ∷ word (κ ∷ ρ ∷ ι ∷ θ ∷ ῶ ∷ σ ∷ ι ∷ ν ∷ []) "2Thess.2.12"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "2Thess.2.12"
  ∷ word (ο ∷ ἱ ∷ []) "2Thess.2.12"
  ∷ word (μ ∷ ὴ ∷ []) "2Thess.2.12"
  ∷ word (π ∷ ι ∷ σ ∷ τ ∷ ε ∷ ύ ∷ σ ∷ α ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "2Thess.2.12"
  ∷ word (τ ∷ ῇ ∷ []) "2Thess.2.12"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ε ∷ ί ∷ ᾳ ∷ []) "2Thess.2.12"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "2Thess.2.12"
  ∷ word (ε ∷ ὐ ∷ δ ∷ ο ∷ κ ∷ ή ∷ σ ∷ α ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "2Thess.2.12"
  ∷ word (τ ∷ ῇ ∷ []) "2Thess.2.12"
  ∷ word (ἀ ∷ δ ∷ ι ∷ κ ∷ ί ∷ ᾳ ∷ []) "2Thess.2.12"
  ∷ word (Ἡ ∷ μ ∷ ε ∷ ῖ ∷ ς ∷ []) "2Thess.2.13"
  ∷ word (δ ∷ ὲ ∷ []) "2Thess.2.13"
  ∷ word (ὀ ∷ φ ∷ ε ∷ ί ∷ ∙λ ∷ ο ∷ μ ∷ ε ∷ ν ∷ []) "2Thess.2.13"
  ∷ word (ε ∷ ὐ ∷ χ ∷ α ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ε ∷ ῖ ∷ ν ∷ []) "2Thess.2.13"
  ∷ word (τ ∷ ῷ ∷ []) "2Thess.2.13"
  ∷ word (θ ∷ ε ∷ ῷ ∷ []) "2Thess.2.13"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ο ∷ τ ∷ ε ∷ []) "2Thess.2.13"
  ∷ word (π ∷ ε ∷ ρ ∷ ὶ ∷ []) "2Thess.2.13"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.2.13"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ ο ∷ ὶ ∷ []) "2Thess.2.13"
  ∷ word (ἠ ∷ γ ∷ α ∷ π ∷ η ∷ μ ∷ έ ∷ ν ∷ ο ∷ ι ∷ []) "2Thess.2.13"
  ∷ word (ὑ ∷ π ∷ ὸ ∷ []) "2Thess.2.13"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Thess.2.13"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2Thess.2.13"
  ∷ word (ε ∷ ἵ ∷ ∙λ ∷ α ∷ τ ∷ ο ∷ []) "2Thess.2.13"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.2.13"
  ∷ word (ὁ ∷ []) "2Thess.2.13"
  ∷ word (θ ∷ ε ∷ ὸ ∷ ς ∷ []) "2Thess.2.13"
  ∷ word (ἀ ∷ π ∷ α ∷ ρ ∷ χ ∷ ὴ ∷ ν ∷ []) "2Thess.2.13"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Thess.2.13"
  ∷ word (σ ∷ ω ∷ τ ∷ η ∷ ρ ∷ ί ∷ α ∷ ν ∷ []) "2Thess.2.13"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.2.13"
  ∷ word (ἁ ∷ γ ∷ ι ∷ α ∷ σ ∷ μ ∷ ῷ ∷ []) "2Thess.2.13"
  ∷ word (π ∷ ν ∷ ε ∷ ύ ∷ μ ∷ α ∷ τ ∷ ο ∷ ς ∷ []) "2Thess.2.13"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.2.13"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ε ∷ ι ∷ []) "2Thess.2.13"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ε ∷ ί ∷ α ∷ ς ∷ []) "2Thess.2.13"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Thess.2.14"
  ∷ word (ὃ ∷ []) "2Thess.2.14"
  ∷ word (ἐ ∷ κ ∷ ά ∷ ∙λ ∷ ε ∷ σ ∷ ε ∷ ν ∷ []) "2Thess.2.14"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.2.14"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "2Thess.2.14"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.2.14"
  ∷ word (ε ∷ ὐ ∷ α ∷ γ ∷ γ ∷ ε ∷ ∙λ ∷ ί ∷ ο ∷ υ ∷ []) "2Thess.2.14"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.2.14"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Thess.2.14"
  ∷ word (π ∷ ε ∷ ρ ∷ ι ∷ π ∷ ο ∷ ί ∷ η ∷ σ ∷ ι ∷ ν ∷ []) "2Thess.2.14"
  ∷ word (δ ∷ ό ∷ ξ ∷ η ∷ ς ∷ []) "2Thess.2.14"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.2.14"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Thess.2.14"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.2.14"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Thess.2.14"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Thess.2.14"
  ∷ word (ἄ ∷ ρ ∷ α ∷ []) "2Thess.2.15"
  ∷ word (ο ∷ ὖ ∷ ν ∷ []) "2Thess.2.15"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ ο ∷ ί ∷ []) "2Thess.2.15"
  ∷ word (σ ∷ τ ∷ ή ∷ κ ∷ ε ∷ τ ∷ ε ∷ []) "2Thess.2.15"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.2.15"
  ∷ word (κ ∷ ρ ∷ α ∷ τ ∷ ε ∷ ῖ ∷ τ ∷ ε ∷ []) "2Thess.2.15"
  ∷ word (τ ∷ ὰ ∷ ς ∷ []) "2Thess.2.15"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ δ ∷ ό ∷ σ ∷ ε ∷ ι ∷ ς ∷ []) "2Thess.2.15"
  ∷ word (ἃ ∷ ς ∷ []) "2Thess.2.15"
  ∷ word (ἐ ∷ δ ∷ ι ∷ δ ∷ ά ∷ χ ∷ θ ∷ η ∷ τ ∷ ε ∷ []) "2Thess.2.15"
  ∷ word (ε ∷ ἴ ∷ τ ∷ ε ∷ []) "2Thess.2.15"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "2Thess.2.15"
  ∷ word (∙λ ∷ ό ∷ γ ∷ ο ∷ υ ∷ []) "2Thess.2.15"
  ∷ word (ε ∷ ἴ ∷ τ ∷ ε ∷ []) "2Thess.2.15"
  ∷ word (δ ∷ ι ∷ []) "2Thess.2.15"
  ∷ word (ἐ ∷ π ∷ ι ∷ σ ∷ τ ∷ ο ∷ ∙λ ∷ ῆ ∷ ς ∷ []) "2Thess.2.15"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.2.15"
  ∷ word (Α ∷ ὐ ∷ τ ∷ ὸ ∷ ς ∷ []) "2Thess.2.16"
  ∷ word (δ ∷ ὲ ∷ []) "2Thess.2.16"
  ∷ word (ὁ ∷ []) "2Thess.2.16"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ς ∷ []) "2Thess.2.16"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.2.16"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ ς ∷ []) "2Thess.2.16"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ὸ ∷ ς ∷ []) "2Thess.2.16"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.2.16"
  ∷ word (θ ∷ ε ∷ ὸ ∷ ς ∷ []) "2Thess.2.16"
  ∷ word (ὁ ∷ []) "2Thess.2.16"
  ∷ word (π ∷ α ∷ τ ∷ ὴ ∷ ρ ∷ []) "2Thess.2.16"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.2.16"
  ∷ word (ὁ ∷ []) "2Thess.2.16"
  ∷ word (ἀ ∷ γ ∷ α ∷ π ∷ ή ∷ σ ∷ α ∷ ς ∷ []) "2Thess.2.16"
  ∷ word (ἡ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.2.16"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.2.16"
  ∷ word (δ ∷ ο ∷ ὺ ∷ ς ∷ []) "2Thess.2.16"
  ∷ word (π ∷ α ∷ ρ ∷ ά ∷ κ ∷ ∙λ ∷ η ∷ σ ∷ ι ∷ ν ∷ []) "2Thess.2.16"
  ∷ word (α ∷ ἰ ∷ ω ∷ ν ∷ ί ∷ α ∷ ν ∷ []) "2Thess.2.16"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.2.16"
  ∷ word (ἐ ∷ ∙λ ∷ π ∷ ί ∷ δ ∷ α ∷ []) "2Thess.2.16"
  ∷ word (ἀ ∷ γ ∷ α ∷ θ ∷ ὴ ∷ ν ∷ []) "2Thess.2.16"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.2.16"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ τ ∷ ι ∷ []) "2Thess.2.16"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ κ ∷ α ∷ ∙λ ∷ έ ∷ σ ∷ α ∷ ι ∷ []) "2Thess.2.17"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.2.17"
  ∷ word (τ ∷ ὰ ∷ ς ∷ []) "2Thess.2.17"
  ∷ word (κ ∷ α ∷ ρ ∷ δ ∷ ί ∷ α ∷ ς ∷ []) "2Thess.2.17"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.2.17"
  ∷ word (σ ∷ τ ∷ η ∷ ρ ∷ ί ∷ ξ ∷ α ∷ ι ∷ []) "2Thess.2.17"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.2.17"
  ∷ word (π ∷ α ∷ ν ∷ τ ∷ ὶ ∷ []) "2Thess.2.17"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ ῳ ∷ []) "2Thess.2.17"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.2.17"
  ∷ word (∙λ ∷ ό ∷ γ ∷ ῳ ∷ []) "2Thess.2.17"
  ∷ word (ἀ ∷ γ ∷ α ∷ θ ∷ ῷ ∷ []) "2Thess.2.17"
  ∷ word (Τ ∷ ὸ ∷ []) "2Thess.3.1"
  ∷ word (∙λ ∷ ο ∷ ι ∷ π ∷ ὸ ∷ ν ∷ []) "2Thess.3.1"
  ∷ word (π ∷ ρ ∷ ο ∷ σ ∷ ε ∷ ύ ∷ χ ∷ ε ∷ σ ∷ θ ∷ ε ∷ []) "2Thess.3.1"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ ο ∷ ί ∷ []) "2Thess.3.1"
  ∷ word (π ∷ ε ∷ ρ ∷ ὶ ∷ []) "2Thess.3.1"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.3.1"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "2Thess.3.1"
  ∷ word (ὁ ∷ []) "2Thess.3.1"
  ∷ word (∙λ ∷ ό ∷ γ ∷ ο ∷ ς ∷ []) "2Thess.3.1"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.3.1"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Thess.3.1"
  ∷ word (τ ∷ ρ ∷ έ ∷ χ ∷ ῃ ∷ []) "2Thess.3.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.3.1"
  ∷ word (δ ∷ ο ∷ ξ ∷ ά ∷ ζ ∷ η ∷ τ ∷ α ∷ ι ∷ []) "2Thess.3.1"
  ∷ word (κ ∷ α ∷ θ ∷ ὼ ∷ ς ∷ []) "2Thess.3.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.3.1"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "2Thess.3.1"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.3.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.3.2"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "2Thess.3.2"
  ∷ word (ῥ ∷ υ ∷ σ ∷ θ ∷ ῶ ∷ μ ∷ ε ∷ ν ∷ []) "2Thess.3.2"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "2Thess.3.2"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "2Thess.3.2"
  ∷ word (ἀ ∷ τ ∷ ό ∷ π ∷ ω ∷ ν ∷ []) "2Thess.3.2"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.3.2"
  ∷ word (π ∷ ο ∷ ν ∷ η ∷ ρ ∷ ῶ ∷ ν ∷ []) "2Thess.3.2"
  ∷ word (ἀ ∷ ν ∷ θ ∷ ρ ∷ ώ ∷ π ∷ ω ∷ ν ∷ []) "2Thess.3.2"
  ∷ word (ο ∷ ὐ ∷ []) "2Thess.3.2"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "2Thess.3.2"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ω ∷ ν ∷ []) "2Thess.3.2"
  ∷ word (ἡ ∷ []) "2Thess.3.2"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ι ∷ ς ∷ []) "2Thess.3.2"
  ∷ word (π ∷ ι ∷ σ ∷ τ ∷ ὸ ∷ ς ∷ []) "2Thess.3.3"
  ∷ word (δ ∷ έ ∷ []) "2Thess.3.3"
  ∷ word (ἐ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "2Thess.3.3"
  ∷ word (ὁ ∷ []) "2Thess.3.3"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ς ∷ []) "2Thess.3.3"
  ∷ word (ὃ ∷ ς ∷ []) "2Thess.3.3"
  ∷ word (σ ∷ τ ∷ η ∷ ρ ∷ ί ∷ ξ ∷ ε ∷ ι ∷ []) "2Thess.3.3"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.3.3"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.3.3"
  ∷ word (φ ∷ υ ∷ ∙λ ∷ ά ∷ ξ ∷ ε ∷ ι ∷ []) "2Thess.3.3"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "2Thess.3.3"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.3.3"
  ∷ word (π ∷ ο ∷ ν ∷ η ∷ ρ ∷ ο ∷ ῦ ∷ []) "2Thess.3.3"
  ∷ word (π ∷ ε ∷ π ∷ ο ∷ ί ∷ θ ∷ α ∷ μ ∷ ε ∷ ν ∷ []) "2Thess.3.4"
  ∷ word (δ ∷ ὲ ∷ []) "2Thess.3.4"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.3.4"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ῳ ∷ []) "2Thess.3.4"
  ∷ word (ἐ ∷ φ ∷ []) "2Thess.3.4"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.3.4"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2Thess.3.4"
  ∷ word (ἃ ∷ []) "2Thess.3.4"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ γ ∷ γ ∷ έ ∷ ∙λ ∷ ∙λ ∷ ο ∷ μ ∷ ε ∷ ν ∷ []) "2Thess.3.4"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.3.4"
  ∷ word (π ∷ ο ∷ ι ∷ ε ∷ ῖ ∷ τ ∷ ε ∷ []) "2Thess.3.4"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.3.4"
  ∷ word (π ∷ ο ∷ ι ∷ ή ∷ σ ∷ ε ∷ τ ∷ ε ∷ []) "2Thess.3.4"
  ∷ word (ὁ ∷ []) "2Thess.3.5"
  ∷ word (δ ∷ ὲ ∷ []) "2Thess.3.5"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ς ∷ []) "2Thess.3.5"
  ∷ word (κ ∷ α ∷ τ ∷ ε ∷ υ ∷ θ ∷ ύ ∷ ν ∷ α ∷ ι ∷ []) "2Thess.3.5"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.3.5"
  ∷ word (τ ∷ ὰ ∷ ς ∷ []) "2Thess.3.5"
  ∷ word (κ ∷ α ∷ ρ ∷ δ ∷ ί ∷ α ∷ ς ∷ []) "2Thess.3.5"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Thess.3.5"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Thess.3.5"
  ∷ word (ἀ ∷ γ ∷ ά ∷ π ∷ η ∷ ν ∷ []) "2Thess.3.5"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.3.5"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "2Thess.3.5"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.3.5"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Thess.3.5"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Thess.3.5"
  ∷ word (ὑ ∷ π ∷ ο ∷ μ ∷ ο ∷ ν ∷ ὴ ∷ ν ∷ []) "2Thess.3.5"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.3.5"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Thess.3.5"
  ∷ word (Π ∷ α ∷ ρ ∷ α ∷ γ ∷ γ ∷ έ ∷ ∙λ ∷ ∙λ ∷ ο ∷ μ ∷ ε ∷ ν ∷ []) "2Thess.3.6"
  ∷ word (δ ∷ ὲ ∷ []) "2Thess.3.6"
  ∷ word (ὑ ∷ μ ∷ ῖ ∷ ν ∷ []) "2Thess.3.6"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ ο ∷ ί ∷ []) "2Thess.3.6"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.3.6"
  ∷ word (ὀ ∷ ν ∷ ό ∷ μ ∷ α ∷ τ ∷ ι ∷ []) "2Thess.3.6"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.3.6"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Thess.3.6"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.3.6"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Thess.3.6"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Thess.3.6"
  ∷ word (σ ∷ τ ∷ έ ∷ ∙λ ∷ ∙λ ∷ ε ∷ σ ∷ θ ∷ α ∷ ι ∷ []) "2Thess.3.6"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.3.6"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "2Thess.3.6"
  ∷ word (π ∷ α ∷ ν ∷ τ ∷ ὸ ∷ ς ∷ []) "2Thess.3.6"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ ο ∷ ῦ ∷ []) "2Thess.3.6"
  ∷ word (ἀ ∷ τ ∷ ά ∷ κ ∷ τ ∷ ω ∷ ς ∷ []) "2Thess.3.6"
  ∷ word (π ∷ ε ∷ ρ ∷ ι ∷ π ∷ α ∷ τ ∷ ο ∷ ῦ ∷ ν ∷ τ ∷ ο ∷ ς ∷ []) "2Thess.3.6"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.3.6"
  ∷ word (μ ∷ ὴ ∷ []) "2Thess.3.6"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "2Thess.3.6"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Thess.3.6"
  ∷ word (π ∷ α ∷ ρ ∷ ά ∷ δ ∷ ο ∷ σ ∷ ι ∷ ν ∷ []) "2Thess.3.6"
  ∷ word (ἣ ∷ ν ∷ []) "2Thess.3.6"
  ∷ word (π ∷ α ∷ ρ ∷ ε ∷ ∙λ ∷ ά ∷ β ∷ ο ∷ σ ∷ α ∷ ν ∷ []) "2Thess.3.6"
  ∷ word (π ∷ α ∷ ρ ∷ []) "2Thess.3.6"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.3.6"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ὶ ∷ []) "2Thess.3.7"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "2Thess.3.7"
  ∷ word (ο ∷ ἴ ∷ δ ∷ α ∷ τ ∷ ε ∷ []) "2Thess.3.7"
  ∷ word (π ∷ ῶ ∷ ς ∷ []) "2Thess.3.7"
  ∷ word (δ ∷ ε ∷ ῖ ∷ []) "2Thess.3.7"
  ∷ word (μ ∷ ι ∷ μ ∷ ε ∷ ῖ ∷ σ ∷ θ ∷ α ∷ ι ∷ []) "2Thess.3.7"
  ∷ word (ἡ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.3.7"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2Thess.3.7"
  ∷ word (ο ∷ ὐ ∷ κ ∷ []) "2Thess.3.7"
  ∷ word (ἠ ∷ τ ∷ α ∷ κ ∷ τ ∷ ή ∷ σ ∷ α ∷ μ ∷ ε ∷ ν ∷ []) "2Thess.3.7"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.3.7"
  ∷ word (ὑ ∷ μ ∷ ῖ ∷ ν ∷ []) "2Thess.3.7"
  ∷ word (ο ∷ ὐ ∷ δ ∷ ὲ ∷ []) "2Thess.3.8"
  ∷ word (δ ∷ ω ∷ ρ ∷ ε ∷ ὰ ∷ ν ∷ []) "2Thess.3.8"
  ∷ word (ἄ ∷ ρ ∷ τ ∷ ο ∷ ν ∷ []) "2Thess.3.8"
  ∷ word (ἐ ∷ φ ∷ ά ∷ γ ∷ ο ∷ μ ∷ ε ∷ ν ∷ []) "2Thess.3.8"
  ∷ word (π ∷ α ∷ ρ ∷ ά ∷ []) "2Thess.3.8"
  ∷ word (τ ∷ ι ∷ ν ∷ ο ∷ ς ∷ []) "2Thess.3.8"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ []) "2Thess.3.8"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.3.8"
  ∷ word (κ ∷ ό ∷ π ∷ ῳ ∷ []) "2Thess.3.8"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.3.8"
  ∷ word (μ ∷ ό ∷ χ ∷ θ ∷ ῳ ∷ []) "2Thess.3.8"
  ∷ word (ν ∷ υ ∷ κ ∷ τ ∷ ὸ ∷ ς ∷ []) "2Thess.3.8"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.3.8"
  ∷ word (ἡ ∷ μ ∷ έ ∷ ρ ∷ α ∷ ς ∷ []) "2Thess.3.8"
  ∷ word (ἐ ∷ ρ ∷ γ ∷ α ∷ ζ ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ι ∷ []) "2Thess.3.8"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "2Thess.3.8"
  ∷ word (τ ∷ ὸ ∷ []) "2Thess.3.8"
  ∷ word (μ ∷ ὴ ∷ []) "2Thess.3.8"
  ∷ word (ἐ ∷ π ∷ ι ∷ β ∷ α ∷ ρ ∷ ῆ ∷ σ ∷ α ∷ ί ∷ []) "2Thess.3.8"
  ∷ word (τ ∷ ι ∷ ν ∷ α ∷ []) "2Thess.3.8"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.3.8"
  ∷ word (ο ∷ ὐ ∷ χ ∷ []) "2Thess.3.9"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2Thess.3.9"
  ∷ word (ο ∷ ὐ ∷ κ ∷ []) "2Thess.3.9"
  ∷ word (ἔ ∷ χ ∷ ο ∷ μ ∷ ε ∷ ν ∷ []) "2Thess.3.9"
  ∷ word (ἐ ∷ ξ ∷ ο ∷ υ ∷ σ ∷ ί ∷ α ∷ ν ∷ []) "2Thess.3.9"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ []) "2Thess.3.9"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "2Thess.3.9"
  ∷ word (ἑ ∷ α ∷ υ ∷ τ ∷ ο ∷ ὺ ∷ ς ∷ []) "2Thess.3.9"
  ∷ word (τ ∷ ύ ∷ π ∷ ο ∷ ν ∷ []) "2Thess.3.9"
  ∷ word (δ ∷ ῶ ∷ μ ∷ ε ∷ ν ∷ []) "2Thess.3.9"
  ∷ word (ὑ ∷ μ ∷ ῖ ∷ ν ∷ []) "2Thess.3.9"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2Thess.3.9"
  ∷ word (τ ∷ ὸ ∷ []) "2Thess.3.9"
  ∷ word (μ ∷ ι ∷ μ ∷ ε ∷ ῖ ∷ σ ∷ θ ∷ α ∷ ι ∷ []) "2Thess.3.9"
  ∷ word (ἡ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.3.9"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.3.10"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "2Thess.3.10"
  ∷ word (ὅ ∷ τ ∷ ε ∷ []) "2Thess.3.10"
  ∷ word (ἦ ∷ μ ∷ ε ∷ ν ∷ []) "2Thess.3.10"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "2Thess.3.10"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2Thess.3.10"
  ∷ word (τ ∷ ο ∷ ῦ ∷ τ ∷ ο ∷ []) "2Thess.3.10"
  ∷ word (π ∷ α ∷ ρ ∷ η ∷ γ ∷ γ ∷ έ ∷ ∙λ ∷ ∙λ ∷ ο ∷ μ ∷ ε ∷ ν ∷ []) "2Thess.3.10"
  ∷ word (ὑ ∷ μ ∷ ῖ ∷ ν ∷ []) "2Thess.3.10"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2Thess.3.10"
  ∷ word (ε ∷ ἴ ∷ []) "2Thess.3.10"
  ∷ word (τ ∷ ι ∷ ς ∷ []) "2Thess.3.10"
  ∷ word (ο ∷ ὐ ∷ []) "2Thess.3.10"
  ∷ word (θ ∷ έ ∷ ∙λ ∷ ε ∷ ι ∷ []) "2Thess.3.10"
  ∷ word (ἐ ∷ ρ ∷ γ ∷ ά ∷ ζ ∷ ε ∷ σ ∷ θ ∷ α ∷ ι ∷ []) "2Thess.3.10"
  ∷ word (μ ∷ η ∷ δ ∷ ὲ ∷ []) "2Thess.3.10"
  ∷ word (ἐ ∷ σ ∷ θ ∷ ι ∷ έ ∷ τ ∷ ω ∷ []) "2Thess.3.10"
  ∷ word (ἀ ∷ κ ∷ ο ∷ ύ ∷ ο ∷ μ ∷ ε ∷ ν ∷ []) "2Thess.3.11"
  ∷ word (γ ∷ ά ∷ ρ ∷ []) "2Thess.3.11"
  ∷ word (τ ∷ ι ∷ ν ∷ α ∷ ς ∷ []) "2Thess.3.11"
  ∷ word (π ∷ ε ∷ ρ ∷ ι ∷ π ∷ α ∷ τ ∷ ο ∷ ῦ ∷ ν ∷ τ ∷ α ∷ ς ∷ []) "2Thess.3.11"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.3.11"
  ∷ word (ὑ ∷ μ ∷ ῖ ∷ ν ∷ []) "2Thess.3.11"
  ∷ word (ἀ ∷ τ ∷ ά ∷ κ ∷ τ ∷ ω ∷ ς ∷ []) "2Thess.3.11"
  ∷ word (μ ∷ η ∷ δ ∷ ὲ ∷ ν ∷ []) "2Thess.3.11"
  ∷ word (ἐ ∷ ρ ∷ γ ∷ α ∷ ζ ∷ ο ∷ μ ∷ έ ∷ ν ∷ ο ∷ υ ∷ ς ∷ []) "2Thess.3.11"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "2Thess.3.11"
  ∷ word (π ∷ ε ∷ ρ ∷ ι ∷ ε ∷ ρ ∷ γ ∷ α ∷ ζ ∷ ο ∷ μ ∷ έ ∷ ν ∷ ο ∷ υ ∷ ς ∷ []) "2Thess.3.11"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2Thess.3.12"
  ∷ word (δ ∷ ὲ ∷ []) "2Thess.3.12"
  ∷ word (τ ∷ ο ∷ ι ∷ ο ∷ ύ ∷ τ ∷ ο ∷ ι ∷ ς ∷ []) "2Thess.3.12"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ γ ∷ γ ∷ έ ∷ ∙λ ∷ ∙λ ∷ ο ∷ μ ∷ ε ∷ ν ∷ []) "2Thess.3.12"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.3.12"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ κ ∷ α ∷ ∙λ ∷ ο ∷ ῦ ∷ μ ∷ ε ∷ ν ∷ []) "2Thess.3.12"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.3.12"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ῳ ∷ []) "2Thess.3.12"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Thess.3.12"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ῷ ∷ []) "2Thess.3.12"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "2Thess.3.12"
  ∷ word (μ ∷ ε ∷ τ ∷ ὰ ∷ []) "2Thess.3.12"
  ∷ word (ἡ ∷ σ ∷ υ ∷ χ ∷ ί ∷ α ∷ ς ∷ []) "2Thess.3.12"
  ∷ word (ἐ ∷ ρ ∷ γ ∷ α ∷ ζ ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ι ∷ []) "2Thess.3.12"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "2Thess.3.12"
  ∷ word (ἑ ∷ α ∷ υ ∷ τ ∷ ῶ ∷ ν ∷ []) "2Thess.3.12"
  ∷ word (ἄ ∷ ρ ∷ τ ∷ ο ∷ ν ∷ []) "2Thess.3.12"
  ∷ word (ἐ ∷ σ ∷ θ ∷ ί ∷ ω ∷ σ ∷ ι ∷ ν ∷ []) "2Thess.3.12"
  ∷ word (ὑ ∷ μ ∷ ε ∷ ῖ ∷ ς ∷ []) "2Thess.3.13"
  ∷ word (δ ∷ έ ∷ []) "2Thess.3.13"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ ο ∷ ί ∷ []) "2Thess.3.13"
  ∷ word (μ ∷ ὴ ∷ []) "2Thess.3.13"
  ∷ word (ἐ ∷ γ ∷ κ ∷ α ∷ κ ∷ ή ∷ σ ∷ η ∷ τ ∷ ε ∷ []) "2Thess.3.13"
  ∷ word (κ ∷ α ∷ ∙λ ∷ ο ∷ π ∷ ο ∷ ι ∷ ο ∷ ῦ ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "2Thess.3.13"
  ∷ word (Ε ∷ ἰ ∷ []) "2Thess.3.14"
  ∷ word (δ ∷ έ ∷ []) "2Thess.3.14"
  ∷ word (τ ∷ ι ∷ ς ∷ []) "2Thess.3.14"
  ∷ word (ο ∷ ὐ ∷ χ ∷ []) "2Thess.3.14"
  ∷ word (ὑ ∷ π ∷ α ∷ κ ∷ ο ∷ ύ ∷ ε ∷ ι ∷ []) "2Thess.3.14"
  ∷ word (τ ∷ ῷ ∷ []) "2Thess.3.14"
  ∷ word (∙λ ∷ ό ∷ γ ∷ ῳ ∷ []) "2Thess.3.14"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.3.14"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "2Thess.3.14"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Thess.3.14"
  ∷ word (ἐ ∷ π ∷ ι ∷ σ ∷ τ ∷ ο ∷ ∙λ ∷ ῆ ∷ ς ∷ []) "2Thess.3.14"
  ∷ word (τ ∷ ο ∷ ῦ ∷ τ ∷ ο ∷ ν ∷ []) "2Thess.3.14"
  ∷ word (σ ∷ η ∷ μ ∷ ε ∷ ι ∷ ο ∷ ῦ ∷ σ ∷ θ ∷ ε ∷ []) "2Thess.3.14"
  ∷ word (μ ∷ ὴ ∷ []) "2Thess.3.14"
  ∷ word (σ ∷ υ ∷ ν ∷ α ∷ ν ∷ α ∷ μ ∷ ί ∷ γ ∷ ν ∷ υ ∷ σ ∷ θ ∷ α ∷ ι ∷ []) "2Thess.3.14"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῷ ∷ []) "2Thess.3.14"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "2Thess.3.14"
  ∷ word (ἐ ∷ ν ∷ τ ∷ ρ ∷ α ∷ π ∷ ῇ ∷ []) "2Thess.3.14"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2Thess.3.15"
  ∷ word (μ ∷ ὴ ∷ []) "2Thess.3.15"
  ∷ word (ὡ ∷ ς ∷ []) "2Thess.3.15"
  ∷ word (ἐ ∷ χ ∷ θ ∷ ρ ∷ ὸ ∷ ν ∷ []) "2Thess.3.15"
  ∷ word (ἡ ∷ γ ∷ ε ∷ ῖ ∷ σ ∷ θ ∷ ε ∷ []) "2Thess.3.15"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "2Thess.3.15"
  ∷ word (ν ∷ ο ∷ υ ∷ θ ∷ ε ∷ τ ∷ ε ∷ ῖ ∷ τ ∷ ε ∷ []) "2Thess.3.15"
  ∷ word (ὡ ∷ ς ∷ []) "2Thess.3.15"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ ό ∷ ν ∷ []) "2Thess.3.15"
  ∷ word (Α ∷ ὐ ∷ τ ∷ ὸ ∷ ς ∷ []) "2Thess.3.16"
  ∷ word (δ ∷ ὲ ∷ []) "2Thess.3.16"
  ∷ word (ὁ ∷ []) "2Thess.3.16"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ς ∷ []) "2Thess.3.16"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2Thess.3.16"
  ∷ word (ε ∷ ἰ ∷ ρ ∷ ή ∷ ν ∷ η ∷ ς ∷ []) "2Thess.3.16"
  ∷ word (δ ∷ ῴ ∷ η ∷ []) "2Thess.3.16"
  ∷ word (ὑ ∷ μ ∷ ῖ ∷ ν ∷ []) "2Thess.3.16"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2Thess.3.16"
  ∷ word (ε ∷ ἰ ∷ ρ ∷ ή ∷ ν ∷ η ∷ ν ∷ []) "2Thess.3.16"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "2Thess.3.16"
  ∷ word (π ∷ α ∷ ν ∷ τ ∷ ὸ ∷ ς ∷ []) "2Thess.3.16"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.3.16"
  ∷ word (π ∷ α ∷ ν ∷ τ ∷ ὶ ∷ []) "2Thess.3.16"
  ∷ word (τ ∷ ρ ∷ ό ∷ π ∷ ῳ ∷ []) "2Thess.3.16"
  ∷ word (ὁ ∷ []) "2Thess.3.16"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ς ∷ []) "2Thess.3.16"
  ∷ word (μ ∷ ε ∷ τ ∷ ὰ ∷ []) "2Thess.3.16"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ω ∷ ν ∷ []) "2Thess.3.16"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.3.16"
  ∷ word (Ὁ ∷ []) "2Thess.3.17"
  ∷ word (ἀ ∷ σ ∷ π ∷ α ∷ σ ∷ μ ∷ ὸ ∷ ς ∷ []) "2Thess.3.17"
  ∷ word (τ ∷ ῇ ∷ []) "2Thess.3.17"
  ∷ word (ἐ ∷ μ ∷ ῇ ∷ []) "2Thess.3.17"
  ∷ word (χ ∷ ε ∷ ι ∷ ρ ∷ ὶ ∷ []) "2Thess.3.17"
  ∷ word (Π ∷ α ∷ ύ ∷ ∙λ ∷ ο ∷ υ ∷ []) "2Thess.3.17"
  ∷ word (ὅ ∷ []) "2Thess.3.17"
  ∷ word (ἐ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "2Thess.3.17"
  ∷ word (σ ∷ η ∷ μ ∷ ε ∷ ῖ ∷ ο ∷ ν ∷ []) "2Thess.3.17"
  ∷ word (ἐ ∷ ν ∷ []) "2Thess.3.17"
  ∷ word (π ∷ ά ∷ σ ∷ ῃ ∷ []) "2Thess.3.17"
  ∷ word (ἐ ∷ π ∷ ι ∷ σ ∷ τ ∷ ο ∷ ∙λ ∷ ῇ ∷ []) "2Thess.3.17"
  ∷ word (ο ∷ ὕ ∷ τ ∷ ω ∷ ς ∷ []) "2Thess.3.17"
  ∷ word (γ ∷ ρ ∷ ά ∷ φ ∷ ω ∷ []) "2Thess.3.17"
  ∷ word (ἡ ∷ []) "2Thess.3.18"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ ς ∷ []) "2Thess.3.18"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2Thess.3.18"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "2Thess.3.18"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.3.18"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2Thess.3.18"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "2Thess.3.18"
  ∷ word (μ ∷ ε ∷ τ ∷ ὰ ∷ []) "2Thess.3.18"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ω ∷ ν ∷ []) "2Thess.3.18"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "2Thess.3.18"
  ∷ []

max_stars_repo_name: scott-fleischman/GreekGrammar

max_issues_repo_name: scott-fleischman/GreekGrammar

max_forks_repo_name: scott-fleischman/GreekGrammar


text:
open import Data.Empty
open import Data.Maybe
open import Data.Product
open import Data.Unit

open import Axiom.Extensionality.Propositional
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary
open import Relation.Nullary.Negation

open import EffectAnnotations
open import Types

module AEff where

-- ARITY ASSIGNMENT TO SIGNATURES OF SIGNALS, INTERRUPTS, AND BASE CONSTANTS

postulate payload : Σₛ → Σ VType (λ X → mobile X)     -- payload type assignment for signal and interrupt names

postulate Σ-base : Set             -- set of base constants
postulate ar-base : Σ-base → BType -- arity assignment to base constants

-- CONTEXTS

data Ctx : Set where
  []  : Ctx
  _∷_ : Ctx → VType → Ctx
  _■  : Ctx → Ctx

infixl 35 _∷_
infixl 35 _■

_++ₖ_ : Ctx → Ctx → Ctx
Γ ++ₖ [] = Γ
Γ ++ₖ (Γ' ∷ X) = (Γ ++ₖ Γ') ∷ X
Γ ++ₖ (Γ' ■) = (Γ ++ₖ Γ') ■

infixl 30 _++ₖ_

-- VARIABLES IN CONTEXTS (I.E., DE BRUIJN INDICES)

data _∈_ (X : VType) : Ctx → Set where
  Hd   : {Γ : Ctx} → X ∈ (Γ ∷ X)
  Tl-v : {Γ : Ctx} {Y : VType} → X ∈ Γ → X ∈ (Γ ∷ Y)
  Tl-■ : {Γ : Ctx} → mobile X → X ∈ Γ → X ∈ (Γ ■)

-- DERIVATIONS OF WELL-TYPED TERMS

mutual

  data _⊢V⦂_ (Γ : Ctx) : VType → Set where

    `_  : {X : VType} →
          X ∈ Γ →
          -------------
          Γ ⊢V⦂ X

    ´_  : (c : Σ-base) →
          --------------
          Γ ⊢V⦂ ``(ar-base c)

    ⋆   : Γ ⊢V⦂ 𝟙

    ƛ   : {X : VType}
          {C : CType} →
          Γ ∷ X ⊢C⦂ C →
          -------------
          Γ ⊢V⦂ X ⇒ C

    ⟨_⟩ : {X : VType} →
          Γ ⊢V⦂ X →
          -------------
          Γ ⊢V⦂ ⟨ X ⟩

    □   : {X : VType} →
          Γ ■ ⊢V⦂ X →
          -------------
          Γ ⊢V⦂ □ X

  infix 40 _·_

  data _⊢C⦂_ (Γ : Ctx) : CType → Set where

    return           : {X : VType}
                       {o : O}
                       {i : I} →
                       Γ ⊢V⦂ X →
                       -----------------
                       Γ ⊢C⦂ X ! (o , i)

    let=_`in_        : {X Y : VType}
                       {o : O}
                       {i : I} →
                       Γ ⊢C⦂ X ! (o , i) →
                       Γ ∷ X ⊢C⦂ Y ! (o , i) →
                       -----------------------
                       Γ ⊢C⦂ Y ! (o , i)

    _·_              : {X : VType}
                       {C : CType} →
                       Γ ⊢V⦂ X ⇒ C →
                       Γ ⊢V⦂ X →
                       -------------
                       Γ ⊢C⦂ C

    ↑                : {X : VType}
                       {o : O}
                       {i : I} →
                       (op : Σₛ) →
                       op ∈ₒ o →
                       Γ ⊢V⦂ proj₁ (payload op) →
                       Γ ⊢C⦂ X ! (o , i) →
                       --------------------------
                       Γ ⊢C⦂ X ! (o , i)

    ↓                : {X : VType}
                       {o : O}
                       {i : I}
                       (op : Σₛ) →
                       Γ ⊢V⦂ proj₁ (payload op) →
                       Γ ⊢C⦂ X ! (o , i) →
                       --------------------------
                       Γ ⊢C⦂ X ! op ↓ₑ (o , i)

    promise_∣_↦_`in_ : {X Y : VType}
                       {o o' : O}
                       {i i' : I} →
                       (op : Σₛ) →
                       (o' , i') ⊑ lkpᵢ op i  →
                       Γ ∷ proj₁ (payload op) ∷ (𝟙 ⇒ (⟨ X ⟩ ! (∅ₒ , ∅ᵢ [ op ↦ just (o' , i') ]ᵢ))) ⊢C⦂ ⟨ X ⟩ ! (o' , i') →
                       Γ ∷ ⟨ X ⟩ ⊢C⦂ Y ! (o , i) →
                       ---------------------------------------------------------------------------------------------------
                       Γ ⊢C⦂ Y ! (o , i)

    await_until_     : {X : VType}
                       {C : CType} →
                       Γ ⊢V⦂ ⟨ X ⟩ →
                       Γ ∷ X ⊢C⦂ C →
                       --------------
                       Γ ⊢C⦂ C

    unbox_`in_       : {X : VType}
                       {C : CType} →
                       Γ ⊢V⦂ □ X →
                       Γ ∷ X ⊢C⦂ C →
                       -------------
                       Γ ⊢C⦂ C

    spawn            : {C D : CType} →
                       Γ ■ ⊢C⦂ C →
                       Γ ⊢C⦂ D →
                       ---------------------
                       Γ ⊢C⦂ D

    coerce           : {X : VType}
                       {o o' : O}
                       {i i' : I} →
                       o ⊑ₒ o' →
                       i ⊑ᵢ i' →
                       Γ ⊢C⦂ X ! (o , i) →
                       -------------------
                       Γ ⊢C⦂ X ! (o' , i')

-- DERIVATIONS OF WELL-TYPED PROCESSES

infix 10 _⊢P⦂_

data _⊢P⦂_ (Γ : Ctx) : {o : O} → PType o → Set where

  run     : {X : VType}
            {o : O}
            {i : I} →
            Γ ⊢C⦂ X ! (o , i) →
            -------------------
            Γ ⊢P⦂ X ‼ o , i

  _∥_     : {o o' : O}
            {PP : PType o} →
            {QQ : PType o'} →
            Γ ⊢P⦂ PP →
            Γ ⊢P⦂ QQ →
            -----------------
            Γ ⊢P⦂ (PP ∥ QQ)

  ↑       : {o : O} →
            {PP : PType o}
            (op : Σₛ) →
            op ∈ₒ o →
            Γ ⊢V⦂ (proj₁ (payload op)) →
            Γ ⊢P⦂ PP →
            ----------------------------
            Γ ⊢P⦂ PP

  ↓       : {o : O}
            {PP : PType o}
            (op : Σₛ) →
            Γ ⊢V⦂ (proj₁ (payload op)) →
            Γ ⊢P⦂ PP →
            ----------------------------
            Γ ⊢P⦂ op ↓ₚ PP

-- ADMISSIBLE TYPING RULES

■-dup-var : {Γ Γ' : Ctx} {X : VType} →
            X ∈ (Γ ■ ++ₖ Γ') →
            --------------------------
            X ∈ (Γ ■ ■ ++ₖ Γ')

■-dup-var {Γ} {[]} (Tl-■ p x) =
  Tl-■ p (Tl-■ p x)
■-dup-var {Γ} {Γ' ∷ Y} Hd =
  Hd
■-dup-var {Γ} {Γ' ∷ Y} (Tl-v x) =
  Tl-v (■-dup-var x)
■-dup-var {Γ} {Γ' ■} (Tl-■ p x) =
  Tl-■ p (■-dup-var x)

mutual

  ■-dup-v : {Γ Γ' : Ctx} {X : VType} →
            (Γ ■ ++ₖ Γ') ⊢V⦂ X →
            --------------------------
            (Γ ■ ■ ++ₖ Γ') ⊢V⦂ X

  ■-dup-v (` x) =
    ` ■-dup-var x
  ■-dup-v (´ c) =
    ´ c
  ■-dup-v ⋆ =
    ⋆
  ■-dup-v (ƛ M) =
    ƛ (■-dup-c M)
  ■-dup-v ⟨ V ⟩ =
    ⟨ ■-dup-v V ⟩
  ■-dup-v (□ V) =
    □ (■-dup-v {Γ' = _ ■} V)

  ■-dup-c : {Γ Γ' : Ctx} {C : CType} →
            (Γ ■ ++ₖ Γ') ⊢C⦂ C →
            --------------------------
            (Γ ■ ■ ++ₖ Γ') ⊢C⦂ C

  ■-dup-c (return V) =
    return (■-dup-v V)
  ■-dup-c (let= M `in N) =
    let= (■-dup-c M) `in (■-dup-c N)
  ■-dup-c (V · W) =
    (■-dup-v V) · (■-dup-v W)
  ■-dup-c (↑ op p V M) =
    ↑ op p (■-dup-v V) (■-dup-c M)
  ■-dup-c (↓ op V M) =
    ↓ op (■-dup-v V) (■-dup-c M)
  ■-dup-c (promise op ∣ x ↦ M `in N) =
    promise op ∣ x ↦ (■-dup-c M) `in (■-dup-c N)
  ■-dup-c (await V until M) =
    await (■-dup-v V) until (■-dup-c M)
  ■-dup-c (unbox V `in M) =
    unbox (■-dup-v V) `in (■-dup-c M)
  ■-dup-c (spawn M N) =
    spawn (■-dup-c {Γ' = _ ■} M) (■-dup-c N)
  ■-dup-c (coerce p q M) =
    coerce p q (■-dup-c M)

■-wk : {Γ : Ctx} {X : VType} →
       mobile X →
       Γ ⊢V⦂ X →
       -----------------------
       Γ ■ ⊢V⦂ X

■-wk p (` x) =
  ` Tl-■ p x
■-wk p (´ c) =
  ´ c
■-wk p ⋆ =
  ⋆
■-wk p (□ V) =
  □ (■-dup-v {_} {[]} V)

■-str-var : {Γ Γ' : Ctx} {X : VType} →
            X ∈ Γ ■ ++ₖ Γ' →
            --------------------------
            X ∈ Γ ++ₖ Γ'

■-str-var {Γ} {[]} (Tl-■ p x) =
  x
■-str-var {Γ} {Γ' ∷ Y} Hd =
  Hd
■-str-var {Γ} {Γ' ∷ Y} (Tl-v x) =
  Tl-v (■-str-var x)
■-str-var {Γ} {Γ' ■} (Tl-■ p x) =
  Tl-■ p (■-str-var x)

mutual

  ■-str-v : {Γ Γ' : Ctx} {X : VType} →
            Γ ■ ++ₖ Γ' ⊢V⦂ X →
            -----------------------
            Γ ++ₖ Γ' ⊢V⦂ X

  ■-str-v (` x) =
    ` ■-str-var x
  ■-str-v (´ c) =
    ´ c
  ■-str-v ⋆ =
    ⋆
  ■-str-v (ƛ M) =
    ƛ (■-str-c M)
  ■-str-v ⟨ V ⟩ =
    ⟨ ■-str-v V ⟩
  ■-str-v {Γ} {Γ'} (□ V) =
    □ (■-str-v {Γ' = _ ■} V)

  ■-str-c : {Γ Γ' : Ctx} {C : CType} →
            Γ ■ ++ₖ Γ' ⊢C⦂ C →
            -----------------------
            Γ ++ₖ Γ' ⊢C⦂ C

  ■-str-c (return V) =
    return (■-str-v V)
  ■-str-c (let= M `in N) =
    let= (■-str-c M) `in (■-str-c N)
  ■-str-c (V · W) =
    (■-str-v V) · (■-str-v W)
  ■-str-c (↑ op p V M) =
    ↑ op p (■-str-v V) (■-str-c M)
  ■-str-c (↓ op V M) =
    ↓ op (■-str-v V) (■-str-c M)
  ■-str-c (promise op ∣ r ↦ M `in N) =
    promise op ∣ r ↦ (■-str-c M) `in (■-str-c N)
  ■-str-c (await V until M) =
    await (■-str-v V) until (■-str-c M)
  ■-str-c (unbox V `in M) =
    unbox (■-str-v V) `in (■-str-c M)
  ■-str-c (spawn M N) =
    spawn (■-str-c {Γ' = _ ■} M) (■-str-c N)
  ■-str-c (coerce p q M) =
    coerce p q (■-str-c M)

ext: agda

max_stars_repo_name: danelahman/higher-order-aeff-agda

max_issues_repo_name: danelahman/modal-aeff-agda

max_forks_repo_name: danelahman/modal-aeff-agda


text:
module BadInductionRecursion3 where

data Bool : Set where
  false : Bool
  true  : Bool

data Two : Bool -> Set where
  zero : Two false
  suc  : Two false -> Two true

mutual
  data D : Set where
    d : forall u -> D′ true u -> D

  D′ : forall b -> Two b -> Set
  D′ ._ zero    = D
  D′ ._ (suc n) = D′ _ n -> Bool

_·_ : D -> D -> D
d (suc zero) f · x = f x

ω : D
ω = d (suc zero) (\x -> x · x)

Ω : D
Ω = ω · ω


text:
-- MIT License

-- Copyright (c) 2021 Luca Ciccone and Luca Padovani

-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:

-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

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

open import Size

open import Data.Empty
open import Data.Product
open import Data.Sum
open import Data.List using ([]; _∷_; _∷ʳ_; _++_)

open import Codata.Thunk

open import Relation.Nullary
open import Relation.Nullary.Negation using (contraposition)
open import Relation.Unary using (_∈_; _⊆_)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (Star; ε; _◅_; return)

open import Function.Base using (case_of_)

open import Common

module FairSubtyping {ℙ : Set} (message : Message ℙ) where

open import Trace message
open import SessionType message
open import Transitions message
open import Session message
open import Compliance message
open import HasTrace message
open import TraceInclusion message
open import Convergence message
open import FairCompliance message

data FairSub : SessionType -> SessionType -> Size -> Set where
  nil<|any : ∀{T i} -> FairSub nil T i
  end<|def : ∀{T S i} (e : End T) (def : Defined S) -> FairSub T S i
  inp<|inp :
    ∀{f g i}
    (con : inp f ↓ inp g)
    (inc : dom f ⊆ dom g)
    (F : (x : ℙ) -> Thunk (FairSub (f x .force) (g x .force)) i) ->
    FairSub (inp f) (inp g) i
  out<|out :
    ∀{f g i}
    (con : out f ↓ out g)
    (W : Witness g)
    (inc : dom g ⊆ dom f)
    (F : ∀{x} (!x : x ∈ dom g) -> Thunk (FairSub (f x .force) (g x .force)) i) ->
    FairSub (out f) (out g) i

_<|_ : SessionType -> SessionType -> Set
_<|_ T S = FairSub T S ∞

-- sub-defined : ∀{T S} -> T <| S -> Defined T -> Defined S
-- sub-defined (end<|def _ def) _ = def
-- sub-defined (inp<|inp _ _) _   = inp
-- sub-defined (out<|out _ _ _) _ = out

fs->convergence : ∀{T S} -> T <| S -> T ↓ S
fs->convergence nil<|any = inclusion->convergence nil<=any
fs->convergence (end<|def e def) = inclusion->convergence (end<=def e def)
fs->convergence (inp<|inp con inc F) = con
fs->convergence (out<|out con W inc F) = con

fc-not-transition+end :
  ∀{R R' T α} ->
  FairComplianceS (R # T) ->
  Transition R α R' ->
  End T ->
  ⊥
fc-not-transition+end comp inp (inp U) with comp ε
... | _ , ε , win#def () _
... | _ , sync () inp ◅ _ , _
fc-not-transition+end comp inp (out U) with comp ε
... | _ , ε , win#def () _
... | _ , sync _ (out fx) ◅ _ , _ = ⊥-elim (U _ fx)
fc-not-transition+end comp (out fx) (inp V) with comp ε
... | _ , ε , win#def (out U) _ = ⊥-elim (U _ fx)
... | _ , sync (out _) inp ◅ reds , win#def w def =
  let _ , rr , tr = unzip-red* reds in
  ⊥-elim (V _ (transitions+defined->defined tr def))
fc-not-transition+end comp (out fx) (out _) with comp ε
... | _ , ε , win#def (out U) _ = ⊥-elim (U _ fx)
... | _ , sync () (out _) ◅ _ , _

sub-red :
  ∀{T S S' R R' α} ->
  FairComplianceS (R # T) ->
  T <| S ->
  Transition R (co-action α) R' ->
  Transition S α S' ->
  ∃[ T' ] (Transition T α T' × T' <| S')
sub-red comp nil<|any _ _ with comp ε
... | _ , ε , win#def _ ()
... | _ , sync _ () ◅ _ , _
sub-red comp (end<|def e _) r _ = ⊥-elim (fc-not-transition+end comp r e)
sub-red comp (inp<|inp con inc F) (out {h} hx) (inp {f}) = _ , inp , F _ .force
sub-red comp (out<|out con W inc F) inp (out fx) = _ , out (inc fx) , F fx .force

sub-red* :
  ∀{T S S' R R' φ} ->
  FairComplianceS (R # T) ->
  T <| S ->
  Transitions R (co-trace φ) R' ->
  Transitions S φ S' ->
  ∃[ T' ] (Transitions T φ T' × T' <| S')
sub-red* comp sub refl refl = _ , refl , sub
sub-red* comp sub (step r rr) (step s sr) =
  let _ , t , sub' = sub-red comp sub r s in
  let comp' = fc-transitions (step r refl) (step t refl) comp in
  let _ , tr , sub'' = sub-red* comp' sub' rr sr in
  _ , step t tr , sub''

sub-sound : ∀{T S R} -> FairComplianceS (R # T) -> T <| S -> FairComplianceS (R # S)
sub-sound comp sub {_ # _} reds =
  let _ , rr , sr = unzip-red* reds in
  let _ , tr , sub' = sub-red* comp sub rr sr in
  let comp' = fair-compliance-red* comp (zip-red* rr tr) in
  con-sound (fs->convergence sub') comp'

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
-- Algorithmic equality.

{-# OPTIONS --safe #-}

module Definition.Conversion where

open import Definition.Untyped
open import Definition.Typed

open import Tools.Nat
import Tools.PropositionalEquality as PE

infix 10 _⊢_~_↑_^_
infix 10 _⊢_[conv↑]_^_
infix 10 _⊢_[conv↓]_^_
infix 10 _⊢_[conv↑]_∷_^_
infix 10 _⊢_[conv↓]_∷_^_
infix 10 _⊢_[genconv↑]_∷_^_

mutual
  -- Neutral equality.
  data _⊢_~_↑!_^_ (Γ : Con Term) : (k l A : Term) → TypeLevel → Set where
    var-refl    : ∀ {x y A l}
                → Γ ⊢ var x ∷ A ^ [ ! , l ]
                → x PE.≡ y
                → Γ ⊢ var x ~ var y ↑! A ^ l
    app-cong    : ∀ {k l t v F rF lF lG G lΠ}
                → Γ ⊢ k ~ l ↓! Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ ι lΠ
                → Γ ⊢ t [genconv↑] v ∷ F ^ [ rF , ι lF ]
                → Γ ⊢ k ∘ t ^ lΠ ~ l ∘ v ^ lΠ ↑! G [ t ] ^ ι lG
    natrec-cong : ∀ {k l h g a₀ b₀ F G lF}
                → Γ ∙ ℕ ^ [ ! , ι ⁰ ] ⊢ F [conv↑] G ^ [ ! , ι lF ]
                → Γ ⊢ a₀ [conv↑] b₀ ∷ F [ zero ] ^ ι lF
                → Γ ⊢ h [conv↑] g ∷ Π ℕ ^ ! ° ⁰ ▹ (F ^ ! ° lF ▹▹ F [ suc (var 0) ]↑ ° lF ° lF) ° lF ° lF ^ ι lF
                → Γ ⊢ k ~ l ↓! ℕ ^ ι ⁰
                → Γ ⊢ natrec lF F a₀ h k ~ natrec lF G b₀ g l ↑! F [ k ] ^ ι lF
    Emptyrec-cong : ∀ {k l F G ll lEmpty}
                  → Γ ⊢ F [conv↑] G ^ [ ! , ι ll ]
                  → Γ ⊢ k ~ l ↑% Empty lEmpty ^ ι lEmpty
                  → Γ ⊢ Emptyrec ll lEmpty F k ~ Emptyrec ll lEmpty G l ↑! F ^ ι ll
    Id-cong : ∀ {l A A' t t' u u'}
              → Γ ⊢ A ~ A' ↓! U l ^ next l
              → Γ ⊢ t [conv↑] t' ∷ A ^ ι l
              → Γ ⊢ u [conv↑] u' ∷ A ^ ι l
              → Γ ⊢ Id A t u ~ Id A' t' u' ↑! SProp l ^ next l
    Id-ℕ : ∀ {t t' u u'}
              → Γ ⊢ t ~ t' ↓! ℕ ^ ι ⁰
              → Γ ⊢ u [conv↑] u' ∷ ℕ ^ ι ⁰
              → Γ ⊢ Id ℕ t u ~ Id ℕ t' u' ↑! SProp ⁰ ^ next ⁰
    Id-ℕ0 : ∀ {t t'}
              → Γ ⊢ t ~ t' ↓! ℕ ^ ι ⁰
              → Γ ⊢ Id ℕ zero t ~ Id ℕ zero t' ↑! SProp ⁰ ^ next ⁰
    Id-ℕS : ∀ {t t' u u'}
              → Γ ⊢ t [conv↑] t' ∷ ℕ ^ ι ⁰
              → Γ ⊢ u ~ u' ↓! ℕ ^ ι ⁰
              → Γ ⊢ Id ℕ (suc t) u ~ Id ℕ (suc t') u' ↑! SProp ⁰ ^ next ⁰
    Id-U : ∀ {t t' u u'}
              → Γ ⊢ t ~ t' ↓! U ⁰ ^ ι ¹
              → Γ ⊢ u [conv↑] u' ∷ U ⁰ ^ ι ¹
              → Γ ⊢ Id (U ⁰) t u ~ Id (U ⁰) t' u' ↑! SProp ¹ ^ next ¹
    Id-Uℕ : ∀ {t t'}
              → Γ ⊢ t ~ t' ↓! U ⁰ ^ ι ¹
              → Γ ⊢ Id (U ⁰) ℕ t ~ Id (U ⁰) ℕ t' ↑! SProp ¹ ^ next ¹
    Id-UΠ : ∀ {A rA B A' B' t t'}
              → Γ ⊢ Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰  [conv↑] Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° ⁰  ∷ U ⁰ ^ ι ¹
              → Γ ⊢ t ~ t' ↓! U ⁰ ^ ι ¹
              → Γ ⊢ Id (U ⁰) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰  ) t ~ Id (U ⁰) (Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° ⁰  ) t' ↑! SProp ¹ ^ next ¹
    cast-cong : ∀ {A A' B B' t t' e e'}
              → Γ ⊢ A ~ A' ↓! U ⁰ ^ next ⁰
              → Γ ⊢ B [conv↑] B' ∷ U ⁰ ^ ι ¹
              → Γ ⊢ t [conv↑] t' ∷ A ^ ι ⁰
              → Γ ⊢ e ∷ (Id (U ⁰) A B) ^ [ % , next ⁰ ]
              → Γ ⊢ e' ∷ (Id (U ⁰) A' B') ^ [ % , next ⁰ ]
              → Γ ⊢ cast ⁰ A B e t ~ cast ⁰ A' B' e' t' ↑! B ^ ι ⁰
    cast-ℕ : ∀ {A A' t t' e e'}
              → Γ ⊢ A ~ A' ↓! U ⁰ ^ next ⁰
              → Γ ⊢ t [conv↑] t' ∷ ℕ ^ ι ⁰
              → Γ ⊢ e ∷ (Id (U ⁰) ℕ A) ^ [ % , next ⁰ ]
              → Γ ⊢ e' ∷ (Id (U ⁰) ℕ A') ^ [ % , next ⁰ ]
              → Γ ⊢ cast ⁰ ℕ A e t ~ cast ⁰ ℕ A' e' t' ↑! A ^ ι ⁰
    cast-ℕℕ : ∀ {t t' e e'}
              → Γ ⊢ t ~ t' ↓! ℕ ^ ι ⁰
              → Γ ⊢ e ∷ (Id (U ⁰) ℕ ℕ) ^ [ % , next ⁰ ]
              → Γ ⊢ e' ∷ (Id (U ⁰) ℕ ℕ) ^ [ % , next ⁰ ]
              → Γ ⊢ cast ⁰ ℕ ℕ e t ~ cast ⁰ ℕ ℕ e' t' ↑! ℕ ^ ι ⁰
    cast-Π : ∀ {A rA P A' P' B B' t t' e e'}
              → Γ ⊢ Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰  [conv↑] Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰  ∷ U ⁰ ^ next ⁰
              → Γ ⊢ B ~ B' ↓! U ⁰ ^ next ⁰
              → Γ ⊢ t [conv↑] t' ∷ Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰  ^ ι ⁰
              → Γ ⊢ e ∷ (Id (U ⁰) (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰ ) B) ^ [ % , next ⁰ ]
              → Γ ⊢ e' ∷ (Id (U ⁰) (Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰ ) B') ^ [ % , next ⁰ ]
              → Γ ⊢ cast ⁰ (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰ ) B e t ~ cast ⁰ (Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰ ) B' e' t' ↑! B ^ ι ⁰
    cast-Πℕ : ∀ {A rA P A' P' t t' e e'}
              → Γ ⊢ Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰  [conv↑] Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰  ∷ U ⁰ ^ ι ¹
              → Γ ⊢ t [conv↑] t' ∷ Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰  ^ ι ⁰
              → Γ ⊢ e ∷ (Id (U ⁰) (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰ ) ℕ) ^ [ % , next ⁰ ]
              → Γ ⊢ e' ∷ (Id (U ⁰) (Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰ ) ℕ) ^ [ % , next ⁰ ]
              → Γ ⊢ cast ⁰ (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰ ) ℕ e t ~ cast ⁰ (Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰ ) ℕ e' t' ↑! ℕ ^ ι ⁰
    cast-ℕΠ : ∀ {A rA P A' P' t t' e e'}
              → Γ ⊢ Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰  [conv↑] Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰  ∷ U ⁰ ^ ι ¹
              → Γ ⊢ t [conv↑] t' ∷ ℕ ^ ι ⁰
              → Γ ⊢ e ∷ (Id (U ⁰) ℕ (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰ )) ^ [ % , next ⁰ ]
              → Γ ⊢ e' ∷ (Id (U ⁰) ℕ (Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰ )) ^ [ % , next ⁰ ]
              → Γ ⊢ cast ⁰ ℕ (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰ ) e t ~ cast ⁰ ℕ (Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰ ) e' t' ↑! (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰ ) ^ ι ⁰
    cast-ΠΠ%! : ∀ {A P A' P' B Q B' Q' t t' e e'}
              → Γ ⊢ Π A ^ % ° ⁰ ▹ P ° ⁰ ° ⁰  [conv↑] Π A' ^ % ° ⁰ ▹ P' ° ⁰ ° ⁰  ∷ U ⁰ ^ ι ¹
              → Γ ⊢ Π B ^ ! ° ⁰ ▹ Q ° ⁰ ° ⁰  [conv↑] Π B' ^ ! ° ⁰ ▹ Q' ° ⁰ ° ⁰  ∷ U ⁰ ^ ι ¹
              → Γ ⊢ t [conv↑] t' ∷ Π A ^ % ° ⁰ ▹ P ° ⁰ ° ⁰  ^ ι ⁰
              → Γ ⊢ e ∷ (Id (U ⁰) (Π A ^ % ° ⁰ ▹ P ° ⁰ ° ⁰ ) (Π B ^ ! ° ⁰ ▹ Q ° ⁰ ° ⁰ )) ^ [ % , next ⁰ ]
              → Γ ⊢ e' ∷ (Id (U ⁰) (Π A' ^ % ° ⁰ ▹ P' ° ⁰ ° ⁰ ) (Π B' ^ ! ° ⁰ ▹ Q' ° ⁰ ° ⁰ )) ^ [ % , next ⁰ ]
              → Γ ⊢ cast ⁰ (Π A ^ % ° ⁰ ▹ P ° ⁰ ° ⁰ ) (Π B ^ ! ° ⁰ ▹ Q ° ⁰ ° ⁰ ) e t ~
                    cast ⁰ (Π A' ^ % ° ⁰ ▹ P' ° ⁰ ° ⁰ ) (Π B' ^ ! ° ⁰ ▹ Q' ° ⁰ ° ⁰ ) e' t' ↑! (Π B ^ ! ° ⁰ ▹ Q ° ⁰ ° ⁰ ) ^ ι ⁰
    cast-ΠΠ!% : ∀ {A P A' P' B Q B' Q' t t' e e'}
              → Γ ⊢ Π A ^ ! ° ⁰ ▹ P ° ⁰ ° ⁰  [conv↑] Π A' ^ ! ° ⁰ ▹ P' ° ⁰ ° ⁰  ∷ U ⁰ ^ ι ¹
              → Γ ⊢ Π B ^ % ° ⁰ ▹ Q ° ⁰ ° ⁰  [conv↑] Π B' ^ % ° ⁰ ▹ Q' ° ⁰ ° ⁰  ∷ U ⁰ ^ ι ¹
              → Γ ⊢ t [conv↑] t' ∷ Π A ^ ! ° ⁰ ▹ P ° ⁰  ° ⁰ ^ ι ⁰
              → Γ ⊢ e ∷ (Id (U ⁰) (Π A ^ ! ° ⁰ ▹ P ° ⁰ ° ⁰ ) (Π B ^ % ° ⁰ ▹ Q ° ⁰ ° ⁰ )) ^ [ % , next ⁰ ]
              → Γ ⊢ e' ∷ (Id (U ⁰) (Π A' ^ ! ° ⁰ ▹ P' ° ⁰ ° ⁰ ) (Π B' ^ % ° ⁰ ▹ Q' ° ⁰ ° ⁰ )) ^ [ % , next ⁰ ]
              → Γ ⊢ cast ⁰ (Π A ^ ! ° ⁰ ▹ P ° ⁰ ° ⁰ ) (Π B ^ % ° ⁰ ▹ Q ° ⁰ ° ⁰ ) e t ~
                    cast ⁰ (Π A' ^ ! ° ⁰ ▹ P' ° ⁰ ° ⁰ ) (Π B' ^ % ° ⁰ ▹ Q' ° ⁰ ° ⁰ ) e' t' ↑! (Π B ^ % ° ⁰ ▹ Q ° ⁰ ° ⁰ ) ^ ι ⁰

  record _⊢_~_↑%_^_ (Γ : Con Term) (k l A : Term) (ll : TypeLevel) : Set where
    inductive
    constructor %~↑
    field
      ⊢k : Γ ⊢ k ∷ A ^ [ % , ll ]
      ⊢l : Γ ⊢ l ∷ A ^ [ % , ll ]

  data _⊢_~_↑_^_ (Γ : Con Term) : (k l A : Term) → TypeInfo → Set where
    ~↑! : ∀ {k l A ll} → Γ ⊢ k ~ l ↑! A ^ ll → Γ ⊢ k ~ l ↑ A ^ [ ! , ll ]
    ~↑% : ∀ {k l A ll} → Γ ⊢ k ~ l ↑% A ^ ll → Γ ⊢ k ~ l ↑ A ^ [ % , ll ]

  -- Neutral equality with types in WHNF.
  record _⊢_~_↓!_^_ (Γ : Con Term) (k l B : Term) (ll : TypeLevel) : Set where
    inductive
    constructor [~]
    field
      A     : Term
      D     : Γ ⊢ A ⇒* B ^ [ ! , ll ]
      whnfB : Whnf B
      k~l   : Γ ⊢ k ~ l ↑! A ^ ll

  -- Type equality.
  record _⊢_[conv↑]_^_ (Γ : Con Term) (A B : Term) (rA : TypeInfo) : Set where
    inductive
    constructor [↑]
    field
      A′ B′  : Term
      D      : Γ ⊢ A ⇒* A′ ^ rA
      D′     : Γ ⊢ B ⇒* B′ ^ rA
      whnfA′ : Whnf A′
      whnfB′ : Whnf B′
      A′<>B′ : Γ ⊢ A′ [conv↓] B′ ^ rA

  -- Type equality with types in WHNF.
  data _⊢_[conv↓]_^_ (Γ : Con Term) : (A B : Term) → TypeInfo → Set where
    U-refl    : ∀ {r r' }
              → r PE.≡ r' -- needed for K issues
              → ⊢ Γ → Γ ⊢ Univ r ¹ [conv↓] Univ r' ¹ ^ [ ! , next ¹ ]
    univ      : ∀ {A B r l}
              → Γ ⊢ A [conv↓] B ∷ Univ r l ^ next l
              → Γ ⊢ A [conv↓] B ^ [ r , ι l ]

  -- Term equality.
  record _⊢_[conv↑]_∷_^_ (Γ : Con Term) (t u A : Term) (l : TypeLevel) : Set where
    inductive
    constructor [↑]ₜ
    field
      B t′ u′ : Term
      D       : Γ ⊢ A ⇒* B ^ [ ! , l ]
      d       : Γ ⊢ t ⇒* t′ ∷ B ^ l
      d′      : Γ ⊢ u ⇒* u′ ∷ B ^ l
      whnfB   : Whnf B
      whnft′  : Whnf t′
      whnfu′  : Whnf u′
      t<>u    : Γ ⊢ t′ [conv↓] u′ ∷ B ^ l

  -- Term equality with types and terms in WHNF.
  data _⊢_[conv↓]_∷_^_ (Γ : Con Term) : (t u A : Term) (l : TypeLevel) → Set where
    U-refl    : ∀ {r r' }
              → r PE.≡ r' -- needed for K issues
              → ⊢ Γ → Γ ⊢ Univ r ⁰ [conv↓] Univ r' ⁰ ∷ U ¹ ^ next ¹
    ne        : ∀ {r K L lU l}
                → Γ ⊢ K ~ L ↓! Univ r lU ^ l
                → Γ ⊢ K [conv↓] L ∷ Univ r lU ^ l
    ℕ-refl    : ⊢ Γ → Γ ⊢ ℕ [conv↓] ℕ ∷ U ⁰ ^ next ⁰
    Empty-refl : ∀ {l ll} → ll PE.≡ next l → ⊢ Γ → Γ ⊢ Empty l [conv↓] Empty l ∷ SProp l ^ ll
    Π-cong    : ∀ {F G H E rF rH rΠ lF lH lG lE lΠ ll}
              → ll PE.≡ next lΠ
              → rF PE.≡ rH -- needed for K issues
              → lF PE.≡ lH -- needed for K issues
              → lG PE.≡ lE -- needed for K issues
              → lF ≤ lΠ
              → lG ≤ lΠ
              → Γ ⊢ F ^ [ rF , ι lF ]
              → Γ ⊢ F [conv↑] H ∷ Univ rF lF ^ next lF
              → Γ ∙ F ^ [ rF , ι lF ] ⊢ G [conv↑] E  ∷ Univ rΠ lG ^ next lG
              → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° lΠ [conv↓] Π H ^ rH ° lH ▹ E ° lE ° lΠ ∷ Univ rΠ lΠ ^ ll
    ∃-cong    : ∀ {F G H E l ll}
              → ll PE.≡ next l
              → Γ ⊢ F ^ [ % , ι l ]
              → Γ ⊢ F [conv↑] H ∷ SProp l ^ next l
              → Γ ∙ F ^ [ % , ι l ] ⊢ G [conv↑] E  ∷ SProp l ^ next l
              → Γ ⊢ ∃ F ▹ G [conv↓] ∃ H ▹ E ∷ SProp l ^ ll
    ℕ-ins     : ∀ {k l}
              → Γ ⊢ k ~ l ↓! ℕ ^ ι ⁰
              → Γ ⊢ k [conv↓] l ∷ ℕ ^ ι ⁰
    ne-ins    : ∀ {k l M N ll}
              → Γ ⊢ k ∷ N ^ [ ! , ι ll ]
              → Γ ⊢ l ∷ N ^ [ ! , ι ll ]
              → Neutral N
              → Γ ⊢ k ~ l ↓! M ^ ι ll
              → Γ ⊢ k [conv↓] l ∷ N ^ ι ll
    zero-refl : ⊢ Γ → Γ ⊢ zero [conv↓] zero ∷ ℕ ^ ι ⁰
    suc-cong  : ∀ {m n}
              → Γ ⊢ m [conv↑] n ∷ ℕ ^ ι ⁰
              → Γ ⊢ suc m [conv↓] suc n ∷ ℕ ^ ι ⁰
    η-eq      : ∀ {f g F G rF lF lG l}
              → lF ≤ l
              → lG ≤ l
              → Γ ⊢ F ^ [ rF , ι lF ]
              → Γ ⊢ f ∷ Π F ^ rF ° lF ▹ G ° lG ° l ^ [ ! , ι l ]
              → Γ ⊢ g ∷ Π F ^ rF ° lF ▹ G ° lG ° l ^ [ ! , ι l ]
              → Function f
              → Function g
              → Γ ∙ F ^ [ rF , ι lF ] ⊢ wk1 f ∘ var 0 ^ l [conv↑] wk1 g ∘ var 0 ^ l ∷ G ^ ι lG
                → Γ ⊢ f [conv↓] g ∷ Π F ^ rF ° lF ▹ G ° lG ° l ^ ι l

  _⊢_[genconv↑]_∷_^_ : (Γ : Con Term) (t u A : Term) (r : TypeInfo) → Set
  _⊢_[genconv↑]_∷_^_ Γ k l A [ ! , ll ] =  Γ ⊢ k [conv↑] l ∷ A ^ ll
  _⊢_[genconv↑]_∷_^_ Γ k l A [ % , ll ] =  Γ ⊢ k ~ l ↑% A ^  ll

var-refl′ : ∀ {Γ x A rA ll}
          → Γ ⊢ var x ∷ A ^ [ rA , ll ]
          → Γ ⊢ var x ~ var x ↑ A ^ [ rA , ll ]
var-refl′ {rA = !} ⊢x = ~↑! (var-refl ⊢x PE.refl)
var-refl′ {rA = %} ⊢x = ~↑% (%~↑ ⊢x ⊢x)

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


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

module Data.Array.Skew where

open import Prelude
open import Data.Binary.Skew
open import Data.List
open import Data.Nat using (_+_)

private
  variable
    p : Level
    P : ℕ → Type p
    n : ℕ
    ns : 𝔹

infixl 6 _∔_
_∔_ : ℕ → ℕ → ℕ
zero  ∔ m = m
suc n ∔ m = n ∔ suc m

infixl 4 _⊕_
_⊕_ : (ℕ → Type p) → ℕ → ℕ → Type p
_⊕_ P n m = P (n ∔ m)

data Spine⁺ {p} (P : ℕ → Type p) : 𝔹 → Type p where
  nil : Spine⁺ P []
  conss : ∀ n → P n → Spine⁺ (P ⊕ suc n) ns → Spine⁺ P (n ∷ ns)

data Spine {p} (P : ℕ → Type p) : 𝔹 → Type p where
  nil : Spine P []
  conss : ∀ n → P n → Spine⁺ (P ⊕ n) ns → Spine P (n ∷ ns)

-- cons : (∀ {m} → P m → P m → P (suc m)) → P zero → Spine P ns → Spine P (inc ns)
-- cons _*_ x nil = conss zero x nil
-- cons _*_ x (conss n x₁ nil) = conss zero x (conss n x₁ nil)
-- cons _*_ x (conss n x₁ (conss zero x₂ xs)) = conss (suc n) (x₁ * x₁) xs
-- cons _*_ x (conss n x₁ (conss (suc m) x₂ xs)) = conss zero x (conss n x₁ (conss m x₂ {!!}))

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Issue #2814 reported by tomjack on 2017-10-18

{-# OPTIONS --cubical --rewriting --confluence-check #-}

-- prelude stolen from Saizan/cubical-demo

open import Agda.Primitive.Cubical public
open import Agda.Builtin.Cubical.Path

Path = _≡_

refl : ∀ {ℓ} {A : Set ℓ} {x : A} → x ≡ x
refl {x = x} = λ _ → x

postulate
  Rewrite : ∀ {ℓ} {A : Set ℓ} → A → A → Set

{-# BUILTIN REWRITE Rewrite #-}

module Good where
  postulate
    Unit : Set
    unit : Unit

  module UnitElim (P : Unit → Set) (unit* : P unit) where
    postulate
      Unit-elim : (x : Unit) → P x
      unit-β : Rewrite (Unit-elim unit) unit*
  open UnitElim public
  {-# REWRITE unit-β #-}

  test₁ : {C : Set} {c₀ : C} → Path {A = C} (Unit-elim (λ _ → C) c₀ unit) c₀
  test₁ = refl

  test₂ : {C : Set} {c₀ : C} → Path {A = Path c₀ c₀} (λ j → Unit-elim (λ _ → C) c₀ unit) refl
  test₂ = refl

-- same code, but with a dummy module parameter
module Bad (Dummy : Set) where
  postulate
    Unit : Set
    unit : Unit

  module UnitElim (P : Unit → Set) (unit* : P unit) where
    postulate
      Unit-elim : (x : Unit) → P x
      unit-β : Rewrite (Unit-elim unit) unit*
  open UnitElim public
  {-# REWRITE unit-β #-}

  test₁ : {C : Set} {c₀ : C} → Path {A = C} (Unit-elim (λ _ → C) c₀ unit) c₀
  test₁ = refl
  test₂ : {C : Set} {c₀ : C} → Path {A = Path c₀ c₀} (λ j → Unit-elim (λ _ → C) c₀ unit) refl
  test₂ = refl

-- WAS:
-- Unit-elim (λ _ → .C) .c₀ unit != .c₀ of type .C
-- when checking that the expression refl has type
-- Path (λ j → Unit-elim (λ _ → .C) .c₀ unit) refl

-- SHOULD: succeed

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --copatterns --sized-types #-}

{- M types done properly coinductive -}
module NewM where

open import Size
open import Coinduction
open import Data.Product
open import Function
open import Data.M as M

record M' {i : Size} (A : Set) (B : A → Set) : Set where
  coinductive
  field
    d : ∀ {j : Size< i} → Σ A (λ x → (B x → M' {j} A B))
open M'

f : ∀{i} → {A : Set} {B : A → Set} → M A B → M' {i} A B
proj₁ (d (f x)) = head x
proj₂ (d (f x)) = f ∘ tail x

g : {A : Set} {B : A → Set} → M' A B → M A B
g x = inf (proj₁ (d x)) (λ b → ♯ g (proj₂ (d x) b))

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


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

module Definition.Typed.Consequences.Substitution where

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.EqRelInstance
open import Definition.Typed.Weakening
open import Definition.Typed.Consequences.Syntactic
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Irrelevance
open import Definition.LogicalRelation.Fundamental

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Well-formed substitution of types.
substitution : ∀ {A Γ Δ σ} → Γ ⊢ A → Δ ⊢ˢ σ ∷ Γ → ⊢ Δ → Δ ⊢ subst σ A
substitution A σ ⊢Δ with fundamental A | fundamentalSubst (wf A) ⊢Δ σ
substitution A σ ⊢Δ | [Γ] , [A] | [Γ]′ , [σ] =
  escape (proj₁ ([A] ⊢Δ (irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ])))

-- Well-formed substitution of type equality.
substitutionEq : ∀ {A B Γ Δ σ σ′}
               → Γ ⊢ A ≡ B → Δ ⊢ˢ σ ≡ σ′ ∷ Γ → ⊢ Δ → Δ ⊢ subst σ A ≡ subst σ′ B
substitutionEq A≡B σ ⊢Δ with fundamentalEq A≡B | fundamentalSubstEq (wfEq A≡B) ⊢Δ σ
substitutionEq A≡B σ ⊢Δ | [Γ] , [A] , [B] , [A≡B] | [Γ]′ , [σ] , [σ′] , [σ≡σ′]  =
  let [σ]′ = irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ]
      [σ′]′ = irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ′]
      [σ≡σ′]′ = irrelevanceSubstEq [Γ]′ [Γ] ⊢Δ ⊢Δ [σ] [σ]′ [σ≡σ′]
  in  escapeEq (proj₁ ([A] ⊢Δ [σ]′))
                   (transEq (proj₁ ([A] ⊢Δ [σ]′)) (proj₁ ([B] ⊢Δ [σ]′))
                            (proj₁ ([B] ⊢Δ [σ′]′)) ([A≡B] ⊢Δ [σ]′)
                            (proj₂ ([B] ⊢Δ [σ]′) [σ′]′ [σ≡σ′]′))

-- Well-formed substitution of terms.
substitutionTerm : ∀ {t A Γ Δ σ}
               → Γ ⊢ t ∷ A → Δ ⊢ˢ σ ∷ Γ → ⊢ Δ → Δ ⊢ subst σ t ∷ subst σ A
substitutionTerm t σ ⊢Δ with fundamentalTerm t | fundamentalSubst (wfTerm t) ⊢Δ σ
substitutionTerm t σ ⊢Δ | [Γ] , [A] , [t] | [Γ]′ , [σ] =
  let [σ]′ = irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ]
  in  escapeTerm (proj₁ ([A] ⊢Δ [σ]′)) (proj₁ ([t] ⊢Δ [σ]′))

-- Well-formed substitution of term equality.
substitutionEqTerm : ∀ {t u A Γ Δ σ σ′}
                   → Γ ⊢ t ≡ u ∷ A → Δ ⊢ˢ σ ≡ σ′ ∷ Γ → ⊢ Δ
                   → Δ ⊢ subst σ t ≡ subst σ′ u ∷ subst σ A
substitutionEqTerm t≡u σ≡σ′ ⊢Δ with fundamentalTermEq t≡u
                                  | fundamentalSubstEq (wfEqTerm t≡u) ⊢Δ σ≡σ′
... | [Γ] , modelsTermEq [A] [t] [u] [t≡u] | [Γ]′ , [σ] , [σ′] , [σ≡σ′] =
  let [σ]′ = irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ]
      [σ′]′ = irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ′]
      [σ≡σ′]′ = irrelevanceSubstEq [Γ]′ [Γ] ⊢Δ ⊢Δ [σ] [σ]′ [σ≡σ′]
  in  escapeTermEq (proj₁ ([A] ⊢Δ [σ]′))
                       (transEqTerm (proj₁ ([A] ⊢Δ [σ]′)) ([t≡u] ⊢Δ [σ]′)
                                    (proj₂ ([u] ⊢Δ [σ]′) [σ′]′ [σ≡σ′]′))

-- Reflexivity of well-formed substitution.
substRefl : ∀ {σ Γ Δ}
          → Δ ⊢ˢ σ ∷ Γ
          → Δ ⊢ˢ σ ≡ σ ∷ Γ
substRefl id = id
substRefl (σ , x) = substRefl σ , refl x

-- Weakening of well-formed substitution.
wkSubst′ : ∀ {ρ σ Γ Δ Δ′} (⊢Γ : ⊢ Γ) (⊢Δ : ⊢ Δ) (⊢Δ′ : ⊢ Δ′)
           ([ρ] : ρ ∷ Δ′ ⊆ Δ)
           ([σ] : Δ ⊢ˢ σ ∷ Γ)
         → Δ′ ⊢ˢ ρ •ₛ σ ∷ Γ
wkSubst′ ε ⊢Δ ⊢Δ′ ρ id = id
wkSubst′ (_∙_ {Γ} {A} ⊢Γ ⊢A) ⊢Δ ⊢Δ′ ρ (tailσ , headσ) =
  wkSubst′ ⊢Γ ⊢Δ ⊢Δ′ ρ tailσ
  , PE.subst (λ x → _ ⊢ _ ∷ x) (wk-subst A) (wkTerm ρ ⊢Δ′ headσ)

-- Weakening of well-formed substitution by one.
wk1Subst′ : ∀ {F σ Γ Δ} (⊢Γ : ⊢ Γ) (⊢Δ : ⊢ Δ)
            (⊢F : Δ ⊢ F)
            ([σ] : Δ ⊢ˢ σ ∷ Γ)
          → (Δ ∙ F) ⊢ˢ wk1Subst σ ∷ Γ
wk1Subst′ {F} {σ} {Γ} {Δ} ⊢Γ ⊢Δ ⊢F [σ] =
  wkSubst′ ⊢Γ ⊢Δ (⊢Δ ∙ ⊢F) (step id) [σ]

-- Lifting of well-formed substitution.
liftSubst′ : ∀ {F σ Γ Δ} (⊢Γ : ⊢ Γ) (⊢Δ : ⊢ Δ)
             (⊢F  : Γ ⊢ F)
             ([σ] : Δ ⊢ˢ σ ∷ Γ)
           → (Δ ∙ subst σ F) ⊢ˢ liftSubst σ ∷ Γ ∙ F
liftSubst′ {F} {σ} {Γ} {Δ} ⊢Γ ⊢Δ ⊢F [σ] =
  let ⊢Δ∙F = ⊢Δ ∙ substitution ⊢F [σ] ⊢Δ
  in  wkSubst′ ⊢Γ ⊢Δ ⊢Δ∙F (step id) [σ]
  ,   var ⊢Δ∙F (PE.subst (λ x → 0 ∷ x ∈ (Δ ∙ subst σ F))
                         (wk-subst F) here)

-- Well-formed identity substitution.
idSubst′ : ∀ {Γ} (⊢Γ : ⊢ Γ)
         → Γ ⊢ˢ idSubst ∷ Γ
idSubst′ ε = id
idSubst′ (_∙_ {Γ} {A} ⊢Γ ⊢A) =
  wk1Subst′ ⊢Γ ⊢Γ ⊢A (idSubst′ ⊢Γ)
  , PE.subst (λ x → Γ ∙ A ⊢ _ ∷ x) (wk1-tailId A) (var (⊢Γ ∙ ⊢A) here)

-- Well-formed substitution composition.
substComp′ : ∀ {σ σ′ Γ Δ Δ′} (⊢Γ : ⊢ Γ) (⊢Δ : ⊢ Δ) (⊢Δ′ : ⊢ Δ′)
             ([σ] : Δ′ ⊢ˢ σ ∷ Δ)
             ([σ′] : Δ ⊢ˢ σ′ ∷ Γ)
           → Δ′ ⊢ˢ σ ₛ•ₛ σ′ ∷ Γ
substComp′ ε ⊢Δ ⊢Δ′ [σ] id = id
substComp′ (_∙_ {Γ} {A} ⊢Γ ⊢A) ⊢Δ ⊢Δ′ [σ] ([tailσ′] , [headσ′]) =
  substComp′ ⊢Γ ⊢Δ ⊢Δ′ [σ] [tailσ′]
  , PE.subst (λ x → _ ⊢ _ ∷ x) (substCompEq A)
             (substitutionTerm [headσ′] [σ] ⊢Δ′)

-- Well-formed singleton substitution of terms.
singleSubst : ∀ {A t Γ} → Γ ⊢ t ∷ A → Γ ⊢ˢ sgSubst t ∷ Γ ∙ A
singleSubst {A} t =
  let ⊢Γ = wfTerm t
  in  idSubst′ ⊢Γ , PE.subst (λ x → _ ⊢ _ ∷ x) (PE.sym (subst-id A)) t

-- Well-formed singleton substitution of term equality.
singleSubstEq : ∀ {A t u Γ} → Γ ⊢ t ≡ u ∷ A
              → Γ ⊢ˢ sgSubst t ≡ sgSubst u ∷ Γ ∙ A
singleSubstEq {A} t =
  let ⊢Γ = wfEqTerm t
  in  substRefl (idSubst′ ⊢Γ) , PE.subst (λ x → _ ⊢ _ ≡ _ ∷ x) (PE.sym (subst-id A)) t

-- Well-formed singleton substitution of terms with lifting.
singleSubst↑ : ∀ {A t Γ} → Γ ∙ A ⊢ t ∷ wk1 A → Γ ∙ A ⊢ˢ consSubst (wk1Subst idSubst) t ∷ Γ ∙ A
singleSubst↑ {A} t with wfTerm t
... | ⊢Γ ∙ ⊢A = wk1Subst′ ⊢Γ ⊢Γ ⊢A (idSubst′ ⊢Γ)
              , PE.subst (λ x → _ ∙ A ⊢ _ ∷ x) (wk1-tailId A) t

-- Well-formed singleton substitution of term equality with lifting.
singleSubst↑Eq : ∀ {A t u Γ} → Γ ∙ A ⊢ t ≡ u ∷ wk1 A
              → Γ ∙ A ⊢ˢ consSubst (wk1Subst idSubst) t ≡ consSubst (wk1Subst idSubst) u ∷ Γ ∙ A
singleSubst↑Eq {A} t with wfEqTerm t
... | ⊢Γ ∙ ⊢A = substRefl (wk1Subst′ ⊢Γ ⊢Γ ⊢A (idSubst′ ⊢Γ))
              , PE.subst (λ x → _ ∙ A ⊢ _ ≡ _ ∷ x) (wk1-tailId A) t

-- Helper lemmas for single substitution

substType : ∀ {t F G Γ} → Γ ∙ F ⊢ G → Γ ⊢ t ∷ F → Γ ⊢ G [ t ]
substType {t} {F} {G} ⊢G ⊢t =
  let ⊢Γ = wfTerm ⊢t
  in  substitution ⊢G (singleSubst ⊢t) ⊢Γ

substTypeEq : ∀ {t u F G E Γ} → Γ ∙ F ⊢ G ≡ E → Γ ⊢ t ≡ u ∷ F → Γ ⊢ G [ t ] ≡ E [ u ]
substTypeEq {F = F} ⊢G ⊢t =
  let ⊢Γ = wfEqTerm ⊢t
  in  substitutionEq ⊢G (singleSubstEq ⊢t) ⊢Γ

substTerm : ∀ {F G t f Γ} → Γ ∙ F ⊢ f ∷ G → Γ ⊢ t ∷ F → Γ ⊢ f [ t ] ∷ G [ t ]
substTerm {F} {G} {t} {f} ⊢f ⊢t =
  let ⊢Γ = wfTerm ⊢t
  in  substitutionTerm ⊢f (singleSubst ⊢t) ⊢Γ

substTypeΠ : ∀ {t F G Γ} → Γ ⊢ Π F ▹ G → Γ ⊢ t ∷ F → Γ ⊢ G [ t ]
substTypeΠ ΠFG t with syntacticΠ ΠFG
substTypeΠ ΠFG t | F , G = substType G t

subst↑Type : ∀ {t F G Γ}
           → Γ ∙ F ⊢ G
           → Γ ∙ F ⊢ t ∷ wk1 F
           → Γ ∙ F ⊢ G [ t ]↑
subst↑Type ⊢G ⊢t = substitution ⊢G (singleSubst↑ ⊢t) (wfTerm ⊢t)

subst↑TypeEq : ∀ {t u F G E Γ}
             → Γ ∙ F ⊢ G ≡ E
             → Γ ∙ F ⊢ t ≡ u ∷ wk1 F
             → Γ ∙ F ⊢ G [ t ]↑ ≡ E [ u ]↑
subst↑TypeEq ⊢G ⊢t = substitutionEq ⊢G (singleSubst↑Eq ⊢t) (wfEqTerm ⊢t)


text:
{- Binary natural numbers (Anders Mörtberg, Jan. 2019)

This file defines two representations of binary numbers. We prove that
they are equivalent to unary numbers and univalence is then used to
transport both programs and properties between the representations.
This is an example of how having computational univalence can be
useful for practical programming.

The first definition is [Binℕ] and the numbers are essentially lists
of 0/1 with no trailing zeroes (in little-endian format). The main
definitions and examples are:

- Equivalence between Binℕ and ℕ ([Binℕ≃ℕ]) with an equality obtained
  using univalence ([Binℕ≡ℕ]).

- Addition on Binℕ defined by transporting addition on ℕ to Binℕ
  ([_+Binℕ_]) along Binℕ≡ℕ together with a proof that addition on Binℕ
  is associative obtained by transporting the proof for ℕ ([+Binℕ-assoc]).

- Functions testing whether a binary number is odd or even in O(1)
  ([oddBinℕ], [evenBinℕ]) and the corresponding functions for ℕ
  obtained by transport. Proof that odd numbers are not even
  transported from Binℕ to ℕ ([oddℕnotEvenℕ]).

- An example of the structure identity principle for natural number
  structures ([NatImpl]). We first prove that Binℕ≡ℕ lifts to natural
  number structures ([NatImplℕ≡Binℕ]) and we then use this to
  transport "+-suc : m + suc n ≡ suc (m + n)" from ℕ to Binℕ ([+Binℕ-suc]).

- An example of program/data refinement using the structure identity
  principle where we transport a property that is infeasible to prove
  by computation for ℕ ([propDoubleℕ]):

      2^20 * 2^10 = 2^5 * (2^15 * 2^10)

  from the corresponding result on Binℕ which is proved instantly by
  refl ([propDoubleBinℕ]).

These examples are inspired from an old cubicaltt formalization:

https://github.com/mortberg/cubicaltt/blob/master/examples/binnat.ctt

which itself is based on an even older cubical formalization (from 2014):

https://github.com/simhu/cubical/blob/master/examples/binnat.cub

The second representation is more non-standard and inspired by:

https://github.com/RedPRL/redtt/blob/master/library/cool/nats.red

Only some of the experiments have been done for this representation,
but it has the virtue of being a bit simpler to prove equivalent to
ℕ. The same representation can be found in:

http://www.cs.bham.ac.uk/~mhe/agda-new/BinaryNaturals.html

-}
{-# OPTIONS --cubical --no-exact-split --safe #-}
module Cubical.Data.BinNat.BinNat where

open import Cubical.Core.Glue

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Nat
open import Cubical.Data.Bool
open import Cubical.Data.Empty

open import Cubical.Relation.Nullary

-- Positive binary numbers
data Pos : Type₀ where
  pos1 : Pos
  x0   : Pos → Pos
  x1   : Pos → Pos

sucPos : Pos → Pos
sucPos pos1    = x0 pos1
sucPos (x0 ps) = x1 ps
sucPos (x1 ps) = x0 (sucPos ps)

Pos→ℕ : Pos → ℕ
Pos→ℕ pos1    = suc zero
Pos→ℕ (x0 ps) = doubleℕ (Pos→ℕ ps)
Pos→ℕ (x1 ps) = suc (doubleℕ (Pos→ℕ ps))

posInd : {P : Pos → Type₀} → P pos1 → ((p : Pos) → P p → P (sucPos p)) → (p : Pos) → P p
posInd {P} h1 hs ps = f ps
  where
  H : (p : Pos) → P (x0 p) → P (x0 (sucPos p))
  H p hx0p = hs (x1 p) (hs (x0 p) hx0p)

  f : (ps : Pos) → P ps
  f pos1    = h1
  f (x0 ps) = posInd (hs pos1 h1) H ps
  f (x1 ps) = hs (x0 ps) (posInd (hs pos1 h1) H ps)

Pos→ℕsucPos : (p : Pos) → Pos→ℕ (sucPos p) ≡ suc (Pos→ℕ p)
Pos→ℕsucPos pos1   = refl
Pos→ℕsucPos (x0 p) = refl
Pos→ℕsucPos (x1 p) = λ i → doubleℕ (Pos→ℕsucPos p i)

zero≠Pos→ℕ : (p : Pos) → ¬ (zero ≡ Pos→ℕ p)
zero≠Pos→ℕ p = posInd (λ prf → znots prf) hs p
  where
  hs : (p : Pos) → ¬ (zero ≡ Pos→ℕ p) → zero ≡ Pos→ℕ (sucPos p) → ⊥
  hs p neq ieq = ⊥-elim (znots (ieq ∙ (Pos→ℕsucPos p)))

ℕ→Pos : ℕ → Pos
ℕ→Pos zero          = pos1
ℕ→Pos (suc zero)    = pos1
ℕ→Pos (suc (suc n)) = sucPos (ℕ→Pos (suc n))

ℕ→PosSuc : ∀ n → ¬ (zero ≡ n) → ℕ→Pos (suc n) ≡ sucPos (ℕ→Pos n)
ℕ→PosSuc zero neq    = ⊥-elim (neq refl)
ℕ→PosSuc (suc n) neq = refl

Pos→ℕ→Pos : (p : Pos) → ℕ→Pos (Pos→ℕ p) ≡ p
Pos→ℕ→Pos p = posInd refl hs p
  where
  hs : (p : Pos) → ℕ→Pos (Pos→ℕ p) ≡ p → ℕ→Pos (Pos→ℕ (sucPos p)) ≡ sucPos p
  hs p hp =
    ℕ→Pos (Pos→ℕ (sucPos p)) ≡⟨ cong ℕ→Pos (Pos→ℕsucPos p) ⟩
    ℕ→Pos (suc (Pos→ℕ p))    ≡⟨ ℕ→PosSuc (Pos→ℕ p) (zero≠Pos→ℕ p) ⟩
    sucPos (ℕ→Pos (Pos→ℕ p)) ≡⟨ cong sucPos hp ⟩
    sucPos p ∎

ℕ→Pos→ℕ : (n : ℕ) → Pos→ℕ (ℕ→Pos (suc n)) ≡ suc n
ℕ→Pos→ℕ zero    = refl
ℕ→Pos→ℕ (suc n) =
  Pos→ℕ (sucPos (ℕ→Pos (suc n))) ≡⟨ Pos→ℕsucPos (ℕ→Pos (suc n)) ⟩
  suc (Pos→ℕ (ℕ→Pos (suc n)))    ≡⟨ cong suc (ℕ→Pos→ℕ n) ⟩
  suc (suc n) ∎

-- Binary numbers
data Binℕ : Type₀ where
  binℕ0   : Binℕ
  binℕpos : Pos → Binℕ

ℕ→Binℕ : ℕ → Binℕ
ℕ→Binℕ zero    = binℕ0
ℕ→Binℕ (suc n) = binℕpos (ℕ→Pos (suc n))

Binℕ→ℕ : Binℕ → ℕ
Binℕ→ℕ binℕ0       = zero
Binℕ→ℕ (binℕpos x) = Pos→ℕ x

ℕ→Binℕ→ℕ : (n : ℕ) → Binℕ→ℕ (ℕ→Binℕ n) ≡ n
ℕ→Binℕ→ℕ zero          = refl
ℕ→Binℕ→ℕ (suc zero)    = refl
ℕ→Binℕ→ℕ (suc (suc n)) =
    Pos→ℕ (sucPos (ℕ→Pos (suc n))) ≡⟨ Pos→ℕsucPos (ℕ→Pos (suc n)) ⟩
    suc (Pos→ℕ (ℕ→Pos (suc n)))    ≡⟨ cong suc (ℕ→Binℕ→ℕ (suc n)) ⟩
    suc (suc n) ∎

Binℕ→ℕ→Binℕ : (n : Binℕ) → ℕ→Binℕ (Binℕ→ℕ n) ≡ n
Binℕ→ℕ→Binℕ binℕ0 = refl
Binℕ→ℕ→Binℕ (binℕpos p) = posInd refl (λ p _ → rem p) p
  where
  rem : (p : Pos) → ℕ→Binℕ (Pos→ℕ (sucPos p)) ≡ binℕpos (sucPos p)
  rem p =
    ℕ→Binℕ (Pos→ℕ (sucPos p))       ≡⟨ cong ℕ→Binℕ (Pos→ℕsucPos p) ⟩
    binℕpos (ℕ→Pos (suc (Pos→ℕ p))) ≡⟨ cong binℕpos ((ℕ→PosSuc (Pos→ℕ p) (zero≠Pos→ℕ p)) ∙
                                                              (cong sucPos (Pos→ℕ→Pos p))) ⟩
    binℕpos (sucPos p) ∎

Binℕ≃ℕ : Binℕ ≃ ℕ
Binℕ≃ℕ = isoToEquiv (iso Binℕ→ℕ ℕ→Binℕ ℕ→Binℕ→ℕ Binℕ→ℕ→Binℕ)

-- Use univalence (in fact only "ua") to get an equality from the
-- above equivalence
Binℕ≡ℕ : Binℕ ≡ ℕ
Binℕ≡ℕ = ua Binℕ≃ℕ

sucBinℕ : Binℕ → Binℕ
sucBinℕ binℕ0       = binℕpos pos1
sucBinℕ (binℕpos x) = binℕpos (sucPos x)

Binℕ→ℕsuc : (x : Binℕ) → suc (Binℕ→ℕ x) ≡ Binℕ→ℕ (sucBinℕ x)
Binℕ→ℕsuc binℕ0       = refl
Binℕ→ℕsuc (binℕpos x) = sym (Pos→ℕsucPos x)

-- We can transport addition on ℕ to Binℕ
_+Binℕ_ : Binℕ → Binℕ → Binℕ
_+Binℕ_ = transport (λ i → Binℕ≡ℕ (~ i) → Binℕ≡ℕ (~ i) → Binℕ≡ℕ (~ i)) _+_

-- Test: 4 + 1 = 5
private
  _ : binℕpos (x0 (x0 pos1)) +Binℕ binℕpos pos1 ≡ binℕpos (x1 (x0 pos1))
  _ = refl

-- It is easy to test if binary numbers are odd
oddBinℕ : Binℕ → Bool
oddBinℕ binℕ0            = false
oddBinℕ (binℕpos pos1)   = true
oddBinℕ (binℕpos (x0 _)) = false
oddBinℕ (binℕpos (x1 _)) = true

evenBinℕ : Binℕ → Bool
evenBinℕ n = oddBinℕ (sucBinℕ n)

-- And prove the following property (without induction)
oddBinℕnotEvenBinℕ : (n : Binℕ) → oddBinℕ n ≡ not (evenBinℕ n)
oddBinℕnotEvenBinℕ binℕ0            = refl
oddBinℕnotEvenBinℕ (binℕpos pos1)   = refl
oddBinℕnotEvenBinℕ (binℕpos (x0 x)) = refl
oddBinℕnotEvenBinℕ (binℕpos (x1 x)) = refl

-- It is also easy to define and prove the property for unary numbers,
-- however the definition uses recursion and the proof induction
private
  oddn : ℕ → Bool
  oddn zero    = true
  oddn (suc x) = not (oddn x)

  evenn : ℕ → Bool
  evenn n = not (oddn n)

  oddnSuc : (n : ℕ) → oddn n ≡ not (evenn n)
  oddnSuc zero    = refl
  oddnSuc (suc n) = cong not (oddnSuc n)

-- So what we can do instead is to transport the odd test from Binℕ to
-- ℕ along the equality
oddℕ : ℕ → Bool
oddℕ = transport (λ i → Binℕ≡ℕ i → Bool) oddBinℕ

evenℕ : ℕ → Bool
evenℕ = transport (λ i → Binℕ≡ℕ i → Bool) evenBinℕ

-- We can then also transport the property
oddℕnotEvenℕ : (n : ℕ) → oddℕ n ≡ not (evenℕ n)
oddℕnotEvenℕ =
  let -- We first build a path from oddBinℕ to oddℕ. When i=1 this is
      -- "transp (λ j → Binℕ≡ℕ j → Bool) i0 oddBinℕ" (i.e. oddℕ)
      oddp : PathP (λ i → Binℕ≡ℕ i → Bool) oddBinℕ oddℕ
      oddp i = transp (λ j → Binℕ≡ℕ (i ∧ j) → Bool) (~ i) oddBinℕ

      -- We then build a path from evenBinℕ to evenℕ
      evenp : PathP (λ i → Binℕ≡ℕ i → Bool) evenBinℕ evenℕ
      evenp i = transp (λ j → Binℕ≡ℕ (i ∧ j) → Bool) (~ i) evenBinℕ
  in -- Then transport oddBinℕnotEvenBinℕ in a suitable equality type
     -- When i=0 this is "(n : Binℕ) → oddBinℕ n ≡ not (evenBinℕ n)"
     -- When i=1 this is "(n : ℕ) → oddℕ n ≡ not (evenℕ n)"
     transport (λ i → (n : Binℕ≡ℕ i) → oddp i n ≡ not (evenp i n)) oddBinℕnotEvenBinℕ

-- We can do the same for natural numbers:

-- First construct the path
addp : PathP (λ i → Binℕ≡ℕ (~ i) → Binℕ≡ℕ (~ i) → Binℕ≡ℕ (~ i)) _+_ _+Binℕ_
addp i = transp (λ j → Binℕ≡ℕ (~ i ∨ ~ j) → Binℕ≡ℕ (~ i ∨ ~ j) → Binℕ≡ℕ (~ i ∨ ~ j)) (~ i) _+_

-- Then transport associativity:
+Binℕ-assoc : ∀ m n o → m +Binℕ (n +Binℕ o) ≡ (m +Binℕ n) +Binℕ o
+Binℕ-assoc =
  transport (λ i → (m n o : Binℕ≡ℕ (~ i))
                 → addp i m (addp i n o) ≡ addp i (addp i m n) o) +-assoc

-- We can also define what it means to be an implementation of natural
-- numbers and use this to transport properties between different
-- implementation of natural numbers. This can be seen as a special
-- case of the structure identity principle: any property that holds
-- for one structure also holds for an equivalent one.

-- An implementation of natural numbers (i.e. a "natural number
-- structure") has a zero and successor.
record NatImpl (A : Type₀) : Type₀ where
  field
    z : A
    s : A → A
open NatImpl

NatImplℕ : NatImpl ℕ
z NatImplℕ = zero
s NatImplℕ = suc

NatImplBinℕ : NatImpl Binℕ
z NatImplBinℕ = binℕ0
s NatImplBinℕ = sucBinℕ

-- Using the equality between binary and unary numbers we can get an
-- equality between the two implementations of the NatImpl interface
NatImplℕ≡Binℕ : PathP (λ i → NatImpl (Binℕ≡ℕ (~ i))) NatImplℕ NatImplBinℕ
z (NatImplℕ≡Binℕ i) = transp (λ j → Binℕ≡ℕ (~ i ∨ ~ j)) (~ i) zero
s (NatImplℕ≡Binℕ i) =
  λ x → glue (λ { (i = i0) → suc x
                ; (i = i1) → sucBinℕ x })
             -- We need to do use and hcomp to do and endpoint
             -- correction as "suc (unglue x)" connects "suc x"
             -- with "suc (Binℕ→ℕ x)" along i (which makes sense as
             -- x varies from ℕ to Binℕ along i), but we need
             -- something from "suc x" to "Binℕ→ℕ (sucBinℕ x)" for
             -- the glue to be well-formed
             (hcomp (λ j → λ { (i = i0) → suc x
                             ; (i = i1) → Binℕ→ℕsuc x j })
                    (suc (unglue (i ∨ ~ i) x)))

-- We then use this to transport +-suc from unary to binary numbers
+Binℕ-suc : ∀ m n → m +Binℕ sucBinℕ n ≡ sucBinℕ (m +Binℕ n)
+Binℕ-suc =
  transport (λ i → (m n : Binℕ≡ℕ (~ i))
                 → addp i m (NatImplℕ≡Binℕ i .s n) ≡ NatImplℕ≡Binℕ i .s (addp i m n)) +-suc

-- Doubling experiment: we define a notion of "doubling structure" and
-- transport a proof that is proved directly using refl for binary
-- numbers to unary numbers. This is an example of program/data
-- refinement: we can use univalence to prove properties about
-- inefficient data-structures using efficient ones.

-- Doubling structures
record Double {ℓ} (A : Type ℓ) : Type (ℓ-suc ℓ) where
  field
    -- doubling function computing 2 * x
    double : A → A
    -- element to double
    elt : A
open Double

-- Compute: 2^n * x
doubles : ∀ {ℓ} {A : Type ℓ} (D : Double A) → ℕ → A → A
doubles D n x = iter n (double D) x

Doubleℕ : Double ℕ
double Doubleℕ = doubleℕ
elt Doubleℕ    = n1024
  where
  -- 1024 = 2^8 * 2^2 = 2^10
  n1024 : ℕ
  n1024 = doublesℕ 8 4

-- The doubling operation on binary numbers is O(1), while for unary
-- numbers it is O(n). What is of course even more problematic is that
-- we cannot handle very big unary natural numbers, but with binary
-- there is no problem to represent very big numbers
doubleBinℕ : Binℕ → Binℕ
doubleBinℕ binℕ0       = binℕ0
doubleBinℕ (binℕpos x) = binℕpos (x0 x)

DoubleBinℕ : Double Binℕ
double DoubleBinℕ = doubleBinℕ
elt DoubleBinℕ    = bin1024
  where
  -- 1024 = 2^10 = 10000000000₂
  bin1024 : Binℕ
  bin1024 = binℕpos (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 pos1))))))))))

-- As these function don't commute strictly we have to prove it
-- separately and insert it in the proof of DoubleBinℕ≡Doubleℕ below
-- (just like we had to in NatImplℕ≡NatImplBinℕ
Binℕ→ℕdouble : (x : Binℕ) → doubleℕ (Binℕ→ℕ x) ≡ Binℕ→ℕ (doubleBinℕ x)
Binℕ→ℕdouble binℕ0       = refl
Binℕ→ℕdouble (binℕpos x) = refl

-- We use the equality between Binℕ and ℕ to get an equality of
-- doubling structures
DoubleBinℕ≡Doubleℕ : PathP (λ i → Double (Binℕ≡ℕ i)) DoubleBinℕ Doubleℕ
double (DoubleBinℕ≡Doubleℕ i) =
  λ x → glue (λ { (i = i0) → doubleBinℕ x
                ; (i = i1) → doubleℕ x })
             (hcomp (λ j → λ { (i = i0) → Binℕ→ℕdouble x j
                             ; (i = i1) → doubleℕ x })
                    (doubleℕ (unglue (i ∨ ~ i) x)))
elt (DoubleBinℕ≡Doubleℕ i) = transp (λ j → Binℕ≡ℕ (i ∨ ~ j)) i (Doubleℕ .elt)

-- We can now use transport to prove a property that is too slow to
-- check with unary numbers. We define the property we want to check
-- as a record so that Agda does not try to unfold it eagerly.
record propDouble {ℓ} {A : Type ℓ} (D : Double A) : Type ℓ where
  field
  -- 2^20 * e = 2^5 * (2^15 * e)
    proof : doubles D 20 (elt D) ≡ doubles D 5 (doubles D 15 (elt D))
open propDouble

-- The property we want to prove takes too long to typecheck for ℕ:
-- propDoubleℕ : propDouble Doubleℕ
-- propDoubleℕ = refl

-- With binary numbers it is instant
propDoubleBinℕ : propDouble DoubleBinℕ
proof propDoubleBinℕ = refl

-- By transporting the proof along the equality we then get it for
-- unary numbers
propDoubleℕ : propDouble Doubleℕ
propDoubleℕ = transport (λ i → propDouble (DoubleBinℕ≡Doubleℕ i)) propDoubleBinℕ

--------------------------------------------------------------------------------
--
-- Alternative encoding of binary natural numbers inspired by:
-- https://github.com/RedPRL/redtt/blob/master/library/cool/nats.red
--
-- This representation makes the equivalence with ℕ a bit easier to
-- prove, but the doubling example wouldn't work as nicely as we
-- cannot define it as an O(1) operation

data binnat : Type₀ where
  zero     : binnat            -- 0
  consOdd  : binnat → binnat   -- 2^n + 1
  consEven : binnat → binnat   -- 2^{n+1}

binnat→ℕ : binnat → ℕ
binnat→ℕ zero         = 0
binnat→ℕ (consOdd n)  = suc (doubleℕ (binnat→ℕ n))
binnat→ℕ (consEven n) = suc (suc (doubleℕ (binnat→ℕ n)))

suc-binnat : binnat → binnat
suc-binnat zero         = consOdd zero
suc-binnat (consOdd n)  = consEven n
suc-binnat (consEven n) = consOdd (suc-binnat n)

ℕ→binnat : ℕ → binnat
ℕ→binnat zero    = zero
ℕ→binnat (suc n) = suc-binnat (ℕ→binnat n)

binnat→ℕ-suc : (n : binnat) → binnat→ℕ (suc-binnat n) ≡ suc (binnat→ℕ n)
binnat→ℕ-suc zero         = refl
binnat→ℕ-suc (consOdd n)  = refl
binnat→ℕ-suc (consEven n) = λ i → suc (doubleℕ (binnat→ℕ-suc n i))

ℕ→binnat→ℕ : (n : ℕ) → binnat→ℕ (ℕ→binnat n) ≡ n
ℕ→binnat→ℕ zero    = refl
ℕ→binnat→ℕ (suc n) = (binnat→ℕ-suc (ℕ→binnat n)) ∙ (cong suc (ℕ→binnat→ℕ n))

suc-ℕ→binnat-double : (n : ℕ) → suc-binnat (ℕ→binnat (doubleℕ n)) ≡ consOdd (ℕ→binnat n)
suc-ℕ→binnat-double zero    = refl
suc-ℕ→binnat-double (suc n) = λ i → suc-binnat (suc-binnat (suc-ℕ→binnat-double n i))

binnat→ℕ→binnat : (n : binnat) → ℕ→binnat (binnat→ℕ n) ≡ n
binnat→ℕ→binnat zero        = refl
binnat→ℕ→binnat (consOdd n) =
           (suc-ℕ→binnat-double (binnat→ℕ n)) ∙ (cong consOdd (binnat→ℕ→binnat n))
binnat→ℕ→binnat (consEven n) =
           (λ i → suc-binnat (suc-ℕ→binnat-double (binnat→ℕ n) i)) ∙ (cong consEven (binnat→ℕ→binnat n))

ℕ≃binnat : ℕ ≃ binnat
ℕ≃binnat = isoToEquiv (iso ℕ→binnat binnat→ℕ binnat→ℕ→binnat ℕ→binnat→ℕ)

ℕ≡binnat : ℕ ≡ binnat
ℕ≡binnat = ua ℕ≃binnat

-- We can transport addition on ℕ to binnat
_+binnat_ : binnat → binnat → binnat
_+binnat_ = transport (λ i → ℕ≡binnat i → ℕ≡binnat i → ℕ≡binnat i) _+_

-- Test: 4 + 1 = 5
_ : consEven (consOdd zero) +binnat consOdd zero ≡ consOdd (consEven zero)
_ = refl

oddbinnat : binnat → Bool
oddbinnat zero         = false
oddbinnat (consOdd _)  = true
oddbinnat (consEven _) = false

oddℕ' : ℕ → Bool
oddℕ' = transport (λ i → ℕ≡binnat (~ i) → Bool) oddbinnat

-- The NatImpl example for this representation of binary numbers
private
  NatImplbinnat : NatImpl binnat
  z NatImplbinnat = zero
  s NatImplbinnat = suc-binnat

  -- Note that the s case is a bit simpler as no end-point correction
  -- is necessary (things commute strictly)
  NatImplℕ≡NatImplbinnat : PathP (λ i → NatImpl (ℕ≡binnat i)) NatImplℕ NatImplbinnat
  z (NatImplℕ≡NatImplbinnat i) = transp (λ j → ℕ≡binnat (i ∨ ~ j)) i zero
  s (NatImplℕ≡NatImplbinnat i) =
    λ x → glue (λ { (i = i0) → suc x
                  ; (i = i1) → suc-binnat x })
               (suc-binnat (unglue (i ∨ ~ i) x))

  oddSuc : (n : binnat) → oddbinnat n ≡ not (oddbinnat (suc-binnat n))
  oddSuc zero         = refl
  oddSuc (consOdd _)  = refl
  oddSuc (consEven _) = refl

  oddℕSuc' : (n : ℕ) → oddℕ' n ≡ not (oddℕ' (suc n))
  oddℕSuc' =
    let eq : (i : I) → ℕ≡binnat (~ i) → Bool
        eq i = transp (λ j → ℕ≡binnat (~ i ∨ ~ j) → Bool) (~ i) oddbinnat
    in transport
         (λ i → (n : ℕ≡binnat (~ i)) → eq i n ≡ not (eq i (NatImplℕ≡NatImplbinnat (~ i) .NatImpl.s n)))
         oddSuc

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


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

module Cubical.Categories.Limits.Pullback where

open import Cubical.Foundations.Prelude
open import Cubical.Categories.Limits.Base
open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Data.Sigma
open import Cubical.Categories.Instances.Cospan public

private
  variable
    ℓ ℓ' : Level

module _ {C : Precategory ℓ ℓ'} where

  open Precategory C
  open Functor

  record Cospan : Type (ℓ-max ℓ ℓ') where
    constructor cospan
    field
      l m r : ob
      s₁ : C [ l , m ]
      s₂ : C [ r , m ]

  record PullbackLegs (cspn : Cospan) (c : ob) : Type (ℓ-max ℓ ℓ') where
    constructor pblegs
    open Cospan cspn
    field
      p₁ : C [ c , l ]
      p₂ : C [ c , r ]

  record PullbackCone (cspn : Cospan) (c : ob) : Type (ℓ-max ℓ ℓ') where
    constructor cone
    open Cospan cspn
    field
      pl : PullbackLegs cspn c
    open PullbackLegs pl public
    field
      sq : p₁ ⋆⟨ C ⟩ s₁ ≡ p₂ ⋆⟨ C ⟩ s₂

  record isPullback (cspn : _) {c} (pb : PullbackLegs cspn c) : Type (ℓ-max ℓ ℓ') where
    open Cospan cspn
    open PullbackLegs
    field
      sq : pb .p₁ ⋆⟨ C ⟩ s₁ ≡ pb .p₂ ⋆⟨ C ⟩ s₂

    open PullbackCone
    field
      up : ∀ {d}
         → (pb' : PullbackCone cspn d)
         → isContr (Σ[ f ∈ (C [ d , c ]) ] ((pb' .p₁ ≡ f ⋆⟨ C ⟩ pb .p₁)
              × (pb' .p₂ ≡ f ⋆⟨ C ⟩ pb .p₂)))

  Cospan→Func : Cospan → Functor CospanCat C
  Cospan→Func (cospan l m r f g) .F-ob ⓪ = l
  Cospan→Func (cospan l m r f g) .F-ob ① = m
  Cospan→Func (cospan l m r f g) .F-ob ② = r
  Cospan→Func (cospan l m r f g) .F-hom {⓪} {①} k = f
  Cospan→Func (cospan l m r f g) .F-hom {②} {①} k = g
  Cospan→Func (cospan l m r f g) .F-hom {⓪} {⓪} k = id l
  Cospan→Func (cospan l m r f g) .F-hom {①} {①} k = id m
  Cospan→Func (cospan l m r f g) .F-hom {②} {②} k = id r
  Cospan→Func (cospan l m r f g) .F-id {⓪} = refl
  Cospan→Func (cospan l m r f g) .F-id {①} = refl
  Cospan→Func (cospan l m r f g) .F-id {②} = refl
  Cospan→Func (cospan l m r f g) .F-seq {⓪} {⓪} {⓪} φ ψ = sym (⋆IdL _)
  Cospan→Func (cospan l m r f g) .F-seq {⓪} {⓪} {①} φ ψ = sym (⋆IdL _)
  Cospan→Func (cospan l m r f g) .F-seq {⓪} {①} {①} φ ψ = sym (⋆IdR _)
  Cospan→Func (cospan l m r f g) .F-seq {①} {①} {①} φ ψ = sym (⋆IdL _)
  Cospan→Func (cospan l m r f g) .F-seq {②} {②} {②} φ ψ = sym (⋆IdL _)
  Cospan→Func (cospan l m r f g) .F-seq {②} {②} {①} φ ψ = sym (⋆IdL _)
  Cospan→Func (cospan l m r f g) .F-seq {②} {①} {①} φ ψ = sym (⋆IdR _)

  -- TODO: show that this definition of Pullback is equivalent to the Cospan limit

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:
open import Agda.Primitive
open import Agda.Builtin.Sigma

data Empty : Set where

_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
A ≃ B = Σ (A → B) λ f → Empty

record Iso {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') : Set (ℓ ⊔ ℓ') where
  field
    inv : B → A

postulate
  isoToEquiv : ∀{ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → Iso A B → A ≃ B

works : Iso (∀ {a : Set} → a) Empty
works = λ where
  .Iso.inv n → {!n!}

-- something like  (∀ {A : Set} → A)  seems to be necessary to trigger

test : (∀ {A : Set} → A) ≃ Empty
test = isoToEquiv λ where
  .Iso.inv n → {!n!}