text:
{- Name: Bowornmet (Ben) Hudson

--Preorders 2: Electric Boogaloo--

-}

open import Preliminaries

module Preorder-withmax where

  {- Doing the same thing as we did in Preorder.agda but this
     time we want to keep our end goal in mind and extend the
     notion of preorders to include information about maximums
     as well. This will make it easier to 'ensure' that functions
     on nats are monotone (because they sometimes aren't - e.g.
     sine, cosine, etc.) so we can give them a reasonable upper bound.
     If we don't monotonize functions on nats then that makes bounding
     more complicated. This also means we have to extend the idea of
     maximums to all our other types...
  -}
  record Preorder-max-str (A : Set) : Set1 where
    constructor preorder-max
    field
      ≤ : A → A → Set
      refl : ∀ x → ≤ x x
      trans : ∀ x y z → ≤ x y → ≤ y z → ≤ x z
      max : A → A → A
      max-l : ∀ l r → ≤ l (max l r)
      max-r : ∀ l r → ≤ r (max l r)
      max-lub : ∀ k l r → ≤ l k → ≤ r k → ≤ (max l r) k

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

  -- order on nats
  ≤nat : Nat → Nat → Set
  ≤nat Z Z = Unit
  ≤nat Z (S y) = Unit
  ≤nat (S x) Z = Void
  ≤nat (S x) (S y) = ≤nat x y

  -- proof that Nat is reflexive under ≤
  nat-refl : ∀ (x : Nat) → ≤nat x x
  nat-refl Z = <>
  nat-refl (S x) = nat-refl x

  -- proof that Nat is transitive under ≤
  nat-trans : ∀ (x y z : Nat) → ≤nat x y → ≤nat y z → ≤nat x z
  nat-trans Z Z Z p q = <>
  nat-trans Z Z (S z) p q = <>
  nat-trans Z (S y) Z p q = <>
  nat-trans Z (S y) (S z) p q = <>
  nat-trans (S x) Z Z p q = p
  nat-trans (S x) Z (S z) () q
  nat-trans (S x) (S y) Z p ()
  nat-trans (S x) (S y) (S z) p q = nat-trans x y z p q

  -- nat max
  nat-max : Nat → Nat → Nat
  nat-max Z n = n
  nat-max (S m) Z = S m
  nat-max (S m) (S n) = S (nat-max m n)

  -- left max
  nat-max-l : ∀ (l r : Nat) → ≤nat l (nat-max l r)
  nat-max-l Z Z = <>
  nat-max-l Z (S n) = <>
  nat-max-l (S m) Z = nat-refl m
  nat-max-l (S m) (S n) = nat-max-l m n

  -- right max
  nat-max-r : ∀ (l r : Nat) → ≤nat r (nat-max l r)
  nat-max-r Z Z = <>
  nat-max-r Z (S n) = nat-refl n
  nat-max-r (S m) Z = <>
  nat-max-r (S m) (S n) = nat-max-r m n

  -- rub a dub dub, Nats have a lub
  nat-max-lub : ∀ (k l r : Nat) → ≤nat l k → ≤nat r k → ≤nat (nat-max l r) k
  nat-max-lub Z Z Z p q = <>
  nat-max-lub Z Z (S r) p ()
  nat-max-lub Z (S l) Z () q
  nat-max-lub Z (S l) (S r) () q
  nat-max-lub (S k) Z Z p q = <>
  nat-max-lub (S k) Z (S r) p q = q
  nat-max-lub (S k) (S l) Z p q = p
  nat-max-lub (S k) (S l) (S r) p q = nat-max-lub k l r p q

  -- Nat is preorder with max
  nat-p : Preorder-max-str Nat
  nat-p = preorder-max ≤nat nat-refl nat-trans nat-max nat-max-l nat-max-r nat-max-lub

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

--same thing for products

  -- relation for products
  ≤axb : ∀ {A B : Set} → Preorder-max-str A → Preorder-max-str B → (A × B) → (A × B) → Set
  ≤axb PA PB (a1 , b1) (a2 , b2) = Preorder-max-str.≤ PA a1 a2 × Preorder-max-str.≤ PB b1 b2

  axb-refl : ∀ {A B : Set} → (PA : Preorder-max-str A) → (PB : Preorder-max-str B) → (x : (A × B)) →  ≤axb PA PB x x
  axb-refl PA PB (a , b) = Preorder-max-str.refl PA a , Preorder-max-str.refl PB b

  axb-trans : ∀ {A B : Set} → (PA : Preorder-max-str A) → (PB : Preorder-max-str B) → (x y z : (A × B)) → ≤axb PA PB x y → ≤axb PA PB y z → ≤axb PA PB x z
  axb-trans PA PB (a1 , b1) (a2 , b2) (a3 , b3) (a1<a2 , b1<b2) (a2<a3 , b2<b3) =
                          Preorder-max-str.trans PA a1 a2 a3 a1<a2 a2<a3 , Preorder-max-str.trans PB b1 b2 b3 b1<b2 b2<b3

  axb-max : ∀ {A B : Set} → Preorder-max-str A → Preorder-max-str B → (A × B) → (A × B) → (A × B)
  axb-max PA PB (a1 , b1) (a2 , b2) = Preorder-max-str.max PA a1 a2 , Preorder-max-str.max PB b1 b2

  axb-max-l : ∀ {A B : Set} → (PA : Preorder-max-str A) → (PB : Preorder-max-str B) → (l r : (A × B)) → ≤axb PA PB l (axb-max PA PB l r)
  axb-max-l PA PB (a1 , b1) (a2 , b2) = Preorder-max-str.max-l PA a1 a2 , Preorder-max-str.max-l PB b1 b2

  axb-max-r : ∀ {A B : Set} → (PA : Preorder-max-str A) → (PB : Preorder-max-str B) → (l r : (A × B)) → ≤axb PA PB r (axb-max PA PB l r)
  axb-max-r PA PB (a1 , b1) (a2 , b2) = Preorder-max-str.max-r PA a1 a2 , Preorder-max-str.max-r PB b1 b2

  axb-max-lub : ∀ {A B : Set}
                → (PA : Preorder-max-str A)
                → (PB : Preorder-max-str B)
                → (k l r : (A × B))
                → ≤axb PA PB l k → ≤axb PA PB r k → ≤axb PA PB (axb-max PA PB l r) k
  axb-max-lub PA PB (k1 , k2) (l1 , l2) (r1 , r2) (l1<k1 , l2<k2) (r1<k1 , r2<k2) =
                 Preorder-max-str.max-lub PA k1 l1 r1 l1<k1 r1<k1 , Preorder-max-str.max-lub PB k2 l2 r2 l2<k2 r2<k2

  axb-p : ∀ (A B : Set) → Preorder-max-str A → Preorder-max-str B → Preorder-max-str (A × B)
  axb-p A B PA PB = preorder-max (≤axb PA PB) (axb-refl PA PB) (axb-trans PA PB) (axb-max PA PB) (axb-max-l PA PB) (axb-max-r PA PB) (axb-max-lub PA PB)

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

  -- the type of monotone functions from A to B
  record Monotone (A : Set) (B : Set) (PA : Preorder-max-str A) (PB : Preorder-max-str B) : Set where
    constructor monotone
    field
      f : A → B
      is-monotone : ∀ (x y : A) → Preorder-max-str.≤ PA x y → Preorder-max-str.≤ PB (f x) (f y)

  ≤mono : ∀ {A B : Set} → (PA : Preorder-max-str A) → (PB : Preorder-max-str B) → (Monotone A B PA PB) → (Monotone A B PA PB) → Set
  ≤mono {A} PA PB f g = (x : A) → Preorder-max-str.≤ PB (Monotone.f f x) (Monotone.f g x)

  mono-refl : ∀ {A B : Set} → (PA : Preorder-max-str A) → (PB : Preorder-max-str B) → (x : (Monotone A B PA PB)) → ≤mono PA PB x x
  mono-refl PA PB f = λ x → Preorder-max-str.refl PB (Monotone.f f x)

  mono-trans : ∀ {A B : Set} → (PA : Preorder-max-str A) → (PB : Preorder-max-str B) → (x y z : (Monotone A B PA PB)) → ≤mono PA PB x y → ≤mono PA PB y z → ≤mono PA PB x z
  mono-trans PA PB f g h p q = λ x → Preorder-max-str.trans PB (Monotone.f f x) (Monotone.f g x) (Monotone.f h x) (p x) (q x)

  mono-max : ∀ {A B : Set} → (PA : Preorder-max-str A) → (PB : Preorder-max-str B) → (Monotone A B PA PB) → (Monotone A B PA PB) → (Monotone A B PA PB)
  mono-max PA PB (monotone f f-ismono) (monotone g g-ismono) =
             monotone (λ x → Preorder-max-str.max PB (f x) (g x)) (λ x y x₁ → Preorder-max-str.max-lub PB (Preorder-max-str.max PB (f y) (g y)) (f x) (g x)
               (Preorder-max-str.trans PB (f x) (f y) (Preorder-max-str.max PB (f y) (g y)) (f-ismono x y x₁) (Preorder-max-str.max-l PB (f y) (g y)))
                 (Preorder-max-str.trans PB (g x) (g y) (Preorder-max-str.max PB (f y) (g y)) (g-ismono x y x₁) (Preorder-max-str.max-r PB (f y) (g y))))

  mono-max-l : ∀ {A B : Set} → (PA : Preorder-max-str A) → (PB : Preorder-max-str B) → (l r : Monotone A B PA PB) → ≤mono PA PB l (mono-max PA PB l r)
  mono-max-l PA PB f g = λ x → Preorder-max-str.max-l PB (Monotone.f f x) (Monotone.f g x)

  mono-max-r : ∀ {A B : Set} → (PA : Preorder-max-str A) → (PB : Preorder-max-str B) → (l r : Monotone A B PA PB) → ≤mono PA PB r (mono-max PA PB l r)
  mono-max-r PA PB f g = λ x → Preorder-max-str.max-r PB (Monotone.f f x) (Monotone.f g x)

  mono-max-lub : ∀ {A B : Set}
                → (PA : Preorder-max-str A)
                → (PB : Preorder-max-str B)
                → (k l r : Monotone A B PA PB)
                → ≤mono PA PB l k → ≤mono PA PB r k → ≤mono PA PB (mono-max PA PB l r) k
  mono-max-lub PA PB f g h p q = λ x → Preorder-max-str.max-lub PB (Monotone.f f x) (Monotone.f g x) (Monotone.f h x) (p x) (q x)

  mono-p : ∀ (A B : Set) → (PA : Preorder-max-str A) → (PB : Preorder-max-str B) → Preorder-max-str (Monotone A B PA PB)
  mono-p A B PA PB = preorder-max (≤mono PA PB) (mono-refl PA PB) (mono-trans PA PB) (mono-max PA PB) (mono-max-l PA PB) (mono-max-r PA PB) (mono-max-lub PA PB)

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

--"Hey, let's make things monotone!"

  -- another way to define the ≤ relation on Nat
  data _≤'_ : Nat → Nat → Set where
    x≤'x : {x : Nat} → x ≤' x
    x≤'y : {x y : Nat} → x ≤' y → x ≤' (S y)

  -- silly lemmas about silly nats
  nat-lemma : (x : Nat) → Z ≤' x
  nat-lemma Z = x≤'x
  nat-lemma (S x) = x≤'y (nat-lemma x)

  nat-lemma2 : (x y : Nat) → x ≤' y → (S x) ≤' (S y)
  nat-lemma2 .y y x≤'x = x≤'x
  nat-lemma2 x .(S y) (x≤'y {.x} {y} p) = x≤'y (nat-lemma2 x y p)

  nat-lemma3 : (x : Nat) → ≤nat x (S x)
  nat-lemma3 Z = <>
  nat-lemma3 (S x) = nat-lemma3 x

  -- maps to and from the old and new definitions of the ≤ relation
  ≤-map : (x y : Nat) → ≤nat x y → x ≤' y
  ≤-map Z Z f = x≤'x
  ≤-map Z (S y) f = nat-lemma (S y)
  ≤-map (S x) Z ()
  ≤-map (S x) (S y) f = nat-lemma2 x y (≤-map x y f)

  ≤-map2 : (x y : Nat) → x ≤' y → ≤nat x y
  ≤-map2 .y y x≤'x = nat-refl y
  ≤-map2 x .(S y) (x≤'y {.x} {y} f) = nat-trans x y (S y) (≤-map2 x y f) (nat-lemma3 y)

  -- a function to find the maximum of a whole set and not just a pair of values
  max' : ∀ {A : Set} → (PA : Preorder-max-str A) → Nat → (Nat → A) → A
  max' PA Z f = f Z
  max' PA (S n) f = Preorder-max-str.max PA (f (S n)) (max' PA n f)

  -- primitive recursion function corresponding to rec
  natrec : ∀{C : Set} → C → (Nat → C → C) → Nat → C
  natrec base step Z = base
  natrec base step (S n) = step n (natrec base step n)

  -- another lemma
  mono-f-lemma : ∀ {A : Set} → (x y : Nat) → x ≤' y → (PA : Preorder-max-str A) → (f : Nat → A) → Preorder-max-str.≤ PA (max' PA x f) (max' PA y f)
  mono-f-lemma .y y x≤'x PA f = Preorder-max-str.refl PA (max' PA y f)
  mono-f-lemma x .(S y) (x≤'y {.x} {y} p) PA f = Preorder-max-str.trans PA (max' PA x f) (max' PA y f) (max' PA (S y) f)
                                                                        (mono-f-lemma x y p PA f) (Preorder-max-str.max-r PA (f (S y)) (max' PA y f))

  -- make a function monotone by taking the max at every point
  mono-f : ∀ {A : Set} → (PA : Preorder-max-str A) → (f : Nat → A) → Monotone Nat A nat-p PA
  mono-f PA f = monotone (λ x → max' PA x f) (λ x y x₁ → mono-f-lemma x y (≤-map x y x₁) PA f)

  -- f ≤ (monotonization of f)
  mono-f-is-monotone : ∀ {A : Set} → (PA : Preorder-max-str A) → (x : Nat) → (f : Nat → A) → Preorder-max-str.≤ PA (f x) (Monotone.f (mono-f PA f) x)
  mono-f-is-monotone PA Z f = Preorder-max-str.refl PA (f Z)
  mono-f-is-monotone PA (S x) f = Preorder-max-str.max-l PA (f (S x)) (max' PA x f)

  -- if f is already monotone, then its monotonization is less than or equal to itself
  mono-f-≤-itself : ∀ {A : Set}
                    → (PA : Preorder-max-str A)
                    → (x : Nat)
                    → (f : Monotone Nat A nat-p PA)
                    →  Preorder-max-str.≤ PA (Monotone.f (mono-f PA (Monotone.f f)) x) (Monotone.f f x)
  mono-f-≤-itself PA Z f = Preorder-max-str.refl PA (Monotone.f (mono-f PA (Monotone.f f)) Z)
  mono-f-≤-itself PA (S x) f = Preorder-max-str.max-lub PA (Monotone.f f (S x)) (Monotone.f f (S x)) (max' PA x (Monotone.f f))
                                                        (Preorder-max-str.refl PA (Monotone.f f (S x)))
                                                          (Preorder-max-str.trans PA (max' PA x (Monotone.f f))
                                                            (Monotone.f f x) (Monotone.f f (S x)) (mono-f-≤-itself PA x f)
                                                              (Monotone.is-monotone f x (S x) (≤-map2 x (S x) (x≤'y x≤'x))))

  -- monotonize at the end
  mnatrec : ∀ {A : Set} → (PA : Preorder-max-str A) → A → (Nat → A → A) → Nat → A
  mnatrec PA zc sc e = max' PA e (natrec zc sc)

  -- still incorrect
  mono-natrec : ∀ {A : Set} → (PA : Preorder-max-str A) → A → (Nat → A → A) → Nat → A
  mono-natrec PA zc sc Z = zc
  mono-natrec PA zc sc (S y') = Preorder-max-str.max PA zc (sc y' (mono-natrec PA zc sc y'))

  data N' : Set where
    Z1 : N'
    Sa : N' → N'
    Sb : N' → N'

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

-- same thing as Preorder.agda but for this module

  PREORDER = Σ (λ (A : Set) → Preorder-max-str A)

  MONOTONE : (PΓ PA : PREORDER) → Set
  MONOTONE (Γ , PΓ) (A , PA) = Monotone Γ A PΓ PA

  -- some operations
  _×p_ : PREORDER → PREORDER → PREORDER
  (A , PA) ×p (B , PB) = A × B , axb-p A B PA PB

  _->p_ : PREORDER → PREORDER → PREORDER
  (A , PA) ->p (B , PB) = Monotone A B PA PB , mono-p A B PA PB

  -- Unit is a preorder
  unit-p : PREORDER
  unit-p = Unit , preorder-max (λ x x₁ → Unit) (λ x → <>) (λ x y z _ _ → <>) (λ _ _ → <>) (λ l r → <>) (λ l r → <>) (λ k l r _ _ → <>)

  -- identity preserves monotonicity
  id : ∀ {Γ} → MONOTONE Γ Γ
  id = λ {Γ} → monotone (λ x → x) (λ x y x₁ → x₁)

  -- composition preserves monotonicity
  comp : ∀ {PA PB PC} → MONOTONE PA PB → MONOTONE PB PC → MONOTONE PA PC
  comp (monotone f f-ismono) (monotone g g-ismono) = monotone (λ x → g (f x)) (λ x y x₁ → g-ismono (f x) (f y) (f-ismono x y x₁))

  -- proofs that types like pairs etc. with preorders are monotone
  pair' : ∀ {PΓ PA PB} → MONOTONE PΓ PA → MONOTONE PΓ PB → MONOTONE PΓ (PA ×p PB)
  pair' (monotone f f-ismono) (monotone g g-ismono) = monotone (λ x → (f x) , (g x)) (λ x y x₁ → f-ismono x y x₁ , g-ismono x y x₁)

  fst' : ∀ {PΓ PA PB} → MONOTONE PΓ (PA ×p PB) → MONOTONE PΓ PA
  fst' (monotone f f-ismono) =
          monotone (λ x → fst (f x)) (λ x y z → fst (f-ismono x y z))

  snd' : ∀ {PΓ PA PB} → MONOTONE PΓ (PA ×p PB) → MONOTONE PΓ PB
  snd' (monotone f f-ismono) =
          monotone (λ x → snd (f x)) (λ x y z → snd (f-ismono x y z))

  lam' : ∀ {PΓ PA PB} → MONOTONE (PΓ ×p PA) PB → MONOTONE PΓ (PA ->p PB)
  lam' {Γ , preorder-max _ reflΓ _ _ _ _ _} {A , preorder-max _ refla _ _ _ _ _} (monotone f f-ismono) =
          monotone (λ x → monotone (λ p → f (x , p)) (λ a b c → f-ismono (x , a) (x , b) ((reflΓ x) , c))) (λ x y z w → f-ismono (x , w) (y , w) (z , (refla w)))

  app' : ∀ {PΓ PA PB} → MONOTONE PΓ (PA ->p PB) → MONOTONE PΓ PA → MONOTONE PΓ PB
  app' {_} {_} {b , preorder-max _ _ transb _ _ _ _} (monotone f f-ismono) (monotone g g-ismono) =
          monotone (λ x → Monotone.f (f x) (g x)) (λ x y z → transb (Monotone.f (f x) (g x)) (Monotone.f (f y) (g x)) (Monotone.f (f y) (g y))
          (f-ismono x y z (g x)) (Monotone.is-monotone (f y) (g x) (g y) (g-ismono x y z)))

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


text:
module Text.Greek.SBLGNT.Jude where

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

ΙΟΥΔΑ : List (Word)
ΙΟΥΔΑ =
    word (Ἰ ∷ ο ∷ ύ ∷ δ ∷ α ∷ ς ∷ []) "Jude.1.1"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "Jude.1.1"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "Jude.1.1"
  ∷ word (δ ∷ ο ∷ ῦ ∷ ∙λ ∷ ο ∷ ς ∷ []) "Jude.1.1"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ ὸ ∷ ς ∷ []) "Jude.1.1"
  ∷ word (δ ∷ ὲ ∷ []) "Jude.1.1"
  ∷ word (Ἰ ∷ α ∷ κ ∷ ώ ∷ β ∷ ο ∷ υ ∷ []) "Jude.1.1"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "Jude.1.1"
  ∷ word (ἐ ∷ ν ∷ []) "Jude.1.1"
  ∷ word (θ ∷ ε ∷ ῷ ∷ []) "Jude.1.1"
  ∷ word (π ∷ α ∷ τ ∷ ρ ∷ ὶ ∷ []) "Jude.1.1"
  ∷ word (ἠ ∷ γ ∷ α ∷ π ∷ η ∷ μ ∷ έ ∷ ν ∷ ο ∷ ι ∷ ς ∷ []) "Jude.1.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.1"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "Jude.1.1"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ῷ ∷ []) "Jude.1.1"
  ∷ word (τ ∷ ε ∷ τ ∷ η ∷ ρ ∷ η ∷ μ ∷ έ ∷ ν ∷ ο ∷ ι ∷ ς ∷ []) "Jude.1.1"
  ∷ word (κ ∷ ∙λ ∷ η ∷ τ ∷ ο ∷ ῖ ∷ ς ∷ []) "Jude.1.1"
  ∷ word (ἔ ∷ ∙λ ∷ ε ∷ ο ∷ ς ∷ []) "Jude.1.2"
  ∷ word (ὑ ∷ μ ∷ ῖ ∷ ν ∷ []) "Jude.1.2"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.2"
  ∷ word (ε ∷ ἰ ∷ ρ ∷ ή ∷ ν ∷ η ∷ []) "Jude.1.2"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.2"
  ∷ word (ἀ ∷ γ ∷ ά ∷ π ∷ η ∷ []) "Jude.1.2"
  ∷ word (π ∷ ∙λ ∷ η ∷ θ ∷ υ ∷ ν ∷ θ ∷ ε ∷ ί ∷ η ∷ []) "Jude.1.2"
  ∷ word (Ἀ ∷ γ ∷ α ∷ π ∷ η ∷ τ ∷ ο ∷ ί ∷ []) "Jude.1.3"
  ∷ word (π ∷ ᾶ ∷ σ ∷ α ∷ ν ∷ []) "Jude.1.3"
  ∷ word (σ ∷ π ∷ ο ∷ υ ∷ δ ∷ ὴ ∷ ν ∷ []) "Jude.1.3"
  ∷ word (π ∷ ο ∷ ι ∷ ο ∷ ύ ∷ μ ∷ ε ∷ ν ∷ ο ∷ ς ∷ []) "Jude.1.3"
  ∷ word (γ ∷ ρ ∷ ά ∷ φ ∷ ε ∷ ι ∷ ν ∷ []) "Jude.1.3"
  ∷ word (ὑ ∷ μ ∷ ῖ ∷ ν ∷ []) "Jude.1.3"
  ∷ word (π ∷ ε ∷ ρ ∷ ὶ ∷ []) "Jude.1.3"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "Jude.1.3"
  ∷ word (κ ∷ ο ∷ ι ∷ ν ∷ ῆ ∷ ς ∷ []) "Jude.1.3"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "Jude.1.3"
  ∷ word (σ ∷ ω ∷ τ ∷ η ∷ ρ ∷ ί ∷ α ∷ ς ∷ []) "Jude.1.3"
  ∷ word (ἀ ∷ ν ∷ ά ∷ γ ∷ κ ∷ η ∷ ν ∷ []) "Jude.1.3"
  ∷ word (ἔ ∷ σ ∷ χ ∷ ο ∷ ν ∷ []) "Jude.1.3"
  ∷ word (γ ∷ ρ ∷ ά ∷ ψ ∷ α ∷ ι ∷ []) "Jude.1.3"
  ∷ word (ὑ ∷ μ ∷ ῖ ∷ ν ∷ []) "Jude.1.3"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ κ ∷ α ∷ ∙λ ∷ ῶ ∷ ν ∷ []) "Jude.1.3"
  ∷ word (ἐ ∷ π ∷ α ∷ γ ∷ ω ∷ ν ∷ ί ∷ ζ ∷ ε ∷ σ ∷ θ ∷ α ∷ ι ∷ []) "Jude.1.3"
  ∷ word (τ ∷ ῇ ∷ []) "Jude.1.3"
  ∷ word (ἅ ∷ π ∷ α ∷ ξ ∷ []) "Jude.1.3"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ δ ∷ ο ∷ θ ∷ ε ∷ ί ∷ σ ∷ ῃ ∷ []) "Jude.1.3"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "Jude.1.3"
  ∷ word (ἁ ∷ γ ∷ ί ∷ ο ∷ ι ∷ ς ∷ []) "Jude.1.3"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ε ∷ ι ∷ []) "Jude.1.3"
  ∷ word (π ∷ α ∷ ρ ∷ ε ∷ ι ∷ σ ∷ έ ∷ δ ∷ υ ∷ σ ∷ α ∷ ν ∷ []) "Jude.1.4"
  ∷ word (γ ∷ ά ∷ ρ ∷ []) "Jude.1.4"
  ∷ word (τ ∷ ι ∷ ν ∷ ε ∷ ς ∷ []) "Jude.1.4"
  ∷ word (ἄ ∷ ν ∷ θ ∷ ρ ∷ ω ∷ π ∷ ο ∷ ι ∷ []) "Jude.1.4"
  ∷ word (ο ∷ ἱ ∷ []) "Jude.1.4"
  ∷ word (π ∷ ά ∷ ∙λ ∷ α ∷ ι ∷ []) "Jude.1.4"
  ∷ word (π ∷ ρ ∷ ο ∷ γ ∷ ε ∷ γ ∷ ρ ∷ α ∷ μ ∷ μ ∷ έ ∷ ν ∷ ο ∷ ι ∷ []) "Jude.1.4"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "Jude.1.4"
  ∷ word (τ ∷ ο ∷ ῦ ∷ τ ∷ ο ∷ []) "Jude.1.4"
  ∷ word (τ ∷ ὸ ∷ []) "Jude.1.4"
  ∷ word (κ ∷ ρ ∷ ί ∷ μ ∷ α ∷ []) "Jude.1.4"
  ∷ word (ἀ ∷ σ ∷ ε ∷ β ∷ ε ∷ ῖ ∷ ς ∷ []) "Jude.1.4"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "Jude.1.4"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Jude.1.4"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "Jude.1.4"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "Jude.1.4"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ τ ∷ α ∷ []) "Jude.1.4"
  ∷ word (μ ∷ ε ∷ τ ∷ α ∷ τ ∷ ι ∷ θ ∷ έ ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "Jude.1.4"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "Jude.1.4"
  ∷ word (ἀ ∷ σ ∷ έ ∷ ∙λ ∷ γ ∷ ε ∷ ι ∷ α ∷ ν ∷ []) "Jude.1.4"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.4"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "Jude.1.4"
  ∷ word (μ ∷ ό ∷ ν ∷ ο ∷ ν ∷ []) "Jude.1.4"
  ∷ word (δ ∷ ε ∷ σ ∷ π ∷ ό ∷ τ ∷ η ∷ ν ∷ []) "Jude.1.4"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.4"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ν ∷ []) "Jude.1.4"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "Jude.1.4"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ ν ∷ []) "Jude.1.4"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ὸ ∷ ν ∷ []) "Jude.1.4"
  ∷ word (ἀ ∷ ρ ∷ ν ∷ ο ∷ ύ ∷ μ ∷ ε ∷ ν ∷ ο ∷ ι ∷ []) "Jude.1.4"
  ∷ word (Ὑ ∷ π ∷ ο ∷ μ ∷ ν ∷ ῆ ∷ σ ∷ α ∷ ι ∷ []) "Jude.1.5"
  ∷ word (δ ∷ ὲ ∷ []) "Jude.1.5"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "Jude.1.5"
  ∷ word (β ∷ ο ∷ ύ ∷ ∙λ ∷ ο ∷ μ ∷ α ∷ ι ∷ []) "Jude.1.5"
  ∷ word (ε ∷ ἰ ∷ δ ∷ ό ∷ τ ∷ α ∷ ς ∷ []) "Jude.1.5"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "Jude.1.5"
  ∷ word (ἅ ∷ π ∷ α ∷ ξ ∷ []) "Jude.1.5"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ α ∷ []) "Jude.1.5"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "Jude.1.5"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ ς ∷ []) "Jude.1.5"
  ∷ word (∙λ ∷ α ∷ ὸ ∷ ν ∷ []) "Jude.1.5"
  ∷ word (ἐ ∷ κ ∷ []) "Jude.1.5"
  ∷ word (γ ∷ ῆ ∷ ς ∷ []) "Jude.1.5"
  ∷ word (Α ∷ ἰ ∷ γ ∷ ύ ∷ π ∷ τ ∷ ο ∷ υ ∷ []) "Jude.1.5"
  ∷ word (σ ∷ ώ ∷ σ ∷ α ∷ ς ∷ []) "Jude.1.5"
  ∷ word (τ ∷ ὸ ∷ []) "Jude.1.5"
  ∷ word (δ ∷ ε ∷ ύ ∷ τ ∷ ε ∷ ρ ∷ ο ∷ ν ∷ []) "Jude.1.5"
  ∷ word (τ ∷ ο ∷ ὺ ∷ ς ∷ []) "Jude.1.5"
  ∷ word (μ ∷ ὴ ∷ []) "Jude.1.5"
  ∷ word (π ∷ ι ∷ σ ∷ τ ∷ ε ∷ ύ ∷ σ ∷ α ∷ ν ∷ τ ∷ α ∷ ς ∷ []) "Jude.1.5"
  ∷ word (ἀ ∷ π ∷ ώ ∷ ∙λ ∷ ε ∷ σ ∷ ε ∷ ν ∷ []) "Jude.1.5"
  ∷ word (ἀ ∷ γ ∷ γ ∷ έ ∷ ∙λ ∷ ο ∷ υ ∷ ς ∷ []) "Jude.1.6"
  ∷ word (τ ∷ ε ∷ []) "Jude.1.6"
  ∷ word (τ ∷ ο ∷ ὺ ∷ ς ∷ []) "Jude.1.6"
  ∷ word (μ ∷ ὴ ∷ []) "Jude.1.6"
  ∷ word (τ ∷ η ∷ ρ ∷ ή ∷ σ ∷ α ∷ ν ∷ τ ∷ α ∷ ς ∷ []) "Jude.1.6"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "Jude.1.6"
  ∷ word (ἑ ∷ α ∷ υ ∷ τ ∷ ῶ ∷ ν ∷ []) "Jude.1.6"
  ∷ word (ἀ ∷ ρ ∷ χ ∷ ὴ ∷ ν ∷ []) "Jude.1.6"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "Jude.1.6"
  ∷ word (ἀ ∷ π ∷ ο ∷ ∙λ ∷ ι ∷ π ∷ ό ∷ ν ∷ τ ∷ α ∷ ς ∷ []) "Jude.1.6"
  ∷ word (τ ∷ ὸ ∷ []) "Jude.1.6"
  ∷ word (ἴ ∷ δ ∷ ι ∷ ο ∷ ν ∷ []) "Jude.1.6"
  ∷ word (ο ∷ ἰ ∷ κ ∷ η ∷ τ ∷ ή ∷ ρ ∷ ι ∷ ο ∷ ν ∷ []) "Jude.1.6"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "Jude.1.6"
  ∷ word (κ ∷ ρ ∷ ί ∷ σ ∷ ι ∷ ν ∷ []) "Jude.1.6"
  ∷ word (μ ∷ ε ∷ γ ∷ ά ∷ ∙λ ∷ η ∷ ς ∷ []) "Jude.1.6"
  ∷ word (ἡ ∷ μ ∷ έ ∷ ρ ∷ α ∷ ς ∷ []) "Jude.1.6"
  ∷ word (δ ∷ ε ∷ σ ∷ μ ∷ ο ∷ ῖ ∷ ς ∷ []) "Jude.1.6"
  ∷ word (ἀ ∷ ϊ ∷ δ ∷ ί ∷ ο ∷ ι ∷ ς ∷ []) "Jude.1.6"
  ∷ word (ὑ ∷ π ∷ ὸ ∷ []) "Jude.1.6"
  ∷ word (ζ ∷ ό ∷ φ ∷ ο ∷ ν ∷ []) "Jude.1.6"
  ∷ word (τ ∷ ε ∷ τ ∷ ή ∷ ρ ∷ η ∷ κ ∷ ε ∷ ν ∷ []) "Jude.1.6"
  ∷ word (ὡ ∷ ς ∷ []) "Jude.1.7"
  ∷ word (Σ ∷ ό ∷ δ ∷ ο ∷ μ ∷ α ∷ []) "Jude.1.7"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.7"
  ∷ word (Γ ∷ ό ∷ μ ∷ ο ∷ ρ ∷ ρ ∷ α ∷ []) "Jude.1.7"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.7"
  ∷ word (α ∷ ἱ ∷ []) "Jude.1.7"
  ∷ word (π ∷ ε ∷ ρ ∷ ὶ ∷ []) "Jude.1.7"
  ∷ word (α ∷ ὐ ∷ τ ∷ ὰ ∷ ς ∷ []) "Jude.1.7"
  ∷ word (π ∷ ό ∷ ∙λ ∷ ε ∷ ι ∷ ς ∷ []) "Jude.1.7"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "Jude.1.7"
  ∷ word (ὅ ∷ μ ∷ ο ∷ ι ∷ ο ∷ ν ∷ []) "Jude.1.7"
  ∷ word (τ ∷ ρ ∷ ό ∷ π ∷ ο ∷ ν ∷ []) "Jude.1.7"
  ∷ word (τ ∷ ο ∷ ύ ∷ τ ∷ ο ∷ ι ∷ ς ∷ []) "Jude.1.7"
  ∷ word (ἐ ∷ κ ∷ π ∷ ο ∷ ρ ∷ ν ∷ ε ∷ ύ ∷ σ ∷ α ∷ σ ∷ α ∷ ι ∷ []) "Jude.1.7"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.7"
  ∷ word (ἀ ∷ π ∷ ε ∷ ∙λ ∷ θ ∷ ο ∷ ῦ ∷ σ ∷ α ∷ ι ∷ []) "Jude.1.7"
  ∷ word (ὀ ∷ π ∷ ί ∷ σ ∷ ω ∷ []) "Jude.1.7"
  ∷ word (σ ∷ α ∷ ρ ∷ κ ∷ ὸ ∷ ς ∷ []) "Jude.1.7"
  ∷ word (ἑ ∷ τ ∷ έ ∷ ρ ∷ α ∷ ς ∷ []) "Jude.1.7"
  ∷ word (π ∷ ρ ∷ ό ∷ κ ∷ ε ∷ ι ∷ ν ∷ τ ∷ α ∷ ι ∷ []) "Jude.1.7"
  ∷ word (δ ∷ ε ∷ ῖ ∷ γ ∷ μ ∷ α ∷ []) "Jude.1.7"
  ∷ word (π ∷ υ ∷ ρ ∷ ὸ ∷ ς ∷ []) "Jude.1.7"
  ∷ word (α ∷ ἰ ∷ ω ∷ ν ∷ ί ∷ ο ∷ υ ∷ []) "Jude.1.7"
  ∷ word (δ ∷ ί ∷ κ ∷ η ∷ ν ∷ []) "Jude.1.7"
  ∷ word (ὑ ∷ π ∷ έ ∷ χ ∷ ο ∷ υ ∷ σ ∷ α ∷ ι ∷ []) "Jude.1.7"
  ∷ word (Ὁ ∷ μ ∷ ο ∷ ί ∷ ω ∷ ς ∷ []) "Jude.1.8"
  ∷ word (μ ∷ έ ∷ ν ∷ τ ∷ ο ∷ ι ∷ []) "Jude.1.8"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.8"
  ∷ word (ο ∷ ὗ ∷ τ ∷ ο ∷ ι ∷ []) "Jude.1.8"
  ∷ word (ἐ ∷ ν ∷ υ ∷ π ∷ ν ∷ ι ∷ α ∷ ζ ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ι ∷ []) "Jude.1.8"
  ∷ word (σ ∷ ά ∷ ρ ∷ κ ∷ α ∷ []) "Jude.1.8"
  ∷ word (μ ∷ ὲ ∷ ν ∷ []) "Jude.1.8"
  ∷ word (μ ∷ ι ∷ α ∷ ί ∷ ν ∷ ο ∷ υ ∷ σ ∷ ι ∷ ν ∷ []) "Jude.1.8"
  ∷ word (κ ∷ υ ∷ ρ ∷ ι ∷ ό ∷ τ ∷ η ∷ τ ∷ α ∷ []) "Jude.1.8"
  ∷ word (δ ∷ ὲ ∷ []) "Jude.1.8"
  ∷ word (ἀ ∷ θ ∷ ε ∷ τ ∷ ο ∷ ῦ ∷ σ ∷ ι ∷ ν ∷ []) "Jude.1.8"
  ∷ word (δ ∷ ό ∷ ξ ∷ α ∷ ς ∷ []) "Jude.1.8"
  ∷ word (δ ∷ ὲ ∷ []) "Jude.1.8"
  ∷ word (β ∷ ∙λ ∷ α ∷ σ ∷ φ ∷ η ∷ μ ∷ ο ∷ ῦ ∷ σ ∷ ι ∷ ν ∷ []) "Jude.1.8"
  ∷ word (ὁ ∷ []) "Jude.1.9"
  ∷ word (δ ∷ ὲ ∷ []) "Jude.1.9"
  ∷ word (Μ ∷ ι ∷ χ ∷ α ∷ ὴ ∷ ∙λ ∷ []) "Jude.1.9"
  ∷ word (ὁ ∷ []) "Jude.1.9"
  ∷ word (ἀ ∷ ρ ∷ χ ∷ ά ∷ γ ∷ γ ∷ ε ∷ ∙λ ∷ ο ∷ ς ∷ []) "Jude.1.9"
  ∷ word (ὅ ∷ τ ∷ ε ∷ []) "Jude.1.9"
  ∷ word (τ ∷ ῷ ∷ []) "Jude.1.9"
  ∷ word (δ ∷ ι ∷ α ∷ β ∷ ό ∷ ∙λ ∷ ῳ ∷ []) "Jude.1.9"
  ∷ word (δ ∷ ι ∷ α ∷ κ ∷ ρ ∷ ι ∷ ν ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ς ∷ []) "Jude.1.9"
  ∷ word (δ ∷ ι ∷ ε ∷ ∙λ ∷ έ ∷ γ ∷ ε ∷ τ ∷ ο ∷ []) "Jude.1.9"
  ∷ word (π ∷ ε ∷ ρ ∷ ὶ ∷ []) "Jude.1.9"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Jude.1.9"
  ∷ word (Μ ∷ ω ∷ ϋ ∷ σ ∷ έ ∷ ω ∷ ς ∷ []) "Jude.1.9"
  ∷ word (σ ∷ ώ ∷ μ ∷ α ∷ τ ∷ ο ∷ ς ∷ []) "Jude.1.9"
  ∷ word (ο ∷ ὐ ∷ κ ∷ []) "Jude.1.9"
  ∷ word (ἐ ∷ τ ∷ ό ∷ ∙λ ∷ μ ∷ η ∷ σ ∷ ε ∷ ν ∷ []) "Jude.1.9"
  ∷ word (κ ∷ ρ ∷ ί ∷ σ ∷ ι ∷ ν ∷ []) "Jude.1.9"
  ∷ word (ἐ ∷ π ∷ ε ∷ ν ∷ ε ∷ γ ∷ κ ∷ ε ∷ ῖ ∷ ν ∷ []) "Jude.1.9"
  ∷ word (β ∷ ∙λ ∷ α ∷ σ ∷ φ ∷ η ∷ μ ∷ ί ∷ α ∷ ς ∷ []) "Jude.1.9"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "Jude.1.9"
  ∷ word (ε ∷ ἶ ∷ π ∷ ε ∷ ν ∷ []) "Jude.1.9"
  ∷ word (Ἐ ∷ π ∷ ι ∷ τ ∷ ι ∷ μ ∷ ή ∷ σ ∷ α ∷ ι ∷ []) "Jude.1.9"
  ∷ word (σ ∷ ο ∷ ι ∷ []) "Jude.1.9"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ς ∷ []) "Jude.1.9"
  ∷ word (ο ∷ ὗ ∷ τ ∷ ο ∷ ι ∷ []) "Jude.1.10"
  ∷ word (δ ∷ ὲ ∷ []) "Jude.1.10"
  ∷ word (ὅ ∷ σ ∷ α ∷ []) "Jude.1.10"
  ∷ word (μ ∷ ὲ ∷ ν ∷ []) "Jude.1.10"
  ∷ word (ο ∷ ὐ ∷ κ ∷ []) "Jude.1.10"
  ∷ word (ο ∷ ἴ ∷ δ ∷ α ∷ σ ∷ ι ∷ ν ∷ []) "Jude.1.10"
  ∷ word (β ∷ ∙λ ∷ α ∷ σ ∷ φ ∷ η ∷ μ ∷ ο ∷ ῦ ∷ σ ∷ ι ∷ ν ∷ []) "Jude.1.10"
  ∷ word (ὅ ∷ σ ∷ α ∷ []) "Jude.1.10"
  ∷ word (δ ∷ ὲ ∷ []) "Jude.1.10"
  ∷ word (φ ∷ υ ∷ σ ∷ ι ∷ κ ∷ ῶ ∷ ς ∷ []) "Jude.1.10"
  ∷ word (ὡ ∷ ς ∷ []) "Jude.1.10"
  ∷ word (τ ∷ ὰ ∷ []) "Jude.1.10"
  ∷ word (ἄ ∷ ∙λ ∷ ο ∷ γ ∷ α ∷ []) "Jude.1.10"
  ∷ word (ζ ∷ ῷ ∷ α ∷ []) "Jude.1.10"
  ∷ word (ἐ ∷ π ∷ ί ∷ σ ∷ τ ∷ α ∷ ν ∷ τ ∷ α ∷ ι ∷ []) "Jude.1.10"
  ∷ word (ἐ ∷ ν ∷ []) "Jude.1.10"
  ∷ word (τ ∷ ο ∷ ύ ∷ τ ∷ ο ∷ ι ∷ ς ∷ []) "Jude.1.10"
  ∷ word (φ ∷ θ ∷ ε ∷ ί ∷ ρ ∷ ο ∷ ν ∷ τ ∷ α ∷ ι ∷ []) "Jude.1.10"
  ∷ word (ο ∷ ὐ ∷ α ∷ ὶ ∷ []) "Jude.1.11"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῖ ∷ ς ∷ []) "Jude.1.11"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "Jude.1.11"
  ∷ word (τ ∷ ῇ ∷ []) "Jude.1.11"
  ∷ word (ὁ ∷ δ ∷ ῷ ∷ []) "Jude.1.11"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Jude.1.11"
  ∷ word (Κ ∷ ά ∷ ϊ ∷ ν ∷ []) "Jude.1.11"
  ∷ word (ἐ ∷ π ∷ ο ∷ ρ ∷ ε ∷ ύ ∷ θ ∷ η ∷ σ ∷ α ∷ ν ∷ []) "Jude.1.11"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.11"
  ∷ word (τ ∷ ῇ ∷ []) "Jude.1.11"
  ∷ word (π ∷ ∙λ ∷ ά ∷ ν ∷ ῃ ∷ []) "Jude.1.11"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Jude.1.11"
  ∷ word (Β ∷ α ∷ ∙λ ∷ α ∷ ὰ ∷ μ ∷ []) "Jude.1.11"
  ∷ word (μ ∷ ι ∷ σ ∷ θ ∷ ο ∷ ῦ ∷ []) "Jude.1.11"
  ∷ word (ἐ ∷ ξ ∷ ε ∷ χ ∷ ύ ∷ θ ∷ η ∷ σ ∷ α ∷ ν ∷ []) "Jude.1.11"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.11"
  ∷ word (τ ∷ ῇ ∷ []) "Jude.1.11"
  ∷ word (ἀ ∷ ν ∷ τ ∷ ι ∷ ∙λ ∷ ο ∷ γ ∷ ί ∷ ᾳ ∷ []) "Jude.1.11"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Jude.1.11"
  ∷ word (Κ ∷ ό ∷ ρ ∷ ε ∷ []) "Jude.1.11"
  ∷ word (ἀ ∷ π ∷ ώ ∷ ∙λ ∷ ο ∷ ν ∷ τ ∷ ο ∷ []) "Jude.1.11"
  ∷ word (ο ∷ ὗ ∷ τ ∷ ο ∷ ί ∷ []) "Jude.1.12"
  ∷ word (ε ∷ ἰ ∷ σ ∷ ι ∷ ν ∷ []) "Jude.1.12"
  ∷ word (ο ∷ ἱ ∷ []) "Jude.1.12"
  ∷ word (ἐ ∷ ν ∷ []) "Jude.1.12"
  ∷ word (τ ∷ α ∷ ῖ ∷ ς ∷ []) "Jude.1.12"
  ∷ word (ἀ ∷ γ ∷ ά ∷ π ∷ α ∷ ι ∷ ς ∷ []) "Jude.1.12"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "Jude.1.12"
  ∷ word (σ ∷ π ∷ ι ∷ ∙λ ∷ ά ∷ δ ∷ ε ∷ ς ∷ []) "Jude.1.12"
  ∷ word (σ ∷ υ ∷ ν ∷ ε ∷ υ ∷ ω ∷ χ ∷ ο ∷ ύ ∷ μ ∷ ε ∷ ν ∷ ο ∷ ι ∷ []) "Jude.1.12"
  ∷ word (ἀ ∷ φ ∷ ό ∷ β ∷ ω ∷ ς ∷ []) "Jude.1.12"
  ∷ word (ἑ ∷ α ∷ υ ∷ τ ∷ ο ∷ ὺ ∷ ς ∷ []) "Jude.1.12"
  ∷ word (π ∷ ο ∷ ι ∷ μ ∷ α ∷ ί ∷ ν ∷ ο ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "Jude.1.12"
  ∷ word (ν ∷ ε ∷ φ ∷ έ ∷ ∙λ ∷ α ∷ ι ∷ []) "Jude.1.12"
  ∷ word (ἄ ∷ ν ∷ υ ∷ δ ∷ ρ ∷ ο ∷ ι ∷ []) "Jude.1.12"
  ∷ word (ὑ ∷ π ∷ ὸ ∷ []) "Jude.1.12"
  ∷ word (ἀ ∷ ν ∷ έ ∷ μ ∷ ω ∷ ν ∷ []) "Jude.1.12"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ φ ∷ ε ∷ ρ ∷ ό ∷ μ ∷ ε ∷ ν ∷ α ∷ ι ∷ []) "Jude.1.12"
  ∷ word (δ ∷ έ ∷ ν ∷ δ ∷ ρ ∷ α ∷ []) "Jude.1.12"
  ∷ word (φ ∷ θ ∷ ι ∷ ν ∷ ο ∷ π ∷ ω ∷ ρ ∷ ι ∷ ν ∷ ὰ ∷ []) "Jude.1.12"
  ∷ word (ἄ ∷ κ ∷ α ∷ ρ ∷ π ∷ α ∷ []) "Jude.1.12"
  ∷ word (δ ∷ ὶ ∷ ς ∷ []) "Jude.1.12"
  ∷ word (ἀ ∷ π ∷ ο ∷ θ ∷ α ∷ ν ∷ ό ∷ ν ∷ τ ∷ α ∷ []) "Jude.1.12"
  ∷ word (ἐ ∷ κ ∷ ρ ∷ ι ∷ ζ ∷ ω ∷ θ ∷ έ ∷ ν ∷ τ ∷ α ∷ []) "Jude.1.12"
  ∷ word (κ ∷ ύ ∷ μ ∷ α ∷ τ ∷ α ∷ []) "Jude.1.13"
  ∷ word (ἄ ∷ γ ∷ ρ ∷ ι ∷ α ∷ []) "Jude.1.13"
  ∷ word (θ ∷ α ∷ ∙λ ∷ ά ∷ σ ∷ σ ∷ η ∷ ς ∷ []) "Jude.1.13"
  ∷ word (ἐ ∷ π ∷ α ∷ φ ∷ ρ ∷ ί ∷ ζ ∷ ο ∷ ν ∷ τ ∷ α ∷ []) "Jude.1.13"
  ∷ word (τ ∷ ὰ ∷ ς ∷ []) "Jude.1.13"
  ∷ word (ἑ ∷ α ∷ υ ∷ τ ∷ ῶ ∷ ν ∷ []) "Jude.1.13"
  ∷ word (α ∷ ἰ ∷ σ ∷ χ ∷ ύ ∷ ν ∷ α ∷ ς ∷ []) "Jude.1.13"
  ∷ word (ἀ ∷ σ ∷ τ ∷ έ ∷ ρ ∷ ε ∷ ς ∷ []) "Jude.1.13"
  ∷ word (π ∷ ∙λ ∷ α ∷ ν ∷ ῆ ∷ τ ∷ α ∷ ι ∷ []) "Jude.1.13"
  ∷ word (ο ∷ ἷ ∷ ς ∷ []) "Jude.1.13"
  ∷ word (ὁ ∷ []) "Jude.1.13"
  ∷ word (ζ ∷ ό ∷ φ ∷ ο ∷ ς ∷ []) "Jude.1.13"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Jude.1.13"
  ∷ word (σ ∷ κ ∷ ό ∷ τ ∷ ο ∷ υ ∷ ς ∷ []) "Jude.1.13"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "Jude.1.13"
  ∷ word (α ∷ ἰ ∷ ῶ ∷ ν ∷ α ∷ []) "Jude.1.13"
  ∷ word (τ ∷ ε ∷ τ ∷ ή ∷ ρ ∷ η ∷ τ ∷ α ∷ ι ∷ []) "Jude.1.13"
  ∷ word (Π ∷ ρ ∷ ο ∷ ε ∷ φ ∷ ή ∷ τ ∷ ε ∷ υ ∷ σ ∷ ε ∷ ν ∷ []) "Jude.1.14"
  ∷ word (δ ∷ ὲ ∷ []) "Jude.1.14"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.14"
  ∷ word (τ ∷ ο ∷ ύ ∷ τ ∷ ο ∷ ι ∷ ς ∷ []) "Jude.1.14"
  ∷ word (ἕ ∷ β ∷ δ ∷ ο ∷ μ ∷ ο ∷ ς ∷ []) "Jude.1.14"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "Jude.1.14"
  ∷ word (Ἀ ∷ δ ∷ ὰ ∷ μ ∷ []) "Jude.1.14"
  ∷ word (Ἑ ∷ ν ∷ ὼ ∷ χ ∷ []) "Jude.1.14"
  ∷ word (∙λ ∷ έ ∷ γ ∷ ω ∷ ν ∷ []) "Jude.1.14"
  ∷ word (Ἰ ∷ δ ∷ ο ∷ ὺ ∷ []) "Jude.1.14"
  ∷ word (ἦ ∷ ∙λ ∷ θ ∷ ε ∷ ν ∷ []) "Jude.1.14"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ς ∷ []) "Jude.1.14"
  ∷ word (ἐ ∷ ν ∷ []) "Jude.1.14"
  ∷ word (ἁ ∷ γ ∷ ί ∷ α ∷ ι ∷ ς ∷ []) "Jude.1.14"
  ∷ word (μ ∷ υ ∷ ρ ∷ ι ∷ ά ∷ σ ∷ ι ∷ ν ∷ []) "Jude.1.14"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "Jude.1.14"
  ∷ word (π ∷ ο ∷ ι ∷ ῆ ∷ σ ∷ α ∷ ι ∷ []) "Jude.1.15"
  ∷ word (κ ∷ ρ ∷ ί ∷ σ ∷ ι ∷ ν ∷ []) "Jude.1.15"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "Jude.1.15"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ω ∷ ν ∷ []) "Jude.1.15"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.15"
  ∷ word (ἐ ∷ ∙λ ∷ έ ∷ γ ∷ ξ ∷ α ∷ ι ∷ []) "Jude.1.15"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ α ∷ ς ∷ []) "Jude.1.15"
  ∷ word (τ ∷ ο ∷ ὺ ∷ ς ∷ []) "Jude.1.15"
  ∷ word (ἀ ∷ σ ∷ ε ∷ β ∷ ε ∷ ῖ ∷ ς ∷ []) "Jude.1.15"
  ∷ word (π ∷ ε ∷ ρ ∷ ὶ ∷ []) "Jude.1.15"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ω ∷ ν ∷ []) "Jude.1.15"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "Jude.1.15"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ ω ∷ ν ∷ []) "Jude.1.15"
  ∷ word (ἀ ∷ σ ∷ ε ∷ β ∷ ε ∷ ί ∷ α ∷ ς ∷ []) "Jude.1.15"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῶ ∷ ν ∷ []) "Jude.1.15"
  ∷ word (ὧ ∷ ν ∷ []) "Jude.1.15"
  ∷ word (ἠ ∷ σ ∷ έ ∷ β ∷ η ∷ σ ∷ α ∷ ν ∷ []) "Jude.1.15"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.15"
  ∷ word (π ∷ ε ∷ ρ ∷ ὶ ∷ []) "Jude.1.15"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ω ∷ ν ∷ []) "Jude.1.15"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "Jude.1.15"
  ∷ word (σ ∷ κ ∷ ∙λ ∷ η ∷ ρ ∷ ῶ ∷ ν ∷ []) "Jude.1.15"
  ∷ word (ὧ ∷ ν ∷ []) "Jude.1.15"
  ∷ word (ἐ ∷ ∙λ ∷ ά ∷ ∙λ ∷ η ∷ σ ∷ α ∷ ν ∷ []) "Jude.1.15"
  ∷ word (κ ∷ α ∷ τ ∷ []) "Jude.1.15"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "Jude.1.15"
  ∷ word (ἁ ∷ μ ∷ α ∷ ρ ∷ τ ∷ ω ∷ ∙λ ∷ ο ∷ ὶ ∷ []) "Jude.1.15"
  ∷ word (ἀ ∷ σ ∷ ε ∷ β ∷ ε ∷ ῖ ∷ ς ∷ []) "Jude.1.15"
  ∷ word (ο ∷ ὗ ∷ τ ∷ ο ∷ ί ∷ []) "Jude.1.16"
  ∷ word (ε ∷ ἰ ∷ σ ∷ ι ∷ ν ∷ []) "Jude.1.16"
  ∷ word (γ ∷ ο ∷ γ ∷ γ ∷ υ ∷ σ ∷ τ ∷ α ∷ ί ∷ []) "Jude.1.16"
  ∷ word (μ ∷ ε ∷ μ ∷ ψ ∷ ί ∷ μ ∷ ο ∷ ι ∷ ρ ∷ ο ∷ ι ∷ []) "Jude.1.16"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "Jude.1.16"
  ∷ word (τ ∷ ὰ ∷ ς ∷ []) "Jude.1.16"
  ∷ word (ἐ ∷ π ∷ ι ∷ θ ∷ υ ∷ μ ∷ ί ∷ α ∷ ς ∷ []) "Jude.1.16"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῶ ∷ ν ∷ []) "Jude.1.16"
  ∷ word (π ∷ ο ∷ ρ ∷ ε ∷ υ ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ι ∷ []) "Jude.1.16"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.16"
  ∷ word (τ ∷ ὸ ∷ []) "Jude.1.16"
  ∷ word (σ ∷ τ ∷ ό ∷ μ ∷ α ∷ []) "Jude.1.16"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῶ ∷ ν ∷ []) "Jude.1.16"
  ∷ word (∙λ ∷ α ∷ ∙λ ∷ ε ∷ ῖ ∷ []) "Jude.1.16"
  ∷ word (ὑ ∷ π ∷ έ ∷ ρ ∷ ο ∷ γ ∷ κ ∷ α ∷ []) "Jude.1.16"
  ∷ word (θ ∷ α ∷ υ ∷ μ ∷ ά ∷ ζ ∷ ο ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "Jude.1.16"
  ∷ word (π ∷ ρ ∷ ό ∷ σ ∷ ω ∷ π ∷ α ∷ []) "Jude.1.16"
  ∷ word (ὠ ∷ φ ∷ ε ∷ ∙λ ∷ ε ∷ ί ∷ α ∷ ς ∷ []) "Jude.1.16"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ ν ∷ []) "Jude.1.16"
  ∷ word (Ὑ ∷ μ ∷ ε ∷ ῖ ∷ ς ∷ []) "Jude.1.17"
  ∷ word (δ ∷ έ ∷ []) "Jude.1.17"
  ∷ word (ἀ ∷ γ ∷ α ∷ π ∷ η ∷ τ ∷ ο ∷ ί ∷ []) "Jude.1.17"
  ∷ word (μ ∷ ν ∷ ή ∷ σ ∷ θ ∷ η ∷ τ ∷ ε ∷ []) "Jude.1.17"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "Jude.1.17"
  ∷ word (ῥ ∷ η ∷ μ ∷ ά ∷ τ ∷ ω ∷ ν ∷ []) "Jude.1.17"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "Jude.1.17"
  ∷ word (π ∷ ρ ∷ ο ∷ ε ∷ ι ∷ ρ ∷ η ∷ μ ∷ έ ∷ ν ∷ ω ∷ ν ∷ []) "Jude.1.17"
  ∷ word (ὑ ∷ π ∷ ὸ ∷ []) "Jude.1.17"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "Jude.1.17"
  ∷ word (ἀ ∷ π ∷ ο ∷ σ ∷ τ ∷ ό ∷ ∙λ ∷ ω ∷ ν ∷ []) "Jude.1.17"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Jude.1.17"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "Jude.1.17"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "Jude.1.17"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "Jude.1.17"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "Jude.1.17"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "Jude.1.18"
  ∷ word (ἔ ∷ ∙λ ∷ ε ∷ γ ∷ ο ∷ ν ∷ []) "Jude.1.18"
  ∷ word (ὑ ∷ μ ∷ ῖ ∷ ν ∷ []) "Jude.1.18"
  ∷ word (Ἐ ∷ π ∷ []) "Jude.1.18"
  ∷ word (ἐ ∷ σ ∷ χ ∷ ά ∷ τ ∷ ο ∷ υ ∷ []) "Jude.1.18"
  ∷ word (χ ∷ ρ ∷ ό ∷ ν ∷ ο ∷ υ ∷ []) "Jude.1.18"
  ∷ word (ἔ ∷ σ ∷ ο ∷ ν ∷ τ ∷ α ∷ ι ∷ []) "Jude.1.18"
  ∷ word (ἐ ∷ μ ∷ π ∷ α ∷ ῖ ∷ κ ∷ τ ∷ α ∷ ι ∷ []) "Jude.1.18"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "Jude.1.18"
  ∷ word (τ ∷ ὰ ∷ ς ∷ []) "Jude.1.18"
  ∷ word (ἑ ∷ α ∷ υ ∷ τ ∷ ῶ ∷ ν ∷ []) "Jude.1.18"
  ∷ word (ἐ ∷ π ∷ ι ∷ θ ∷ υ ∷ μ ∷ ί ∷ α ∷ ς ∷ []) "Jude.1.18"
  ∷ word (π ∷ ο ∷ ρ ∷ ε ∷ υ ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ι ∷ []) "Jude.1.18"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "Jude.1.18"
  ∷ word (ἀ ∷ σ ∷ ε ∷ β ∷ ε ∷ ι ∷ ῶ ∷ ν ∷ []) "Jude.1.18"
  ∷ word (ο ∷ ὗ ∷ τ ∷ ο ∷ ί ∷ []) "Jude.1.19"
  ∷ word (ε ∷ ἰ ∷ σ ∷ ι ∷ ν ∷ []) "Jude.1.19"
  ∷ word (ο ∷ ἱ ∷ []) "Jude.1.19"
  ∷ word (ἀ ∷ π ∷ ο ∷ δ ∷ ι ∷ ο ∷ ρ ∷ ί ∷ ζ ∷ ο ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "Jude.1.19"
  ∷ word (ψ ∷ υ ∷ χ ∷ ι ∷ κ ∷ ο ∷ ί ∷ []) "Jude.1.19"
  ∷ word (π ∷ ν ∷ ε ∷ ῦ ∷ μ ∷ α ∷ []) "Jude.1.19"
  ∷ word (μ ∷ ὴ ∷ []) "Jude.1.19"
  ∷ word (ἔ ∷ χ ∷ ο ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "Jude.1.19"
  ∷ word (ὑ ∷ μ ∷ ε ∷ ῖ ∷ ς ∷ []) "Jude.1.20"
  ∷ word (δ ∷ έ ∷ []) "Jude.1.20"
  ∷ word (ἀ ∷ γ ∷ α ∷ π ∷ η ∷ τ ∷ ο ∷ ί ∷ []) "Jude.1.20"
  ∷ word (ἐ ∷ π ∷ ο ∷ ι ∷ κ ∷ ο ∷ δ ∷ ο ∷ μ ∷ ο ∷ ῦ ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "Jude.1.20"
  ∷ word (ἑ ∷ α ∷ υ ∷ τ ∷ ο ∷ ὺ ∷ ς ∷ []) "Jude.1.20"
  ∷ word (τ ∷ ῇ ∷ []) "Jude.1.20"
  ∷ word (ἁ ∷ γ ∷ ι ∷ ω ∷ τ ∷ ά ∷ τ ∷ ῃ ∷ []) "Jude.1.20"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "Jude.1.20"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ε ∷ ι ∷ []) "Jude.1.20"
  ∷ word (ἐ ∷ ν ∷ []) "Jude.1.20"
  ∷ word (π ∷ ν ∷ ε ∷ ύ ∷ μ ∷ α ∷ τ ∷ ι ∷ []) "Jude.1.20"
  ∷ word (ἁ ∷ γ ∷ ί ∷ ῳ ∷ []) "Jude.1.20"
  ∷ word (π ∷ ρ ∷ ο ∷ σ ∷ ε ∷ υ ∷ χ ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ι ∷ []) "Jude.1.20"
  ∷ word (ἑ ∷ α ∷ υ ∷ τ ∷ ο ∷ ὺ ∷ ς ∷ []) "Jude.1.21"
  ∷ word (ἐ ∷ ν ∷ []) "Jude.1.21"
  ∷ word (ἀ ∷ γ ∷ ά ∷ π ∷ ῃ ∷ []) "Jude.1.21"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "Jude.1.21"
  ∷ word (τ ∷ η ∷ ρ ∷ ή ∷ σ ∷ α ∷ τ ∷ ε ∷ []) "Jude.1.21"
  ∷ word (π ∷ ρ ∷ ο ∷ σ ∷ δ ∷ ε ∷ χ ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ι ∷ []) "Jude.1.21"
  ∷ word (τ ∷ ὸ ∷ []) "Jude.1.21"
  ∷ word (ἔ ∷ ∙λ ∷ ε ∷ ο ∷ ς ∷ []) "Jude.1.21"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Jude.1.21"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "Jude.1.21"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "Jude.1.21"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "Jude.1.21"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "Jude.1.21"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "Jude.1.21"
  ∷ word (ζ ∷ ω ∷ ὴ ∷ ν ∷ []) "Jude.1.21"
  ∷ word (α ∷ ἰ ∷ ώ ∷ ν ∷ ι ∷ ο ∷ ν ∷ []) "Jude.1.21"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.22"
  ∷ word (ο ∷ ὓ ∷ ς ∷ []) "Jude.1.22"
  ∷ word (μ ∷ ὲ ∷ ν ∷ []) "Jude.1.22"
  ∷ word (ἐ ∷ ∙λ ∷ ε ∷ ᾶ ∷ τ ∷ ε ∷ []) "Jude.1.22"
  ∷ word (δ ∷ ι ∷ α ∷ κ ∷ ρ ∷ ι ∷ ν ∷ ο ∷ μ ∷ έ ∷ ν ∷ ο ∷ υ ∷ ς ∷ []) "Jude.1.22"
  ∷ word (ο ∷ ὓ ∷ ς ∷ []) "Jude.1.23"
  ∷ word (δ ∷ ὲ ∷ []) "Jude.1.23"
  ∷ word (σ ∷ ῴ ∷ ζ ∷ ε ∷ τ ∷ ε ∷ []) "Jude.1.23"
  ∷ word (ἐ ∷ κ ∷ []) "Jude.1.23"
  ∷ word (π ∷ υ ∷ ρ ∷ ὸ ∷ ς ∷ []) "Jude.1.23"
  ∷ word (ἁ ∷ ρ ∷ π ∷ ά ∷ ζ ∷ ο ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "Jude.1.23"
  ∷ word (ο ∷ ὓ ∷ ς ∷ []) "Jude.1.23"
  ∷ word (δ ∷ ὲ ∷ []) "Jude.1.23"
  ∷ word (ἐ ∷ ∙λ ∷ ε ∷ ᾶ ∷ τ ∷ ε ∷ []) "Jude.1.23"
  ∷ word (ἐ ∷ ν ∷ []) "Jude.1.23"
  ∷ word (φ ∷ ό ∷ β ∷ ῳ ∷ []) "Jude.1.23"
  ∷ word (μ ∷ ι ∷ σ ∷ ο ∷ ῦ ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "Jude.1.23"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.23"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "Jude.1.23"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "Jude.1.23"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "Jude.1.23"
  ∷ word (σ ∷ α ∷ ρ ∷ κ ∷ ὸ ∷ ς ∷ []) "Jude.1.23"
  ∷ word (ἐ ∷ σ ∷ π ∷ ι ∷ ∙λ ∷ ω ∷ μ ∷ έ ∷ ν ∷ ο ∷ ν ∷ []) "Jude.1.23"
  ∷ word (χ ∷ ι ∷ τ ∷ ῶ ∷ ν ∷ α ∷ []) "Jude.1.23"
  ∷ word (Τ ∷ ῷ ∷ []) "Jude.1.24"
  ∷ word (δ ∷ ὲ ∷ []) "Jude.1.24"
  ∷ word (δ ∷ υ ∷ ν ∷ α ∷ μ ∷ έ ∷ ν ∷ ῳ ∷ []) "Jude.1.24"
  ∷ word (φ ∷ υ ∷ ∙λ ∷ ά ∷ ξ ∷ α ∷ ι ∷ []) "Jude.1.24"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "Jude.1.24"
  ∷ word (ἀ ∷ π ∷ τ ∷ α ∷ ί ∷ σ ∷ τ ∷ ο ∷ υ ∷ ς ∷ []) "Jude.1.24"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.24"
  ∷ word (σ ∷ τ ∷ ῆ ∷ σ ∷ α ∷ ι ∷ []) "Jude.1.24"
  ∷ word (κ ∷ α ∷ τ ∷ ε ∷ ν ∷ ώ ∷ π ∷ ι ∷ ο ∷ ν ∷ []) "Jude.1.24"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "Jude.1.24"
  ∷ word (δ ∷ ό ∷ ξ ∷ η ∷ ς ∷ []) "Jude.1.24"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "Jude.1.24"
  ∷ word (ἀ ∷ μ ∷ ώ ∷ μ ∷ ο ∷ υ ∷ ς ∷ []) "Jude.1.24"
  ∷ word (ἐ ∷ ν ∷ []) "Jude.1.24"
  ∷ word (ἀ ∷ γ ∷ α ∷ ∙λ ∷ ∙λ ∷ ι ∷ ά ∷ σ ∷ ε ∷ ι ∷ []) "Jude.1.24"
  ∷ word (μ ∷ ό ∷ ν ∷ ῳ ∷ []) "Jude.1.25"
  ∷ word (θ ∷ ε ∷ ῷ ∷ []) "Jude.1.25"
  ∷ word (σ ∷ ω ∷ τ ∷ ῆ ∷ ρ ∷ ι ∷ []) "Jude.1.25"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "Jude.1.25"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "Jude.1.25"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "Jude.1.25"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "Jude.1.25"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Jude.1.25"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "Jude.1.25"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "Jude.1.25"
  ∷ word (δ ∷ ό ∷ ξ ∷ α ∷ []) "Jude.1.25"
  ∷ word (μ ∷ ε ∷ γ ∷ α ∷ ∙λ ∷ ω ∷ σ ∷ ύ ∷ ν ∷ η ∷ []) "Jude.1.25"
  ∷ word (κ ∷ ρ ∷ ά ∷ τ ∷ ο ∷ ς ∷ []) "Jude.1.25"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.25"
  ∷ word (ἐ ∷ ξ ∷ ο ∷ υ ∷ σ ∷ ί ∷ α ∷ []) "Jude.1.25"
  ∷ word (π ∷ ρ ∷ ὸ ∷ []) "Jude.1.25"
  ∷ word (π ∷ α ∷ ν ∷ τ ∷ ὸ ∷ ς ∷ []) "Jude.1.25"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Jude.1.25"
  ∷ word (α ∷ ἰ ∷ ῶ ∷ ν ∷ ο ∷ ς ∷ []) "Jude.1.25"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.25"
  ∷ word (ν ∷ ῦ ∷ ν ∷ []) "Jude.1.25"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Jude.1.25"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "Jude.1.25"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ α ∷ ς ∷ []) "Jude.1.25"
  ∷ word (τ ∷ ο ∷ ὺ ∷ ς ∷ []) "Jude.1.25"
  ∷ word (α ∷ ἰ ∷ ῶ ∷ ν ∷ α ∷ ς ∷ []) "Jude.1.25"
  ∷ word (ἀ ∷ μ ∷ ή ∷ ν ∷ []) "Jude.1.25"
  ∷ []

ext: agda

max_stars_repo_name: scott-fleischman/GreekGrammar

max_issues_repo_name: scott-fleischman/GreekGrammar

max_forks_repo_name: scott-fleischman/GreekGrammar


text:
open import Level
import Categories.Category
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst; cong)

open import Syntax
open import Renaming
open import Substitution
open import Instantiation

module SyntaxMap where

  open Signature
  open Expression
  open Equality

  infix 5 _→ᵐ_

  -- syntax map

  _→ᵐ_ : Signature → Signature → Set
  𝕊 →ᵐ 𝕋 = ∀ {cl} (S : symb 𝕊 cl) → Expr 𝕋 (obj cl) (symb-arg 𝕊 S) 𝟘

  -- equality of syntax maps

  infix 4 _≈ᵐ_

  _≈ᵐ_ : ∀ {𝕊 𝕋} (f g : 𝕊 →ᵐ 𝕋) → Set
  _≈ᵐ_ {𝕊 = 𝕊} {𝕋 = 𝕋} f g =
    ∀ {cl} (S : symb 𝕊 cl) → f S ≈ g S

  -- equality is an equivalence relation

  ≈ᵐ-refl : ∀ {𝕊 𝕋} {f : 𝕊 →ᵐ 𝕋} → f ≈ᵐ f
  ≈ᵐ-refl {𝕋 = 𝕋} S = ≈-refl

  ≈ᵐ-sym : ∀ {𝕊 𝕋} {f g : 𝕊 →ᵐ 𝕋} → f ≈ᵐ g → g ≈ᵐ f
  ≈ᵐ-sym {𝕋 = 𝕋} ξ S = ≈-sym (ξ S)

  ≈ᵐ-trans : ∀ {𝕊 𝕋} {f g h : 𝕊 →ᵐ 𝕋} → f ≈ᵐ g → g ≈ᵐ h → f ≈ᵐ h
  ≈ᵐ-trans {𝕋 = 𝕋} ζ ξ S = ≈-trans (ζ S) (ξ S)

  -- The identity raw syntax map

  𝟙ᵐ : ∀ {𝕊} → (𝕊 →ᵐ 𝕊)
  𝟙ᵐ {𝕊} S = expr-symb S (expr-meta-generic 𝕊)

  -- Action of a raw syntax map

  infixr 10 [_]ᵐ_

  [_]ᵐ_ : ∀ {𝕊 𝕋} → (𝕊 →ᵐ 𝕋) → ∀ {cl 𝕄 γ} → Expr 𝕊 𝕄 cl γ → Expr 𝕋 𝕄 cl γ
  [ f ]ᵐ (expr-var x) = expr-var x
  [_]ᵐ_ {𝕋 = 𝕋} f {𝕄 = 𝕄} (expr-symb S es) =
    [ (λ M → [ f ]ᵐ es M) ]ⁱ ([ 𝟘-initial ]ʳ f S)
  [ f ]ᵐ (expr-meta M ts) = expr-meta M (λ i → [ f ]ᵐ (ts i))
  [ f ]ᵐ expr-eqty = expr-eqty
  [ f ]ᵐ expr-eqtm = expr-eqtm

  -- Action preserves equality

  []ᵐ-resp-≈ : ∀ {𝕊 𝕋} {cl 𝕄 γ} (f : 𝕊 →ᵐ 𝕋) {t u : Expr 𝕊 𝕄 cl γ} →
               t ≈ u → [ f ]ᵐ t ≈ [ f ]ᵐ u
  []ᵐ-resp-≈ f (≈-≡ ξ) = ≈-≡ (cong ([ f ]ᵐ_) ξ)
  []ᵐ-resp-≈ {𝕋 = 𝕋} f (≈-symb {S = S} ξ) =
    []ⁱ-resp-≈ⁱ ([ 𝟘-initial ]ʳ f S) λ M → []ᵐ-resp-≈ f (ξ M)
  []ᵐ-resp-≈ f (≈-meta ξ) = ≈-meta (λ i → []ᵐ-resp-≈ f (ξ i))

  []ᵐ-resp-≈ᵐ : ∀ {𝕊 𝕋} {cl 𝕄 γ} {f g : 𝕊 →ᵐ 𝕋} (t : Expr 𝕊 𝕄 cl γ) →
               f ≈ᵐ g → [ f ]ᵐ t ≈ [ g ]ᵐ t
  []ᵐ-resp-≈ᵐ (expr-var x) ξ = ≈-refl
  []ᵐ-resp-≈ᵐ {f = f} {g = g} (expr-symb S es) ξ =
     []ⁱ-resp-≈ⁱ-≈ {I = λ M → [ f ]ᵐ es M} {J = λ M → [ g ]ᵐ es M}
       (λ M → []ᵐ-resp-≈ᵐ (es M) ξ)
       ([]ʳ-resp-≈ 𝟘-initial (ξ S))
  []ᵐ-resp-≈ᵐ (expr-meta M ts) ξ = ≈-meta (λ i → []ᵐ-resp-≈ᵐ (ts i) ξ)
  []ᵐ-resp-≈ᵐ expr-eqty ξ = ≈-eqty
  []ᵐ-resp-≈ᵐ expr-eqtm ξ = ≈-eqtm

  []ᵐ-resp-≈ᵐ-≈ : ∀ {𝕊 𝕋} {cl 𝕄 γ} {f g : 𝕊 →ᵐ 𝕋} {t u : Expr 𝕊 𝕄 cl γ} →
                  f ≈ᵐ g → t ≈ u → [ f ]ᵐ t ≈ [ g ]ᵐ u
  []ᵐ-resp-≈ᵐ-≈ {g = g} {t = t} ζ ξ = ≈-trans ([]ᵐ-resp-≈ᵐ t ζ) ([]ᵐ-resp-≈ g ξ)

  -- Composition of raw syntax maps

  infixl 7 _∘ᵐ_

  _∘ᵐ_ : ∀ {𝕊 𝕋 𝕌} → (𝕋 →ᵐ 𝕌) → (𝕊 →ᵐ 𝕋) → (𝕊 →ᵐ 𝕌)
  (g ∘ᵐ f) S =  [ g ]ᵐ (f S)

  -- Action preserves identity
  module _ {𝕊} where
    open Equality
    open Renaming
    open Substitution

    [𝟙ᵐ] : ∀ {cl 𝕄 γ} (t : Expr 𝕊 cl 𝕄 γ) → [ 𝟙ᵐ ]ᵐ t ≈ t
    [𝟙ᵐ] (expr-var x) = ≈-refl
    [𝟙ᵐ] (expr-symb S es) =
      ≈-symb (λ {cⁱ γⁱ} i → [𝟙ᵐ]-arg cⁱ γⁱ i)
        where [𝟙ᵐ]-arg : ∀ cⁱ γⁱ (i : [ cⁱ , γⁱ ]∈ symb-arg 𝕊 S) → _
              [𝟙ᵐ]-arg (obj x) γⁱ i =
                ≈-trans
                  ([]ˢ-resp-≈ _ ([]ʳ-resp-≈ _ ([𝟙ᵐ] (es i))))
                  (≈-trans (≈-sym ([ˢ∘ʳ] (es i))) ([]ˢ-id (λ { (var-left _) → ≈-refl ; (var-right _) → ≈-refl })))
              [𝟙ᵐ]-arg EqTy γⁱ i = ≈-eqty
              [𝟙ᵐ]-arg EqTm γⁱ i = ≈-eqtm
    [𝟙ᵐ] (expr-meta M ts) = ≈-meta λ i → [𝟙ᵐ] (ts i)
    [𝟙ᵐ] expr-eqty = ≈-eqty
    [𝟙ᵐ] expr-eqtm = ≈-eqtm

  -- interaction of maps with instantiation and substitution
  module _ {𝕊 𝕋} where
    open Substitution

    infixl 7 _ᵐ∘ˢ_
    _ᵐ∘ˢ_ : ∀ {𝕊 𝕋} {𝕄 γ δ} (f : 𝕊 →ᵐ 𝕋) (σ : 𝕊 % 𝕄 ∥ γ →ˢ δ) → (𝕋 % 𝕄 ∥ γ →ˢ δ)
    (f ᵐ∘ˢ σ) x = [ f ]ᵐ σ x

    []ᵐ-[]ʳ : ∀ {f : 𝕊 →ᵐ 𝕋} {cl 𝕄 γ δ} {ρ : γ →ʳ δ} (t : Expr 𝕊 cl 𝕄 γ) →
              ([ f ]ᵐ ([ ρ ]ʳ t)) ≈ ([ ρ ]ʳ [ f ]ᵐ t)
    []ᵐ-[]ʳ (expr-var x) = ≈-refl
    []ᵐ-[]ʳ {f = f} {ρ = ρ} (expr-symb S es) =
      ≈-trans
        ([]ⁱ-resp-≈ⁱ ([ 𝟘-initial ]ʳ f S) λ M → []ᵐ-[]ʳ (es M))
        (≈-trans
           ([]ⁱ-resp-≈ⁱ-≈
              {t = [ 𝟘-initial ]ʳ f S}
              {u = [ ρ ]ʳ ([ 𝟘-initial ]ʳ f S)}
              (λ M → ≈-refl)
              (≈-trans ([]ʳ-resp-≡ʳ (f S) (λ {()})) ([∘ʳ] (f S))))
           (≈-sym ([ʳ∘ⁱ] ([ 𝟘-initial ]ʳ f S))))
    []ᵐ-[]ʳ (expr-meta M ts) = ≈-meta (λ i → []ᵐ-[]ʳ (ts i))
    []ᵐ-[]ʳ expr-eqty = ≈-eqty
    []ᵐ-[]ʳ expr-eqtm = ≈-eqtm

    []ᵐ-[]ˢ : ∀ {cl 𝕄 γ δ} {f : 𝕊 →ᵐ 𝕋} {σ : 𝕊 % 𝕄 ∥ γ →ˢ δ} (t : Expr 𝕊 cl 𝕄 γ) →
              [ f ]ᵐ ([ σ ]ˢ t) ≈ [ f ᵐ∘ˢ σ ]ˢ [ f ]ᵐ t
    []ᵐ-[]ˢ (expr-var x) = ≈-refl
    []ᵐ-[]ˢ {f = f} {σ = σ} (expr-symb S es) =
      ≈-trans
        ([]ⁱ-resp-≈ⁱ ([ 𝟘-initial ]ʳ f S) (λ M → []ᵐ-[]ˢ (es M)))
        (≈-trans
           ([]ⁱ-resp-≈ⁱ
              ([ 𝟘-initial ]ʳ f S)
              (λ M → []ˢ-resp-≈ˢ
                       (λ { (var-left x) → []ᵐ-[]ʳ (σ x)
                          ; (var-right _) → ≈-refl})
                       ([ f ]ᵐ es M)))
           (≈-sym ([]ˢ-[]ⁱ {ρ = 𝟘-initial} (f S) λ {()})))
    []ᵐ-[]ˢ (expr-meta M ts) = ≈-meta (λ i → []ᵐ-[]ˢ (ts i))
    []ᵐ-[]ˢ expr-eqty = ≈-eqty
    []ᵐ-[]ˢ expr-eqtm = ≈-eqtm

    infixl 7 _ᵐ∘ⁱ_
    _ᵐ∘ⁱ_ : ∀ {𝕂 𝕄 γ} (f : 𝕊 →ᵐ 𝕋) (I : 𝕊 % 𝕂 →ⁱ 𝕄 ∥ γ) → 𝕋 % 𝕂 →ⁱ 𝕄 ∥ γ
    (f ᵐ∘ⁱ I) M =  [ f ]ᵐ I M

    ⇑ⁱ-resp-ᵐ∘ⁱ : ∀ {𝕂 𝕄 γ δ} {f : 𝕊 →ᵐ 𝕋} {I : 𝕊 % 𝕂 →ⁱ 𝕄 ∥ γ} →
                  ⇑ⁱ {δ = δ} (f ᵐ∘ⁱ I) ≈ⁱ f ᵐ∘ⁱ ⇑ⁱ I
    ⇑ⁱ-resp-ᵐ∘ⁱ {I = I} M = ≈-sym ([]ᵐ-[]ʳ (I M))

    []ᵐ-[]ⁱ : ∀ {cl 𝕂 𝕄 γ} {f : 𝕊 →ᵐ 𝕋} {I : 𝕊 % 𝕂 →ⁱ 𝕄 ∥ γ} (t : Expr 𝕊 cl 𝕂 γ) →
              [ f ]ᵐ ([ I ]ⁱ t) ≈ [ f ᵐ∘ⁱ I ]ⁱ [ f ]ᵐ t
    []ᵐ-[]ⁱ (expr-var x) = ≈-refl
    []ᵐ-[]ⁱ {f = f} {I = I} (expr-symb S es) =
      ≈-trans
        ([]ⁱ-resp-≈ⁱ
           ([ 𝟘-initial ]ʳ f S)
           λ M → ≈-trans
                   ([]ᵐ-[]ⁱ (es M))
                   ([]ⁱ-resp-≈ⁱ ([ f ]ᵐ es M) (≈ⁱ-sym (⇑ⁱ-resp-ᵐ∘ⁱ {I = I}))))
        ([∘ⁱ] ([ 𝟘-initial ]ʳ f S))
    []ᵐ-[]ⁱ {f = f} {I = I} (expr-meta M ts) =
      ≈-trans
        ([]ᵐ-[]ˢ (I M))
        ([]ˢ-resp-≈ˢ (λ { (var-left _) → ≈-refl ; (var-right x) → []ᵐ-[]ⁱ (ts x)}) ([ f ]ᵐ I M))
    []ᵐ-[]ⁱ expr-eqty = ≈-eqty
    []ᵐ-[]ⁱ expr-eqtm = ≈-eqtm

  -- idenity is right-neutral

  []ᵐ-meta-generic : ∀ {𝕊 𝕋} {𝕄 γ} {f : 𝕊 →ᵐ 𝕋} {clᴹ γᴹ} {M : [ clᴹ , γᴹ ]∈ 𝕄} →
                     [ f ]ᵐ (expr-meta-generic 𝕊 {γ = γ} M) ≈ expr-meta-generic 𝕋 M
  []ᵐ-meta-generic {clᴹ = obj _} = ≈-refl
  []ᵐ-meta-generic {clᴹ = EqTy} = ≈-eqty
  []ᵐ-meta-generic {clᴹ = EqTm} = ≈-eqtm

  𝟙ᵐ-right : ∀ {𝕊 𝕋} {f : 𝕊 →ᵐ 𝕋} → f ∘ᵐ 𝟙ᵐ ≈ᵐ f
  𝟙ᵐ-right {f = f} S =
    ≈-trans
      ([]ⁱ-resp-≈ⁱ ([ 𝟘-initial ]ʳ (f S)) λ M → []ᵐ-meta-generic {M = M})
      (≈-trans ([𝟙ⁱ] ([ 𝟘-initial ]ʳ f S)) ([]ʳ-id (λ { ()})))

  -- Action preserves composition

  module _ {𝕊 𝕋 𝕌} where
    [∘ᵐ] : ∀ {f : 𝕊 →ᵐ 𝕋} {g : 𝕋 →ᵐ 𝕌} {cl 𝕄 γ} (t : Expr 𝕊 cl 𝕄 γ) → [ g ∘ᵐ f ]ᵐ t ≈ [ g ]ᵐ [ f ]ᵐ t
    [∘ᵐ] (expr-var x) = ≈-refl
    [∘ᵐ] {f = f} {g = g} (expr-symb S es) =
      ≈-trans
        ([]ⁱ-resp-≈ⁱ-≈ (λ M → [∘ᵐ] (es M)) (≈-sym ([]ᵐ-[]ʳ (f S))))
        (≈-sym ([]ᵐ-[]ⁱ ([ 𝟘-initial ]ʳ f S)))
    [∘ᵐ] (expr-meta M ts) = ≈-meta (λ i → [∘ᵐ] (ts i))
    [∘ᵐ] expr-eqty = ≈-eqty
    [∘ᵐ] expr-eqtm = ≈-eqtm

  -- Associativity of composition

  assocᵐ : ∀ {𝕊 𝕋 𝕌 𝕍} {f : 𝕊 →ᵐ 𝕋} {g : 𝕋 →ᵐ 𝕌} {h : 𝕌 →ᵐ 𝕍} →
           (h ∘ᵐ g) ∘ᵐ f ≈ᵐ h ∘ᵐ (g ∘ᵐ f)
  assocᵐ {f = f} S = [∘ᵐ] (f S)

  -- The category of signatures and syntax maps

  module _ where

   open Categories.Category

   SyntaxMaps : Category (suc zero) zero zero
   SyntaxMaps =
     record
       { Obj = Signature
       ; _⇒_ = _→ᵐ_
       ; _≈_ = _≈ᵐ_
       ; id = 𝟙ᵐ
       ; _∘_ = _∘ᵐ_
       ; assoc = λ {_} {_} {_} {_} {f} {_} {_} {_} S → [∘ᵐ] (f S)
       ; sym-assoc = λ {_} {_} {_} {𝕍} {f} {_} {_} {_} S → ≈-sym ([∘ᵐ] (f S))
       ; identityˡ = λ S → [𝟙ᵐ] _
       ; identityʳ = λ {_} {_} {f} {_} → 𝟙ᵐ-right {f = f}
       ; identity² = λ _ → [𝟙ᵐ] _
       ; equiv = record { refl = λ _ → ≈-refl ; sym = ≈ᵐ-sym ; trans = ≈ᵐ-trans }
       ; ∘-resp-≈ = λ ζ ξ S → []ᵐ-resp-≈ᵐ-≈ ζ (ξ S)
       }


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

module Categories.Object.BinaryCoproducts {o ℓ e} (C : Category o ℓ e) where

open Category C
open Equiv

open import Level

import Categories.Object.Coproduct as Coproduct
open import Categories.Morphisms C

open module CP = Coproduct C hiding (module BinCoproducts)
open CP public using (BinCoproducts)

record BinaryCoproducts : Set (o ⊔ ℓ ⊔ e) where
  infix 10 _⧻_

  field
    coproduct : ∀ {A B} → Coproduct A B

  _∐_ : Obj → Obj → Obj
  A ∐ B = Coproduct.A+B (coproduct {A} {B})

  ∐-comm : ∀ {A B} → _≅_ (A ∐ B) (B ∐ A)
  ∐-comm = Commutative coproduct coproduct

  ∐-assoc : ∀ {X Y Z} → _≅_ (X ∐ (Y ∐ Z)) ((X ∐ Y) ∐ Z)
  ∐-assoc = Associative coproduct coproduct coproduct coproduct

  -- Convenience!
  i₁ : {A B : Obj} → (A ⇒ (A ∐ B))
  i₁ = Coproduct.i₁ coproduct

  i₂ : {A B : Obj} → (B ⇒ (A ∐ B))
  i₂ = Coproduct.i₂ coproduct

  [_,_] : ∀ {A B Q} → (A ⇒ Q) → (B ⇒ Q) → ((A ∐ B) ⇒ Q)
  [_,_] = Coproduct.[_,_] coproduct

  .commute₁ : ∀ {A B C} {f : A ⇒ C} {g : B ⇒ C} → [ f , g ] ∘ i₁ ≡ f
  commute₁ = Coproduct.commute₁ coproduct

  .commute₂ : ∀ {A B C} {f : A ⇒ C} {g : B ⇒ C} → [ f , g ] ∘ i₂ ≡ g
  commute₂ = Coproduct.commute₂ coproduct

  .universal : ∀ {A B C} {f : A ⇒ C} {g : B ⇒ C} {i : (A ∐ B) ⇒ C}
               → i ∘ i₁ ≡ f → i ∘ i₂ ≡ g → [ f , g ] ≡ i
  universal = Coproduct.universal coproduct

  assocˡ : ∀ {A B C} → (((A ∐ B) ∐ C) ⇒ (A ∐ (B ∐ C)))
  assocˡ = _≅_.g ∐-assoc

  assocʳ : ∀ {A B C} → ((A ∐ (B ∐ C)) ⇒ ((A ∐ B) ∐ C))
  assocʳ = _≅_.f ∐-assoc

  .g-η : ∀ {A B C} {f : (A ∐ B) ⇒ C} → [ f ∘ i₁ , f ∘ i₂ ] ≡ f
  g-η = Coproduct.g-η coproduct

  .η : ∀ {A B} → [ i₁ , i₂ ] ≡ id {A ∐ B}
  η = Coproduct.η coproduct

  .[]-cong₂ : ∀ {A B C} → {f f′ : A ⇒ C} {g g′ : B ⇒ C} → f ≡ f′ → g ≡ g′ → [ f , g ] ≡ [ f′ , g′ ]
  []-cong₂ = Coproduct.[]-cong₂ coproduct

  -- If I _really_ wanted to, I could do this for a specific pair of coproducts like the rest above, but I'll write that one
  -- when I need it.
  _⧻_ : ∀ {A B C D} → (A ⇒ B) → (C ⇒ D) → ((A ∐ C) ⇒ (B ∐ D))
  f ⧻ g = [ i₁ ∘ f , i₂ ∘ g ]

  -- TODO: this is probably harder to use than necessary because of this definition. Maybe make a version
  -- that doesn't have an explicit id in it, too?
  left : ∀ {A B C} → (A ⇒ B) → ((A ∐ C) ⇒ (B ∐ C))
  left f = f ⧻ id

  right : ∀ {A C D} → (C ⇒ D) → ((A ∐ C) ⇒ (A ∐ D))
  right g = id ⧻ g

  -- Just to make this more obvious
  .⧻∘i₁ : ∀ {A B C D} → {f : A ⇒ B} → {g : C ⇒ D} → (f ⧻ g) ∘ i₁ ≡ i₁ ∘ f
  ⧻∘i₁ {f = f} {g} = commute₁

  .⧻∘i₂ : ∀ {A B C D} → {f : A ⇒ B} → {g : C ⇒ D} → (f ⧻ g) ∘ i₂ ≡ i₂ ∘ g
  ⧻∘i₂ {f = f} {g} = commute₂

  .[]∘⧻ : ∀ {A B C D E} → {f : B ⇒ E} {f′ : A ⇒ B} {g : D ⇒ E} {g′ : C ⇒ D} → [ f , g ] ∘ ( f′ ⧻ g′ ) ≡ [ f ∘ f′ , g ∘ g′ ]
  []∘⧻ {f = f} {f′} {g} {g′} = sym (universal helper₁ helper₂)
    where
    helper₁ : ([ f , g ] ∘ (f′ ⧻ g′)) ∘ i₁ ≡ f ∘ f′
    helper₁ =
      begin
        ([ f , g ] ∘ (f′ ⧻ g′)) ∘ i₁
      ↓⟨ assoc ⟩
        [ f , g ] ∘ ((f′ ⧻ g′) ∘ i₁)
      ↓⟨ ∘-resp-≡ʳ ⧻∘i₁ ⟩
        [ f , g ] ∘ (i₁ ∘ f′)
      ↑⟨ assoc ⟩
        ([ f , g ] ∘ i₁) ∘ f′
      ↓⟨ ∘-resp-≡ˡ commute₁ ⟩
        f ∘ f′
      ∎
      where
      open HomReasoning

    helper₂ : ([ f , g ] ∘ (f′ ⧻ g′)) ∘ i₂ ≡ g ∘ g′
    helper₂ =
      begin
        ([ f , g ] ∘ (f′ ⧻ g′)) ∘ i₂
      ↓⟨ assoc ⟩
        [ f , g ] ∘ ((f′ ⧻ g′) ∘ i₂)
      ↓⟨ ∘-resp-≡ʳ ⧻∘i₂ ⟩
        [ f , g ] ∘ (i₂ ∘ g′)
      ↑⟨ assoc ⟩
        ([ f , g ] ∘ i₂) ∘ g′
      ↓⟨ ∘-resp-≡ˡ commute₂ ⟩
        g ∘ g′
      ∎
      where
      open HomReasoning

  .[]∘left : ∀ {A B C D} → {f : C ⇒ B} {f′ : B ⇒ A} {g′ : D ⇒ A} → [ f′ , g′ ] ∘ left f ≡ [ f′ ∘ f , g′ ]
  []∘left {f = f} {f′} {g′} =
    begin
      [ f′ , g′ ] ∘ left f
    ↓⟨ []∘⧻ ⟩
      [ f′ ∘ f , g′ ∘ id ]
    ↓⟨ []-cong₂ refl identityʳ ⟩
      [ f′ ∘ f , g′ ]
    ∎
    where
    open HomReasoning

  .[]∘right : ∀ {A B D E} → {f′ : B ⇒ A} {g : E ⇒ D} {g′ : D ⇒ A} → [ f′ , g′ ] ∘ right g ≡ [ f′ , g′ ∘ g ]
  []∘right {f′ = f′} {g} {g′} =
    begin
      [ f′ , g′ ] ∘ right g
    ↓⟨ []∘⧻ ⟩
      [ f′ ∘ id , g′ ∘ g ]
    ↓⟨ []-cong₂ identityʳ refl ⟩
      [ f′ , g′ ∘ g ]
    ∎
    where
    open HomReasoning

  .⧻∘⧻ : ∀ {A B C D E F} → {f : B ⇒ C} → {f′ : A ⇒ B} {g : E ⇒ F} {g′ : D ⇒ E} → (f ⧻ g) ∘ (f′ ⧻ g′) ≡ (f ∘ f′) ⧻ (g ∘ g′)
  ⧻∘⧻ {B = B} {E = E} {f = f} {f′} {g} {g′} =
    begin
      (f ⧻ g) ∘ (f′ ⧻ g′)
    ↓⟨ []∘⧻ ⟩
      [ (i₁ ∘ f) ∘ f′ , (i₂ ∘ g) ∘ g′ ]
    ↓⟨ []-cong₂ assoc assoc ⟩
      (f ∘ f′) ⧻ (g ∘ g′)
    ∎
    where
    open HomReasoning

  .∘[] : ∀ {A B C D} {f : B ⇒ A} {g : C ⇒ A} {q : A ⇒ D} → q ∘ [ f , g ] ≡ [ q ∘ f , q ∘ g ]
  ∘[] = sym (universal (trans assoc (∘-resp-≡ʳ commute₁)) (trans assoc (∘-resp-≡ʳ commute₂)))

Bin→Binary : BinCoproducts -> BinaryCoproducts
Bin→Binary bc = record { coproduct = λ {A} {B} → record {
                                               A+B = A + B;
                                               i₁ = i₁;
                                               i₂ = i₂;
                                               [_,_] = [_,_];
                                               commute₁ = commute₁;
                                               commute₂ = commute₂;
                                               universal = universal } }
  where
    open CP.BinCoproducts bc

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
-- Andreas, 2014-12-02, issue reported by Jesper Cockx

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

subst : ∀ (A : Set)(P : A → Set)(x y : A) → x ≡ y → P x → P y
subst A P x .x refl t = t

mutual
  Type : Set
  postulate
    type : Type
    Term : Type → Set

  Type = Term type

mutual
  weakenType : Type → Type → Type
  weaken : (ty ty' : Type) → Term ty → Term (weakenType ty' ty)

  weakenType ty ty' =
    let X : Type
        X = {!!}
    in  subst Type Term (weakenType X type) type {!!} (weaken type X ty)
  weaken ty ty' t = {!!}

data Test : Type → Set where
  test : Test (weakenType type type)

-- Checking the constructor declaration was looping
-- should work now.

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
------------------------------------------------------------------------
-- Half adjoint equivalences
------------------------------------------------------------------------

-- This development is partly based on the presentation of half
-- adjoint equivalences in the HoTT book, and partly based on
-- Voevodsky's work on univalent foundations.

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

open import Equality

module Equivalence.Half-adjoint
  {e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where

open Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection eq as B using (_↔_)
import Equivalence.Contractible-preimages eq as CP
open import H-level eq as H-level
open import H-level.Closure eq
open import Preimage eq as Preimage using (_⁻¹_)
open import Surjection eq as S hiding (id; _∘_)

private
  variable
    a b p q : Level
    A B C   : Type a
    P       : A → Type p
    Q       : (x : A) → P x → Type q
    f g     : A → B
    A↔B     : A ↔ B

------------------------------------------------------------------------
-- The definition of Is-equivalence

mutual

  -- Is-equivalence f means that f is a half adjoint equivalence.

  Is-equivalence :
    {A : Type a} {B : Type b} →
    (A → B) → Type (a ⊔ b)
  Is-equivalence {A = A} {B = B} f =
    ∃ λ (f⁻¹ : B → A) → Proofs f f⁻¹

  -- The "proofs" contained in Is-equivalence f.

  Proofs :
    {A : Type a} {B : Type b} →
    (A → B) → (B → A) → Type (a ⊔ b)
  Proofs f f⁻¹ =
    ∃ λ (f-f⁻¹ : ∀ x → f (f⁻¹ x) ≡ x) →
    ∃ λ (f⁻¹-f : ∀ x → f⁻¹ (f x) ≡ x) →
      ∀ x → cong f (f⁻¹-f x) ≡ f-f⁻¹ (f x)

-- Some projections.

inverse :
  {@0 A : Type a} {@0 B : Type b} {@0 f : A → B} →
  Is-equivalence f → B → A
inverse = proj₁

right-inverse-of :
  {@0 A : Type a} {@0 B : Type b} {@0 f : A → B} →
  (eq : Is-equivalence f) →
  ∀ x → f (inverse eq x) ≡ x
right-inverse-of = proj₁ ∘ proj₂

left-inverse-of :
  {@0 A : Type a} {@0 B : Type b} {@0 f : A → B} →
  (eq : Is-equivalence f) →
  ∀ x → inverse eq (f x) ≡ x
left-inverse-of = proj₁ ∘ proj₂ ∘ proj₂

------------------------------------------------------------------------
-- Identity, inverse, composition

-- The identity function is an equivalence.

id-equivalence : Is-equivalence (id {A = A})
id-equivalence =
    id
  , refl
  , refl
  , (λ x →
       cong id (refl x)  ≡⟨ sym $ cong-id _ ⟩∎
       refl x            ∎)

-- If f is an equivalence, then its inverse is also an equivalence.

inverse-equivalence :
  (eq : Is-equivalence f) → Is-equivalence (inverse eq)
inverse-equivalence {f = f} (f⁻¹ , f-f⁻¹ , f⁻¹-f , f-f⁻¹-f) =
  f , f⁻¹-f , f-f⁻¹ , f⁻¹-f-f⁻¹
  where

  abstract

    f⁻¹-f-f⁻¹ : ∀ x → cong f⁻¹ (f-f⁻¹ x) ≡ f⁻¹-f (f⁻¹ x)
    f⁻¹-f-f⁻¹ x = subst
      (λ x → cong f⁻¹ (f-f⁻¹ x) ≡ f⁻¹-f (f⁻¹ x))
      (f-f⁻¹ x)
      (cong f⁻¹ (f-f⁻¹ (f (f⁻¹ x)))       ≡⟨ cong (cong f⁻¹) $ sym $ f-f⁻¹-f _ ⟩

       cong f⁻¹ (cong f (f⁻¹-f (f⁻¹ x)))  ≡⟨ cong-∘ f⁻¹ f _ ⟩

       cong (f⁻¹ ∘ f) (f⁻¹-f (f⁻¹ x))     ≡⟨ cong-≡id-≡-≡id f⁻¹-f ⟩∎

       f⁻¹-f (f⁻¹ (f (f⁻¹ x)))            ∎)

-- If f and g are inverses, then f ∘ g is an equivalence.

composition-equivalence :
  Is-equivalence f → Is-equivalence g → Is-equivalence (f ∘ g)
composition-equivalence
  {f = f} {g = g}
  (f⁻¹ , f-f⁻¹ , f⁻¹-f , f-f⁻¹-f)
  (g⁻¹ , g-g⁻¹ , g⁻¹-g , g-g⁻¹-g) =
    [f-g]⁻¹
  , [f-g]-[f-g]⁻¹
  , [f-g]⁻¹-[f-g]
  , [f-g]-[f-g]⁻¹-[f-g]
  where
  [f-g] = f ∘ g

  [f-g]⁻¹ = g⁻¹ ∘ f⁻¹

  [f-g]-[f-g]⁻¹ = λ x →
    f (g (g⁻¹ (f⁻¹ x)))  ≡⟨ cong f $ g-g⁻¹ _ ⟩
    f (f⁻¹ x)            ≡⟨ f-f⁻¹ _ ⟩∎
    x                    ∎

  [f-g]⁻¹-[f-g] = λ x →
    g⁻¹ (f⁻¹ (f (g x)))  ≡⟨ cong g⁻¹ $ f⁻¹-f _ ⟩
    g⁻¹ (g x)            ≡⟨ g⁻¹-g _ ⟩∎
    x                    ∎

  abstract

    [f-g]-[f-g]⁻¹-[f-g] :
      ∀ x → cong [f-g] ([f-g]⁻¹-[f-g] x) ≡ [f-g]-[f-g]⁻¹ ([f-g] x)
    [f-g]-[f-g]⁻¹-[f-g] x =
      cong (f ∘ g) (trans (cong g⁻¹ (f⁻¹-f (g x))) (g⁻¹-g x))           ≡⟨ trans (sym $ cong-∘ _ _ _) $
                                                                           cong (cong _) $
                                                                           trans (cong-trans _ _ _) $
                                                                           cong (flip trans _) $
                                                                           cong-∘ _ _ _ ⟩
      cong f (trans (cong (g ∘ g⁻¹) (f⁻¹-f (g x))) (cong g (g⁻¹-g x)))  ≡⟨ cong (cong _) $ cong (trans _) $ g-g⁻¹-g _ ⟩
      cong f (trans (cong (g ∘ g⁻¹) (f⁻¹-f (g x))) (g-g⁻¹ (g x)))       ≡⟨ cong (cong f) $ naturality g-g⁻¹ ⟩
      cong f (trans (g-g⁻¹ (f⁻¹ (f (g x)))) (cong id (f⁻¹-f (g x))))    ≡⟨ cong (cong _) $ cong (trans _) $ sym $ cong-id _ ⟩
      cong f (trans (g-g⁻¹ (f⁻¹ (f (g x)))) (f⁻¹-f (g x)))              ≡⟨ cong-trans _ _ _ ⟩
      trans (cong f (g-g⁻¹ (f⁻¹ (f (g x))))) (cong f (f⁻¹-f (g x)))     ≡⟨ cong (trans _) $ f-f⁻¹-f _ ⟩∎
      trans (cong f (g-g⁻¹ (f⁻¹ (f (g x))))) (f-f⁻¹ (f (g x)))          ∎

------------------------------------------------------------------------
-- Conversions to and from bijections

-- Equivalences are bijections (functions with quasi-inverses).

Is-equivalence→↔ :
  {@0 A : Type a} {@0 B : Type b} {f : A → B} →
  Is-equivalence f → A ↔ B
Is-equivalence→↔ {f = f} (f⁻¹ , f-f⁻¹ , f⁻¹-f , _) = record
  { surjection = record
    { logical-equivalence = record
      { to   = f
      ; from = f⁻¹
      }
    ; right-inverse-of = f-f⁻¹
    }
  ; left-inverse-of = f⁻¹-f
  }

-- Functions with quasi-inverses are equivalences.
--
-- Note that the left inverse proof is preserved unchanged.

↔→Is-equivalenceˡ :
  (A↔B : A ↔ B) → Is-equivalence (_↔_.to A↔B)
↔→Is-equivalenceˡ A↔B =
    from
  , right-inverse-of′
  , A↔B.left-inverse-of
  , left-right
  where
  open module A↔B = _↔_ A↔B using (to; from)

  abstract

    right-inverse-of′ : ∀ x → to (from x) ≡ x
    right-inverse-of′ x =
      to (from x)              ≡⟨ sym (A↔B.right-inverse-of _) ⟩
      to (from (to (from x)))  ≡⟨ cong to (A↔B.left-inverse-of _) ⟩
      to (from x)              ≡⟨ A↔B.right-inverse-of _ ⟩∎
      x                        ∎

    left-right :
      ∀ x → cong to (A↔B.left-inverse-of x) ≡ right-inverse-of′ (to x)
    left-right x =
      let lemma =
            trans (A↔B.right-inverse-of _)
              (cong to (A↔B.left-inverse-of _))                         ≡⟨ cong (trans _) $
                                                                           cong-id _ ⟩
            trans (A↔B.right-inverse-of _)
              (cong id (cong to (A↔B.left-inverse-of _)))               ≡⟨ sym $ naturality A↔B.right-inverse-of ⟩

            trans (cong (to ∘ from) (cong to (A↔B.left-inverse-of _)))
              (A↔B.right-inverse-of _)                                  ≡⟨ cong (flip trans _) $
                                                                           cong-∘ _ _ _ ⟩
            trans (cong (to ∘ from ∘ to) (A↔B.left-inverse-of _))
              (A↔B.right-inverse-of _)                                  ≡⟨ cong (flip trans _) $ sym $
                                                                           cong-∘ _ _ _ ⟩
            trans (cong to (cong (from ∘ to) (A↔B.left-inverse-of _)))
              (A↔B.right-inverse-of _)                                  ≡⟨ cong (flip trans _ ∘ cong to) $
                                                                           cong-≡id-≡-≡id A↔B.left-inverse-of ⟩∎
            trans (cong to (A↔B.left-inverse-of _))
              (A↔B.right-inverse-of _)                                  ∎
      in
      cong to (A↔B.left-inverse-of x)             ≡⟨ sym $ trans-sym-[trans] _ _ ⟩

      trans (sym (A↔B.right-inverse-of _))
        (trans (A↔B.right-inverse-of _)
           (cong to (A↔B.left-inverse-of _)))     ≡⟨ cong (trans _) lemma ⟩∎

      trans (sym (A↔B.right-inverse-of _))
        (trans (cong to (A↔B.left-inverse-of _))
           (A↔B.right-inverse-of _))              ∎

_ : proj₁ (↔→Is-equivalenceˡ A↔B) ≡ _↔_.from A↔B
_ = refl _

_ :
  proj₁ (proj₂ (proj₂ (↔→Is-equivalenceˡ A↔B))) ≡
  _↔_.left-inverse-of A↔B
_ = refl _

-- Functions with quasi-inverses are equivalences.
--
-- Note that the right inverse proof is preserved unchanged.

↔→Is-equivalenceʳ :
  (A↔B : A ↔ B) → Is-equivalence (_↔_.to A↔B)
↔→Is-equivalenceʳ =
  inverse-equivalence ∘
  ↔→Is-equivalenceˡ ∘
  B.inverse

_ : proj₁ (↔→Is-equivalenceʳ A↔B) ≡ _↔_.from A↔B
_ = refl _

_ : proj₁ (proj₂ (↔→Is-equivalenceʳ A↔B)) ≡ _↔_.right-inverse-of A↔B
_ = refl _

------------------------------------------------------------------------
-- Is-equivalence is related to CP.Is-equivalence (part one)

-- Is-equivalence f and CP.Is-equivalence f are logically equivalent.

Is-equivalence⇔Is-equivalence-CP :
  Is-equivalence f ⇔ CP.Is-equivalence f
Is-equivalence⇔Is-equivalence-CP = record
  { to   = to
  ; from = from
  }
  where
  to : Is-equivalence f → CP.Is-equivalence f
  to {f = f} (f⁻¹ , f-f⁻¹ , f⁻¹-f , f-f⁻¹-f) y =
      (f⁻¹ y , f-f⁻¹ y)
    , λ (x , f-f⁻¹′) →
      Σ-≡,≡→≡
        (f⁻¹ y      ≡⟨ sym $ cong f⁻¹ f-f⁻¹′ ⟩
         f⁻¹ (f x)  ≡⟨ f⁻¹-f x ⟩∎
         x          ∎)
        (elim¹
           (λ {y} f-f⁻¹′ →
              subst (λ x → f x ≡ y)
                (trans (sym (cong f⁻¹ f-f⁻¹′)) (f⁻¹-f x))
                (f-f⁻¹ y) ≡
              f-f⁻¹′)
           (subst (λ x′ → f x′ ≡ f x)
              (trans (sym (cong f⁻¹ (refl _))) (f⁻¹-f x))
              (f-f⁻¹ (f x))                                    ≡⟨ cong (flip (subst _) _) $
                                                                  trans (cong (flip trans _) $
                                                                         trans (cong sym $ cong-refl _) $
                                                                         sym-refl) $
                                                                  trans-reflˡ _ ⟩

            subst (λ x′ → f x′ ≡ f x) (f⁻¹-f x) (f-f⁻¹ (f x))  ≡⟨ subst-∘ _ _ _ ⟩

            subst (_≡ f x) (cong f (f⁻¹-f x)) (f-f⁻¹ (f x))    ≡⟨ subst-trans-sym ⟩

            trans (sym (cong f (f⁻¹-f x))) (f-f⁻¹ (f x))       ≡⟨ cong (flip trans _ ∘ sym) $
                                                                  f-f⁻¹-f _ ⟩

            trans (sym (f-f⁻¹ (f x))) (f-f⁻¹ (f x))            ≡⟨ trans-symˡ _ ⟩∎

            refl _                                             ∎)
           f-f⁻¹′)

  from : CP.Is-equivalence f → Is-equivalence f
  from eq =
      CP.inverse eq
    , CP.right-inverse-of eq
    , CP.left-inverse-of eq
    , CP.left-right-lemma eq

-- All fibres of an equivalence over a given point are equal to a
-- given fibre.

irrelevance :
  (eq : Is-equivalence f) →
  ∀ y (p : f ⁻¹ y) → (inverse eq y , right-inverse-of eq y) ≡ p
irrelevance =
  CP.irrelevance ∘
  _⇔_.to Is-equivalence⇔Is-equivalence-CP

-- When proving that a function is an equivalence one can assume that
-- the codomain is inhabited.

[inhabited→Is-equivalence]→Is-equivalence :
  {f : A → B} →
  (B → Is-equivalence f) → Is-equivalence f
[inhabited→Is-equivalence]→Is-equivalence hyp =
  _⇔_.from Is-equivalence⇔Is-equivalence-CP $ λ x →
  _⇔_.to Is-equivalence⇔Is-equivalence-CP (hyp x) x

------------------------------------------------------------------------
-- The "inverse of extensionality" is an equivalence (assuming
-- extensionality)

-- Is-equivalence respects extensional equality.

respects-extensional-equality :
  (∀ x → f x ≡ g x) →
  Is-equivalence f → Is-equivalence g
respects-extensional-equality
  {f = f} {g = g} f≡g (f⁻¹ , f-f⁻¹ , f⁻¹-f , f-f⁻¹-f) =
  ↔→Is-equivalenceʳ (record
    { surjection = record
      { logical-equivalence = record
        { to   = g
        ; from = f⁻¹
        }
      ; right-inverse-of = λ x →
          g (f⁻¹ x)  ≡⟨ sym $ f≡g _ ⟩
          f (f⁻¹ x)  ≡⟨ f-f⁻¹ _ ⟩∎
          x          ∎
      }
    ; left-inverse-of = λ x →
        f⁻¹ (g x)  ≡⟨ cong f⁻¹ $ sym $ f≡g _ ⟩
        f⁻¹ (f x)  ≡⟨ f⁻¹-f _ ⟩∎
        x          ∎
    })

-- Functions between contractible types are equivalences.

function-between-contractible-types-is-equivalence :
  ∀ {a b} {A : Type a} {B : Type b} (f : A → B) →
  Contractible A → Contractible B → Is-equivalence f
function-between-contractible-types-is-equivalence f A-contr B-contr =
  ↔→Is-equivalenceˡ (record
    { surjection = record
      { logical-equivalence = record
        { from = λ _ → proj₁ A-contr
        }
      ; right-inverse-of = λ x →
          f (proj₁ A-contr)  ≡⟨ sym $ proj₂ B-contr _ ⟩
          proj₁ B-contr      ≡⟨ proj₂ B-contr _ ⟩∎
          x                  ∎
      }
    ; left-inverse-of = proj₂ A-contr
    })

abstract

  -- If Σ-map id f is an equivalence, then f is also an equivalence.

  drop-Σ-map-id :
    {A : Type a} {P : A → Type p} {Q : A → Type q}
    (f : ∀ {x} → P x → Q x) →
    Is-equivalence {A = Σ A P} {B = Σ A Q} (Σ-map id f) →
    ∀ x → Is-equivalence (f {x = x})
  drop-Σ-map-id f eq x =
    _⇔_.from Is-equivalence⇔Is-equivalence-CP $
    CP.drop-Σ-map-id f
      (_⇔_.to Is-equivalence⇔Is-equivalence-CP eq)
      x

  -- A "computation" rule for drop-Σ-map-id.

  inverse-drop-Σ-map-id :
    {A : Type a} {P : A → Type p} {Q : A → Type q}
    {f : ∀ {x} → P x → Q x} {x : A} {y : Q x}
    {eq : Is-equivalence {A = Σ A P} {B = Σ A Q} (Σ-map id f)} →
    inverse (drop-Σ-map-id f eq x) y ≡
    subst P (cong proj₁ (right-inverse-of eq (x , y)))
      (proj₂ (inverse eq (x , y)))
  inverse-drop-Σ-map-id = CP.inverse-drop-Σ-map-id

  -- The function ext⁻¹ is an equivalence (assuming extensionality).

  ext⁻¹-is-equivalence :
    ({P : A → Type b} → Extensionality′ A P) →
    {P : A → Type b} {f g : (x : A) → P x} →
    Is-equivalence (ext⁻¹ {f = f} {g = g})
  ext⁻¹-is-equivalence {A = A} ext {P = P} {f = f} {g = g} =
    drop-Σ-map-id ext⁻¹ lemma₂ f
    where
    surj :
      (∀ x → Singleton (g x)) ↠
      (∃ λ (f : (x : A) → P x) → ∀ x → f x ≡ g x)
    surj = record
      { logical-equivalence = record
        { to   = λ f → proj₁ ∘ f , proj₂ ∘ f
        ; from = λ p x → proj₁ p x , proj₂ p x
        }
      ; right-inverse-of = refl
      }

    lemma₁ : Contractible (∃ λ (f : (x : A) → P x) → ∀ x → f x ≡ g x)
    lemma₁ =
      H-level.respects-surjection surj 0 $
        _⇔_.from Π-closure-contractible⇔extensionality
          ext (singleton-contractible ∘ g)

    lemma₂ :
      Is-equivalence
        {A = ∃ λ f → f ≡ g}
        {B = ∃ λ f → ∀ x → f x ≡ g x}
        (Σ-map id ext⁻¹)
    lemma₂ = function-between-contractible-types-is-equivalence
               _ (singleton-contractible g) lemma₁

------------------------------------------------------------------------
-- Results related to h-levels

abstract

  -- Is-equivalence f is a proposition (assuming extensionality).

  propositional :
    {A : Type a} {B : Type b} →
    Extensionality (a ⊔ b) (a ⊔ b) →
    (f : A → B) → Is-proposition (Is-equivalence f)
  propositional {a = a} {b = b} {A = A} {B = B} ext f =
    [inhabited⇒+]⇒+ 0 λ eq →
    mono₁ 0 $
    H-level.respects-surjection
      ((∃ λ ((f⁻¹ , f-f⁻¹) : ∃ λ f⁻¹ → ∀ x → f (f⁻¹ x) ≡ x) →
        ∃ λ (f⁻¹-f : ∀ x → f⁻¹ (f x) ≡ x) →
            ∀ x → cong f (f⁻¹-f x) ≡ f-f⁻¹ (f x))              ↠⟨ _↔_.surjection $ B.inverse B.Σ-assoc ⟩□

       Is-equivalence f                                        □)
      0 $
    Σ-closure 0 (lemma₁ eq) (uncurry $ lemma₂ eq)
    where
    ext₁ : Extensionality b b
    ext₁ = lower-extensionality a a ext

    ext₁′ : Extensionality b a
    ext₁′ = lower-extensionality a b ext

    ext-↠ :
      {A B : Type b} {f g : A → B} →
      f ≡ g ↠ (∀ x → f x ≡ g x)
    ext-↠ =
      _↔_.surjection $
      Is-equivalence→↔ $
      ext⁻¹-is-equivalence (apply-ext ext₁)

    lemma₁ :
      Is-equivalence f →
      Contractible (∃ λ (f⁻¹ : B → A) → ∀ x → f (f⁻¹ x) ≡ x)
    lemma₁ (f⁻¹ , f-f⁻¹ , f⁻¹-f , f-f⁻¹-f) =
      H-level.respects-surjection
        ((∃ λ f⁻¹ → f ∘ f⁻¹ ≡ id)         ↠⟨ (∃-cong λ _ → ext-↠) ⟩□
         (∃ λ f⁻¹ → ∀ x → f (f⁻¹ x) ≡ x)  □)
        0 $
      Preimage.bijection⁻¹-contractible
        (record
           { surjection = record
             { logical-equivalence = record
               { to   = f   ∘_
               ; from = f⁻¹ ∘_
               }
             ; right-inverse-of = λ g → apply-ext ext₁ λ x →
                 f (f⁻¹ (g x))  ≡⟨ f-f⁻¹ (g x) ⟩∎
                 g x            ∎
             }
           ; left-inverse-of = λ g → apply-ext ext₁′ λ x →
               f⁻¹ (f (g x))  ≡⟨ f⁻¹-f (g x) ⟩∎
               g x            ∎
           })
        id

    ext₂ : Extensionality a (a ⊔ b)
    ext₂ = lower-extensionality b lzero ext

    lemma₂ :
      Is-equivalence f →
      (f⁻¹ : B → A) (f-f⁻¹ : ∀ x → f (f⁻¹ x) ≡ x) →
      Contractible
        (∃ λ (f⁻¹-f : ∀ x → f⁻¹ (f x) ≡ x) →
           ∀ x → cong f (f⁻¹-f x) ≡ f-f⁻¹ (f x))
    lemma₂ eq f⁻¹ f-f⁻¹ =
      H-level.respects-surjection
        ((∀ x → (f⁻¹ (f x) , f-f⁻¹ (f x)) ≡ (x , refl (f x)))             ↠⟨ (∀-cong ext₂ λ _ → _↔_.surjection $ B.inverse B.Σ-≡,≡↔≡) ⟩

         (∀ x → ∃ λ f⁻¹-f →
                  subst (λ y → f y ≡ f x) f⁻¹-f (f-f⁻¹ (f x)) ≡
                  refl (f x))                                             ↠⟨ (∀-cong ext₂ λ x → ∃-cong λ f⁻¹-f →
                                                                              elim (λ {A B} _ → A ↠ B) (λ _ → S.id) (

             subst (λ y → f y ≡ f x) f⁻¹-f (f-f⁻¹ (f x)) ≡ refl (f x)           ≡⟨ cong (_≡ _) $ subst-∘ _ _ _ ⟩
             subst (_≡ f x) (cong f f⁻¹-f) (f-f⁻¹ (f x)) ≡ refl (f x)           ≡⟨ cong (_≡ _) subst-trans-sym ⟩
             trans (sym (cong f f⁻¹-f)) (f-f⁻¹ (f x)) ≡ refl (f x)              ≡⟨ [trans≡]≡[≡trans-symˡ] _ _ _ ⟩
             f-f⁻¹ (f x) ≡ trans (sym (sym (cong f f⁻¹-f))) (refl (f x))        ≡⟨ cong (_ ≡_) $ trans-reflʳ _ ⟩
             f-f⁻¹ (f x) ≡ sym (sym (cong f f⁻¹-f))                             ≡⟨ cong (_ ≡_) $ sym-sym _ ⟩∎
             f-f⁻¹ (f x) ≡ cong f f⁻¹-f                                         ∎)) ⟩

         (∀ x → ∃ λ f⁻¹-f → f-f⁻¹ (f x) ≡ cong f f⁻¹-f)                   ↠⟨ (∀-cong ext₂ λ _ → ∃-cong λ _ →
                                                                              _↔_.surjection B.≡-comm) ⟩

         (∀ x → ∃ λ f⁻¹-f → cong f f⁻¹-f ≡ f-f⁻¹ (f x))                   ↠⟨ _↔_.surjection B.ΠΣ-comm ⟩□

         (∃ λ f⁻¹-f → ∀ x → cong f (f⁻¹-f x) ≡ f-f⁻¹ (f x))               □)
        0 $
      Π-closure ext₂ 0 λ x →
      H-level.⇒≡ 0 $
      _⇔_.to Is-equivalence⇔Is-equivalence-CP eq (f x)

-- If the domain of f is contractible and the codomain is
-- propositional, then Is-equivalence f is contractible (assuming
-- extensionality).

sometimes-contractible :
  Extensionality (a ⊔ b) (a ⊔ b) →
  {A : Type a} {B : Type b} {f : A → B} →
  Contractible A → Is-proposition B →
  Contractible (Is-equivalence f)
sometimes-contractible {a = a} {b = b} ext A-contr B-prop =
  Σ-closure 0 (Π-closure ext-b-a 0 λ _ → A-contr)              λ _ →
  Σ-closure 0 (Π-closure ext-b-b 0 λ _ → H-level.+⇒≡ B-prop)   λ _ →
  Σ-closure 0 (Π-closure ext-a-a 0 λ _ → H-level.⇒≡ 0 A-contr) λ _ →
  Π-closure ext-a-b 0 λ _ → H-level.⇒≡ 0 $ H-level.+⇒≡ B-prop
  where
  ext-a-a : Extensionality a a
  ext-a-a = lower-extensionality b b ext

  ext-a-b : Extensionality a b
  ext-a-b = lower-extensionality b a ext

  ext-b-a : Extensionality b a
  ext-b-a = lower-extensionality a b ext

  ext-b-b : Extensionality b b
  ext-b-b = lower-extensionality a a ext

------------------------------------------------------------------------
-- Is-equivalence is related to CP.Is-equivalence (part two)

-- Is-equivalence f and CP.Is-equivalence f are isomorphic (assuming
-- extensionality).

Is-equivalence↔Is-equivalence-CP :
  {A : Type a} {B : Type b} {f : A → B} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  Is-equivalence f ↔ CP.Is-equivalence f
Is-equivalence↔Is-equivalence-CP ext = record
  { surjection = record
    { logical-equivalence = Is-equivalence⇔Is-equivalence-CP
    ; right-inverse-of    = λ _ → CP.propositional ext _ _ _
    }
  ; left-inverse-of = λ _ → propositional ext _ _ _
  }

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Prelude where

open import Agda.Primitive      public

open import Prelude.Unit        public
open import Prelude.Empty       public
open import Prelude.Function    public
open import Prelude.Char        public
open import Prelude.String      public
open import Prelude.Bool        public
open import Prelude.Nat         public
open import Prelude.Word        public
open import Prelude.Int         public
open import Prelude.Bytes       public
open import Prelude.Product     public
open import Prelude.Sum         public
open import Prelude.List        public
open import Prelude.Maybe       public
open import Prelude.Fin         public
open import Prelude.Vec         public
open import Prelude.Semiring    public
open import Prelude.Number      public
open import Prelude.Fractional  public
open import Prelude.Erased      public
open import Prelude.Strict      public

open import Prelude.Monoid      public
open import Prelude.Equality    public
open import Prelude.Decidable   public
open import Prelude.Functor     public
open import Prelude.Applicative public
open import Prelude.Alternative public
open import Prelude.Monad       public
open import Prelude.Show        public
open import Prelude.Ord         public
open import Prelude.Ord.Reasoning public
open import Prelude.Smashed     public

open import Prelude.IO          public

open import Prelude.Equality.Unsafe  public using (eraseEquality)
open import Prelude.Equality.Inspect public

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
module MUniverse where

-- This is universe polymorphism and extensional equality module
open import Sec2
-- import Data.List

data _≃₀_ {A : Set} (a : A) (b : A) : Set where
  a≃b : (a ≡ b) → a ≃₀ b

data _≃₁_ {A : Set} (f : A → A) (g : A → A) : Set where
  f≃g : ((x y : A) → (x ≃₀ y) → (f x ≃₀ g y)) → f ≃₁ g

B==B : 1 ≃₀ 1
B==B = a≃b refl

B==B1 : T ≃₀ T
B==B1 = a≃b refl

-- This is the same as + for natural numbers
_⋆_ : (x y : ℕ) → ℕ
Z ⋆ y = y
(S x) ⋆ y = S (x ⋆ y)

-- Proof that + and ⋆ are equivalent functions!
+==⋆ : (x : ℕ) → ((_+_) x) ≃₁ ((_⋆_) x)
+==⋆ x = f≃g (λ x₁ y x₂ → a≃b (prove x x₁ y x₂))
  where
    fcong : (x y : ℕ) → (p : (x + y) ≡ (x ⋆ y)) → S (x + y) ≡ S (x ⋆ y)
    fcong x y p with (x + y) | (x ⋆ y)
    fcong x y refl | m | .m = refl

    prove' : (x y : ℕ) → (x + y) ≡ (x ⋆ y)
    prove' Z y = refl
    prove' (S x) y with (prove' x y)
    prove' (S x) y | p = fcong x y p

    prove : (x y z : ℕ) → (p : y ≃₀ z) → (x + y) ≡ (x ⋆ z)
    prove x y .y (a≃b refl) = prove' x y

elim≃₁ : {A : Set} → (f g : A → A) (a : f ≃₁ g)
                 → (x y : A) → (p : x ≃₀ y)
                 → (f x ≃₀ g y)
elim≃₁ f g (f≃g a) x .x (a≃b refl) = a x x (a≃b refl)

-- Theorem that ≃₁ is a partial equivalence relation
≃₁-symmetric : {A : Set} → {f g : A → A} → (f ≃₁ g) → (g ≃₁ f)
≃₁-symmetric {A} {f} {g} (f≃g x) = f≃g (λ x₁ y x₂ → a≃b (prove x₁ y x₂ (f≃g x)))
  where
    prove : (z y : A) → (p : z ≃₀ y) → (f ≃₁ g) → (g z ≡ f y)
    prove z .z (a≃b refl) (f≃g x) with (x z z (a≃b refl) )
    prove z .z (a≃b refl) (f≃g x₁) | a≃b p with (f z) | (g z)
    prove z .z (a≃b refl) (f≃g x₁) | a≃b refl | m | .m = refl

≃₁-transitive : {A : Set} → {f g h : A → A}
                → (f ≃₁ g) → (g ≃₁ h) → (f ≃₁ h)
≃₁-transitive {A} {f} {g} {h} (f≃g x) (f≃g y) = f≃g (λ x₁ y₁ x₂ → a≃b (prove x₁ y₁ x₂ (f≃g x) (f≃g y)))
  where
    prove : (x y : A) (p : x ≃₀ y)
            → (f ≃₁ g)
            → (g ≃₁ h)
            → (f x ≡ h y)
    prove x₁ .x₁ (a≃b refl) (f≃g x₂) (f≃g x₃) with (x₂ x₁ x₁ (a≃b refl)) | (x₃ x₁ x₁ (a≃b refl))
    prove x₁ .x₁ (a≃b refl) (f≃g x₂) (f≃g x₃) | a≃b x₄ | a≃b x₅ with (f x₁) | (g x₁) | (h x₁)
    prove x₁ .x₁ (a≃b refl) (f≃g x₂) (f≃g x₃) | a≃b refl | a≃b refl | p1 | .p1 | .p1 = refl


text:
-- Andreas, 2014-05-21, reported and test case by Fabien Renaud

module Issue1138 where

open import Common.Equality

postulate
  Var    : Set
  Varset : Set
  _∖_    : Varset -> Var -> Varset
  _⊆_    : Varset -> Varset -> Set

data Expression : Set where
  abs : Var -> Expression -> Expression

FV : Expression -> Varset
FV (abs x M) = FV M ∖ x

data Env (A : Set) : Set where
  <>     : Env A
  _,_:=_ : Env A -> Var -> A -> Env A

postulate
  dom        : ∀ {A} -> Env A -> Varset
  extend-dom : ∀ {A : Set} {a : A} {x xs ρ}
               -> (xs ∖ x) ⊆ dom ρ
               -> xs ⊆ dom (ρ , x := a)

record Model (D : Set) : Set where
  field
    eval : (e : Expression) (ρ : Env D) -> FV e ⊆ dom ρ -> D
    d    : D
    law  : ∀ {M N ρ ν x y}
           -> eval M (ρ , x := d) (extend-dom {!!}) ≡
              eval N (ν , y := d) (extend-dom {!!})
           -> eval (abs x M) ρ {!!} ≡
              eval (abs y N) ν {!!}

-- Expected:  For holes numbered 0,1,2,3 above and four goals below:

-- ?0 : (FV M ∖ x) ⊆ dom ρ
-- ?1 : (FV N ∖ y) ⊆ dom ν
-- ?2 : FV (abs x M) ⊆ dom ρ
-- ?3 : FV (abs y N) ⊆ dom ν

-- There was a problem that two interaction points were created
-- per ? in record fields, thus, they were off in emacs.
-- (Introduced by fix for issue 1083).

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the polymorphic unit type
-- Defines Decidable Equality and Decidable Ordering as well
------------------------------------------------------------------------

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

module Data.Unit.Polymorphic.Properties where

open import Level
open import Data.Sum.Base using (inj₁)
open import Data.Unit.Polymorphic.Base using (⊤; tt)
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

private
  variable
    ℓ : Level

------------------------------------------------------------------------
-- Equality
------------------------------------------------------------------------

infix 4 _≟_

_≟_ : Decidable {A = ⊤ {ℓ}} _≡_
_ ≟ _ = yes refl

≡-setoid : ∀ ℓ → Setoid ℓ ℓ
≡-setoid _ = setoid ⊤

≡-decSetoid : ∀ ℓ → DecSetoid ℓ ℓ
≡-decSetoid _ = decSetoid _≟_

------------------------------------------------------------------------
-- Ordering
------------------------------------------------------------------------

≡-total : Total {A = ⊤ {ℓ}} _≡_
≡-total _ _ = inj₁ refl

≡-antisym : Antisymmetric {A = ⊤ {ℓ}} _≡_ _≡_
≡-antisym p _ = p

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

≡-isPreorder : ∀ ℓ → IsPreorder {ℓ} {_} {⊤} _≡_ _≡_
≡-isPreorder ℓ = record
  { isEquivalence = isEquivalence
  ; reflexive     = λ x → x
  ; trans         = trans
  }

≡-isPartialOrder : ∀ ℓ → IsPartialOrder {ℓ} _≡_ _≡_
≡-isPartialOrder ℓ = record
  { isPreorder = ≡-isPreorder ℓ
  ; antisym    = ≡-antisym
  }

≡-isTotalOrder : ∀ ℓ → IsTotalOrder {ℓ} _≡_ _≡_
≡-isTotalOrder ℓ = record
  { isPartialOrder = ≡-isPartialOrder ℓ
  ; total          = ≡-total
  }

≡-isDecTotalOrder : ∀ ℓ → IsDecTotalOrder {ℓ} _≡_ _≡_
≡-isDecTotalOrder ℓ = record
  { isTotalOrder = ≡-isTotalOrder ℓ
  ; _≟_          = _≟_
  ; _≤?_         = _≟_
  }

------------------------------------------------------------------------
-- Bundles

≡-preorder : ∀ ℓ → Preorder ℓ ℓ ℓ
≡-preorder ℓ = record
  { isPreorder = ≡-isPreorder ℓ
  }

≡-poset : ∀ ℓ → Poset ℓ ℓ ℓ
≡-poset ℓ = record
  { isPartialOrder = ≡-isPartialOrder ℓ
  }

≡-totalOrder : ∀ ℓ → TotalOrder ℓ ℓ ℓ
≡-totalOrder ℓ = record
  { isTotalOrder = ≡-isTotalOrder ℓ
  }

≡-decTotalOrder : ∀ ℓ → DecTotalOrder ℓ ℓ ℓ
≡-decTotalOrder ℓ = record
  { isDecTotalOrder = ≡-isDecTotalOrder ℓ
  }


text:
{-# OPTIONS --universe-polymorphism #-}
module Data.BitVector.Properties where

open import Algebra using (CommutativeRing)
open import Data.Bool using (_∧_; _∨_; _xor_)
                   renaming (Bool to Bit; false to 0#; true to 1#)
open import Data.Nat using (ℕ) renaming (zero to Nzero; suc to Nsuc)
open import Data.Product using (_,_)
open import Data.Vec hiding (last)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open import Data.BitVector

last-cons : ∀ {n} x (xs : BitVector (Nsuc n)) → last (x ∷ xs) ≡ last xs
last-cons _ (x ∷ xs) = refl

last-snoc : ∀ {n} (xs : BitVector n) x → last (snoc xs x) ≡ x
last-snoc []            _                                  = refl
last-snoc (y ∷ [])      _                                  = refl
last-snoc (y ∷ y′ ∷ ys) x rewrite last-cons y′ (snoc ys x) = last-snoc ys x

droplast-snoc : ∀ {n} (xs : BitVector n) x → droplast (snoc xs x) ≡ xs
droplast-snoc []       _                            = refl
droplast-snoc (y ∷ ys) x rewrite droplast-snoc ys x = refl

droplast-snoc-last : ∀ {n} (x : BitVector (Nsuc n)) → snoc (droplast x) (last x) ≡ x
droplast-snoc-last (x ∷ [])                                           = refl
droplast-snoc-last (x ∷ x′ ∷ xs) rewrite droplast-snoc-last (x′ ∷ xs) = refl

rotate∘unrotate≡id : ∀ {n} (x : BitVector n) → rotate (unrotate x) ≡ x
rotate∘unrotate≡id [] = refl
rotate∘unrotate≡id (x ∷ []) = refl
rotate∘unrotate≡id (x ∷ x′ ∷ xs) rewrite last-cons x′ (snoc xs x)
                                      | last-snoc xs x
                                      | droplast-snoc xs x = refl

unrotate∘rotate≡id : ∀ {n} (x : BitVector n) → unrotate (rotate x) ≡ x
unrotate∘rotate≡id [] = refl
unrotate∘rotate≡id (x ∷ xs) = droplast-snoc-last (x ∷ xs)

private
  module P {n : ℕ} where
    import Algebra.FunctionProperties as FP; open FP (_≡_ {A = BitVector n}) public
  open P

  +-identityˡ : ∀ {n} → LeftIdentity (zero n) _+_
  +-identityˡ []                               = refl
  +-identityˡ (1# ∷ xs) rewrite +-identityˡ xs = refl
  +-identityˡ (0# ∷ xs) rewrite +-identityˡ xs = refl

  +-identityʳ : ∀ {n} → RightIdentity (zero n) _+_
  +-identityʳ []                               = refl
  +-identityʳ (1# ∷ xs) rewrite +-identityʳ xs = refl
  +-identityʳ (0# ∷ xs) rewrite +-identityʳ xs = refl

  add-carry : ∀ {n} c₁ c₂ (x y z : BitVector n) → add′ c₁ x (add′ c₂ y z) ≡ add′ c₂ x (add′ c₁ y z)
  add-carry c₁ c₂ []        []        []                                         = refl
  add-carry 0# 0# (0# ∷ xs) (y  ∷ ys) (z  ∷ zs)                                  = refl
  add-carry 0# 0# (1# ∷ xs) (0# ∷ ys) (0# ∷ zs)                                  = refl
  add-carry 0# 0# (1# ∷ xs) (0# ∷ ys) (1# ∷ zs)                                  = refl
  add-carry 0# 0# (1# ∷ xs) (1# ∷ ys) (0# ∷ zs)                                  = refl
  add-carry 0# 0# (1# ∷ xs) (1# ∷ ys) (1# ∷ zs)                                  = refl
  add-carry 0# 1# (0# ∷ xs) (0# ∷ ys) (0# ∷ zs)                                  = refl
  add-carry 0# 1# (0# ∷ xs) (0# ∷ ys) (1# ∷ zs) rewrite add-carry 0# 1# xs ys zs = refl
  add-carry 0# 1# (0# ∷ xs) (1# ∷ ys) (0# ∷ zs) rewrite add-carry 0# 1# xs ys zs = refl
  add-carry 0# 1# (0# ∷ xs) (1# ∷ ys) (1# ∷ zs)                                  = refl
  add-carry 0# 1# (1# ∷ xs) (0# ∷ ys) (0# ∷ zs)                                  = refl
  add-carry 0# 1# (1# ∷ xs) (0# ∷ ys) (1# ∷ zs) rewrite add-carry 0# 1# xs ys zs = refl
  add-carry 0# 1# (1# ∷ xs) (1# ∷ ys) (0# ∷ zs) rewrite add-carry 0# 1# xs ys zs = refl
  add-carry 0# 1# (1# ∷ xs) (1# ∷ ys) (1# ∷ zs)                                  = refl
  add-carry 1# 0# (0# ∷ xs) (0# ∷ ys) (0# ∷ zs)                                  = refl
  add-carry 1# 0# (0# ∷ xs) (0# ∷ ys) (1# ∷ zs) rewrite add-carry 1# 0# xs ys zs = refl
  add-carry 1# 0# (0# ∷ xs) (1# ∷ ys) (0# ∷ zs) rewrite add-carry 1# 0# xs ys zs = refl
  add-carry 1# 0# (0# ∷ xs) (1# ∷ ys) (1# ∷ zs)                                  = refl
  add-carry 1# 0# (1# ∷ xs) (0# ∷ ys) (0# ∷ zs)                                  = refl
  add-carry 1# 0# (1# ∷ xs) (0# ∷ ys) (1# ∷ zs) rewrite add-carry 1# 0# xs ys zs = refl
  add-carry 1# 0# (1# ∷ xs) (1# ∷ ys) (0# ∷ zs) rewrite add-carry 1# 0# xs ys zs = refl
  add-carry 1# 0# (1# ∷ xs) (1# ∷ ys) (1# ∷ zs)                                  = refl
  add-carry 1# 1# (0# ∷ xs) (y  ∷ ys) (z  ∷ zs)                                  = refl
  add-carry 1# 1# (1# ∷ xs) (0# ∷ ys) (0# ∷ zs)                                  = refl
  add-carry 1# 1# (1# ∷ xs) (0# ∷ ys) (1# ∷ zs)                                  = refl
  add-carry 1# 1# (1# ∷ xs) (1# ∷ ys) (0# ∷ zs)                                  = refl
  add-carry 1# 1# (1# ∷ xs) (1# ∷ ys) (1# ∷ zs)                                  = refl

  add-assoc : ∀ {n} c₁ c₂ (x y z : BitVector n) → add′ c₁ (add′ c₂ x y) z ≡ add′ c₁ x (add′ c₂ y z)
  add-assoc c₁ c₂ []        []        []                                         = refl
  add-assoc c₁ 1# (1# ∷ xs) (1# ∷ ys) (1# ∷ zs) rewrite add-assoc 1# 1# xs ys zs = refl
  add-assoc c₁ 1# (1# ∷ xs) (1# ∷ ys) (0# ∷ zs) rewrite add-assoc c₁ 1# xs ys zs = refl
  add-assoc c₁ 1# (1# ∷ xs) (0# ∷ ys) (1# ∷ zs) rewrite add-assoc c₁ 1# xs ys zs = refl
  add-assoc c₁ 1# (1# ∷ xs) (0# ∷ ys) (0# ∷ zs) rewrite add-assoc 0# 1# xs ys zs
                                                      | add-carry 0# 1# xs ys zs = refl
  add-assoc c₁ 1# (0# ∷ xs) (1# ∷ ys) (1# ∷ zs) rewrite add-assoc c₁ 1# xs ys zs = refl
  add-assoc c₁ 1# (0# ∷ xs) (1# ∷ ys) (0# ∷ zs) rewrite add-assoc 0# 1# xs ys zs = refl
  add-assoc c₁ 1# (0# ∷ xs) (0# ∷ ys) (1# ∷ zs) rewrite add-assoc 1# 0# xs ys zs
                                                      | add-carry 1# 0# xs ys zs = refl
  add-assoc c₁ 1# (0# ∷ xs) (0# ∷ ys) (0# ∷ zs) rewrite add-assoc c₁ 0# xs ys zs = refl
  add-assoc c₁ 0# (1# ∷ xs) (1# ∷ ys) (1# ∷ zs) rewrite add-assoc c₁ 1# xs ys zs = refl
  add-assoc c₁ 0# (1# ∷ xs) (1# ∷ ys) (0# ∷ zs) rewrite add-assoc 0# 1# xs ys zs
                                                      | add-carry 0# 1# xs ys zs = refl
  add-assoc c₁ 0# (1# ∷ xs) (0# ∷ ys) (1# ∷ zs) rewrite add-assoc 1# 0# xs ys zs = refl
  add-assoc c₁ 0# (1# ∷ xs) (0# ∷ ys) (0# ∷ zs) rewrite add-assoc c₁ 0# xs ys zs = refl
  add-assoc c₁ 0# (0# ∷ xs) (1# ∷ ys) (1# ∷ zs) rewrite add-assoc 1# 0# xs ys zs
                                                      | add-carry 1# 0# xs ys zs = refl
  add-assoc c₁ 0# (0# ∷ xs) (1# ∷ ys) (0# ∷ zs) rewrite add-assoc c₁ 0# xs ys zs = refl
  add-assoc c₁ 0# (0# ∷ xs) (0# ∷ ys) (1# ∷ zs) rewrite add-assoc c₁ 0# xs ys zs = refl
  add-assoc c₁ 0# (0# ∷ xs) (0# ∷ ys) (0# ∷ zs) rewrite add-assoc 0# 0# xs ys zs = refl

  +-assoc : ∀ {n} → Associative {n} _+_
  +-assoc []        []        []                                         = refl
  +-assoc (1# ∷ xs) (1# ∷ ys) (1# ∷ zs) rewrite add-assoc 0# 1# xs ys zs = refl
  +-assoc (1# ∷ xs) (1# ∷ ys) (0# ∷ zs) rewrite add-assoc 0# 1# xs ys zs
                                              | add-carry 0# 1# xs ys zs = refl
  +-assoc (1# ∷ xs) (0# ∷ ys) (1# ∷ zs) rewrite add-assoc 1# 0# xs ys zs = refl
  +-assoc (1# ∷ xs) (0# ∷ ys) (0# ∷ zs) rewrite add-assoc 0# 0# xs ys zs = refl
  +-assoc (0# ∷ xs) (1# ∷ ys) (1# ∷ zs) rewrite add-assoc 1# 0# xs ys zs
                                              | add-carry 1# 0# xs ys zs = refl
  +-assoc (0# ∷ xs) (1# ∷ ys) (0# ∷ zs) rewrite add-assoc 0# 0# xs ys zs = refl
  +-assoc (0# ∷ xs) (0# ∷ ys) (1# ∷ zs) rewrite add-assoc 0# 0# xs ys zs = refl
  +-assoc (0# ∷ xs) (0# ∷ ys) (0# ∷ zs) rewrite add-assoc 0# 0# xs ys zs = refl

  add-comm : ∀ {n} c (x y : BitVector n) → add′ c x y ≡ add′ c y x
  add-comm c []        []                                  = refl
  add-comm c (1# ∷ xs) (1# ∷ ys) rewrite add-comm 1# xs ys = refl
  add-comm c (1# ∷ xs) (0# ∷ ys) rewrite add-comm c  xs ys = refl
  add-comm c (0# ∷ xs) (1# ∷ ys) rewrite add-comm c  xs ys = refl
  add-comm c (0# ∷ xs) (0# ∷ ys) rewrite add-comm 0# xs ys = refl

  +-comm : ∀ {n} → Commutative {n} _+_
  +-comm = add-comm 0#

  add-inverse : ∀ {n} xs → add′ 1# (zero n + bitwise-negation xs) xs ≡ zero n
  add-inverse []                               = refl
  add-inverse (1# ∷ xs) rewrite add-inverse xs = refl
  add-inverse (0# ∷ xs) rewrite add-inverse xs = refl

  inverseˡ : ∀ {n} → LeftInverse (zero n) -_ _+_
  inverseˡ [] = refl
  inverseˡ (1# ∷ xs) rewrite add-inverse xs = refl
  inverseˡ (0# ∷ xs) rewrite      add-assoc 0# 1# (zero _) (bitwise-negation xs) xs
                           |      add-carry 0# 1# (zero _) (bitwise-negation xs) xs
                           | sym (add-assoc 1# 0# (zero _) (bitwise-negation xs) xs)
                           | add-inverse xs = refl

  inverseʳ : ∀ {n} → RightInverse (zero n) -_ _+_
  inverseʳ x = trans (+-comm x (- x)) (inverseˡ x)

  *-zeroˡ : ∀ {n} → LeftZero (zero n) _*_
  *-zeroˡ []                                      = refl
  *-zeroˡ {Nsuc n} x rewrite *-zeroˡ (droplast x) = refl

  2*_ : ∀ {n} → Op₁ {0} (BitVector n)
  2* x = droplast (0# ∷ x)

  1+2*_ : ∀ {n} → Op₁ {0} (BitVector n)
  1+2* x = droplast (1# ∷ x)

  _+2*_ : ∀ {n} → Bit → BitVector n → BitVector n
  b +2* x = droplast (b ∷ x)

  *-identityˡ : ∀ {n} → LeftIdentity (one n) _*_
  *-identityˡ []                                                   = refl
  *-identityˡ (0# ∷ xs) rewrite *-zeroˡ (  2* xs) | +-identityʳ xs = refl
  *-identityˡ (1# ∷ xs) rewrite *-zeroˡ (1+2* xs) | +-identityʳ xs = refl

  *-comm : ∀ {n} → Commutative {n} _*_
  *-comm          [] [] = refl
  *-comm {Nsuc n} x  y  = *-comm1 x y
   where
   *-comm1 : ∀ {n} → Commutative {Nsuc n} _*_
   *-comm1          (0# ∷ []) (0# ∷ [])                                            = refl
   *-comm1          (0# ∷ []) (1# ∷ [])                                            = refl
   *-comm1          (1# ∷ []) (0# ∷ [])                                            = refl
   *-comm1          (1# ∷ []) (1# ∷ [])                                            = refl
   *-comm1 {Nsuc _} (0# ∷ xs) (0# ∷ ys) rewrite *-comm1 xs (2* ys)
                                              | *-comm1 ys (2* xs)
                                              | *-comm (droplast ys) (droplast xs) = refl
   *-comm1 {Nsuc _} (0# ∷ xs) (1# ∷ ys) rewrite *-comm1 xs (1+2* ys)
                                              | *-comm1 ys (2* xs)
                                              | *-comm (droplast ys) (droplast xs) = refl
   *-comm1 {Nsuc _} (1# ∷ xs) (0# ∷ ys) rewrite *-comm1 xs (2* ys)
                                              | *-comm1 ys (1+2* xs)
                                              | *-comm (droplast ys) (droplast xs) = refl
   *-comm1 {Nsuc _} (1# ∷ xs) (1# ∷ ys) rewrite *-comm1 xs (1+2* ys)
                                              | *-comm1 ys (1+2* xs)
                                              | *-comm (droplast ys) (droplast xs)
                                              | sym (+-assoc ys xs (0# ∷ droplast xs * droplast ys))
                                              | +-comm ys xs
                                              | +-assoc xs ys (0# ∷ droplast xs * droplast ys) = refl

  droplast-distrib-+ : ∀ {n} (x y : BitVector (Nsuc n))
                     → droplast (x + y) ≡ droplast x + droplast y
  droplast-distrib-+ {Nzero}  _         _                                          = refl
  droplast-distrib-+ {Nsuc _} (0# ∷ xs) (0# ∷ ys) rewrite droplast-distrib-+ xs ys = refl
  droplast-distrib-+ {Nsuc _} (0# ∷ xs) (1# ∷ ys) rewrite droplast-distrib-+ xs ys = refl
  droplast-distrib-+ {Nsuc _} (1# ∷ xs) (0# ∷ ys) rewrite droplast-distrib-+ xs ys = refl
  droplast-distrib-+ {Nsuc _} (1# ∷ xs) (1# ∷ ys) rewrite droplast-distrib-+ xs ys
                                                        = cong (_∷_ 0#) (lemma xs ys)
   where
   lemma : ∀ {n} (xs ys : BitVector (Nsuc n))
         → droplast (add′ 1# xs ys) ≡ add′ 1# (droplast xs) (droplast ys)
   lemma {Nzero}  _         _                                          = refl
   lemma {Nsuc _} (0# ∷ xs) (0# ∷ ys) rewrite droplast-distrib-+ xs ys = refl
   lemma {Nsuc _} (0# ∷ xs) (1# ∷ ys) rewrite lemma xs ys              = refl
   lemma {Nsuc _} (1# ∷ xs) (0# ∷ ys) rewrite lemma xs ys              = refl
   lemma {Nsuc _} (1# ∷ xs) (1# ∷ ys) rewrite lemma xs ys              = refl

  droplast-distrib-* : ∀ {n} (x y : BitVector (Nsuc n))
                     → droplast (x * y) ≡ droplast x * droplast y
  droplast-distrib-* {Nzero}  _         _ = refl
  droplast-distrib-* {Nsuc _} (0# ∷ xs) (y  ∷ ys)
    rewrite droplast-distrib-* xs (y +2* ys) = refl
  droplast-distrib-* {Nsuc _} (1# ∷ xs) (0# ∷ ys)
    rewrite droplast-distrib-+ ys (xs * (2* ys))
          | droplast-distrib-* xs (2* ys) = refl
  droplast-distrib-* {Nsuc _} (1# ∷ xs) (1# ∷ ys)
    rewrite droplast-distrib-+ ys (xs * (1+2* ys))
          | droplast-distrib-* xs (1+2* ys) = refl

  extract-carry : ∀ {n} (xs ys : BitVector n) → add′ 1# xs ys ≡ one _ + (xs + ys)
  extract-carry []        []                                            = refl
  extract-carry (0# ∷ xs) (0# ∷ ys) rewrite +-identityˡ (xs + ys)       = refl
  extract-carry (0# ∷ xs) (1# ∷ ys) rewrite add-carry 1# 0# (zero _) xs ys
                                          | +-identityˡ (add′ 1# xs ys) = refl
  extract-carry (1# ∷ xs) (0# ∷ ys) rewrite add-carry 1# 0# (zero _) xs ys
                                          | +-identityˡ (add′ 1# xs ys) = refl
  extract-carry (1# ∷ xs) (1# ∷ ys) rewrite +-identityˡ (add′ 1# xs ys) = refl

  shift-to-add : ∀ c {n} (x : BitVector n) → c +2* x ≡ add′ c x x
  shift-to-add _ []                                   = refl
  shift-to-add c (0# ∷ xs) rewrite shift-to-add 0# xs = refl
  shift-to-add c (1# ∷ xs) rewrite shift-to-add 1# xs = refl

  *-distribʳ : ∀ {n} → (_*_ {n}) DistributesOverʳ _+_
  *-distribʳ          [] [] [] = refl
  *-distribʳ {Nsuc n} xs ys zs = *-distribʳ1 xs ys zs

    where
    lemma : ∀ {n} c (xs ys zs : BitVector n)
          → add′ 1# ys zs * c +2* xs
          ≡ add′ c (xs + (ys * c +2* xs)) (xs + (zs * c +2* xs))
    lemma c xs ys zs rewrite
         extract-carry ys zs
       | *-distribʳ (c +2* xs) (one _) (ys + zs)
       | *-identityˡ (c +2* xs)
       | *-distribʳ (c +2* xs) ys zs
       | shift-to-add c xs
       | *-comm ys (add′ c xs xs)
       | *-comm zs (add′ c xs xs)
       | +-comm (add′ c xs xs) (add′ c xs xs * ys + add′ c xs xs * zs)
       | add-carry 0# c (add′ c xs xs * ys + add′ c xs xs * zs) xs xs
       | add-assoc c 0# (add′ c xs xs * ys) (add′ c xs xs * zs) (xs + xs)
       | sym (+-assoc (add′ c xs xs * zs) xs xs)
       | +-comm (add′ c xs xs * zs) xs
       | +-comm (xs + add′ c xs xs * zs) xs
       | sym (add-assoc c 0# (add′ c xs xs * ys) xs (xs + add′ c xs xs * zs))
       | +-comm  (add′ c xs xs * ys) xs
       = refl

    *-distribʳ1 : ∀ {n} → (_*_ {Nsuc n}) DistributesOverʳ _+_
    *-distribʳ1 xs (0# ∷ ys) (0# ∷ zs) rewrite *-distribʳ (droplast xs) ys zs = refl
    *-distribʳ1 (0# ∷ xs) (0# ∷ ys) (1# ∷ zs)
             rewrite *-distribʳ (2* xs) ys zs
                   | sym (+-assoc xs (ys * 2* xs) (zs * 2* xs))
                   | +-comm xs (ys * 2* xs)
                   | +-assoc (ys * 2* xs) xs (zs * 2* xs) = refl
    *-distribʳ1 (1# ∷ xs) (0# ∷ ys) (1# ∷ zs)
             rewrite *-distribʳ (1+2* xs) ys zs
                   | sym (+-assoc xs (ys * 1+2* xs) (zs * 1+2* xs))
                   | +-comm xs (ys * 1+2* xs)
                   | +-assoc (ys * 1+2* xs) xs (zs * 1+2* xs) = refl
    *-distribʳ1 (0# ∷ xs) (1# ∷ ys) (0# ∷ zs)
             rewrite *-distribʳ (2* xs) ys zs
                   | +-assoc xs (ys * 2* xs) (zs * 2* xs) = refl
    *-distribʳ1 (1# ∷ xs) (1# ∷ ys) (0# ∷ zs)
             rewrite *-distribʳ (1+2* xs) ys zs
                   | +-assoc xs (ys * 1+2* xs) (zs * 1+2* xs) = refl
    *-distribʳ1 (0# ∷ xs) (1# ∷ ys) (1# ∷ zs) rewrite lemma 0# xs ys zs = refl
    *-distribʳ1 (1# ∷ xs) (1# ∷ ys) (1# ∷ zs) rewrite lemma 1# xs ys zs = refl

  *-assoc : ∀ {n} → Associative {n} _*_
  *-assoc          [] [] [] = refl
  *-assoc {Nsuc n} x  y  z  = *-assoc1 x y z

   where
   *-assoc1 : ∀ {n} → Associative {Nsuc n} _*_
   *-assoc1 (0# ∷ xs) ys zs rewrite *-assoc xs (droplast ys) (droplast zs)
                                  | droplast-distrib-* ys zs = refl
   *-assoc1 (1# ∷ xs) ys zs rewrite *-distribʳ zs ys (0# ∷ xs * droplast ys)
                                  | *-assoc xs (droplast ys) (droplast zs)
                                  | droplast-distrib-* ys zs = refl

  *-identityʳ : ∀ {n} → RightIdentity (one n) _*_
  *-identityʳ x rewrite *-comm x (one _) = *-identityˡ x

  *-distribˡ : ∀ {n} → (_*_ {n}) DistributesOverˡ _+_
  *-distribˡ x y z rewrite *-comm x (y + z)
                         | *-distribʳ x y z
                         | *-comm x y
                         | *-comm x z = refl

  module Properties (n : ℕ) where
    open import Algebra.Structures

    +-isSemigroup : IsSemigroup {A = BitVector n} _≡_ _+_
    +-isSemigroup = record
       { isEquivalence = isEquivalence; assoc = +-assoc; ∙-cong = cong₂ _+_ }

    +-isMonoid : IsMonoid _≡_ _+_ (zero n)
    +-isMonoid = record
       { isSemigroup = +-isSemigroup; identity = +-identityˡ , +-identityʳ }

    +-isGroup : IsGroup _≡_ _+_ (zero n) -_
    +-isGroup = record
       { isMonoid = +-isMonoid; inverse = inverseˡ , inverseʳ; ⁻¹-cong = cong -_ }

    +-isAbelianGroup : IsAbelianGroup _≡_ _+_ (zero n) -_
    +-isAbelianGroup = record { isGroup = +-isGroup; comm = +-comm }

    *-isSemigroup : IsSemigroup {A = BitVector n} _≡_ _*_
    *-isSemigroup = record
       { isEquivalence = isEquivalence; assoc = *-assoc; ∙-cong = cong₂ _*_ }

    *-isMonoid : IsMonoid _≡_ _*_ (one n)
    *-isMonoid = record
       { isSemigroup = *-isSemigroup; identity = *-identityˡ , *-identityʳ }

    isRing : IsRing _≡_ _+_ _*_ -_ (zero n) (one n)
    isRing = record { +-isAbelianGroup = +-isAbelianGroup;
                      *-isMonoid = *-isMonoid;
                      distrib = *-distribˡ , *-distribʳ }

    isCommutativeRing : IsCommutativeRing _≡_ _+_ _*_ -_ (zero n) (one n)
    isCommutativeRing = record { isRing = isRing; *-comm = *-comm }

commutativeRing : ∀ n → CommutativeRing _ _
commutativeRing n = record
  { Carrier = BitVector n;
    _≈_ = _≡_; _+_ = _+_; _*_ = _*_; -_ = -_;
    0# = zero n; 1# = one n;
    isCommutativeRing = Properties.isCommutativeRing n }

max_stars_repo_name: copumpkin/bitvector

max_issues_repo_name: copumpkin/bitvector

max_forks_repo_name: copumpkin/bitvector


text:
open import Signature
import Logic

module Model (Σ Δ : Sig) (V : Set) (Φ : Logic.Program Σ Δ V) where

open import Function
open import Data.Empty renaming (⊥ to Ø)
open import Data.Sum
open import Data.Product renaming (Σ to ∐)
open import Relation.Unary
open import Relation.Binary.PropositionalEquality hiding ([_])

open import Logic Σ Δ V
open import Terms Σ

-- | I-ary relations over A
Rel : Set → Set → Set₁
Rel I A = (I → A) → Set

_⊆ᵣ_ : ∀{I A} → Rel I A → Rel I A → Set
R₁ ⊆ᵣ R₂ = ∀{t} → R₁ t → R₂ t

PredInterpret : Set₁
PredInterpret = (Q : ∥ Δ ∥) → Rel (ar Δ Q) (T∞ Ø)

_⊑ᵢ_ : PredInterpret → PredInterpret → Set
I₁ ⊑ᵢ I₂ = ∀ {Q} → I₁ Q ⊆ᵣ I₂ Q

liftApp∞ : ∀ {V W} {I : Set} → Subst∞ V W → (I → T∞ V) → (I → T∞ W)
liftApp∞ σ f i = app∞ σ (f i)

_≡[_]_ : T∞ Ø → Subst∞ V Ø → T V → Set
t ≡[ σ ] s = t ~ app∞ σ (χ s)

{-
_⊨[_]_ : PredInterpret → Subst∞ V Ø → Formula → Set
I ⊨[ σ ] (inj₁ (Q , ts)) = liftApp∞ σ (χ ∘ ts) ∈ I Q
I ⊨[ σ ] (inj₂ _) = Ø
-}

_⊨[_]_ : PredInterpret → Subst∞ V Ø → Formula → Set
I ⊨[ σ ] (Q , ts) = liftApp∞ σ (χ ∘ ts) ∈ I Q

⟦_⟧ : dom Φ → PredInterpret → PredInterpret
⟦ C ⟧ I = F (get Φ C)
  where
    -- | Forward closure for inductive clauses is given by
    -- F(h ⊢μ Q'(t))(I)(Q)
    --   = {t[σ] | σ : V → Ø ∧ Q ≡ Q' ∧ ∀ P(s) ∈ h. s[σ] ∈ I(P)}.
    -- The backwards closure for coinductive clauses is, on the other hand,
    -- given by
    -- F(h ⊢ν P(s))(I)(Q) = {t[σ] | σ : V → Ø ∧ Q(t) ∈ h ∧ s ∈ I(Q)}
    F : Clause → PredInterpret
    F (h ⊢[ ind ] (Q' , pat)) Q ts =
      ∐ (Q' ≡ Q) (λ p →
      ∃ (λ σ →
        ∀ i → ts (subst _ p i) ≡[ σ ] pat i
        × (∀ j → I ⊨[ σ ] get h j)))
    F (h ⊢[ coind ] φ) Q ts =
      ∃ (λ j →
      ∐ (proj₁ (get h j) ≡ Q) (λ p →
      ∃ (λ σ →
        ∀ i → ts (subst _ p i) ≡[ σ ] proj₂ (get h j) i
        × I ⊨[ σ ] φ)))

FormInterpret : PredInterpret → Formula → Pred (Subst∞ V Ø) _
FormInterpret I (Q , ts) σ = (λ i → app∞ σ (χ (ts i))) ∈ I Q

B : (Formula → Pred (Subst∞ V Ø) _) → (Formula → Pred (Subst∞ V Ø) _)
B D F = {!!}

record ModelData : Set₁ where
  field
    preds : PredInterpret

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox