text:
open import Agda.Builtin.Bool

works : Bool → Bool
works b with b | true
... | b′ | _ = b′

fails : Bool → Bool
fails b with b′ ← b | true
... | _ = b′


text:
module CS410-Functor where

open import CS410-Prelude

record Functor (T : Set -> Set) : Set1 where
  field
    -- OPERATIONS ----------------------------------------------
    map     : forall {X Y} -> (X -> Y) -> T X -> T Y
    -- LAWS ----------------------------------------------------
    mapid   : forall {X}(x : T X) -> map id x == x
    mapcomp : forall {X Y Z}(f : Y -> Z)(g : X -> Y)(x : T X) ->
              map (f o g) x == map f (map g x)

record Applicative (T : Set -> Set) : Set1 where
  field
    -- OPERATIONS ----------------------------------------------
    pure         : forall {X} -> X -> T X
    _<*>_        : forall {X Y} -> T (X -> Y) -> T X -> T Y
    -- LAWS ----------------------------------------------------
    identity     : forall {X}(v : T X) ->

                      pure id <*> v == v

    composition  : forall {X Y Z}(u : T (Y -> Z))(v : T (X -> Y))(w : T X) ->

                      pure (\ f g x -> f (g x)) <*> u <*> v <*> w == u <*> (v <*> w)

    homomorphism : forall {X Y}(f : X -> Y)(x : X) ->

                      pure (f x) == pure f <*> pure x

    interchange  : forall {X Y}(u : T (X -> Y))(y : X) ->

                      u <*> pure y == pure (\ f -> f y) <*> u

  infixl 10 _<*>_

App2Fun : {T : Set -> Set} -> Applicative T -> Functor T
App2Fun {T} app = record {
  map     = \ f x -> pure f <*> x;
  mapid   = identity;
  mapcomp = lem}
  where
    open Applicative app
    lem : forall {X Y Z}(f : Y -> Z)(g : X -> Y)(x : T X) ->
          pure (\ x -> f (g x)) <*> x == pure f <*> (pure g <*> x)
    lem {X}{Y}{Z} f g x rewrite
        (sym (composition (pure f) (pure g) x))
      | (sym (homomorphism (\ (f : Y -> Z)(g : X -> Y) x -> f (g x)) f))
      | (sym (homomorphism (\ (g : X -> Y) x -> f (g x)) g))
      = refl

record Traversable (T : Set -> Set) : Set1 where
  field
    -- OPERATIONS ----------------------------------------------
    traverse  : forall {F} -> Applicative F ->
                forall {A B} -> (A -> F B) -> T A -> F (T B)
    -- LAWS ----------------------------------------------------
    -- maybe later

record Monad (T : Set -> Set) : Set1 where
  field
    -- OPERATIONS ----------------------------------------------
    return       : forall {X} -> X -> T X
    _>>=_        : forall {X Y} -> T X -> (X -> T Y) -> T Y
    -- LAWS ----------------------------------------------------
    law1 : forall {X Y}(x : X)(f : X -> T Y) -> return x >>= f == f x
    law2 : forall {X}(t : T X) -> t >>= return == t
    law3 : forall {X Y Z}(f : X -> T Y)(g : Y -> T Z)(t : T X) ->
           (t >>= f) >>= g == t >>= (\ x -> f x >>= g)
  -- DERIVED OPERATIONS
  _<=<_ : {X Y Z : Set} -> (Y -> T Z) -> (X -> T Y) -> (X -> T Z)
  (f <=< g) x = g x >>= f

  infixr 5 _>>=_

record Monad-Alg {T : Set -> Set}(M : Monad T) : Set1 where
  field
    -- OPERATIONS ----------------------------------------------
    A : Set
    A-map : forall {X} -> (X -> A) -> T X -> A
  open Monad M
     -- LAWS ----------------------------------------------------
  field
    A-law1 : forall {X}(f : X -> A)(x : X) -> A-map f (return x) == f x
    A-law2 : forall {X Y}(g : X -> T Y)(f : Y -> A)(t : T X) ->
             A-map (A-map f o g) t == A-map f (t >>= g)

ext: agda


text:
module DualTail1 where

open import Data.Nat
open import Data.Fin using (Fin; zero; suc)
open import Data.Product

open import Function using (id; _∘_)

open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import Types.Direction

open import Types.IND1 as IND hiding (GType; Type; SType; _≈_; _≈'_)
import Types.COI as COI
open import Types.Tail1

private
  variable
    n : ℕ

-- instead of unrolling and substituting, we maintain a stack of bodies of recursive types

data Stack {GType : ℕ → Set} : ℕ → Set where
  ε : Stack 0
  ⟪_,_⟫ : Stack {GType} n → GType (suc n) → Stack (suc n)

-- obtain an entry from the stack
-- technically m = n - i, but we don't need to know

get : ∀ {GType} (i : Fin n) → Stack {GType} n → Σ ℕ λ m → Stack {GType} m × GType (suc m)
get zero ⟪ σ , x ⟫ = _ , (σ , x)
get (suc i) ⟪ σ , x ⟫ = get i σ

-- the dual of a stack

dual-stack : Stack {GType} n → Stack  {GType} n
dual-stack ε = ε
dual-stack ⟪ σ , g ⟫ = ⟪ dual-stack σ , dualG g ⟫

-- relate a stack entry to the corresponding entry on the dual stack

get-dual-stack : (x : Fin n) (σ : Stack n) →
  get x (dual-stack σ) ≡ map id (map dual-stack dualG) (get x σ)
get-dual-stack zero ⟪ σ , x ⟫ = refl
get-dual-stack (suc x) ⟪ σ , x₁ ⟫ = get-dual-stack x σ

-- stacked version of general mapping of inductive session type to COI

ind2coiS : Stack {IND.GType} n → IND.SType n → COI.SType
ind2coiG : Stack {IND.GType} n → IND.GType n → COI.STypeF COI.SType
ind2coiT : Stack {IND.GType} n → IND.TType n → COI.Type

COI.SType.force (ind2coiS σ (gdd G)) = ind2coiG σ G
COI.SType.force (ind2coiS σ (rec G)) = ind2coiG ⟪ σ , G ⟫ G
COI.SType.force (ind2coiS σ (var x)) with get x σ
... | m , σ' , gxs = ind2coiG ⟪ σ' , gxs ⟫ gxs

ind2coiG σ (transmit d T S) = COI.transmit d (ind2coiT σ T) (ind2coiS σ S)
ind2coiG σ (choice d m alt) = COI.choice d m (ind2coiS σ ∘ alt)
ind2coiG σ end = COI.end

ind2coiT σ TUnit = COI.TUnit
ind2coiT σ TInt = COI.TInt
ind2coiT σ (TPair T T₁) = COI.TPair (ind2coiT σ T) (ind2coiT σ T₁)
ind2coiT σ (TChan S) = COI.TChan (ind2coiS σ S)

-- mapping tail recursive session types to coinductive session types
-- relies on a stack to unfold variables on the fly

tail2coiT : Type → COI.Type
tail2coiS : Stack {GType} n → SType n → COI.SType
tail2coiG : Stack {GType} n → GType n → COI.STypeF COI.SType

tail2coiT TUnit = COI.TUnit
tail2coiT TInt = COI.TInt
tail2coiT (TPair t t₁) = COI.TPair (tail2coiT t) (tail2coiT t₁)
tail2coiT (TChan s) = COI.TChan (ind2coiS ε s)

COI.SType.force (tail2coiS σ (gdd g)) = tail2coiG σ g
COI.SType.force (tail2coiS σ (rec g)) = tail2coiG ⟪ σ , g ⟫ g
COI.SType.force (tail2coiS σ (var x))
  with get x σ
... | m , σ' , gxs = tail2coiG ⟪ σ' , gxs ⟫ gxs

tail2coiG σ (transmit d t s) = COI.transmit d (tail2coiT t) (tail2coiS σ s)
tail2coiG σ (choice d m alt) = COI.choice d m (tail2coiS σ ∘ alt)
tail2coiG σ end = COI.end

-- get coinductive bisimulation in scope

_≈_ = COI._≈_
_≈'_ = COI._≈'_

-- main proposition

dual-tailS : (σ : Stack {GType} n) (s : SType n) →
  COI.dual (tail2coiS σ s) ≈ tail2coiS (dual-stack σ) (dualS s)
dual-tailG : (σ : Stack {GType} n) (g : GType n) →
  COI.dualF (tail2coiG σ g) ≈' tail2coiG (dual-stack σ) (dualG g)

COI.Equiv.force (dual-tailS σ (gdd g)) = dual-tailG σ g
COI.Equiv.force (dual-tailS σ (rec g)) = dual-tailG ⟪ σ , g ⟫ g
COI.Equiv.force (dual-tailS σ (var x))
  rewrite get-dual-stack x σ
  with get x σ
... | m , σ' , g = dual-tailG ⟪ σ' , g ⟫ g

dual-tailG σ (transmit d t s) = COI.eq-transmit (dual-dir d) COI.≈ᵗ-refl (dual-tailS σ s)
dual-tailG σ (choice d m alt) = COI.eq-choice (dual-dir d) (dual-tailS σ ∘ alt)
dual-tailG σ end = COI.eq-end

-- corrolary for SType 0

dual-tail : ∀ s → COI.dual (tail2coiS ε s) ≈ tail2coiS ε (dualS s)
dual-tail = dual-tailS ε

max_stars_repo_name: peterthiemann/dual-session

max_issues_repo_name: peterthiemann/dual-session

max_forks_repo_name: peterthiemann/dual-session


text:
open import Data.Nat
open import Data.Nat.Show
open import IO

module Ackermann where

ack : ℕ -> ℕ -> ℕ
ack zero n = n + 1
ack (suc m) zero = ack m 1
ack (suc m) (suc n) = ack m (ack (suc m) n)

main = run (putStrLn (show (ack 3 9)))

max_issues_repo_name: seanwallawalla-forks/RosettaCodeData

max_forks_repo_name: seanwallawalla-forks/RosettaCodeData


text:
{-# OPTIONS --type-in-type #-}
module CS410-Categories where

open import CS410-Prelude

postulate
  extensionality : {S : Set}{T : S -> Set}
                   {f g : (x : S) -> T x} ->
                   ((x : S) -> f x == g x) ->
                   f == g

imp : {S : Set}{T : S -> Set}(f : (x : S) -> T x){x : S} -> T x
imp f {x} = f x

extensionality' : {S : Set}{T : S -> Set}
                   {f g : {x : S} -> T x} ->
                   ((x : S) -> f {x} == g {x}) ->
                   _==_ {forall {x : S} -> T x} f g
extensionality' {f = f}{g = g} q =
  refl imp =$= extensionality {f = \ x -> f {x}}{g = \ x -> g {x}}
    q

_=$'_ : {S : Set}{T : S -> Set}
       {f g : {x : S} -> T x} ->
       _==_ {forall {x : S} -> T x} f g ->
       (x : S) -> f {x} == g {x}
refl f =$' x = refl (f {x})

infixl 2 _=$'_

record Category : Set where
  field

    -- two types of thing
    Obj  : Set                  -- "objects"
    _~>_ : Obj -> Obj -> Set    -- "arrows" or "morphisms"
                                -- or "homomorphisms"

    -- two operations
    id~>        : {T : Obj} ->      T ~> T
    _>~>_       : {R S T : Obj} ->  R ~> S  ->  S ~> T  ->  R ~> T

    -- three laws
    law-id~>>~> : {S T : Obj}     (f : S ~> T) ->
                    (id~> >~> f) == f
    law->~>id~> : {S T : Obj}     (f : S ~> T) ->
                    (f >~> id~>) == f
    law->~>>~>  : {Q R S T : Obj} (f : Q ~> R)(g : R ~> S)(h : S ~> T) ->
                    ((f >~> g) >~> h) == (f >~> (g >~> h))

  assocn : {Q R R' S T : Obj}
            {f  : Q ~> R} {g : R ~> S}
            {f' : Q ~> R'}{g' : R' ~> S}
            {h : S ~> T} ->
            (f >~> g) == (f' >~> g') ->
            (f >~> g >~> h) == (f' >~> g' >~> h)
  assocn {f = f} {g = g} {f' = f'} {g' = g'} {h = h} q =
    f >~> g >~> h
      =< law->~>>~> _ _ _ ]=
    (f >~> g) >~> h
      =[ refl _>~>_ =$= q =$= refl h >=
    (f' >~> g') >~> h
      =[ law->~>>~> _ _ _ >=
    f' >~> g' >~> h
      [QED]

  infixr 3 _>~>_

-- Sets and functions are the classic example of a category.
SET : Category
SET = record
        { Obj         = Set
        ; _~>_        = \ S T -> S -> T
        ; id~>        = id
        ; _>~>_       = _>>_
        ; law-id~>>~> = \ f -> refl f
        ; law->~>id~> = \ f -> refl f
        ; law->~>>~>  = \ f g h -> refl (f >> (g >> h))
        }

module FUNCTOR where
  open Category

  record _=>_ (C D : Category) : Set where  -- "Functor from C to D"
    field
      -- two actions
      F-Obj : Obj C -> Obj D
      F-map : {S T : Obj C} -> _~>_ C S T -> _~>_ D (F-Obj S) (F-Obj T)

      -- two laws
      F-map-id~> : {T : Obj C} -> F-map (id~> C {T}) == id~> D {F-Obj T}
      F-map->~>  : {R S T : Obj C}(f : _~>_ C R S)(g : _~>_ C S T) ->
                     F-map (_>~>_ C f g) == _>~>_ D (F-map f) (F-map g)

open FUNCTOR public

ID : {C : Category} -> C => C
ID = record
   { F-Obj = id
   ; F-map = id
   ; F-map-id~> = refl _
   ; F-map->~>  = \ f g -> refl _
   }

module FUNCTOR-CP {C D E : Category} where
  open _=>_
  open Category

  _>=>_ : C => D  ->  D => E  ->  C => E

  F-Obj (F >=> G) = F-Obj F >> F-Obj G

  F-map (F >=> G) = F-map F >> F-map G

  F-map-id~> (F >=> G) =
    F-map G (F-map F (id~> C))
      =[ refl (F-map G) =$= F-map-id~> F >=
    F-map G (id~> D)
      =[ F-map-id~> G >=
    id~> E
      [QED]

  F-map->~> (F >=> G) f g =
    F-map G (F-map F (_>~>_ C f g))
      =[ refl (F-map G) =$= F-map->~> F f g >=
    F-map G (_>~>_ D (F-map F f) (F-map F g))
      =[ F-map->~> G (F-map F f) (F-map F g) >=
    _>~>_ E (F-map G (F-map F f)) (F-map G (F-map F g))
      [QED]

open FUNCTOR-CP public

module NATURAL-TRANSFORMATION {C D : Category} where
  open Category
  open _=>_

  record _~~>_ (F G : C => D) : Set where
    field
      -- one operation
      xf : {X : Obj C} -> _~>_ D (F-Obj F X) (F-Obj G X)
      -- one law
      naturality : {X Y : Obj C}(f : _~>_ C X Y) ->
                   _>~>_ D (F-map F f) (xf {Y})
                   ==
                   _>~>_ D (xf {X}) (F-map G f)

open NATURAL-TRANSFORMATION public
open _~~>_ public

module MONAD {C : Category}(M : C => C) where
  open Category C
  open _=>_ M

  record Monad : Set where
    field
      unit :        ID ~~> M
      mult : (M >=> M) ~~> M

      unitMult : {X : Obj} -> (xf unit >~> xf mult) == id~> {F-Obj X}
      multUnit : {X : Obj} -> (F-map (xf unit) >~> xf mult) == id~> {F-Obj X}
      multMult : {X : Obj} -> (xf mult >~> xf mult) == (F-map (xf mult) >~> xf mult {X})

    KLEISLI : Category
    KLEISLI = record
      { Obj = Obj
      ; _~>_ = \ S T -> S ~> F-Obj T
      ; id~>  = xf unit
      ; _>~>_ = \ f g -> f >~> F-map g >~> xf mult
      ; law-id~>>~> = \ f ->
        xf unit >~> F-map f >~> xf mult
          =< law->~>>~> _ _ _ ]=
        (xf unit >~> F-map f) >~> xf mult
          =< refl (_>~> xf mult) =$= naturality unit f ]=
        (f >~> xf unit) >~> xf mult
          =[ law->~>>~> _ _ _ >=
        f >~> (xf unit >~> xf mult)
          =[ refl (f >~>_) =$= unitMult >=
        f >~> id~>
          =[ law->~>id~> f >=
        f [QED]
      ; law->~>id~> = \ f ->
        f >~> (F-map (xf unit) >~> xf mult)
          =[ refl (f >~>_) =$= multUnit >=
        f >~> id~>
          =[ law->~>id~> f >=
        f [QED]
      ; law->~>>~> = \ f g h ->
        (f >~> F-map g >~> xf mult) >~> F-map h >~> xf mult
          =[ law->~>>~> _ _ _ >=
        f >~> (F-map g >~> xf mult) >~> (F-map h >~> xf mult)
          =[ refl (\ x -> _ >~> x) =$= law->~>>~> _ _ _ >=
        f >~> F-map g >~> xf mult >~> F-map h >~> xf mult
          =< refl (\ x -> _ >~> _ >~> x) =$= assocn (naturality mult _) ]=
        f >~> F-map g >~> F-map (F-map h) >~> xf mult >~> xf mult
          =[ refl (\ x -> _ >~> _ >~> _ >~> x) =$= multMult >=
        f >~> F-map g >~> F-map (F-map h) >~> F-map (xf mult) >~> xf mult
          =< refl (\ x -> _ >~> _ >~> x) =$= law->~>>~> _ _ _ ]=
        f >~> F-map g >~> (F-map (F-map h) >~> F-map (xf mult)) >~> xf mult
          =< refl (\ x -> _ >~> _ >~> x >~> _) =$= F-map->~> _ _ ]=
        f >~> F-map g >~> F-map (F-map h >~> xf mult) >~> xf mult
          =< refl (\ x -> _ >~> x) =$= law->~>>~> _ _ _ ]=
        f >~> (F-map g >~> F-map (F-map h >~> xf mult)) >~> xf mult
          =< refl (\ x -> _ >~> x >~> _) =$= F-map->~> _ _ ]=
        f >~> F-map (g >~> F-map h >~> xf mult) >~> xf mult
          [QED]
      }


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.Pair {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening as T hiding (wk; wkTerm; wkEqTerm)
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Weakening
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Application
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties
open import Definition.LogicalRelation.Substitution.Reflexivity
open import Definition.LogicalRelation.Substitution.Introductions.Sigma
open import Definition.LogicalRelation.Substitution.Introductions.Pi
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Valid pair construction.
⦅⦆ᵛ : ∀ {F G l∃ t u Γ l}
       ([Γ] : ⊩ᵛ Γ)
       ([F] : Γ ⊩ᵛ⟨ l ⟩ F ^ [ % , ι l∃ ] / [Γ])
       ([G] : Γ ∙ F ^ [ % , ι l∃ ] ⊩ᵛ⟨ l ⟩ G ^ [ % , ι l∃ ] / [Γ] ∙ [F])
       ([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ F ^ [ % , ι l∃ ] / [Γ] / [F])
       ([u] : Γ ⊩ᵛ⟨ l ⟩ u ∷ G [ t ] ^ [ % , ι l∃ ] / [Γ] / substS {F} {G} {t} [Γ] [F] [G] [t])
          → Γ ⊩ᵛ⟨ l ⟩ ⦅ G , t , u ⦆ ∷ ∃ F ▹ G ^ [ % , ι l∃ ] / [Γ] / ∃ᵛ {F} {G} [Γ] [F] [G]
⦅⦆ᵛ {F} {G} {l∃} {t} {u} {Γ} {l} [Γ] [F] [G] [t] [u] {Δ = Δ} {σ = σ} ⊢Δ [σ] =
  let [G[t]] = substS {F} {G} {t} [Γ] [F] [G] [t]
      [ΠFG] = Πᵛ {F = F} {G = G} (≡is≤ PE.refl) (≡is≤ PE.refl) [Γ] [F] [G]
      [σF] = proj₁ ([F] ⊢Δ [σ])
      ⊢F = escape [σF]
      [σG] = proj₁ ([G] (⊢Δ ∙ ⊢F) (liftSubstS {F = F} [Γ] ⊢Δ [F] [σ]))
      ⊢G = escape [σG]
      [σt] = proj₁ ([t] (⊢Δ) [σ])
      ⊢t = escapeTerm [σF] [σt]
      [σu] = proj₁ ([u] (⊢Δ) [σ])
      [σG[t]] = proj₁ ([G[t]] ⊢Δ [σ])
      [σΠFG] = proj₁ ([ΠFG] ⊢Δ [σ])
      [σG[t]]′ = irrelevance′ (singleSubstLift G t) [σG[t]]
      [σu]′ = irrelevanceTerm′ (singleSubstLift G t) PE.refl PE.refl [σG[t]] [σG[t]]′ [σu]
      ⊢u = escapeTerm [σG[t]]′ [σu]′
      ⦅t,u⦆ⱼ = ⦅_,_,_,_⦆ⱼ {F = subst σ F} {G = subst (liftSubst σ) G} {t = subst σ t} {u = subst σ u}
                      ⊢F ⊢G ⊢t ⊢u
  in ⦅t,u⦆ⱼ , λ {σ′} [σ′] [σ≡σ′] →
            ⦅t,u⦆ⱼ ,
            let ⊢Γ = wfTerm ⊢t
                [σt′] = proj₁ ([t] ⊢Δ [σ′])
                [σt≡σt′] = proj₂ ([t] ⊢Δ [σ]) [σ′] [σ≡σ′]
                [σF′] = proj₁ ([F] ⊢Δ [σ′])
                ⊢F′ = escape [σF′]
                ⊢t′ = escapeTerm [σF′] [σt′]
                [σG′] = proj₁ ([G] {σ = liftSubst σ′} (⊢Δ ∙ ⊢F′) (liftSubstS {F = F} [Γ] ⊢Δ [F] [σ′]))
                ⊢G′ = escape [σG′]
                _ , Πᵣ _ _ _  _ _ F′ G′ D′ _ _  A≡A′ [F]₁ [G]₁ G-ext =
                  extractMaybeEmb (Π-elim (proj₁ ([ΠFG] ⊢Δ [σ′])))
                [σ′u] = proj₁ ([u] ⊢Δ [σ′])
                [σ′G[t]] = proj₁ ([G[t]] ⊢Δ [σ′])
                [σ′G[t]]′ = irrelevance′ (singleSubstLift G t) [σ′G[t]]
                [σ′u]′ = irrelevanceTerm′ (singleSubstLift G t) PE.refl PE.refl [σ′G[t]] [σ′G[t]]′ [σ′u]
                ⊢u′ = escapeTerm [σ′G[t]]′ [σ′u]′
                pair' =  ⦅_,_,_,_⦆ⱼ {F = subst σ′ F} {G = subst (liftSubst σ′) G} {t = subst σ′ t}
                                  {u = subst σ′ u} ⊢F′ ⊢G′ ⊢t′ ⊢u′
                [σ′≡σ]  = symS [Γ] ⊢Δ [σ] [σ′] [σ≡σ′]
                [σF′≡σF] = proj₂ ([F] ⊢Δ [σ′]) [σ] [σ′≡σ]
                σF′≡σF = escapeEq [σF′] [σF′≡σF]
                [liftσ] = liftSubstS {F = F} [Γ] ⊢Δ [F] [σ]
                [wk1σ′] = wk1SubstS [Γ] ⊢Δ ⊢F′ [σ′]
                [wk1σ] = wk1SubstS [Γ] ⊢Δ ⊢F′ [σ]
                foo = proj₁ ([F] (⊢Δ ∙ ⊢F′) [wk1σ′])
                [liftσ′] : (Δ ∙ subst σ′ F ^ [ % , ι l∃ ]) ⊩ˢ liftSubst σ ∷
                           Γ ∙ F ^ [ % , ι l∃ ] / [Γ] ∙ [F] / (⊢Δ ∙ escape (proj₁ ([F] ⊢Δ [σ′])))
                [liftσ′] =   let ⊢F = escape (proj₁ ([F] ⊢Δ [σ]))
                                 [tailσ] = wk1SubstS {F = subst σ′ F} [Γ] ⊢Δ (escape (proj₁ ([F] ⊢Δ [σ′]))) [σ]
                                 var0′ : (Δ ∙ subst σ′ F ^ [ % , ι l∃ ]) ⊢ var 0 ∷ subst (wk1Subst σ′) F ^ [ % , ι l∃ ]
                                 var0′ = var (⊢Δ ∙ ⊢F′) (PE.subst (λ x → 0 ∷ x ^ _ ∈ (Δ ∙ subst σ′ F ^ _))
                                             (wk-subst F) here)
                                 var0 = conv var0′ (≅-eq (escapeEq (proj₁ ([F] (⊢Δ ∙ ⊢F′) [wk1σ′])) (proj₂ ([F] (⊢Δ ∙ ⊢F′) [wk1σ′]) [wk1σ]
                                                            (wk1SubstSEq [Γ] ⊢Δ ⊢F′ [σ′] [σ′≡σ]))))
                             in  [tailσ] , neuTerm (proj₁ ([F] (⊢Δ ∙ ⊢F′) [tailσ])) (var 0)
                                 var0 (~-var var0)
                [σG′≡σG] = proj₂ ([G] (⊢Δ ∙ ⊢F′) (liftSubstS {F = F} [Γ] ⊢Δ [F] [σ′] )) [liftσ′]
                                 (liftSubstSEq {F = F} [Γ] ⊢Δ [F] [σ′] (symS [Γ] ⊢Δ [σ] [σ′] [σ≡σ′]))
                σG′≡σG = escapeEq [σG′] [σG′≡σG]
             in conv pair' (univ (∃-cong ⊢F′ (un-univ≡ (≅-eq σF′≡σF)) (un-univ≡ (≅-eq σG′≡σG))) )

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


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

open import lib.Basics
open import lib.types.Lift
open import lib.types.Paths
open import lib.types.Pointed

module lib.types.Unit where

tt = unit

⊙Unit : Ptd₀
⊙Unit = ⊙[ Unit , unit ]

abstract
  -- Unit is contractible
  Unit-is-contr : is-contr Unit
  Unit-is-contr = (unit , λ y → idp)

  Unit-has-level : {n : ℕ₋₂} → has-level n Unit
  Unit-has-level = contr-has-level Unit-is-contr

  -- [Unit-has-level#instance] produces unsolved metas
  Unit-has-level-S#instance : {n : ℕ₋₂} → has-level (S n) Unit
  Unit-has-level-S#instance = contr-has-level Unit-is-contr

  Unit-is-prop : is-prop Unit
  Unit-is-prop = Unit-has-level

  Unit-is-set : is-set Unit
  Unit-is-set = Unit-has-level

Unit-level = Unit-is-contr
⊤-is-contr = Unit-is-contr
⊤-level = Unit-is-contr
⊤-has-level = Unit-has-level
⊤-is-prop = Unit-is-prop
⊤-is-set = Unit-is-set

LiftUnit-⊙in-level : ∀ {i j} {X : Ptd i}
  → is-contr (fst (X ⊙→ ⊙Lift {j = j} ⊙Unit))
LiftUnit-⊙in-level {X = X} =
  (⊙cst {X = X} ,
   λ f → pair= idp
           (prop-has-all-paths ((Lift-level Unit-is-set) _ _) idp (snd f)))

LiftUnit-⊙out-level : ∀ {i j} {X : Ptd i}
  → is-contr (fst (⊙Lift {j = j} ⊙Unit ⊙→ X))
LiftUnit-⊙out-level {X = X} =
  (⊙cst {Y = X} ,
   λ f → ⊙λ= (λ _ → ! (snd f)) (! (!-inv-l (snd f))))

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
module _ where

-- Should not be able to give by name
id : {_ = A : Set} → A → A
id x = x

works : (X : Set) → X → X
works X = id {X}

fails : (X : Set) → X → X
fails X = id {A = X}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

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

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

max_stars_repo_name: scott-fleischman/GreekGrammar

max_issues_repo_name: scott-fleischman/GreekGrammar

max_forks_repo_name: scott-fleischman/GreekGrammar


text:
module Chain
    { A : Set }
    (_==_  : A -> A -> Set )
    (refl  : (x : A) -> x == x)
    (trans : (x y z : A) -> x == y -> y == z -> x == z)
  where

  infix 2 chain>_
  infixl 2 _===_
  infix 3 _by_

  chain>_ : (x : A) -> x == x
  chain> x = refl _

  _===_ : {x y z : A} -> x == y -> y == z -> x == z
  xy === yz = trans _ _ _ xy yz

  _by_ : {x : A}(y : A) -> x == y -> x == y
  y by eq = eq


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

open import Algebra.Construct.DirectProduct

module Construct.DirectProduct where

open import Algebra.Bundles
import Algebra.Construct.DirectProduct as DirectProduct
open import Data.Product
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Level using (Level; _⊔_)

private
  variable
    a b ℓ₁ ℓ₂ : Level


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Core lemmas for division and modulus operations
------------------------------------------------------------------------

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

module Data.Nat.DivMod.Core where

open import Agda.Builtin.Nat using ()
  renaming (div-helper to divₕ; mod-helper to modₕ)

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality

open ≡-Reasoning

-------------------------------------------------------------------------
-- mod lemmas

modₕ-skipTo0 : ∀ acc n a b → modₕ acc n (b + a) a ≡ modₕ (a + acc) n b 0
modₕ-skipTo0 acc n zero    b = cong (λ v → modₕ acc n v 0) (+-identityʳ b)
modₕ-skipTo0 acc n (suc a) b = begin
  modₕ acc n (b + suc a) (suc a) ≡⟨ cong (λ v → modₕ acc n v (suc a)) (+-suc b a) ⟩
  modₕ acc n (suc b + a) (suc a) ≡⟨⟩
  modₕ (suc acc) n (b + a) a     ≡⟨ modₕ-skipTo0 (suc acc) n a b ⟩
  modₕ (a + suc acc) n b 0       ≡⟨ cong (λ v → modₕ v n b 0) (+-suc a acc) ⟩
  modₕ (suc a + acc) n b 0       ∎

modₕ-skipToEnd : ∀ acc n a b → modₕ acc n a (a + b) ≡ acc + a
modₕ-skipToEnd acc n zero    b = sym (+-identityʳ acc)
modₕ-skipToEnd acc n (suc a) b = begin
  modₕ (suc acc) n a (a + b) ≡⟨ modₕ-skipToEnd (suc acc) n a b ⟩
  suc acc + a                ≡⟨ sym (+-suc acc a) ⟩
  acc + suc a                ∎

a[modₕ]1≡0 : ∀ a → modₕ 0 0 a 0 ≡ 0
a[modₕ]1≡0 zero    = refl
a[modₕ]1≡0 (suc a) = a[modₕ]1≡0 a

n[modₕ]n≡0 : ∀ acc v → modₕ acc (acc + v) (suc v) v ≡ 0
n[modₕ]n≡0 acc v = modₕ-skipTo0 acc (acc + v) v 1

a[modₕ]n<n : ∀ acc d n → modₕ acc (acc + n) d n ≤ acc + n
a[modₕ]n<n acc zero    n       = m≤m+n acc n
a[modₕ]n<n acc (suc d) zero    = a[modₕ]n<n zero d (acc + 0)
a[modₕ]n<n acc (suc d) (suc n)
           rewrite +-suc acc n = a[modₕ]n<n (suc acc) d n

modₕ-idem : ∀ acc a n → modₕ 0 (acc + n) (modₕ acc (acc + n) a n) (acc + n) ≡ modₕ acc (acc + n) a n
modₕ-idem acc zero    n       = modₕ-skipToEnd 0 (acc + n) acc n
modₕ-idem acc (suc a) zero    rewrite +-identityʳ acc = modₕ-idem 0 a acc
modₕ-idem acc (suc a) (suc n) rewrite +-suc acc n = modₕ-idem (suc acc) a n

a+n[modₕ]n≡a[modₕ]n : ∀ acc a n → modₕ acc (acc + n) (acc + a + suc n) n ≡ modₕ acc (acc + n) a n
a+n[modₕ]n≡a[modₕ]n acc zero n rewrite +-identityʳ acc = begin
  modₕ acc (acc + n) (acc + suc n) n   ≡⟨ cong (λ v → modₕ acc (acc + n) v n) (+-suc acc n) ⟩
  modₕ acc (acc + n) (suc acc + n) n   ≡⟨ modₕ-skipTo0 acc (acc + n) n (suc acc) ⟩
  modₕ (acc + n) (acc + n) (suc acc) 0 ≡⟨⟩
  modₕ 0 (acc + n) acc (acc + n)       ≡⟨ modₕ-skipToEnd 0 (acc + n) acc n ⟩
  acc                                  ∎
a+n[modₕ]n≡a[modₕ]n acc (suc a) zero rewrite +-identityʳ acc = begin
  modₕ acc acc (acc + suc a + 1)   0   ≡⟨ cong (λ v → modₕ acc acc v 0) (+-comm (acc + suc a) 1) ⟩
  modₕ acc acc (1 + (acc + suc a)) 0   ≡⟨⟩
  modₕ 0   acc (acc + suc a)       acc ≡⟨ cong (λ v → modₕ 0 acc v acc) (+-comm acc (suc a)) ⟩
  modₕ 0   acc (suc a + acc)       acc ≡⟨ cong (λ v → modₕ 0 acc v acc) (sym (+-suc a acc)) ⟩
  modₕ 0   acc (a + suc acc)       acc ≡⟨ a+n[modₕ]n≡a[modₕ]n 0 a acc ⟩
  modₕ 0   acc a                   acc ∎
a+n[modₕ]n≡a[modₕ]n acc (suc a) (suc n) rewrite +-suc acc n = begin
  mod₁ (acc + suc a + (2 + n)) (suc n) ≡⟨ cong (λ v → mod₁ (v + suc (suc n)) (suc n)) (+-suc acc a) ⟩
  mod₁ (suc acc + a + (2 + n)) (suc n) ≡⟨⟩
  mod₂ (acc + a + (2 + n))     n       ≡⟨ cong (λ v → mod₂ v n) (sym (+-assoc (acc + a) 1 (suc n))) ⟩
  mod₂ (acc + a + 1 + suc n)   n       ≡⟨ cong (λ v → mod₂ (v + suc n) n) (+-comm (acc + a) 1) ⟩
  mod₂ (suc acc + a + suc n)   n       ≡⟨ a+n[modₕ]n≡a[modₕ]n (suc acc) a n ⟩
  mod₂ a                       n       ∎
  where
  mod₁ = modₕ acc       (suc acc + n)
  mod₂ = modₕ (suc acc) (suc acc + n)

-------------------------------------------------------------------------
-- division lemmas

-- The quotient and remainder are related to the dividend and
-- divisor in the right way.

division-lemma : ∀ accᵐ accᵈ d n →
    accᵐ + accᵈ * suc (accᵐ + n) + d ≡
    modₕ accᵐ (accᵐ + n) d n + divₕ accᵈ (accᵐ + n) d n * suc (accᵐ + n)
division-lemma accᵐ accᵈ zero    n    = +-identityʳ _
division-lemma accᵐ accᵈ (suc d) zero rewrite +-identityʳ accᵐ = begin
  accᵐ + accᵈ * suc accᵐ + suc d          ≡⟨ +-suc _ d ⟩
  suc accᵈ * suc accᵐ + d                 ≡⟨ division-lemma zero (suc accᵈ) d accᵐ ⟩
  modₕ 0          accᵐ d accᵐ +
  divₕ (suc accᵈ) accᵐ d accᵐ * suc accᵐ  ≡⟨⟩
  modₕ accᵐ accᵐ (suc d) 0 +
  divₕ accᵈ accᵐ (suc d) 0 * suc accᵐ     ∎
division-lemma accᵐ accᵈ (suc d) (suc n) rewrite +-suc accᵐ n = begin
  accᵐ + accᵈ * m + suc d             ≡⟨ +-suc _ d ⟩
  suc (accᵐ + accᵈ * m + d)           ≡⟨ division-lemma (suc accᵐ) accᵈ d n ⟩
  modₕ _ _ d n + divₕ accᵈ _ d n * m  ∎
  where
  m = 2 + accᵐ + n


text:
open import SOAS.Metatheory.Syntax

-- Metasubstitution operation
module SOAS.Metatheory.SecondOrder.Metasubstitution {T : Set}(Syn : Syntax {T}) where

open Syntax Syn

open import SOAS.Metatheory.FreeMonoid Syn

open import SOAS.Common
open import SOAS.Families.Core {T}
open import SOAS.Families.Build
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Construction.Structure as Structure
open import SOAS.ContextMaps.Combinators
open import SOAS.ContextMaps.CategoryOfRenamings

open import SOAS.Abstract.Hom
open import SOAS.Abstract.ExpStrength
import SOAS.Abstract.Coalgebra as →□
open →□.Sorted
import SOAS.Abstract.Box as □ ; open □.Sorted

open import Categories.Monad

open import SOAS.Coalgebraic.Monoid

open import SOAS.Metatheory Syn

private
  variable
    Γ Δ Π : Ctx
    α β τ : T
    𝔛 𝔜 ℨ : Familyₛ
    𝔐 𝔑 : MCtx

open Theory

-- Ground metasubstitution from the monad structure
msub₀ : (𝔛 ⇾̣ 𝕋 𝔜) → 𝕋 𝔛 ⇾̣ 𝕋 𝔜
msub₀ {𝔛}{𝔜} κ t = μ.η 𝔜 (F.₁ κ t) where open Monad ΣMon:Monad

-- Meta-algebra structure on the exponential [ 𝔛 ⊸ 𝒫 ] ⇨ ℳ
[_⊸_]⇨_ᵃ : (𝔛 {𝒫}{ℳ} : Familyₛ) → Coalg 𝒫 → ΣMon ℳ → (𝒫 ⇾̣ ℳ)
         → MetaAlg 𝔛 ([ 𝔛 ⊸ 𝒫 ] ⇨ ℳ)
[_⊸_]⇨_ᵃ 𝔛 {𝒫}{ℳ} 𝒫ᵇ Σℳᵐ ψ = record
  { 𝑎𝑙𝑔 = λ t ζ → ℳ.𝑎𝑙𝑔 (estr [ 𝔛 ⊸ 𝒫ᵇ ]ᵇ ℳ t ζ)
  ; 𝑣𝑎𝑟 = λ v ζ → ℳ.η v
  ; 𝑚𝑣𝑎𝑟 = λ 𝔪 ε ζ → ℳ.μ (ψ (ζ 𝔪)) (copair ℳ (λ x → ε x ζ) ℳ.η)
  } where module ℳ = ΣMon Σℳᵐ

□[_⊸_]⇨_ᵃ : (𝔛 {𝒫}{ℳ} : Familyₛ) → Coalg 𝒫 → ΣMon ℳ → (𝒫 ⇾̣ ℳ)
           → MetaAlg 𝔛 ([ 𝔛 ⊸ 𝒫 ] ➡ ℳ)
□[ 𝔛 ⊸ 𝒫ᵇ ]⇨ Σℳᵐ ᵃ ψ = □ᵃ 𝔛 ([ 𝔛 ⊸ 𝒫ᵇ ]⇨ Σℳᵐ ᵃ ψ)

-- Derived meta-algebra instance for [ 𝔛 ⊸ 𝕋 𝔜 ] ⇨ 𝕋 𝔜
⟅_⇨_⟆ᵃ : (𝔛 𝔜 : Familyₛ) → MetaAlg 𝔛 ⟅ 𝔛 ⇨ 𝕋 𝔜 ⟆
⟅ 𝔛 ⇨ 𝔜 ⟆ᵃ = [ 𝔛 ⊸ 𝕋ᵇ 𝔜 ]⇨ Σ𝕋ᵐ 𝔜 ᵃ id

module MS {𝔛 𝔜 : Familyₛ} =  Semantics 𝔛 ⟅ 𝔛 ⇨ 𝔜 ⟆ᵃ
module □MS {𝔛 𝔜 : Familyₛ} = □Traversal 𝔛 ⟅ 𝔛 ⇨ 𝔜 ⟆ᵃ

-- Metasubstitution operations
-- Base
msub : 𝕋 𝔛 ⇾̣ ⟅ 𝔛 ⇨ 𝕋 𝔜 ⟆
msub = MS.𝕤𝕖𝕞
-- Parametrised
□msub : 𝕋 𝔛 ⇾̣ ⟅ 𝔛 ➡ 𝕋 𝔜 ⟆
□msub = □MS.𝕥𝕣𝕒𝕧
-- Linear
○msub : 𝕋 𝔛 ⇾̣ ⟅ 𝔛 ⊸ 𝕋 𝔜 ⟆
○msub {𝔜 = 𝔜}{Γ = Γ} t ζ = □msub t (inl Γ) λ {_}{Π} 𝔪 → 𝕣𝕖𝕟 𝔜 (ζ 𝔪) (Π ∔∣ inr Γ)

-- Unit parametrisation
□msub-id : (t : 𝕋 𝔛 α Γ)(κ : [ 𝔛 ⊸ 𝕋 𝔜 ] Γ) → □msub t id κ ≡ msub t κ
□msub-id {𝔛}{𝔜 = 𝔜} t κ = cong (λ - → - κ) (□𝕥𝕣𝕒𝕧-id≈𝕤𝕖𝕞 𝔛 ⟅ 𝔛 ⇨ 𝔜 ⟆ᵃ)

-- Unit metasubstitution mapping
ms-unit : [ 𝔛 ⊸ 𝕋 𝔛 ] Γ
ms-unit {𝔛}{Δ = Δ} 𝔪 = 𝕞𝕧𝕒𝕣 𝔛 𝔪 (𝕧𝕒𝕣 𝔛 ∘ inl Δ)

-- | Inductive metasubstitution

-- List of terms in an extended (object variable) context mapped to every element of a metavariable context
data MSub (Γ : Ctx) : MCtx → MCtx → Set₁ where
  ◦   : MSub Γ ⁅⁆ 𝔑
  _◃_ : (𝔑 ▷ 𝕋) α (Π ∔ Γ) → MSub Γ 𝔐 𝔑 → MSub Γ (⁅ Π ⊩ₙ α ⁆ 𝔐) 𝔑

infixr 15 _◃_ _▹_

-- Add term to the end of a metasubstitution map
_▹_ : MSub Γ 𝔐 𝔑 → (𝔑 ▷ 𝕋) τ (Π ∔ Γ) → MSub Γ (𝔐 ⁅ Π ⊩ₙ τ ⁆) 𝔑
◦ ▹ t = t ◃ ◦
(s ◃ ζ) ▹ t = s ◃ (ζ ▹ t)

-- Application of a metasubstitution to a metavariable
ix≀ : MSub Γ 𝔐 𝔑 → [ ∥ 𝔐 ∥ ⊸ 𝔑 ▷ 𝕋 ] Γ
ix≀ (t ◃ ζ) ↓ = t
ix≀ (t ◃ ζ) (↑ 𝔪) = ix≀ ζ 𝔪

-- Term corresponding to the topmost distinguished metavariable of an extended mvar context
_⊩◌ : (Π : Ctx) → (⁅ Π ⊩ₙ β ⁆ 𝔐 ▷ 𝕋) β (Π ∔ Γ)
_⊩◌ {β}{𝔐} Π = ms-unit ↓

◌ : (⁅ β ⁆ 𝔐 ▷ 𝕋) β Γ
◌ = ∅ ⊩◌

-- Weakening of metavariable context
wk≀ : (𝔐 ▷ 𝕋) α Γ →  (⁅ Π ⊩ₙ τ ⁆ 𝔐 ▷ 𝕋) α Γ
wk≀ t = 𝕋₁ ↑_ t

-- Extension of the codomain of a metasubstitution
ext≀ : (Π : Ctx)(τ : T) → MSub Γ 𝔐 𝔑 → MSub Γ 𝔐 (⁅ Π ⊩ₙ τ ⁆ 𝔑)
ext≀ Π τ ◦ = ◦
ext≀ Π τ (t ◃ κ) = wk≀ t ◃ (ext≀ Π τ κ)

-- Lifting of a metasubstitution
lift≀ : (Π : Ctx)(τ : T) → MSub Γ 𝔐 𝔑 → MSub Γ (⁅ Π ⊩ₙ τ ⁆ 𝔐) (⁅ Π ⊩ₙ τ ⁆ 𝔑)
lift≀ Π τ κ = (Π ⊩◌) ◃ (ext≀ Π τ κ)

-- Identity metasubstitution
id≀ : (Γ : Ctx) →  MSub Γ 𝔐 𝔐
id≀ {⁅⁆} Γ = ◦
id≀ {⁅ Π ⊩ₙ τ ⁆ 𝔐} Γ = lift≀ Π τ (id≀ Γ)

-- Left and right weakening of object context of a metasubstitution
inl≀ : MSub Γ 𝔐 𝔑 → MSub (Γ ∔ Δ) 𝔐 𝔑
inl≀ ◦ = ◦
inl≀ {𝔑 = 𝔑} (_◃_ {Π = Π} t κ) = 𝕣𝕖𝕟 ∥ 𝔑 ∥ t (Π ∔∣ inl _) ◃ (inl≀ κ)

inr≀ : (Γ : Ctx) → MSub Δ 𝔐 𝔑 → MSub (Γ ∔ Δ) 𝔐 𝔑
inr≀ _ ◦ = ◦
inr≀ {Δ}{𝔑 = 𝔑} Γ (_◃_ {Π = Π} t κ) = (𝕣𝕖𝕟 ∥ 𝔑 ∥ t (Π ∔∣ inr Γ)) ◃ (inr≀ Γ κ)

-- Application of weakened metasubstitution corresponds to centre weakening
ix-inr≀ : (κ : MSub Δ 𝔐 𝔑)(𝔪 : Π ⊩ τ ∈ 𝔐)
        → ix≀ (inr≀ Γ κ) 𝔪 ≡ (𝕣𝕖𝕟 ∥ 𝔑 ∥ (ix≀ κ 𝔪) (Π ∔∣ inr Γ))
ix-inr≀ (x ◃ κ) ↓ = refl
ix-inr≀ (x ◃ κ) (↑ 𝔪) = ix-inr≀ κ 𝔪

-- Correctness lemmas of weakening, lifting, identity
ext≀≈𝕋₁pop : (κ : MSub Γ 𝔐 𝔑)(𝔪 : Π ⊩ τ ∈ 𝔐) → ix≀ (ext≀ Δ β κ) 𝔪 ≡ wk≀ (ix≀ κ 𝔪)
ext≀≈𝕋₁pop (x ◃ κ) ↓ = refl
ext≀≈𝕋₁pop (x ◃ κ) (↑ 𝔪) = ext≀≈𝕋₁pop κ 𝔪

lift≀≈𝕋₁pop : (κ : MSub Γ 𝔐 𝔑)(𝔪 : Γ ⊩ α ∈ 𝔐) → ix≀ (lift≀ Γ α κ) (↑ 𝔪) ≡ wk≀ (ix≀ κ 𝔪)
lift≀≈𝕋₁pop (x ◃ κ) ↓ = refl
lift≀≈𝕋₁pop (x ◃ κ) (↑ 𝔪) = lift≀≈𝕋₁pop κ 𝔪

id≀≈ms-unit : (Γ : Ctx)(𝔪 : Π ⊩ τ ∈ 𝔐) → ix≀ (id≀ Γ) 𝔪 ≡ ms-unit 𝔪
id≀≈ms-unit {𝔐 = ⁅ Π ⊩ₙ τ ⁆ 𝔐} Γ ↓ = refl
id≀≈ms-unit {𝔐 = ⁅ Π ⊩ₙ τ ⁆ 𝔐} Γ (↑_ {Δ}{β}{Γ = .Π}{.τ} 𝔪) = begin
      ix≀ (ext≀ Π τ (id≀ Γ)) 𝔪
  ≡⟨ ext≀≈𝕋₁pop (id≀ Γ) 𝔪 ⟩
      wk≀ (ix≀ (id≀ Γ) 𝔪)
  ≡⟨ cong (wk≀) (id≀≈ms-unit Γ 𝔪) ⟩
      wk≀ (ms-unit 𝔪)
  ≡⟨⟩
      wk≀ (𝕞𝕧𝕒𝕣 ∥ 𝔐 ∥ 𝔪 (𝕧𝕒𝕣 ∥ 𝔐 ∥ ∘ ∔.i₁))
  ≡⟨ 𝕋₁∘𝕞𝕧𝕒𝕣[𝕧𝕒𝕣] ↑_ 𝔪 (∔.i₁) ⟩
      𝕞𝕧𝕒𝕣 ∥ ⁅ Π ⊩ₙ τ ⁆ 𝔐 ∥ (↑ 𝔪) (𝕧𝕒𝕣 ∥ ⁅ Π ⊩ₙ τ ⁆ 𝔐 ∥ ∘ ∔.i₁)
  ∎ where open ≡-Reasoning

-- Inductive metasubstitution operations
-- Base
msub≀ : (𝔐 ▷ 𝕋) α Γ → MSub Γ 𝔐 𝔑 → (𝔑 ▷ 𝕋) α Γ
msub≀ t ζ = msub t (ix≀ ζ)
-- Parametrised
□msub≀ : (𝔐 ▷ 𝕋) α Γ → (Γ ↝ Δ) → MSub Δ 𝔐 𝔑 → (𝔑 ▷ 𝕋) α Δ
□msub≀ t ρ ζ = □msub t ρ (ix≀ ζ)
-- Linear
○msub≀ : (𝔐 ▷ 𝕋) α Γ → MSub Δ 𝔐 𝔑 → (𝔑 ▷ 𝕋) α (Γ ∔ Δ)
○msub≀ {Γ = Γ} t ζ = □msub≀ t (inl Γ) (inr≀ Γ ζ)

-- Syntactic sugar for metasubstitution application
_》 : (𝔑 ▷ 𝕋) α (Π ∔ Γ) → MSub Γ (⁅ Π ⊩ₙ α ⁆̣) 𝔑
t 》  = t ◃ ◦
_《_ : (𝔐 ▷ 𝕋) α Γ → MSub Γ 𝔐 𝔑 → (𝔑 ▷ 𝕋) α Γ
_《_ = msub≀

infixr 25 _》
infix 15 _《_

-- Instantiation of a term extended at the start of the context
instₛ : (⁅ Π ⊩ₙ α ⁆ 𝔐 ▷ 𝕋) β Γ → (𝔐 ▷ 𝕋) α (Π ∔ Γ) → (𝔐 ▷ 𝕋) β Γ
instₛ {Γ = Γ} h s = msub≀ h (s ◃ id≀ Γ)

-- Instantiation of a term extended at the end of the context
instₑ : (𝔐 ⁅ Π ⊩ₙ α ⁆ ▷ 𝕋) β Γ → (𝔐 ▷ 𝕋) α (Π ∔ Γ) → (𝔐 ▷ 𝕋) β Γ
instₑ {Γ = Γ} h s = msub≀ h ((id≀ Γ) ▹ s)

-- Instantiation of a term extended twice at the end of the context
instₑ₂ : {Π₁ Π₂ : Ctx}{α₁ α₂ : T}
       → ((𝔐 ⁅ Π₁ ⊩ₙ α₁ ⁆) ⁅ Π₂ ⊩ₙ α₂ ⁆ ▷ 𝕋) β Γ
       → (𝔐 ▷ 𝕋) α₁ (Π₁ ∔ Γ) → (𝔐 ▷ 𝕋) α₂ (Π₂ ∔ Γ) → (𝔐 ▷ 𝕋) β Γ
instₑ₂ {Γ = Γ} h s t = msub≀ h ((id≀ Γ ▹ s) ▹ t)


text:
-- Andreas, 2016-10-11, AIM XXIV, issue #2248
-- COMPILED_TYPE should only work on postulates

data Unit : Set where
  unit : Unit

abstract
  IO : Set → Set
  IO A = A

  doNothing : IO Unit
  doNothing = unit

{-# COMPILED_TYPE IO IO #-}

main : IO unit
main = doNothing

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
-- an example showing how to use sigma types to define a type for non-zero natural numbers
module nat-nonzero where

open import bool
open import eq
open import nat
open import nat-thms
open import product

ℕ⁺ : Set
ℕ⁺ = Σ ℕ (λ n → iszero n ≡ ff)

suc⁺ : ℕ⁺ → ℕ⁺
suc⁺ (x , p) = (suc x , refl)

_+⁺_ : ℕ⁺ → ℕ⁺ → ℕ⁺
(x , p) +⁺ (y , q) = x + y , iszerosum2 x y p

_*⁺_ : ℕ⁺ → ℕ⁺ → ℕ⁺
(x , p) *⁺ (y , q) = (x * y , iszeromult x y p q)

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


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

module Definition.Typed.Consequences.Inequality where

open import Definition.Untyped hiding (U≢ℕ; U≢Π; U≢ne; ℕ≢Π; ℕ≢ne; Π≢ne; U≢Empty; ℕ≢Empty; Empty≢Π; Empty≢ne)
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.EqRelInstance
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Fundamental.Reducibility
open import Definition.Typed.Consequences.Syntactic

open import Tools.Product
open import Tools.Empty
import Tools.PropositionalEquality as PE

A≢B : ∀ {A B rA rB Γ} (_⊩′⟨_⟩A_ _⊩′⟨_⟩B_ : Con Term → TypeLevel → Term → Set)
      (A-intr : ∀ {l} → Γ ⊩′⟨ l ⟩A A → Γ ⊩⟨ l ⟩ A ^ rA)
      (B-intr : ∀ {l} → Γ ⊩′⟨ l ⟩B B → Γ ⊩⟨ l ⟩ B ^ rB)
      (A-elim : ∀ {l} → Γ ⊩⟨ l ⟩ A ^ rA → ∃ λ l′ → Γ ⊩′⟨ l′ ⟩A A)
      (B-elim : ∀ {l} → Γ ⊩⟨ l ⟩ B ^ rA → ∃ λ l′ → Γ ⊩′⟨ l′ ⟩B B)
      (A≢B′ : ∀ {l l′} ([A] : Γ ⊩′⟨ l ⟩A A) ([B] : Γ ⊩′⟨ l′ ⟩B B)
            → ShapeView Γ l l′ A B rA rB (A-intr [A]) (B-intr [B]) → ⊥)
    → Γ ⊢ A ≡ B ^ rA → ⊥
A≢B {A} {B} _ _ A-intr B-intr A-elim B-elim A≢B′ A≡B =
  let X = reducibleEq A≡B
      [A] = proj₁ X
      [B] = proj₁ (proj₂ X)
      [A≡B] = proj₂ (proj₂ X)
      _ , [A]′ = A-elim ([A])
      _ , [B]′ = B-elim ([B])
      [A≡B]′ = irrelevanceEq [A] (A-intr [A]′) [A≡B]
  in  A≢B′ [A]′ [B]′ (goodCases (A-intr [A]′) (B-intr [B]′) [A≡B]′)

U≢ℕ′ : ∀ {Γ A ll B l l′}
       ([U] : Γ ⊩′⟨ l ⟩U A ^ ll)
       ([ℕ] : Γ ⊩ℕ B)
     → ShapeView Γ l l′ _ _ [ ! , _ ] [ ! , _ ] (Uᵣ {ll = ll} [U]) (ℕᵣ [ℕ]) → ⊥
U≢ℕ′ a b ()

U≢ℕ-red : ∀ {ll r lU B Γ} → Γ ⊢ B ⇒* ℕ ^ [ ! , ll ] → Γ ⊢ Univ r lU ≡ B ^ [ ! , ll ] → ⊥
U≢ℕ-red {ll} D = A≢B (λ Γ l A → Γ ⊩′⟨ l ⟩U A ^ ll) (λ Γ l B → Γ ⊩ℕ B) Uᵣ ℕᵣ
                (λ x → extractMaybeEmb (U-elim x))
                (λ x → extractMaybeEmb (ℕ-elim′ D x))
                U≢ℕ′

-- U and ℕ cannot be judgmentally equal.
U≢ℕ! : ∀ {r l ll Γ} → Γ ⊢ Univ r l ≡ ℕ ^ [ ! , ll ] → ⊥
U≢ℕ! U≡ℕ =
  let _ , ⊢ℕ = syntacticEq U≡ℕ
  in  U≢ℕ-red (id ⊢ℕ) U≡ℕ

-- U vs Pi
U≢Π′ : ∀ {A lA B rB lB Γ l l′}
       ([U] : Γ ⊩′⟨ l ⟩U A ^ lA)
       ([Π] : Γ ⊩′⟨ l′ ⟩Π B ^[ rB , lB ])
     → ShapeView Γ l l′ _ _ _ _ (Uᵣ {ll = lA} [U]) (Πᵣ [Π]) → ⊥
U≢Π′ a b ()

U≢Π-red : ∀ {ll B F G rF lF lG rU lU Γ} → Γ ⊢ B ⇒* Π F ^ rF ° lF ▹ G ° lG ° ll ^ [ ! , ι ll ]
            → Γ ⊢ Univ rU lU ≡ B ^ [ ! , ι ll ] → ⊥
U≢Π-red {ll} D = A≢B (λ Γ l A → Γ ⊩′⟨ l ⟩U A ^ ι ll)
                (λ Γ l A → Γ ⊩′⟨ l ⟩Π A ^[ ! , ll ]) Uᵣ Πᵣ
                (λ x → extractMaybeEmb (U-elim x))
                (λ x → extractMaybeEmb (Π-elim′ D x))
                U≢Π′

-- U and Π F ▹ G for any F and G cannot be judgmentally equal.
U≢Π! : ∀ {rU lU F rF lF lG G l Γ} → Γ ⊢ Univ rU lU ≡ Π F ^ rF ° lF ▹ G  ° lG ° l ^ [ ! , ι l ] → ⊥
U≢Π! U≡Π =
  let _ , ⊢Π = syntacticEq U≡Π
  in  U≢Π-red (id ⊢Π) U≡Π

-- ∃ vs Pi

∃≢Π′ : ∀ {A lA B rB lB Γ l l′}
       ([∃] : Γ ⊩′⟨ l ⟩∃ A ^ lA)
       ([Π] : Γ ⊩′⟨ l′ ⟩Π B ^[ rB , lB ])
     → ShapeView Γ l l′ _ _ _ _ (∃ᵣ [∃]) (Πᵣ [Π]) → ⊥
∃≢Π′ a b ()

∃≢Π-red : ∀ {ll B F G rF lF lG P Q Γ} → Γ ⊢ B ⇒* Π F ^ rF ° lF ▹ G ° lG ° ll ^ [ % , ι ll ]
            → Γ ⊢ ∃ P ▹ Q ≡ B ^ [ % , ι ll ] → ⊥
∃≢Π-red {ll} D = A≢B (λ Γ l A → Γ ⊩′⟨ l ⟩∃ A ^ ll)
                (λ Γ l A → Γ ⊩′⟨ l ⟩Π A ^[ % , ll ]) ∃ᵣ Πᵣ
                (λ x → extractMaybeEmb (∃-elim x))
                (λ x → extractMaybeEmb (Π-elim′ D x))
                ∃≢Π′

-- U and Π F ▹ G for any F and G cannot be judgmentally equal.
∃≢Π! : ∀ {P Q F rF lF lG G l Γ} → Γ ⊢ ∃ P ▹ Q ≡ Π F ^ rF ° lF ▹ G  ° lG ° l ^ [ % , ι l ] → ⊥
∃≢Π! ∃≡Π =
  let _ , ⊢Π = syntacticEq ∃≡Π
  in ∃≢Π-red (id ⊢Π) ∃≡Π

U≢ne′ : ∀ {A lU r lK K Γ l l′}
       ([U] : Γ ⊩′⟨ l ⟩U A ^ lU)
       ([K] : Γ ⊩ne K ^[ r , lK ] )
     → ShapeView Γ l l′ _ _ _ _ (Uᵣ {ll = lU} [U]) (ne [K]) → ⊥
U≢ne′ a b ()

U≢ne-red : ∀ {ll rU lU B K Γ} → Γ ⊢ B ⇒* K ^ [ ! , ι ll ] → Neutral K → Γ ⊢ Univ rU lU ≡ B ^ [ ! , ι ll ] → ⊥
U≢ne-red {ll} D neK = A≢B (λ Γ l A → Γ ⊩′⟨ l ⟩U A ^ ι ll) (λ Γ l B → Γ ⊩ne B ^[ ! , ll ]) Uᵣ ne
                     (λ x → extractMaybeEmb (U-elim x))
                     (λ x → extractMaybeEmb (ne-elim′ D neK x PE.refl))
                     U≢ne′

-- U and K for any neutral K cannot be judgmentally equal.
U≢ne! : ∀ {r l ll K Γ} → Neutral K → Γ ⊢ Univ r l ≡ K ^ [ ! , ι ll ] → ⊥
U≢ne! neK U≡K =
  let _ , ⊢K = syntacticEq U≡K
  in  U≢ne-red (id ⊢K) neK U≡K

ℕ≢Π′ : ∀ {A B Γ ll l l′}
       ([ℕ] : Γ ⊩ℕ A)
       ([Π] : Γ ⊩′⟨ l′ ⟩Π B ^[ ! , ll ])
     → ShapeView Γ l l′ _ _ _ _ (ℕᵣ [ℕ]) (Πᵣ [Π]) → ⊥
ℕ≢Π′ a b ()

ℕ≢Π-red : ∀ {A B F rF lF lG G Γ} → Γ ⊢ A ⇒* ℕ ^ [ ! , ι ⁰ ] → Γ ⊢ B ⇒* Π F ^ rF ° lF ▹ G ° lG ° ⁰ ^ [ ! , ι ⁰ ] → Γ ⊢ A ≡ B ^ [ ! , ι ⁰ ] → ⊥
ℕ≢Π-red D D′ = A≢B (λ Γ l A → Γ ⊩ℕ A)
                   (λ Γ l A → Γ ⊩′⟨ l ⟩Π A ^[ ! , ⁰ ]) ℕᵣ Πᵣ
                   (λ x → extractMaybeEmb (ℕ-elim′ D x))
                   (λ x → extractMaybeEmb (Π-elim′ D′ x))
                   ℕ≢Π′

-- ℕ and Π F ▹ G for any F and G cannot be judgmentally equal.
ℕ≢Π! : ∀ {F rF G lF lG  Γ} → Γ ⊢ ℕ ≡ Π F ^ rF ° lF ▹ G ° lG ° ⁰ ^ [ ! , ι ⁰ ]  → ⊥
ℕ≢Π! ℕ≡Π =
  let ⊢ℕ , ⊢Π = syntacticEq ℕ≡Π
  in  ℕ≢Π-red (id ⊢ℕ) (id ⊢Π) ℕ≡Π

-- Empty and Π
Empty≢Π′ : ∀ {ll A B Γ l l′}
       ([Empty] : Γ ⊩Empty A ^ ll)
       ([Π] : Γ ⊩′⟨ l′ ⟩Π B ^[ % , ll ])
     → ShapeView Γ l l′ _ _ _ _ (Emptyᵣ [Empty]) (Πᵣ [Π]) → ⊥
Empty≢Π′ a b ()

Empty≢Π-red : ∀ {ll A B F rF lF lG G Γ} → Γ ⊢ A ⇒* Empty ll ^ [ % , ι ll ] → Γ ⊢ B ⇒* Π F ^ rF ° lF ▹ G ° lG ° ll ^ [ % , ι ll ]
                → Γ ⊢ A ≡ B ^ [ % , ι ll ] → ⊥
Empty≢Π-red {ll} D D′ = A≢B (λ Γ l A → Γ ⊩Empty A ^ ll)
                   (λ Γ l A → Γ ⊩′⟨ l ⟩Π A ^[ % , ll ]) Emptyᵣ Πᵣ
                   (λ x → extractMaybeEmb (Empty-elim′ D x))
                   (λ x → extractMaybeEmb (Π-elim′ D′ x))
                   Empty≢Π′

Empty≢Π% : ∀ {F rF lF lG l G Γ} → Γ ⊢ Empty l ≡ Π F ^ rF ° lF ▹ G ° lG ° l ^ [ % , ι l ] → ⊥
Empty≢Π% Empty≡Π =
  let ⊢Empty , ⊢Π = syntacticEq Empty≡Π
  in  Empty≢Π-red (id ⊢Empty) (id ⊢Π) Empty≡Π

ℕ≢ne′ : ∀ {ll A K Γ l l′}
       ([ℕ] : Γ ⊩ℕ A)
       ([K] : Γ ⊩ne K ^[ ! , ll ])
     → ShapeView Γ l l′ _ _ _ _ (ℕᵣ [ℕ]) (ne [K]) → ⊥
ℕ≢ne′ a b ()

ℕ≢ne-red : ∀ {A B K Γ} → Γ ⊢ A ⇒* ℕ ^ [ ! , ι ⁰ ] → Γ ⊢ B ⇒* K ^ [ ! , ι ⁰ ] → Neutral K → Γ ⊢ A ≡ B ^ [ ! , ι ⁰ ] → ⊥
ℕ≢ne-red D D′ neK = A≢B (λ Γ l A → Γ ⊩ℕ A) (λ Γ l B → Γ ⊩ne B ^[ ! , ⁰ ]) ℕᵣ ne
                        (λ x → extractMaybeEmb (ℕ-elim′ D x))
                        (λ x → extractMaybeEmb (ne-elim′ D′ neK x PE.refl ))
                        ℕ≢ne′

-- ℕ and K for any neutral K cannot be judgmentally equal.
ℕ≢ne! : ∀ {K Γ} → Neutral K → Γ ⊢ ℕ ≡ K ^ [ ! , ι ⁰ ] → ⊥
ℕ≢ne! neK ℕ≡K =
  let ⊢ℕ , ⊢K = syntacticEq ℕ≡K
  in  ℕ≢ne-red (id ⊢ℕ) (id ⊢K) neK ℕ≡K

-- Empty and neutral
Empty≢ne′ : ∀ {ll A K Γ l l′}
       ([Empty] : Γ ⊩Empty A ^ ll)
       ([K] : Γ ⊩ne K ^[ % , ll ])
     → ShapeView Γ l l′ _ _ _ _ (Emptyᵣ [Empty]) (ne [K]) → ⊥
Empty≢ne′ a b ()

Empty≢ne-red : ∀ {ll A B K Γ} → Γ ⊢ A ⇒* Empty ll ^ [ % , ι ll ] → Γ ⊢ B ⇒* K ^ [ % , ι ll ] →
                                Neutral K → Γ ⊢ A ≡ B ^ [ % , ι ll ] → ⊥
Empty≢ne-red {ll} D D′ neK = A≢B (λ Γ l A → Γ ⊩Empty A ^ ll) (λ Γ l B → Γ ⊩ne B ^[ % , ll ]) Emptyᵣ ne
                        (λ x → extractMaybeEmb (Empty-elim′ D x))
                        (λ x → extractMaybeEmb (ne-elim′ D′ neK x PE.refl))
                        Empty≢ne′

Empty≢ne% : ∀ {l K Γ} → Neutral K → Γ ⊢ Empty l ≡ K ^ [ % , ι l ]  → ⊥
Empty≢ne% neK Empty≡K =
  let ⊢Empty , ⊢K = syntacticEq Empty≡K
  in  Empty≢ne-red (id ⊢Empty) (id ⊢K) neK Empty≡K

Π≢ne′ : ∀ {ll A K r Γ l l′}
       ([Π] : Γ ⊩′⟨ l ⟩Π A ^[ r , ll ])
       ([K] : Γ ⊩ne K ^[ r , ll ])
     → ShapeView Γ l l′ _ _ _ _ (Πᵣ [Π]) (ne [K]) → ⊥
Π≢ne′ a b ()

Π≢ne-red : ∀ {ll r A B F rF lF lG G K Γ} → Γ ⊢ A ⇒* Π F ^ rF ° lF ▹ G ° lG ° ll ^ [ r , ι ll ]
                                         → Γ ⊢ B ⇒* K ^ [ r , ι ll ] → Neutral K
                                         → Γ ⊢ A ≡ B ^ [ r , ι ll ] → ⊥
Π≢ne-red {ll} {r} D D′ neK = A≢B (λ Γ l A → Γ ⊩′⟨ l ⟩Π A ^[ r , ll ])
                        (λ Γ l B → Γ ⊩ne B ^[ r , ll ]) Πᵣ ne
                        (λ x → extractMaybeEmb (Π-elim′ D x))
                        (λ x → extractMaybeEmb (ne-elim′ D′ neK x PE.refl))
                        Π≢ne′

-- Π F ▹ G and K for any F and G and neutral K cannot be judgmentally equal.
Π≢ne : ∀ {F rF lF lG G K r l Γ} → Neutral K → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° l ≡ K ^ [ r , ι l ] → ⊥
Π≢ne neK Π≡K =
  let ⊢Π , ⊢K = syntacticEq Π≡K
  in  Π≢ne-red (id ⊢Π) (id ⊢K) neK Π≡K


text:
{-

This file contains:

- Definitions equivalences

- Glue types

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Core.Glue where

open import Cubical.Core.Primitives

open import Agda.Builtin.Cubical.Glue public
  using ( isEquiv       -- ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) → Type (ℓ ⊔ ℓ')

        ; equiv-proof   -- ∀ (y : B) → isContr (fiber f y)

        ; _≃_           -- ∀ {ℓ ℓ'} (A : Type ℓ) (B : Type ℓ') → Type (ℓ ⊔ ℓ')

        ; equivFun      -- ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → A ≃ B → A → B

        ; equivProof    -- ∀ {ℓ ℓ'} (T : Type ℓ) (A : Type ℓ') (w : T ≃ A) (a : A) φ →
                        -- Partial φ (fiber (equivFun w) a) → fiber (equivFun w) a

        ; primGlue      -- ∀ {ℓ ℓ'} (A : Type ℓ) {φ : I} (T : Partial φ (Type ℓ'))
                        -- → (e : PartialP φ (λ o → T o ≃ A)) → Type ℓ'

        ; prim^unglue   -- ∀ {ℓ ℓ'} {A : Type ℓ} {φ : I} {T : Partial φ (Type ℓ')}
                        -- → {e : PartialP φ (λ o → T o ≃ A)} → primGlue A T e → A

        -- The ∀ operation on I. This is commented out as it is not currently used for anything
        -- ; primFaceForall -- (I → I) → I
        )
  renaming ( prim^glue   to glue         -- ∀ {ℓ ℓ'} {A : Type ℓ} {φ : I} {T : Partial φ (Type ℓ')}
                                         -- → {e : PartialP φ (λ o → T o ≃ A)}
                                         -- → PartialP φ T → A → primGlue A T e

           ; pathToEquiv to lineToEquiv  -- ∀ {ℓ : I → Level} (P : (i : I) → Type (ℓ i)) → P i0 ≃ P i1
           )

private
  variable
    ℓ ℓ' : Level

-- Uncurry Glue to make it more pleasant to use
Glue : (A : Type ℓ) {φ : I}
       → (Te : Partial φ (Σ[ T ∈ Type ℓ' ] T ≃ A))
       → Type ℓ'
Glue A Te = primGlue A (λ x → Te x .fst) (λ x → Te x .snd)

-- Make the φ argument of prim^unglue explicit
unglue : {A : Type ℓ} (φ : I) {T : Partial φ (Type ℓ')}
         {e : PartialP φ (λ o → T o ≃ A)} → primGlue A T e → A
unglue φ = prim^unglue {φ = φ}

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
-- This module explains how to combine elimination of empty types with pattern
-- match style definitions without running into problems with decidability.

module Introduction.Data.Empty where

-- First we introduce an empty and a singleton type.
data Zero : Set where
data One  : Set where
  one : One

-- There is a special pattern () which matches any element of an (obviously)
-- empty type. If there is a ()-pattern in a left-hand side the right-hand side
-- can be omitted.
elim-Zero : {A : Set} -> Zero -> A
elim-Zero ()

data _×_ (A B : Set) : Set where
  pair : A -> B -> A × B

-- The algorithm for checking if a type is empty is very naive. In this example
-- you cannot replace pair () _ with () because the type checker cannot see
-- that Zero × B is empty.
elim-EmptyPair : {A B : Set} -> Zero × B -> A
elim-EmptyPair (pair () _)

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

-- For some empty types finite unfolding is not enough.
ConstZero : Nat -> Set
ConstZero  zero   = Zero
ConstZero (suc n) = ConstZero n

-- We can still define the elimination function but we have to do it
-- recursively over the n.
elim-ConstZero : (n : Nat) -> ConstZero n -> {A : Set} -> A
elim-ConstZero  zero   ()
elim-ConstZero (suc n)  x = elim-ConstZero n x