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

--open import Data.Nat using (ℕ; zero; suc; _+_)
open import Cubical.Data.Nat using (ℕ; zero; suc; _+_)
open import Cubical.Foundations.Prelude using (refl; _≡_; subst; cong; transport; transp; ℓ-zero; ℓ-suc) -- hiding (_≡⟨_⟩_)
open import Cubical.Foundations.Function using (_∘_)

data Captured {a} (A : Set a) : Set a where
  cap : A → Captured A

Id : ∀ {a} {A} → Captured A → Set a
Id {_} {A} (cap _) = A

id : ∀ {a} {A} → (n : Captured A) → Id {a} n
id (cap n) = n

data ⟨Set⟩ {a} (A : Set a) : Set a where
  empty : ⟨Set⟩ A
  insert : A → ⟨Set⟩ A → ⟨Set⟩ A
  dup : ∀ a sa → insert a (insert a sa) ≡ insert a sa
  com : ∀ a b sa → insert a (insert b sa) ≡ insert b (insert a sa)

rem-dup ()

--_in_ : A → ⟨Set⟩ A →

--insert 3 (insert 3 empty)
--transport (dup 3 empty))

--transport (dup {ℓ-zero} 3 empty)
--insert 3 (insert 3 empty)
--subst {A = insert 3 (insert 3 empty)} (dup 3 empty)
--transport {ℓ-zero} {ℕ} refl
--cong cap (dup 3 empty)
--transport (cong (Id ∘ cap) (dup 3 empty)) (id (cap (insert 3 (insert 3 empty))))
--id (cap (insert 3 (insert 3 empty)))

ext: agda


text:
-- Terms using Agdas Sized Types --
module TermsSized where

open import Data.Vec hiding (_++_)
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.List
open import Data.List.Relation.Unary.All
open import Data.Fin.Base

open import Size

-- Ranked alphabet: Vector of natural numbers, where vec[i] denotes the arity of symbol i
RankedAlphabet : ℕ → Set
RankedAlphabet n = Vec ℕ n

-- Types
data Type : Set where
  TTerm : ∀ {n} → RankedAlphabet n → Type
  TFun  : Type → Type → Type

-- Type environment
Env : Set
Env = List Type

-- Environment lookup
data _∈`_ : Type → Env → Set where
  here  : ∀ {φ A}    → A ∈` (A ∷ φ)
  there : ∀ {φ A A'} → A ∈` φ → A ∈` (A' ∷ φ)

-- Bind a type n times on top of an environment
bind : Env → (A : Type) → ℕ → Env
bind φ A zero    = φ
bind φ A (suc n) = A ∷ (bind φ A n)

-- Zero & Successor, Variables, prim. recursion, Abstraction, Application
data Expr : {j : Size} → Env → Type → Set where
  ETerm      : ∀ {j : Size} {φ n} {vec : RankedAlphabet n} {sym : Fin n} → Vec (Expr {j} φ (TTerm vec)) (Data.Vec.lookup vec sym) → Expr {↑ j} φ (TTerm vec)
  ETerm-Rec  : ∀ {j : Size} {φ n} {vec : RankedAlphabet n} {A} → (∀ {sym : Fin n} → Expr {j} (bind φ A (Data.Vec.lookup vec sym)) A) → Expr {j} φ (TTerm vec) → Expr {↑ j} φ A
  Var        : ∀ {φ A}   → A ∈` φ → Expr {∞} φ A
  Abs        : ∀ {φ A B} → Expr (A ∷ φ) B → Expr φ (TFun A B)
  App        : ∀ {φ A B} → Expr φ (TFun A B) → Expr φ A → Expr φ B

-- Terms
data Term {n} (ra : RankedAlphabet n) : {i : Size} → Set where
  mk : ∀ {i} → (sym : Fin n) → Vec (Term ra {i}) (Data.Vec.lookup ra sym) → Term ra {↑ i}

-- Values
Value : Type → Set
Value (TTerm ra) = Term ra
Value (TFun A B) = Value A → Value B

-- Lookup in environment of all Values
access : ∀ {A φ} → A ∈` φ → All Value φ → Value A
access here      (px ∷ p) = px
access (there x) (px ∷ p) = access x p

extend : ∀ {ϕ A} →
  (m : ℕ) →
  (ϱ₁    : Vec (Value A) m) →
  (ϱ     : All Value ϕ) →
  All Value (bind ϕ A m)
extend 0F [] ϱ = ϱ
extend (suc m) (x ∷ ϱ₁) ϱ = x ∷ extend m ϱ₁ ϱ

trec : ∀ {j : Size} {a} {n} {VA : Set a} (ra : RankedAlphabet n) → ((sym : Fin n) → Vec VA (Data.Vec.lookup ra sym) → VA) → Term ra {j} → VA
trec ra g (mk sym₁ subterms) = g sym₁ (Data.Vec.map (trec ra g) subterms)

-- Evaluation
eval : ∀ {j : Size} {ϕ A} → Expr{j} ϕ A → All Value ϕ → Value A
eval (ETerm{sym = sym} x) ϱ   = mk sym (Data.Vec.map (λ exp → eval exp ϱ) x)
eval {j} {ϕ} {A} (ETerm-Rec{n = n}{vec = ra} exprs body) ϱ with eval body ϱ
...          | term = trec {VA = Value A} ra (λ sym₁ ϱ₁ → eval {A = A} (exprs {sym₁}) (extend (Data.Vec.lookup ra sym₁) ϱ₁ ϱ)) term
eval (Var x) ϱ            = access x ϱ
eval (Abs expr) ϱ         = λ x → eval expr (x ∷ ϱ)
eval (App expr expr₁) ϱ   = (eval expr ϱ) (eval expr₁ ϱ)

-- Example: Very tiny subset of propositional logic
-- Σ = {¬, ⊤, ⊥}, α(¬) = 1, α(⊤) = 0, α(⊥) = 0
Σ : Vec ℕ 3
Σ = (1 ∷ 0 ∷ 0 ∷ [])

PropLog : Type
PropLog = TTerm Σ

1≤3 : 1 Data.Nat.< 3
1≤3 = s≤s (s≤s z≤n)

2≤3 : 2 Data.Nat.< 3
2≤3 = s≤s (s≤s (s≤s z≤n))

⊤ : Expr [] PropLog
⊤ = ETerm{n = 3} {sym = fromℕ< {1} {3} 1≤3} []

⊥ : Expr [] PropLog
⊥ = ETerm{n = 3} {sym = fromℕ< {2} {3} 2≤3} []

NegFunc : ∀ {sym : Fin 3} → Expr (bind [] PropLog (Data.Vec.lookup Σ sym)) PropLog
NegFunc {zero}       = Var here
NegFunc {suc zero}       = ⊥
NegFunc {suc (suc zero)} = ⊤

¬⊥ : Expr [] PropLog
¬⊥ = ETerm-Rec{vec = Σ} (λ {sym} → NegFunc {sym}) (ETerm{n = 3} {sym = fromℕ< {0} {3} (s≤s z≤n)} (⊥ ∷ []) )

_ : (eval ¬⊥ []) ≡ (eval ⊤ [])
_ = refl

max_stars_repo_name: kcaliban/ldlc

max_issues_repo_name: kcaliban/ldlc

max_forks_repo_name: kcaliban/ldlc


text:
{-# OPTIONS --no-coverage-check #-}
module FlexibleFunArity where

data Bool : Set where true false : Bool

g : Bool -> Bool -> Bool
g true = \ x -> true
g false true  = false
g false false = true

T : Bool -> Set
T true  = Bool
T false = Bool -> Bool

f : (b : Bool) -> T b
f true = true
f false true  = false
f false false = true

{- checking clause

  f false true

starts with

  f (b : Bool) : T b

splits on b

  f true   -- no match, discard
  f false  -- matches

instantiate type

  f false : T false = Bool -> Bool

extend clause

  f false (y : Bool) : Bool

split on y

  f false true  -- matches
  f false false -- no match, discard

done
-}

{- coverage check starts with

  f (x : Bool)

splits on x

  f true   -- finds clause 1
  f false

NEW: remaing clauses have bigger arity, so expands to

  f false (y : Bool)

splits on y

  f false true  -- finds clause 2
  f false false -- finds clause 3

done
-}

max_stars_repo_name: dagit/agda

max_issues_repo_name: dagit/agda

max_forks_repo_name: dagit/agda


text:
module Data.Empty.Instance where

open import Class.Equality
open import Class.Show
open import Data.Empty

instance
  Empty-Eq : Eq ⊥
  Empty-Eq = record { _≟_ = λ x () }

  Empty-Show : Show ⊥
  Empty-Show = record { show = λ () }

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning
open import Function using (_∘_)
open import Data.Product using (_×_) using (_,_; proj₁; proj₂)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)

postulate
  extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g

β-×₁ : ∀ {A B : Set} (x : A) (y : B) → proj₁ (x , y) ≡ x
β-×₁ x y = refl

β-×₂ : ∀ {A B : Set} (x : A) (y : B) → proj₂ (x , y) ≡ y
β-×₂ x y = refl

η-× : ∀ {A B : Set} (w : A × B) → (proj₁ w , proj₂ w) ≡ w
η-× (x , y) = refl

uniq-× : ∀ {A B C : Set} (h : C → A × B) (v : C) → (proj₁ (h v) , proj₂ (h v)) ≡ h v
uniq-× h v = η-× (h v)

⊎-elim : ∀ {A B C : Set} → (A → C) → (B → C) → (A ⊎ B → C)
⊎-elim f g (inj₁ x) = f x
⊎-elim f g (inj₂ y) = g y

β-⊎₁ : ∀ {A B C : Set} (f : A → C) (g : B → C) (x : A) → ⊎-elim f g (inj₁ x) ≡ f x
β-⊎₁ f g x = refl

β-⊎₂ : ∀ {A B C : Set} (f : A → C) (g : B → C) (y : B) → ⊎-elim f g (inj₂ y) ≡ g y
β-⊎₂ f g x = refl

η-⊎ : ∀ {A B : Set} (w : A ⊎ B) → ⊎-elim inj₁ inj₂ w ≡ w
η-⊎ (inj₁ x) = refl
η-⊎ (inj₂ y) = refl

natural-⊎ : ∀ {A B C D : Set} (f : A → C) (g : B → C) (h : C → D) (w : A ⊎ B) → ⊎-elim (h ∘ f) (h ∘ g) w ≡ (h ∘ ⊎-elim f g) w
natural-⊎ f g h (inj₁ x) = refl
natural-⊎ f g h (inj₂ y) = refl

uniq-⊎ : ∀ {A B C  : Set} (h : A ⊎ B → C) (w : A ⊎ B) → ⊎-elim (h ∘ inj₁) (h ∘ inj₂) w ≡ h w
uniq-⊎ h w rewrite natural-⊎ inj₁ inj₂ h w | η-⊎ w = refl

η-⊤ : ∀ (w : ⊤) → tt ≡ w
η-⊤ tt = refl

uniq-⊤ : ∀ {C : Set} (h : C → ⊤) (v : C) → tt ≡ h v
uniq-⊤ h v = η-⊤ (h v)

η-⊥ : ∀ (w : ⊥) → ⊥-elim w ≡ w
η-⊥ ()

natural-⊥ : ∀ {C D : Set} (h : C → D) (w : ⊥) → ⊥-elim w ≡ (h ∘ ⊥-elim) w
natural-⊥ h ()

uniq-⊥ : ∀ {C : Set} (h : ⊥ → C) (w : ⊥) → ⊥-elim w ≡ h w
uniq-⊥ h w rewrite natural-⊥ h w | η-⊥ w = refl

η-→ : ∀ {A B : Set} (f : A → B) → (λ{x → f x}) ≡ f
η-→ {A} {B} f = extensionality η-helper
  where
  η-lhs : A → B
  η-lhs = λ{x → f x}

  η-helper : (x : A) → η-lhs x ≡ f x
  η-helper x = refl


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

module Data.Binary.Operations.Subtraction where

open import Data.Binary.Definitions
open import Data.Product as Product using (map₁; map₂; proj₁; proj₂; _,_; _×_)
open import Data.Bool
import Data.Maybe as Maybe
import Data.Binary.Operations.Addition as +
open import Data.Binary.Operations.Unary

infixr 5 Is_∷_ O∷_
Is_∷_ : Bit → 𝔹± → 𝔹±
Is s ∷ xs = 0< Maybe.maybe′ (map₂ (I ∷_)) (s , 1ᵇ) xs

O∷_ : 𝔹± → 𝔹±
O∷_ = Maybe.map (map₂ (O ∷_))

mutual
  sub₀ : 𝔹⁺ → 𝔹⁺ → 𝔹±
  sub₀ 1ᵇ ys = Maybe.map (I ,_) (dec⁺ ys)
  sub₀ (x ∷ xs) 1ᵇ = 0< (O , dec⁺⁺ x xs)
  sub₀ (O ∷ xs) (O ∷ ys) = O∷ sub₀ xs ys
  sub₀ (O ∷ xs) (I ∷ ys) = Is I ∷ sub₁ xs ys
  sub₀ (I ∷ xs) (O ∷ ys) = Is O ∷ sub₀ xs ys
  sub₀ (I ∷ xs) (I ∷ ys) = O∷ sub₀ xs ys

  sub₁ : 𝔹⁺ → 𝔹⁺ → 𝔹±
  sub₁ 1ᵇ ys = 0< (I , ys)
  sub₁ (O ∷ xs) (O ∷ ys) = Is I ∷ sub₁ xs ys
  sub₁ (O ∷ xs) (I ∷ ys) = O∷ sub₁ xs ys
  sub₁ (O ∷ 1ᵇ) 1ᵇ = 0ᵇ
  sub₁ (O ∷ x ∷ xs) 1ᵇ = 0< (O , O ∷ dec⁺⁺ x xs)
  sub₁ (I ∷ xs) (O ∷ ys) = O∷ sub₀ xs ys
  sub₁ (I ∷ xs) (I ∷ ys) = Is I ∷ sub₁ xs ys
  sub₁ (I ∷ 1ᵇ) 1ᵇ = 0< (O , 1ᵇ)
  sub₁ (I ∷ x ∷ xs) 1ᵇ = 0< (O , I ∷ dec⁺⁺ x xs)

_+_ : 𝔹± → 𝔹± → 𝔹±
0ᵇ + ys = ys
(0< xs) + 0ᵇ = 0< xs
(0< (O , xs)) + (0< (O , ys)) = 0< (O , +.add O xs ys)
(0< (O , xs)) + (0< (I , ys)) = sub₀ xs ys
(0< (I , xs)) + (0< (O , ys)) = sub₀ ys xs
(0< (I , xs)) + (0< (I , ys)) = 0< (I , +.add O xs ys)

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


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

open import Agda.Builtin.Equality

postulate f : Set₁ → Set₁

module _ (A : Set) where
  postulate rew : f Set ≡ Set

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE rew #-}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module CwF where

open import Setoid
open EqChain

infixr 30 _⇒_
infixl 50 _/_ _/ˢ_
infixr 45 _◄_
infixl 45 _▷_

Cxt : Set
Cxt = Setoid

_⇒_ : Cxt -> Cxt -> Set
Γ ⇒ Δ = El (Γ ==> Δ)

Type : Cxt -> Set
Type Γ = Fam Γ

_/_ : {Γ Δ : Cxt} -> Type Γ -> (Δ ⇒ Γ) -> Type Δ
A / σ = A ○ σ

lem-/id : {Γ : Cxt}{A : Type Γ} -> A / id == A
lem-/id = lem-○-id

Term : (Γ : Cxt) -> Type Γ -> Set
Term Γ A = El (Π Γ A)

_◄_ : {Γ : Cxt}{A B : Type Γ} -> B == A -> Term Γ A -> Term Γ B
B=A ◄ u = eqΠ refl B=A << u

_/ˢ_ : {Γ Δ : Cxt}{A : Type Γ} -> Term Γ A -> (σ : Δ ⇒ Γ) -> Term Δ (A / σ)
u /ˢ σ = u ∘ σ

_▷_ : (Γ : Cxt) -> Type Γ -> Cxt
Γ ▷ A = Σ Γ A

wk : {Γ : Cxt}(A : Type Γ) -> Γ ▷ A ⇒ Γ
wk A = ƛ fst \ x y x=y -> fst-eq x=y

vz : {Γ : Cxt}(A : Type Γ) -> Term (Γ ▷ A) (A / wk A)
vz A = ƛ snd \ x y x=y -> snd-eq x=y

ext : {Γ Δ : Cxt}(A : Type Γ)(σ : Δ ⇒ Γ)(u : Term Δ (A / σ)) -> Δ ⇒ Γ ▷ A
ext A σ u = ƛ (\x -> (σ # x , u # x))
               \x y x=y -> eqInΣ refl (#-cong-R σ x=y) (#-cong-R u x=y)

lem-/-· : {Γ Δ Θ : Cxt}(A : Type Γ)(σ : Δ ⇒ Γ)(δ : Θ ⇒ Δ) ->
          A / σ · δ == A / σ / δ
lem-/-· A σ δ = eqFam refl \x y x=y ->
  !-cong-R A (sym (cast-id' _ (#-cong-R σ (#-cong-R δ (cast-id' _ (sym x=y))))))

lem-wk-∘-ext : {Γ Δ : Cxt}(A : Type Δ)(σ : Γ ⇒ Δ)(u : Term Γ (A / σ)) ->
            wk A ∘ ext A σ u == σ
lem-wk-∘-ext A (ƛ σ pσ) u = eqInΠ refl pσ

lem-vz-/-ext : {Γ Δ : Cxt}(A : Type Δ)(σ : Γ ⇒ Δ)(u : Term Γ (A / σ)) ->
               vz A /ˢ (ext A σ u) == u
lem-vz-/-ext A σ (ƛ u pu) = eqInΠ refl pu

-- (σ , u) ∘ δ == (σ ∘ δ , u / δ)
lem-ext-∘ : {Γ Δ Θ : Cxt}{A : Type Γ}(σ : Δ ⇒ Γ)(δ : Θ ⇒ Δ)(u : Term Δ (A / σ)) ->
            ext A σ u · δ == ext A (σ · δ) (lem-/-· A σ δ ◄ u /ˢ δ)
lem-ext-∘ σ δ u = eqInΠ refl \x y x=y ->
  eqInΣ refl
    (cast-irr _ _ (#-cong-R σ (#-cong-R δ (cast-irr _ _ x=y))))
    (cast-irr _ _ (#-cong-R u (#-cong-R δ (cast-irr _ _ x=y))))

<_> : {Γ : Cxt}{A : Type Γ} -> Term Γ A -> Γ ⇒ Γ ▷ A
< u > = ext _ id (lem-○-id ◄ u)

lift : {Γ Δ : Cxt}(A : Type Γ)(σ : Δ ⇒ Γ) -> Δ ▷ (A / σ) ⇒ Γ ▷ A
lift A σ = ƛ (\x -> σ # fst x , snd x)
              \x y x=y -> eqInΣ refl (#-cong-R σ (fst-eq x=y)) (snd-eq x=y)

curryFam : {A : Setoid}{F : Fam A} -> Fam (Σ A F) -> (x : El A) -> Fam (F ! x)
curryFam G x = fam (\y -> G ! (x , y))
                   \z w z=w -> !-cong-R G (eqInΣ refl refl z=w)

Pi : {Γ : Cxt}(A : Type Γ)(B : Type (Γ ▷ A)) -> Type Γ
Pi A B = fam (\x -> Π (A ! x) (curryFam B x))
              \x y x=y ->
                eqΠ (!-cong-R A (sym x=y))
                    (eqFam (!-cong-R A (sym x=y)) \z w z=w ->
                            !-cong-R B (eqInΣ refl x=y z=w)
                    )

lem-Pi-/ : {Γ Δ : Cxt}(A : Type Γ)(B : Type (Γ ▷ A))(σ : Δ ⇒ Γ) ->
           Pi A B / σ == Pi (A / σ) (B / lift A σ)
lem-Pi-/ A B σ = eqFam refl \x y x=y ->
  eqΠ (Aσ-eq x=y)
      (eqFam (Aσ-eq x=y) \z w z=w ->
        !-cong-R B (eqInΣ refl (#-cong-R σ x=y) z=w)
      )
  where
    Aσ-eq : forall {x y} -> x == y -> A ! σ # y == A ! σ # x
    Aσ-eq x=y = !-cong-R A (#-cong-R σ (sym x=y))

lam : {Γ : Cxt}{A : Type Γ}{B : Type (Γ ▷ A)} -> Term (Γ ▷ A) B -> Term Γ (Pi A B)
lam {A = A} f =
  ƛ (\γ -> ƛ (\x -> f # (γ , x)) (prf₁ γ)) prf₂
  where
      prf₁ : forall γ x y x=y -> _
      prf₁ = \γ x y x=y -> #-cong-R f (eqInΣ refl refl x=y)

      prf₂ = \x y x=y ->
        eqInΠ (!-cong-R A (sym x=y)) \z w z=w ->
          #-cong-R f (eqInΣ refl x=y z=w)

app : {Γ : Cxt}(A : Type Γ)(B : Type (Γ ▷ A))
      (v : Term Γ (Pi A B))(u : Term Γ A) -> Term Γ (B / < u >)
app A B v u = ƛ (\γ -> prf₁ γ << v # γ # (u # γ)) prf₂
  where
      lem : forall γ -> < u > # γ == (γ , u # γ)
      lem γ = eqInΣ refl refl (#-cong (lem-○-id ◄ u) u (sym (cast-id _)) refl)

      prf₁ : forall γ -> (B / < u >) ! γ == B ! (γ , u # γ)
      prf₁ γ = !-cong-R B (lem γ)

      prf₂ = \x y x=y -> cast-irr _ _ (#-cong (v # x) (v # y)
                                              (#-cong-R v x=y)
                                              (#-cong-R u x=y)
                                      )

lem-β : {Γ : Cxt}(A : Type Γ)(B : Type (Γ ▷ A))
        (v : Term (Γ ▷ A) B)(u : Term Γ A) ->
        app A B (lam v) u == v /ˢ < u >
lem-β A B v u = eqInΠ refl \x y x=y ->
  sym (cast-id' _
    (#-cong-R v
      (eqInΣ refl (sym x=y)
        (#-cong (lem-○-id ◄ u) u (sym (cast-id _)) (sym x=y)))
      )
    )

-- The stack blows when trying to prove η.
-- I'm not sure it does anymore, but I have no idea how to prove η,
-- I struggled just giving the type.
-- lem-η : {Γ : Cxt}(A : Type Γ)(B : Type (Γ ▷ A))
--         (v : Term Γ (Pi A B)) →
--         v == lam (app (A / wk A) (B / lift A (wk A)) (sym (lem-Pi-/ A B (wk A)) ◄ v /ˢ wk A) (vz A))
-- lem-η {Γ} A B (ƛ f pf) =
--   eqInΠ =S=-refl λ γ δ γ=δ →
--   proof f γ ≡ ƛ (_#_ (f γ)) (λ _ _ → #-cong-R (f γ)) by η (f γ)
--             ≡ _ by eqInΠ (!-cong-R A (sym γ=δ)) (λ x y x=y →
--     proof f γ # x
--       ≡ (_ << (_ << f (_ << δ))) # y by {!!}
--     qed)
--   qed

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import HoTT
open import cohomology.Exactness
open import cohomology.FunctionOver
open import cohomology.Theory
open import cohomology.CofiberSequence

module cohomology.LongExactSequence {i} (CT : CohomologyTheory i)
  {X Y : Ptd i} (n : ℤ) (f : fst (X ⊙→ Y)) where

open CohomologyTheory CT
open import cohomology.Functor CT
open import cohomology.BaseIndependence CT

co∂ : C n X →ᴳ C (succ n) (⊙Cof f)
co∂ = CF-hom (succ n) ⊙ext-glue ∘ᴳ fst ((C-Susp n X)⁻¹ᴳ)

long-cofiber-seq : HomSequence _ _
long-cofiber-seq =
  C n Y                ⟨ CF-hom n f                 ⟩→
  C n X                ⟨ co∂                        ⟩→
  C (succ n) (⊙Cof f)  ⟨ CF-hom (succ n) (⊙cfcod f) ⟩→
  C (succ n) Y         ⟨ CF-hom (succ n) f          ⟩→
  C (succ n) X         ⊣|

long-cofiber-exact : is-exact-seq long-cofiber-seq
long-cofiber-exact =
  {- apply the suspension isomorphism -}
  transport
    (λ {(r , s) → is-exact-seq s})
    (pair= _ $ sequence= _ _ $
      group-ua (C-Susp n Y)
        ∥⟨ C-Susp-↓ n f ⟩∥
      group-ua (C-Susp n X)
        ∥⟨ ↓-over-×-in _→ᴳ_
             (domain-over-iso
               (λ= (! ∘ ap (GroupHom.f (CF-hom _ ⊙ext-glue))
                      ∘ is-equiv.g-f (snd (C-Susp n X)))
                ◃ domain-over-equiv _ _))
             idp ⟩∥
      idp    ∥⟨ idp ⟩∥
      idp    ∥⟨ idp ⟩∥
      idp    ∥⊣|)
    {- fix the function basepoints -}
    (transport
      (λ {(φ , ψ) → is-exact-seq $
        _ ⟨ φ ⟩→ _ ⟨ ψ ⟩→
        _ ⟨ CF-hom (succ n) (⊙cfcod f) ⟩→ _ ⟨ CF-hom (succ n) f ⟩→ _ ⊣|})
      (pair×= (CF-base-indep (succ n) _ _ _)
              (CF-base-indep (succ n) _ _ _))
      {- do the CofiberSequence transport -}
      (transport {A = Σ _ (λ {((U , V) , g , h) →
                        (g (cfbase _) == snd U) × (h (snd U) == snd V)})}
        (λ {((_ , g , h) , (p , q)) → is-exact-seq $
          _ ⟨ CF-hom (succ n) (h , q) ⟩→ _ ⟨ CF-hom (succ n) (g , p) ⟩→
          _ ⟨ CF-hom (succ n) (⊙cfcod f) ⟩→ _ ⟨ CF-hom (succ n) f ⟩→ _ ⊣|})
        (pair= (cofiber-sequence f)
               (↓-×-in (from-transp _ _ idp) (from-transp _ _ idp)))
        (exact-build
          (_ ⟨ CF-hom (succ n) (⊙cfcod³ f) ⟩→ _ ⟨ CF-hom (succ n) (⊙cfcod² f) ⟩→
           _ ⟨ CF-hom (succ n) (⊙cfcod f) ⟩→ _ ⟨ CF-hom (succ n) f ⟩→ _ ⊣|)
          (C-exact (succ n) (⊙cfcod² f))
          (C-exact (succ n) (⊙cfcod f)) (C-exact (succ n) f))))

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
open import Prelude
open import Nat
open import dynamics-core
open import contexts
open import disjointness

-- this module contains lemmas and properties about the holes-disjoint
-- judgement that double check that it acts as we would expect

module holes-disjoint-checks where
  -- these lemmas are all structurally recursive and quite
  -- mechanical. morally, they establish the properties about reduction
  -- that would be obvious / baked into Agda if holes-disjoint was defined
  -- as a function rather than a judgement (datatype), or if we had defined
  -- all the O(n^2) cases rather than relying on a little indirection to
  -- only have O(n) cases. that work has to go somewhwere, and we prefer
  -- that it goes here.
  ds-lem-num  : ∀{e n} → holes-disjoint e (N n)
  ds-lem-num {N x} = HDNum
  ds-lem-num {e ·+ e₁} = HDPlus ds-lem-num ds-lem-num
  ds-lem-num {e ·: x} = HDAsc ds-lem-num
  ds-lem-num {X x} = HDVar
  ds-lem-num {·λ x e} = HDLam1 ds-lem-num
  ds-lem-num {·λ x ·[ x₁ ] e} = HDLam2 ds-lem-num
  ds-lem-num {e ∘ e₁} = HDAp ds-lem-num ds-lem-num
  ds-lem-num {inl e} = HDInl ds-lem-num
  ds-lem-num {inr e} = HDInr ds-lem-num
  ds-lem-num {case e x e₁ x₁ e₂} = HDCase ds-lem-num ds-lem-num ds-lem-num
  ds-lem-num {⟨ e , e₁ ⟩} = HDPair ds-lem-num ds-lem-num
  ds-lem-num {fst e} = HDFst ds-lem-num
  ds-lem-num {snd e} = HDSnd ds-lem-num
  ds-lem-num {⦇-⦈[ x ]} = HDHole HNNum
  ds-lem-num {⦇⌜ e ⌟⦈[ x ]} = HDNEHole HNNum ds-lem-num

  ds-lem-plus : ∀{e1 e2 e3} → holes-disjoint e3 e1 → holes-disjoint e3 e2 → holes-disjoint e3 (e1 ·+ e2)
  ds-lem-plus HDNum ν = HDNum
  ds-lem-plus (HDPlus hd hd₁) (HDPlus ν ν₁) = HDPlus (ds-lem-plus hd ν) (ds-lem-plus hd₁ ν₁)
  ds-lem-plus (HDAsc hd) (HDAsc ν) = HDAsc (ds-lem-plus hd ν)
  ds-lem-plus HDVar HDVar = HDVar
  ds-lem-plus (HDLam1 hd) (HDLam1 ν) = HDLam1 (ds-lem-plus hd ν)
  ds-lem-plus (HDLam2 hd) (HDLam2 ν) = HDLam2 (ds-lem-plus hd ν)
  ds-lem-plus (HDAp hd hd₁) (HDAp ν ν₁) = HDAp (ds-lem-plus hd ν) (ds-lem-plus hd₁ ν₁)
  ds-lem-plus (HDInl hd) (HDInl ν) = HDInl (ds-lem-plus hd ν)
  ds-lem-plus (HDInr hd) (HDInr ν) = HDInr (ds-lem-plus hd ν)
  ds-lem-plus (HDCase hd hd₁ hd₂) (HDCase ν ν₁ ν₂) = HDCase (ds-lem-plus hd ν) (ds-lem-plus hd₁ ν₁) (ds-lem-plus hd₂ ν₂)
  ds-lem-plus (HDPair hd hd₁) (HDPair ν ν₁) = HDPair (ds-lem-plus hd ν) (ds-lem-plus hd₁ ν₁)
  ds-lem-plus (HDFst hd) (HDFst ν) = HDFst (ds-lem-plus hd ν)
  ds-lem-plus (HDSnd hd) (HDSnd ν) = HDSnd (ds-lem-plus hd ν)
  ds-lem-plus (HDHole x) (HDHole x₁) = HDHole (HNPlus x x₁)
  ds-lem-plus (HDNEHole x hd) (HDNEHole x₁ ν) = HDNEHole (HNPlus x x₁) (ds-lem-plus hd ν)

  ds-lem-var : ∀{e x} → holes-disjoint e (X x)
  ds-lem-var {N x} = HDNum
  ds-lem-var {e ·+ e₁} = HDPlus ds-lem-var ds-lem-var
  ds-lem-var {e ·: x} = HDAsc ds-lem-var
  ds-lem-var {X x} = HDVar
  ds-lem-var {·λ x e} = HDLam1 ds-lem-var
  ds-lem-var {·λ x ·[ x₁ ] e} = HDLam2 ds-lem-var
  ds-lem-var {e ∘ e₁} = HDAp ds-lem-var ds-lem-var
  ds-lem-var {inl e} = HDInl ds-lem-var
  ds-lem-var {inr e} = HDInr ds-lem-var
  ds-lem-var {case e x e₁ x₁ e₂} = HDCase ds-lem-var ds-lem-var ds-lem-var
  ds-lem-var {⟨ e , e₁ ⟩} = HDPair ds-lem-var ds-lem-var
  ds-lem-var {fst e} = HDFst ds-lem-var
  ds-lem-var {snd e} = HDSnd ds-lem-var
  ds-lem-var {⦇-⦈[ x ]} = HDHole HNVar
  ds-lem-var {⦇⌜ e ⌟⦈[ x ]} = HDNEHole HNVar ds-lem-var

  ds-lem-asc : ∀{e1 e2 τ} → holes-disjoint e2 e1 → holes-disjoint e2 (e1 ·: τ)
  ds-lem-asc HDNum = HDNum
  ds-lem-asc (HDPlus hd hd₁) = HDPlus (ds-lem-asc hd) (ds-lem-asc hd₁)
  ds-lem-asc (HDAsc hd) = HDAsc (ds-lem-asc hd)
  ds-lem-asc HDVar = HDVar
  ds-lem-asc (HDLam1 hd) = HDLam1 (ds-lem-asc hd)
  ds-lem-asc (HDLam2 hd) = HDLam2 (ds-lem-asc hd)
  ds-lem-asc (HDAp hd hd₁) = HDAp (ds-lem-asc hd) (ds-lem-asc hd₁)
  ds-lem-asc (HDInl hd) = HDInl (ds-lem-asc hd)
  ds-lem-asc (HDInr hd) = HDInr (ds-lem-asc hd)
  ds-lem-asc (HDCase hd hd₁ hd₂) = HDCase (ds-lem-asc hd) (ds-lem-asc hd₁) (ds-lem-asc hd₂)
  ds-lem-asc (HDPair hd hd₁) = HDPair (ds-lem-asc hd) (ds-lem-asc hd₁)
  ds-lem-asc (HDFst hd) = HDFst (ds-lem-asc hd)
  ds-lem-asc (HDSnd hd) = HDSnd (ds-lem-asc hd)
  ds-lem-asc (HDHole x) = HDHole (HNAsc x)
  ds-lem-asc (HDNEHole x hd) = HDNEHole (HNAsc x) (ds-lem-asc hd)

  ds-lem-lam1 : ∀{e1 e2 x} → holes-disjoint e2 e1 → holes-disjoint e2 (·λ x e1)
  ds-lem-lam1 HDNum = HDNum
  ds-lem-lam1 (HDPlus hd hd₁) = HDPlus (ds-lem-lam1 hd) (ds-lem-lam1 hd₁)
  ds-lem-lam1 (HDAsc hd) = HDAsc (ds-lem-lam1 hd)
  ds-lem-lam1 HDVar = HDVar
  ds-lem-lam1 (HDLam1 hd) = HDLam1 (ds-lem-lam1 hd)
  ds-lem-lam1 (HDLam2 hd) = HDLam2 (ds-lem-lam1 hd)
  ds-lem-lam1 (HDAp hd hd₁) = HDAp (ds-lem-lam1 hd) (ds-lem-lam1 hd₁)
  ds-lem-lam1 (HDInl hd) = HDInl (ds-lem-lam1 hd)
  ds-lem-lam1 (HDInr hd) = HDInr (ds-lem-lam1 hd)
  ds-lem-lam1 (HDCase hd hd₁ hd₂) = HDCase (ds-lem-lam1 hd) (ds-lem-lam1 hd₁) (ds-lem-lam1 hd₂)
  ds-lem-lam1 (HDPair hd hd₁) = HDPair (ds-lem-lam1 hd) (ds-lem-lam1 hd₁)
  ds-lem-lam1 (HDFst hd) = HDFst (ds-lem-lam1 hd)
  ds-lem-lam1 (HDSnd hd) = HDSnd (ds-lem-lam1 hd)
  ds-lem-lam1 (HDHole x₁) = HDHole (HNLam1 x₁)
  ds-lem-lam1 (HDNEHole x₁ hd) = HDNEHole (HNLam1 x₁) (ds-lem-lam1 hd)

  ds-lem-lam2 : ∀{e1 e2 x τ} → holes-disjoint e2 e1 → holes-disjoint e2 (·λ x ·[ τ ] e1)
  ds-lem-lam2 HDNum = HDNum
  ds-lem-lam2 (HDPlus hd hd₁) = HDPlus (ds-lem-lam2 hd) (ds-lem-lam2 hd₁)
  ds-lem-lam2 (HDAsc hd) = HDAsc (ds-lem-lam2 hd)
  ds-lem-lam2 HDVar = HDVar
  ds-lem-lam2 (HDLam1 hd) = HDLam1 (ds-lem-lam2 hd)
  ds-lem-lam2 (HDLam2 hd) = HDLam2 (ds-lem-lam2 hd)
  ds-lem-lam2 (HDAp hd hd₁) = HDAp (ds-lem-lam2 hd) (ds-lem-lam2 hd₁)
  ds-lem-lam2 (HDInl hd) = HDInl (ds-lem-lam2 hd)
  ds-lem-lam2 (HDInr hd) = HDInr (ds-lem-lam2 hd)
  ds-lem-lam2 (HDCase hd hd₁ hd₂) = HDCase (ds-lem-lam2 hd) (ds-lem-lam2 hd₁) (ds-lem-lam2 hd₂)
  ds-lem-lam2 (HDPair hd hd₁) = HDPair (ds-lem-lam2 hd) (ds-lem-lam2 hd₁)
  ds-lem-lam2 (HDFst hd) = HDFst (ds-lem-lam2 hd)
  ds-lem-lam2 (HDSnd hd) = HDSnd (ds-lem-lam2 hd)
  ds-lem-lam2 (HDHole x₁) = HDHole (HNLam2 x₁)
  ds-lem-lam2 (HDNEHole x₁ hd) = HDNEHole (HNLam2 x₁) (ds-lem-lam2 hd)

  ds-lem-ap : ∀{e1 e2 e3} → holes-disjoint e3 e1 → holes-disjoint e3 e2 → holes-disjoint e3 (e1 ∘ e2)
  ds-lem-ap HDNum hd2 = HDNum
  ds-lem-ap (HDPlus hd1 hd2) (HDPlus hd3 hd4) = HDPlus (ds-lem-ap hd1 hd3) (ds-lem-ap hd2 hd4)
  ds-lem-ap (HDAsc hd1) (HDAsc hd2) = HDAsc (ds-lem-ap hd1 hd2)
  ds-lem-ap HDVar hd2 = HDVar
  ds-lem-ap (HDLam1 hd1) (HDLam1 hd2) = HDLam1 (ds-lem-ap hd1 hd2)
  ds-lem-ap (HDLam2 hd1) (HDLam2 hd2) = HDLam2 (ds-lem-ap hd1 hd2)
  ds-lem-ap (HDAp hd1 hd2) (HDAp hd3 hd4) = HDAp (ds-lem-ap hd1 hd3) (ds-lem-ap hd2 hd4)
  ds-lem-ap (HDInl hd) (HDInl ν) = HDInl (ds-lem-ap hd ν)
  ds-lem-ap (HDInr hd) (HDInr ν) = HDInr (ds-lem-ap hd ν)
  ds-lem-ap (HDCase hd hd₁ hd₂) (HDCase ν ν₁ ν₂) = HDCase (ds-lem-ap hd ν) (ds-lem-ap hd₁ ν₁) (ds-lem-ap hd₂ ν₂)
  ds-lem-ap (HDPair hd hd₁) (HDPair ν ν₁) = HDPair (ds-lem-ap hd ν) (ds-lem-ap hd₁ ν₁)
  ds-lem-ap (HDFst hd) (HDFst ν) = HDFst (ds-lem-ap hd ν)
  ds-lem-ap (HDSnd hd) (HDSnd ν) = HDSnd (ds-lem-ap hd ν)
  ds-lem-ap (HDHole x) (HDHole x₁) = HDHole (HNAp x x₁)
  ds-lem-ap (HDNEHole x hd1) (HDNEHole x₁ hd2) = HDNEHole (HNAp x x₁) (ds-lem-ap hd1 hd2)

  ds-lem-inl : ∀{e1 e2} → holes-disjoint e2 e1 → holes-disjoint e2 (inl e1)
  ds-lem-inl HDNum = HDNum
  ds-lem-inl (HDPlus hd hd₁) = HDPlus (ds-lem-inl hd) (ds-lem-inl hd₁)
  ds-lem-inl (HDAsc hd) = HDAsc (ds-lem-inl hd)
  ds-lem-inl HDVar = HDVar
  ds-lem-inl (HDLam1 hd) = HDLam1 (ds-lem-inl hd)
  ds-lem-inl (HDLam2 hd) = HDLam2 (ds-lem-inl hd)
  ds-lem-inl (HDAp hd hd₁) = HDAp (ds-lem-inl hd) (ds-lem-inl hd₁)
  ds-lem-inl (HDInl hd) = HDInl (ds-lem-inl hd)
  ds-lem-inl (HDInr hd) = HDInr (ds-lem-inl hd)
  ds-lem-inl (HDCase hd hd₁ hd₂) = HDCase (ds-lem-inl hd) (ds-lem-inl hd₁) (ds-lem-inl hd₂)
  ds-lem-inl (HDPair hd hd₁) = HDPair (ds-lem-inl hd) (ds-lem-inl hd₁)
  ds-lem-inl (HDFst hd) = HDFst (ds-lem-inl hd)
  ds-lem-inl (HDSnd hd) = HDSnd (ds-lem-inl hd)
  ds-lem-inl (HDHole x) = HDHole (HNInl x)
  ds-lem-inl (HDNEHole x hd) = HDNEHole (HNInl x) (ds-lem-inl hd)

  ds-lem-inr : ∀{e1 e2} → holes-disjoint e2 e1 → holes-disjoint e2 (inr e1)
  ds-lem-inr HDNum = HDNum
  ds-lem-inr (HDPlus hd hd₁) = HDPlus (ds-lem-inr hd) (ds-lem-inr hd₁)
  ds-lem-inr (HDAsc hd) = HDAsc (ds-lem-inr hd)
  ds-lem-inr HDVar = HDVar
  ds-lem-inr (HDLam1 hd) = HDLam1 (ds-lem-inr hd)
  ds-lem-inr (HDLam2 hd) = HDLam2 (ds-lem-inr hd)
  ds-lem-inr (HDAp hd hd₁) = HDAp (ds-lem-inr hd) (ds-lem-inr hd₁)
  ds-lem-inr (HDInl hd) = HDInl (ds-lem-inr hd)
  ds-lem-inr (HDInr hd) = HDInr (ds-lem-inr hd)
  ds-lem-inr (HDCase hd hd₁ hd₂) = HDCase (ds-lem-inr hd) (ds-lem-inr hd₁) (ds-lem-inr hd₂)
  ds-lem-inr (HDPair hd hd₁) = HDPair (ds-lem-inr hd) (ds-lem-inr hd₁)
  ds-lem-inr (HDFst hd) = HDFst (ds-lem-inr hd)
  ds-lem-inr (HDSnd hd) = HDSnd (ds-lem-inr hd)
  ds-lem-inr (HDHole x) = HDHole (HNInr x)
  ds-lem-inr (HDNEHole x hd) = HDNEHole (HNInr x) (ds-lem-inr hd)

  ds-lem-case : ∀{e3 e x e1 y e2} → holes-disjoint e3 e → holes-disjoint e3 e1 → holes-disjoint e3 e2 → holes-disjoint e3 (case e x e1 y e2)
  ds-lem-case HDNum HDNum HDNum = HDNum
  ds-lem-case (HDPlus hd hd₁) (HDPlus ν ν₂) (HDPlus ν₁ ν₃) = HDPlus (ds-lem-case hd ν ν₁) (ds-lem-case hd₁ ν₂ ν₃)
  ds-lem-case (HDAsc hd) (HDAsc ν) (HDAsc ν₁) = HDAsc (ds-lem-case hd ν ν₁)
  ds-lem-case HDVar HDVar HDVar = HDVar
  ds-lem-case (HDLam1 hd) (HDLam1 ν) (HDLam1 ν₁) = HDLam1 (ds-lem-case hd ν ν₁)
  ds-lem-case (HDLam2 hd) (HDLam2 ν) (HDLam2 ν₁) = HDLam2 (ds-lem-case hd ν ν₁)
  ds-lem-case (HDAp hd hd₁) (HDAp ν ν₁) (HDAp ν₂ ν₃) = HDAp (ds-lem-case hd ν ν₂) (ds-lem-case hd₁ ν₁ ν₃)
  ds-lem-case (HDInl hd) (HDInl ν) (HDInl ν₁) = HDInl (ds-lem-case hd ν ν₁)
  ds-lem-case (HDInr hd) (HDInr ν) (HDInr ν₁) = HDInr (ds-lem-case hd ν ν₁)
  ds-lem-case (HDCase hd hd₁ hd₂) (HDCase ν ν₁ ν₂) (HDCase ν₃ ν₄ ν₅) = HDCase (ds-lem-case hd ν ν₃) (ds-lem-case hd₁ ν₁ ν₄) (ds-lem-case hd₂ ν₂ ν₅)
  ds-lem-case (HDPair hd hd₁) (HDPair ν ν₁) (HDPair ν₂ ν₃) = HDPair (ds-lem-case hd ν ν₂) (ds-lem-case hd₁ ν₁ ν₃)
  ds-lem-case (HDFst hd) (HDFst ν) (HDFst ν₁) = HDFst (ds-lem-case hd ν ν₁)
  ds-lem-case (HDSnd hd) (HDSnd ν) (HDSnd ν₁) = HDSnd (ds-lem-case hd ν ν₁)
  ds-lem-case (HDHole x) (HDHole x₁) (HDHole x₂) = HDHole (HNCase x x₁ x₂)
  ds-lem-case (HDNEHole x hd) (HDNEHole x₁ ν) (HDNEHole x₂ ν₁) = HDNEHole (HNCase x x₁ x₂) (ds-lem-case hd ν ν₁)

  ds-lem-pair : ∀{e1 e2 e3} → holes-disjoint e3 e1 → holes-disjoint e3 e2 → holes-disjoint e3 ⟨ e1 , e2 ⟩
  ds-lem-pair HDNum HDNum = HDNum
  ds-lem-pair (HDPlus hd hd₁) (HDPlus ν ν₁) = HDPlus (ds-lem-pair hd ν) (ds-lem-pair hd₁ ν₁)
  ds-lem-pair (HDAsc hd) (HDAsc ν) = HDAsc (ds-lem-pair hd ν)
  ds-lem-pair HDVar HDVar = HDVar
  ds-lem-pair (HDLam1 hd) (HDLam1 ν) = HDLam1 (ds-lem-pair hd ν)
  ds-lem-pair (HDLam2 hd) (HDLam2 ν) = HDLam2 (ds-lem-pair hd ν)
  ds-lem-pair (HDAp hd hd₁) (HDAp ν ν₁) = HDAp (ds-lem-pair hd ν) (ds-lem-pair hd₁ ν₁)
  ds-lem-pair (HDInl hd) (HDInl ν) = HDInl (ds-lem-pair hd ν)
  ds-lem-pair (HDInr hd) (HDInr ν) = HDInr (ds-lem-pair hd ν)
  ds-lem-pair (HDCase hd hd₁ hd₂) (HDCase ν ν₁ ν₂) = HDCase (ds-lem-pair hd ν) (ds-lem-pair hd₁ ν₁) (ds-lem-pair hd₂ ν₂)
  ds-lem-pair (HDPair hd hd₁) (HDPair ν ν₁) = HDPair (ds-lem-pair hd ν) (ds-lem-pair hd₁ ν₁)
  ds-lem-pair (HDFst hd) (HDFst ν) = HDFst (ds-lem-pair hd ν)
  ds-lem-pair (HDSnd hd) (HDSnd ν) = HDSnd (ds-lem-pair hd ν)
  ds-lem-pair (HDHole x) (HDHole x₁) = HDHole (HNPair x x₁)
  ds-lem-pair (HDNEHole x hd) (HDNEHole x₁ ν) = HDNEHole (HNPair x x₁) (ds-lem-pair hd ν)

  ds-lem-fst : ∀{e1 e2} → holes-disjoint e2 e1 → holes-disjoint e2 (fst e1)
  ds-lem-fst HDNum = HDNum
  ds-lem-fst (HDPlus hd hd₁) = HDPlus (ds-lem-fst hd) (ds-lem-fst hd₁)
  ds-lem-fst (HDAsc hd) = HDAsc (ds-lem-fst hd)
  ds-lem-fst HDVar = HDVar
  ds-lem-fst (HDLam1 hd) = HDLam1 (ds-lem-fst hd)
  ds-lem-fst (HDLam2 hd) = HDLam2 (ds-lem-fst hd)
  ds-lem-fst (HDAp hd hd₁) = HDAp (ds-lem-fst hd) (ds-lem-fst hd₁)
  ds-lem-fst (HDInl hd) = HDInl (ds-lem-fst hd)
  ds-lem-fst (HDInr hd) = HDInr (ds-lem-fst hd)
  ds-lem-fst (HDCase hd hd₁ hd₂) = HDCase (ds-lem-fst hd) (ds-lem-fst hd₁) (ds-lem-fst hd₂)
  ds-lem-fst (HDPair hd hd₁) = HDPair (ds-lem-fst hd) (ds-lem-fst hd₁)
  ds-lem-fst (HDFst hd) = HDFst (ds-lem-fst hd)
  ds-lem-fst (HDSnd hd) = HDSnd (ds-lem-fst hd)
  ds-lem-fst (HDHole x) = HDHole (HNFst x)
  ds-lem-fst (HDNEHole x hd) = HDNEHole (HNFst x) (ds-lem-fst hd)

  ds-lem-snd : ∀{e1 e2} → holes-disjoint e2 e1 → holes-disjoint e2 (snd e1)
  ds-lem-snd HDNum = HDNum
  ds-lem-snd (HDPlus hd hd₁) = HDPlus (ds-lem-snd hd) (ds-lem-snd hd₁)
  ds-lem-snd (HDAsc hd) = HDAsc (ds-lem-snd hd)
  ds-lem-snd HDVar = HDVar
  ds-lem-snd (HDLam1 hd) = HDLam1 (ds-lem-snd hd)
  ds-lem-snd (HDLam2 hd) = HDLam2 (ds-lem-snd hd)
  ds-lem-snd (HDAp hd hd₁) = HDAp (ds-lem-snd hd) (ds-lem-snd hd₁)
  ds-lem-snd (HDInl hd) = HDInl (ds-lem-snd hd)
  ds-lem-snd (HDInr hd) = HDInr (ds-lem-snd hd)
  ds-lem-snd (HDCase hd hd₁ hd₂) = HDCase (ds-lem-snd hd) (ds-lem-snd hd₁) (ds-lem-snd hd₂)
  ds-lem-snd (HDPair hd hd₁) = HDPair (ds-lem-snd hd) (ds-lem-snd hd₁)
  ds-lem-snd (HDFst hd) = HDFst (ds-lem-snd hd)
  ds-lem-snd (HDSnd hd) = HDSnd (ds-lem-snd hd)
  ds-lem-snd (HDHole x) = HDHole (HNSnd x)
  ds-lem-snd (HDNEHole x hd) = HDNEHole (HNSnd x) (ds-lem-snd hd)

  ds-lem-hole : ∀{e u} → hole-name-new e u → holes-disjoint e ⦇-⦈[ u ]
  ds-lem-hole HNNum = HDNum
  ds-lem-hole (HNPlus hnn hnn₁) = HDPlus (ds-lem-hole hnn) (ds-lem-hole hnn₁)
  ds-lem-hole (HNAsc hnn) = HDAsc (ds-lem-hole hnn)
  ds-lem-hole HNVar = HDVar
  ds-lem-hole (HNLam1 hnn) = HDLam1 (ds-lem-hole hnn)
  ds-lem-hole (HNLam2 hnn) = HDLam2 (ds-lem-hole hnn)
  ds-lem-hole (HNAp hnn hnn₁) = HDAp (ds-lem-hole hnn) (ds-lem-hole hnn₁)
  ds-lem-hole (HNInl hnn) = HDInl (ds-lem-hole hnn)
  ds-lem-hole (HNInr hnn) = HDInr (ds-lem-hole hnn)
  ds-lem-hole (HNCase hnn hnn₁ hnn₂) = HDCase (ds-lem-hole hnn) (ds-lem-hole hnn₁) (ds-lem-hole hnn₂)
  ds-lem-hole (HNPair hn hn₁) = HDPair (ds-lem-hole hn) (ds-lem-hole hn₁)
  ds-lem-hole (HNFst hn) = HDFst (ds-lem-hole hn)
  ds-lem-hole (HNSnd hn) = HDSnd (ds-lem-hole hn)
  ds-lem-hole (HNHole x) = HDHole (HNHole (flip x))
  ds-lem-hole (HNNEHole x hnn) = HDNEHole (HNHole (flip x)) (ds-lem-hole hnn)

  ds-lem-nehole : ∀{e e1 u} →
                  holes-disjoint e e1 →
                  hole-name-new e u →
                  holes-disjoint e ⦇⌜ e1 ⌟⦈[ u ]
  ds-lem-nehole HDNum ν = HDNum
  ds-lem-nehole (HDPlus hd hd₁) (HNPlus ν ν₁) = HDPlus (ds-lem-nehole hd ν) (ds-lem-nehole hd₁ ν₁)
  ds-lem-nehole (HDAsc hd) (HNAsc ν) = HDAsc (ds-lem-nehole hd ν)
  ds-lem-nehole HDVar ν = HDVar
  ds-lem-nehole (HDLam1 hd) (HNLam1 ν) = HDLam1 (ds-lem-nehole hd ν)
  ds-lem-nehole (HDLam2 hd) (HNLam2 ν) = HDLam2 (ds-lem-nehole hd ν)
  ds-lem-nehole (HDAp hd hd₁) (HNAp ν ν₁) = HDAp (ds-lem-nehole hd ν) (ds-lem-nehole hd₁ ν₁)
  ds-lem-nehole (HDInl hd) (HNInl ν) = HDInl (ds-lem-nehole hd ν)
  ds-lem-nehole (HDInr hd) (HNInr ν) = HDInr (ds-lem-nehole hd ν)
  ds-lem-nehole (HDCase hd hd₁ hd₂) (HNCase ν ν₁ ν₂) = HDCase (ds-lem-nehole hd ν) (ds-lem-nehole hd₁ ν₁) (ds-lem-nehole hd₂ ν₂)
  ds-lem-nehole (HDPair hd hd₁) (HNPair ν ν₁) = HDPair (ds-lem-nehole hd ν) (ds-lem-nehole hd₁ ν₁)
  ds-lem-nehole (HDFst hd) (HNFst ν) = HDFst (ds-lem-nehole hd ν)
  ds-lem-nehole (HDSnd hd) (HNSnd ν) = HDSnd (ds-lem-nehole hd ν)
  ds-lem-nehole (HDHole x) (HNHole x₁) = HDHole (HNNEHole (flip x₁) x)
  ds-lem-nehole (HDNEHole x hd) (HNNEHole x₁ ν) = HDNEHole (HNNEHole (flip x₁) x) (ds-lem-nehole hd ν)

  -- holes-disjoint is symmetric
  disjoint-sym : ∀{e1 e2} → holes-disjoint e1 e2 → holes-disjoint e2 e1
  disjoint-sym HDNum = ds-lem-num
  disjoint-sym (HDPlus hd hd₁) = ds-lem-plus (disjoint-sym hd) (disjoint-sym hd₁)
  disjoint-sym (HDAsc hd) = ds-lem-asc (disjoint-sym hd)
  disjoint-sym HDVar = ds-lem-var
  disjoint-sym (HDLam1 hd) = ds-lem-lam1 (disjoint-sym hd)
  disjoint-sym (HDLam2 hd) = ds-lem-lam2 (disjoint-sym hd)
  disjoint-sym (HDAp hd hd₁) = ds-lem-ap (disjoint-sym hd) (disjoint-sym hd₁)
  disjoint-sym (HDInl hd) = ds-lem-inl (disjoint-sym hd)
  disjoint-sym (HDInr hd) = ds-lem-inr (disjoint-sym hd)
  disjoint-sym (HDCase hd hd₁ hd₂) = ds-lem-case (disjoint-sym hd) (disjoint-sym hd₁) (disjoint-sym hd₂)
  disjoint-sym (HDPair hd hd₁) = ds-lem-pair (disjoint-sym hd) (disjoint-sym hd₁)
  disjoint-sym (HDFst hd) = ds-lem-fst (disjoint-sym hd)
  disjoint-sym (HDSnd hd) = ds-lem-snd (disjoint-sym hd)
  disjoint-sym (HDHole x) = ds-lem-hole x
  disjoint-sym (HDNEHole x hd) = ds-lem-nehole (disjoint-sym hd) x

  -- note that this is false, so holes-disjoint isn't transitive
  -- disjoint-new : ∀{e1 e2 u} → holes-disjoint e1 e2 → hole-name-new e1 u → hole-name-new e2 u

  -- it's also not reflexive, because ⦇-⦈[ u ] isn't hole-disjoint with
  -- itself since refl : u == u; it's also not anti-reflexive, because the
  -- expression c *is* hole-disjoint with itself (albeit vacuously)

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


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

open import Base

module Algebra.F2NotCommutative where

import Algebra.FreeGroup
open Algebra.FreeGroup (bool {zero}) renaming (freegroup to F2)

X : Set
X = bool × bool

X-is-set : is-set X
X-is-set = ×-is-truncated _ bool-is-set bool-is-set

pattern a = (true  , true )
pattern b = (true  , false)
pattern c = (false , true )
pattern d = (false , false)

-- [map1] and [map2] are two involutive noncommutating bijections of [X]

map1 : X → X
map1 a = b
map1 b = a
map1 c = c
map1 d = d

map2 : X → X
map2 a = c
map2 b = b
map2 c = a
map2 d = d

act : bool {zero} → (X → X)
act true  = map1
act false = map2

act-involutive : (b : bool) (x : X) → (act b (act b x) ≡ x)
act-involutive true  a = refl
act-involutive true  b = refl
act-involutive true  c = refl
act-involutive true  d = refl
act-involutive false a = refl
act-involutive false b = refl
act-involutive false c = refl
act-involutive false d = refl

F2-act-on-X : F2 → (X → X)
F2-act-on-X = freegroup-rec-nondep (X → X)
  (id X)
  (λ b f → f ◯ act b)
  (λ b f → f ◯ act b)
  (λ b f → funext (λ x → ap f (act-involutive b x)))
  (λ b f → funext (λ x → ap f (act-involutive b x)))
  (→-is-truncated _ X-is-set)

ab : F2
ab = true  · (false · e)

ba : F2
ba = false · (true  · e)

F2-non-commutative : ab ≢ ba
F2-non-commutative p =
  bool-true≢false (base-path (happly (ap F2-act-on-X p) a))

max_stars_repo_name: timjb/HoTT-Agda


text:
module Structure.Sets.Relator where

open import Functional
import      Lvl
open import Logic
open import Logic.Propositional
open import Logic.Predicate
import      Structure.Sets.Names as Names
open import Type

private variable ℓ ℓₗ ℓᵣ ℓᵣₑₗ : Lvl.Level
private variable S Sₗ Sᵣ E Eₗ Eᵣ : Type{ℓ}
private variable _∈ₗ_ : E → Sₗ → Stmt{ℓₗ}
private variable _∈ᵣ_ : E → Sᵣ → Stmt{ℓᵣ}

module _ (_∈ₗ_ : E → Sₗ → Stmt{ℓₗ}) (_∈ᵣ_ : E → Sᵣ → Stmt{ℓᵣ}) where
  record SetEqualityRelation (_≡_ : Sₗ → Sᵣ → Stmt{ℓᵣₑₗ}) : Type{Lvl.of(E) Lvl.⊔ Lvl.of(Sₗ) Lvl.⊔ Lvl.of(Sᵣ) Lvl.⊔ ℓₗ Lvl.⊔ ℓᵣ Lvl.⊔ ℓᵣₑₗ} where
    constructor intro
    field membership : Names.SetEqualityMembership(_∈ₗ_)(_∈ᵣ_)(_≡_)

  record SubsetRelation (_⊆_ : Sₗ → Sᵣ → Stmt{ℓᵣₑₗ}) : Type{Lvl.of(E) Lvl.⊔ Lvl.of(Sₗ) Lvl.⊔ Lvl.of(Sᵣ) Lvl.⊔ ℓₗ Lvl.⊔ ℓᵣ Lvl.⊔ ℓᵣₑₗ} where
    constructor intro
    field membership : Names.SubsetMembership(_∈ₗ_)(_∈ᵣ_)(_⊆_)

module _ ⦃ eq : ∃(SetEqualityRelation(_∈ₗ_)(_∈ᵣ_){ℓᵣₑₗ}) ⦄ where
  open ∃(eq) using () renaming (witness to _≡_) public
  open SetEqualityRelation([∃]-proof eq) using () renaming (membership to [≡]-membership) public

  _≢_ = (¬_) ∘₂ (_≡_)

module _ ⦃ subset : ∃(SubsetRelation(_∈ₗ_)(_∈ᵣ_){ℓᵣ}) ⦄ where
  open ∃(subset) using () renaming (witness to _⊆_) public
  open SubsetRelation([∃]-proof subset) using () renaming (membership to [⊆]-membership) public
  open Names.From-[⊆] (_⊆_) public

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- W-types
------------------------------------------------------------------------

module Data.W where

open import Level
open import Relation.Nullary

-- The family of W-types.

data W {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  sup : (x : A) (f : B x → W A B) → W A B

-- Projections.

head : ∀ {a b} {A : Set a} {B : A → Set b} →
       W A B → A
head (sup x f) = x

tail : ∀ {a b} {A : Set a} {B : A → Set b} →
       (x : W A B) → B (head x) → W A B
tail (sup x f) = f

-- If B is always inhabited, then W A B is empty.

inhabited⇒empty : ∀ {a b} {A : Set a} {B : A → Set b} →
                  (∀ x → B x) → ¬ W A B
inhabited⇒empty b (sup x f) = inhabited⇒empty b (f (b x))


text:
{-# OPTIONS --without-K #-}
module function.isomorphism.properties where

open import level
open import sum
open import sets.nat.core
open import equality.core
open import equality.calculus
open import equality.reasoning
open import function.fibration
open import function.overloading
open import function.extensionality.core
open import function.extensionality.proof
open import function.isomorphism.core
open import function.isomorphism.coherent
open import function.isomorphism.lift
open import function.isomorphism.utils
open import hott.equivalence.core
open import hott.equivalence.alternative
open import hott.level.core
open import sets.unit

iso-adjunction : ∀ {i j}{X : Set i}{Y : Set j}
               → (isom : X ≅ Y)(x : X)(y : Y)
               → (apply isom x ≡ y) ≅ (x ≡ invert isom y)
iso-adjunction {i}{j}{X}{Y} isom x y
  = family-eq-iso total' (λ { (y , x) q → comm' x y q }) (y , x)
  where
    open _≅_ isom
    open ≅-Reasoning

    to-we : weak-equiv to
    to-we = proj₂ (≅⇒≈ isom)

    total' : (Σ (Y × X) λ { (y , x) → to x ≡ y })
           ≅ (Σ (Y × X) λ { (y , x) → x ≡ from y})
    total' = Σ-assoc-iso
           ·≅ ( Σ-ap-iso refl≅ λ y
              → contr-⊤-iso (to-we y)
              ·≅ sym≅ (contr-⊤-iso (singl-contr' (from y))) )
           ·≅ sym≅ Σ-assoc-iso

    comm' : (x : X)(y : Y)(p : to x ≡ y)
          → proj₁ (apply total' ((y , x) , p)) ≡ (y , x)
    comm' x y q = ap (_,_ y) (sym (ap from q) · iso₁ x)

iso≡ : ∀ {i j}{X : Set i}{Y : Set j}
     → (isom : X ≅ Y)
     → {x x' : X}
     → (x ≡ x')
     ≅ (apply isom x ≡ apply isom x')
iso≡ isom {x}{x'} = trans≡-iso (_≅_.iso₁ isom x)
                  ·≅ iso-adjunction (sym≅ isom) _ _

abstract
  subtype-eq : ∀ {i j k}{A : Set i}{P : A → Set j}
             → ((x : A) → h 1 (P x))
             → {X : Set k}
             → (isom : X ≅ Σ A P)
             → {x y : X}
             → (proj₁ (apply isom x) ≡ proj₁ (apply isom y))
             → x ≡ y
  subtype-eq hP isom p = iso⇒inj isom
    (unapΣ (p , h1⇒prop (hP _) _ _))

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
module Text.Greek.SBLGNT.Phlm where

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

ΠΡΟΣ-ΦΙΛΗΜΟΝΑ : List (Word)
ΠΡΟΣ-ΦΙΛΗΜΟΝΑ =
    word (Π ∷ α ∷ ῦ ∷ ∙λ ∷ ο ∷ ς ∷ []) "Phlm.1.1"
  ∷ word (δ ∷ έ ∷ σ ∷ μ ∷ ι ∷ ο ∷ ς ∷ []) "Phlm.1.1"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "Phlm.1.1"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "Phlm.1.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Phlm.1.1"
  ∷ word (Τ ∷ ι ∷ μ ∷ ό ∷ θ ∷ ε ∷ ο ∷ ς ∷ []) "Phlm.1.1"
  ∷ word (ὁ ∷ []) "Phlm.1.1"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ ὸ ∷ ς ∷ []) "Phlm.1.1"
  ∷ word (Φ ∷ ι ∷ ∙λ ∷ ή ∷ μ ∷ ο ∷ ν ∷ ι ∷ []) "Phlm.1.1"
  ∷ word (τ ∷ ῷ ∷ []) "Phlm.1.1"
  ∷ word (ἀ ∷ γ ∷ α ∷ π ∷ η ∷ τ ∷ ῷ ∷ []) "Phlm.1.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Phlm.1.1"
  ∷ word (σ ∷ υ ∷ ν ∷ ε ∷ ρ ∷ γ ∷ ῷ ∷ []) "Phlm.1.1"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "Phlm.1.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Phlm.1.2"
  ∷ word (Ἀ ∷ π ∷ φ ∷ ί ∷ ᾳ ∷ []) "Phlm.1.2"
  ∷ word (τ ∷ ῇ ∷ []) "Phlm.1.2"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ ῇ ∷ []) "Phlm.1.2"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Phlm.1.2"
  ∷ word (Ἀ ∷ ρ ∷ χ ∷ ί ∷ π ∷ π ∷ ῳ ∷ []) "Phlm.1.2"
  ∷ word (τ ∷ ῷ ∷ []) "Phlm.1.2"
  ∷ word (σ ∷ υ ∷ σ ∷ τ ∷ ρ ∷ α ∷ τ ∷ ι ∷ ώ ∷ τ ∷ ῃ ∷ []) "Phlm.1.2"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "Phlm.1.2"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Phlm.1.2"
  ∷ word (τ ∷ ῇ ∷ []) "Phlm.1.2"
  ∷ word (κ ∷ α ∷ τ ∷ []) "Phlm.1.2"
  ∷ word (ο ∷ ἶ ∷ κ ∷ ό ∷ ν ∷ []) "Phlm.1.2"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "Phlm.1.2"
  ∷ word (ἐ ∷ κ ∷ κ ∷ ∙λ ∷ η ∷ σ ∷ ί ∷ ᾳ ∷ []) "Phlm.1.2"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ ς ∷ []) "Phlm.1.3"
  ∷ word (ὑ ∷ μ ∷ ῖ ∷ ν ∷ []) "Phlm.1.3"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Phlm.1.3"
  ∷ word (ε ∷ ἰ ∷ ρ ∷ ή ∷ ν ∷ η ∷ []) "Phlm.1.3"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "Phlm.1.3"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "Phlm.1.3"
  ∷ word (π ∷ α ∷ τ ∷ ρ ∷ ὸ ∷ ς ∷ []) "Phlm.1.3"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "Phlm.1.3"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Phlm.1.3"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "Phlm.1.3"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "Phlm.1.3"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "Phlm.1.3"
  ∷ word (Ε ∷ ὐ ∷ χ ∷ α ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ῶ ∷ []) "Phlm.1.4"
  ∷ word (τ ∷ ῷ ∷ []) "Phlm.1.4"
  ∷ word (θ ∷ ε ∷ ῷ ∷ []) "Phlm.1.4"
  ∷ word (μ ∷ ο ∷ υ ∷ []) "Phlm.1.4"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ο ∷ τ ∷ ε ∷ []) "Phlm.1.4"
  ∷ word (μ ∷ ν ∷ ε ∷ ί ∷ α ∷ ν ∷ []) "Phlm.1.4"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "Phlm.1.4"
  ∷ word (π ∷ ο ∷ ι ∷ ο ∷ ύ ∷ μ ∷ ε ∷ ν ∷ ο ∷ ς ∷ []) "Phlm.1.4"
  ∷ word (ἐ ∷ π ∷ ὶ ∷ []) "Phlm.1.4"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "Phlm.1.4"
  ∷ word (π ∷ ρ ∷ ο ∷ σ ∷ ε ∷ υ ∷ χ ∷ ῶ ∷ ν ∷ []) "Phlm.1.4"
  ∷ word (μ ∷ ο ∷ υ ∷ []) "Phlm.1.4"
  ∷ word (ἀ ∷ κ ∷ ο ∷ ύ ∷ ω ∷ ν ∷ []) "Phlm.1.5"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "Phlm.1.5"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "Phlm.1.5"
  ∷ word (ἀ ∷ γ ∷ ά ∷ π ∷ η ∷ ν ∷ []) "Phlm.1.5"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Phlm.1.5"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "Phlm.1.5"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "Phlm.1.5"
  ∷ word (ἣ ∷ ν ∷ []) "Phlm.1.5"
  ∷ word (ἔ ∷ χ ∷ ε ∷ ι ∷ ς ∷ []) "Phlm.1.5"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "Phlm.1.5"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "Phlm.1.5"
  ∷ word (κ ∷ ύ ∷ ρ ∷ ι ∷ ο ∷ ν ∷ []) "Phlm.1.5"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ ν ∷ []) "Phlm.1.5"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Phlm.1.5"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "Phlm.1.5"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ α ∷ ς ∷ []) "Phlm.1.5"
  ∷ word (τ ∷ ο ∷ ὺ ∷ ς ∷ []) "Phlm.1.5"
  ∷ word (ἁ ∷ γ ∷ ί ∷ ο ∷ υ ∷ ς ∷ []) "Phlm.1.5"
  ∷ word (ὅ ∷ π ∷ ω ∷ ς ∷ []) "Phlm.1.6"
  ∷ word (ἡ ∷ []) "Phlm.1.6"
  ∷ word (κ ∷ ο ∷ ι ∷ ν ∷ ω ∷ ν ∷ ί ∷ α ∷ []) "Phlm.1.6"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "Phlm.1.6"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ε ∷ ώ ∷ ς ∷ []) "Phlm.1.6"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "Phlm.1.6"
  ∷ word (ἐ ∷ ν ∷ ε ∷ ρ ∷ γ ∷ ὴ ∷ ς ∷ []) "Phlm.1.6"
  ∷ word (γ ∷ έ ∷ ν ∷ η ∷ τ ∷ α ∷ ι ∷ []) "Phlm.1.6"
  ∷ word (ἐ ∷ ν ∷ []) "Phlm.1.6"
  ∷ word (ἐ ∷ π ∷ ι ∷ γ ∷ ν ∷ ώ ∷ σ ∷ ε ∷ ι ∷ []) "Phlm.1.6"
  ∷ word (π ∷ α ∷ ν ∷ τ ∷ ὸ ∷ ς ∷ []) "Phlm.1.6"
  ∷ word (ἀ ∷ γ ∷ α ∷ θ ∷ ο ∷ ῦ ∷ []) "Phlm.1.6"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Phlm.1.6"
  ∷ word (ἐ ∷ ν ∷ []) "Phlm.1.6"
  ∷ word (ἡ ∷ μ ∷ ῖ ∷ ν ∷ []) "Phlm.1.6"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "Phlm.1.6"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ό ∷ ν ∷ []) "Phlm.1.6"
  ∷ word (χ ∷ α ∷ ρ ∷ ὰ ∷ ν ∷ []) "Phlm.1.7"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "Phlm.1.7"
  ∷ word (π ∷ ο ∷ ∙λ ∷ ∙λ ∷ ὴ ∷ ν ∷ []) "Phlm.1.7"
  ∷ word (ἔ ∷ σ ∷ χ ∷ ο ∷ ν ∷ []) "Phlm.1.7"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Phlm.1.7"
  ∷ word (π ∷ α ∷ ρ ∷ ά ∷ κ ∷ ∙λ ∷ η ∷ σ ∷ ι ∷ ν ∷ []) "Phlm.1.7"
  ∷ word (ἐ ∷ π ∷ ὶ ∷ []) "Phlm.1.7"
  ∷ word (τ ∷ ῇ ∷ []) "Phlm.1.7"
  ∷ word (ἀ ∷ γ ∷ ά ∷ π ∷ ῃ ∷ []) "Phlm.1.7"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "Phlm.1.7"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "Phlm.1.7"
  ∷ word (τ ∷ ὰ ∷ []) "Phlm.1.7"
  ∷ word (σ ∷ π ∷ ∙λ ∷ ά ∷ γ ∷ χ ∷ ν ∷ α ∷ []) "Phlm.1.7"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "Phlm.1.7"
  ∷ word (ἁ ∷ γ ∷ ί ∷ ω ∷ ν ∷ []) "Phlm.1.7"
  ∷ word (ἀ ∷ ν ∷ α ∷ π ∷ έ ∷ π ∷ α ∷ υ ∷ τ ∷ α ∷ ι ∷ []) "Phlm.1.7"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "Phlm.1.7"
  ∷ word (σ ∷ ο ∷ ῦ ∷ []) "Phlm.1.7"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ έ ∷ []) "Phlm.1.7"
  ∷ word (Δ ∷ ι ∷ ό ∷ []) "Phlm.1.8"
  ∷ word (π ∷ ο ∷ ∙λ ∷ ∙λ ∷ ὴ ∷ ν ∷ []) "Phlm.1.8"
  ∷ word (ἐ ∷ ν ∷ []) "Phlm.1.8"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ῷ ∷ []) "Phlm.1.8"
  ∷ word (π ∷ α ∷ ρ ∷ ρ ∷ η ∷ σ ∷ ί ∷ α ∷ ν ∷ []) "Phlm.1.8"
  ∷ word (ἔ ∷ χ ∷ ω ∷ ν ∷ []) "Phlm.1.8"
  ∷ word (ἐ ∷ π ∷ ι ∷ τ ∷ ά ∷ σ ∷ σ ∷ ε ∷ ι ∷ ν ∷ []) "Phlm.1.8"
  ∷ word (σ ∷ ο ∷ ι ∷ []) "Phlm.1.8"
  ∷ word (τ ∷ ὸ ∷ []) "Phlm.1.8"
  ∷ word (ἀ ∷ ν ∷ ῆ ∷ κ ∷ ο ∷ ν ∷ []) "Phlm.1.8"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "Phlm.1.9"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "Phlm.1.9"
  ∷ word (ἀ ∷ γ ∷ ά ∷ π ∷ η ∷ ν ∷ []) "Phlm.1.9"
  ∷ word (μ ∷ ᾶ ∷ ∙λ ∷ ∙λ ∷ ο ∷ ν ∷ []) "Phlm.1.9"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ κ ∷ α ∷ ∙λ ∷ ῶ ∷ []) "Phlm.1.9"
  ∷ word (τ ∷ ο ∷ ι ∷ ο ∷ ῦ ∷ τ ∷ ο ∷ ς ∷ []) "Phlm.1.9"
  ∷ word (ὢ ∷ ν ∷ []) "Phlm.1.9"
  ∷ word (ὡ ∷ ς ∷ []) "Phlm.1.9"
  ∷ word (Π ∷ α ∷ ῦ ∷ ∙λ ∷ ο ∷ ς ∷ []) "Phlm.1.9"
  ∷ word (π ∷ ρ ∷ ε ∷ σ ∷ β ∷ ύ ∷ τ ∷ η ∷ ς ∷ []) "Phlm.1.9"
  ∷ word (ν ∷ υ ∷ ν ∷ ὶ ∷ []) "Phlm.1.9"
  ∷ word (δ ∷ ὲ ∷ []) "Phlm.1.9"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Phlm.1.9"
  ∷ word (δ ∷ έ ∷ σ ∷ μ ∷ ι ∷ ο ∷ ς ∷ []) "Phlm.1.9"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "Phlm.1.9"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "Phlm.1.9"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ κ ∷ α ∷ ∙λ ∷ ῶ ∷ []) "Phlm.1.10"
  ∷ word (σ ∷ ε ∷ []) "Phlm.1.10"
  ∷ word (π ∷ ε ∷ ρ ∷ ὶ ∷ []) "Phlm.1.10"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Phlm.1.10"
  ∷ word (ἐ ∷ μ ∷ ο ∷ ῦ ∷ []) "Phlm.1.10"
  ∷ word (τ ∷ έ ∷ κ ∷ ν ∷ ο ∷ υ ∷ []) "Phlm.1.10"
  ∷ word (ὃ ∷ ν ∷ []) "Phlm.1.10"
  ∷ word (ἐ ∷ γ ∷ έ ∷ ν ∷ ν ∷ η ∷ σ ∷ α ∷ []) "Phlm.1.10"
  ∷ word (ἐ ∷ ν ∷ []) "Phlm.1.10"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "Phlm.1.10"
  ∷ word (δ ∷ ε ∷ σ ∷ μ ∷ ο ∷ ῖ ∷ ς ∷ []) "Phlm.1.10"
  ∷ word (Ὀ ∷ ν ∷ ή ∷ σ ∷ ι ∷ μ ∷ ο ∷ ν ∷ []) "Phlm.1.10"
  ∷ word (τ ∷ ό ∷ ν ∷ []) "Phlm.1.11"
  ∷ word (π ∷ ο ∷ τ ∷ έ ∷ []) "Phlm.1.11"
  ∷ word (σ ∷ ο ∷ ι ∷ []) "Phlm.1.11"
  ∷ word (ἄ ∷ χ ∷ ρ ∷ η ∷ σ ∷ τ ∷ ο ∷ ν ∷ []) "Phlm.1.11"
  ∷ word (ν ∷ υ ∷ ν ∷ ὶ ∷ []) "Phlm.1.11"
  ∷ word (δ ∷ ὲ ∷ []) "Phlm.1.11"
  ∷ word (σ ∷ ο ∷ ὶ ∷ []) "Phlm.1.11"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Phlm.1.11"
  ∷ word (ἐ ∷ μ ∷ ο ∷ ὶ ∷ []) "Phlm.1.11"
  ∷ word (ε ∷ ὔ ∷ χ ∷ ρ ∷ η ∷ σ ∷ τ ∷ ο ∷ ν ∷ []) "Phlm.1.11"
  ∷ word (ὃ ∷ ν ∷ []) "Phlm.1.12"
  ∷ word (ἀ ∷ ν ∷ έ ∷ π ∷ ε ∷ μ ∷ ψ ∷ ά ∷ []) "Phlm.1.12"
  ∷ word (σ ∷ ο ∷ ι ∷ []) "Phlm.1.12"
  ∷ word (α ∷ ὐ ∷ τ ∷ ό ∷ ν ∷ []) "Phlm.1.12"
  ∷ word (τ ∷ ο ∷ ῦ ∷ τ ∷ []) "Phlm.1.12"
  ∷ word (ἔ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "Phlm.1.12"
  ∷ word (τ ∷ ὰ ∷ []) "Phlm.1.12"
  ∷ word (ἐ ∷ μ ∷ ὰ ∷ []) "Phlm.1.12"
  ∷ word (σ ∷ π ∷ ∙λ ∷ ά ∷ γ ∷ χ ∷ ν ∷ α ∷ []) "Phlm.1.12"
  ∷ word (ὃ ∷ ν ∷ []) "Phlm.1.13"
  ∷ word (ἐ ∷ γ ∷ ὼ ∷ []) "Phlm.1.13"
  ∷ word (ἐ ∷ β ∷ ο ∷ υ ∷ ∙λ ∷ ό ∷ μ ∷ η ∷ ν ∷ []) "Phlm.1.13"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "Phlm.1.13"
  ∷ word (ἐ ∷ μ ∷ α ∷ υ ∷ τ ∷ ὸ ∷ ν ∷ []) "Phlm.1.13"
  ∷ word (κ ∷ α ∷ τ ∷ έ ∷ χ ∷ ε ∷ ι ∷ ν ∷ []) "Phlm.1.13"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "Phlm.1.13"
  ∷ word (ὑ ∷ π ∷ ὲ ∷ ρ ∷ []) "Phlm.1.13"
  ∷ word (σ ∷ ο ∷ ῦ ∷ []) "Phlm.1.13"
  ∷ word (μ ∷ ο ∷ ι ∷ []) "Phlm.1.13"
  ∷ word (δ ∷ ι ∷ α ∷ κ ∷ ο ∷ ν ∷ ῇ ∷ []) "Phlm.1.13"
  ∷ word (ἐ ∷ ν ∷ []) "Phlm.1.13"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "Phlm.1.13"
  ∷ word (δ ∷ ε ∷ σ ∷ μ ∷ ο ∷ ῖ ∷ ς ∷ []) "Phlm.1.13"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Phlm.1.13"
  ∷ word (ε ∷ ὐ ∷ α ∷ γ ∷ γ ∷ ε ∷ ∙λ ∷ ί ∷ ο ∷ υ ∷ []) "Phlm.1.13"
  ∷ word (χ ∷ ω ∷ ρ ∷ ὶ ∷ ς ∷ []) "Phlm.1.14"
  ∷ word (δ ∷ ὲ ∷ []) "Phlm.1.14"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "Phlm.1.14"
  ∷ word (σ ∷ ῆ ∷ ς ∷ []) "Phlm.1.14"
  ∷ word (γ ∷ ν ∷ ώ ∷ μ ∷ η ∷ ς ∷ []) "Phlm.1.14"
  ∷ word (ο ∷ ὐ ∷ δ ∷ ὲ ∷ ν ∷ []) "Phlm.1.14"
  ∷ word (ἠ ∷ θ ∷ έ ∷ ∙λ ∷ η ∷ σ ∷ α ∷ []) "Phlm.1.14"
  ∷ word (π ∷ ο ∷ ι ∷ ῆ ∷ σ ∷ α ∷ ι ∷ []) "Phlm.1.14"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "Phlm.1.14"
  ∷ word (μ ∷ ὴ ∷ []) "Phlm.1.14"
  ∷ word (ὡ ∷ ς ∷ []) "Phlm.1.14"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "Phlm.1.14"
  ∷ word (ἀ ∷ ν ∷ ά ∷ γ ∷ κ ∷ η ∷ ν ∷ []) "Phlm.1.14"
  ∷ word (τ ∷ ὸ ∷ []) "Phlm.1.14"
  ∷ word (ἀ ∷ γ ∷ α ∷ θ ∷ ό ∷ ν ∷ []) "Phlm.1.14"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "Phlm.1.14"
  ∷ word (ᾖ ∷ []) "Phlm.1.14"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "Phlm.1.14"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "Phlm.1.14"
  ∷ word (ἑ ∷ κ ∷ ο ∷ ύ ∷ σ ∷ ι ∷ ο ∷ ν ∷ []) "Phlm.1.14"
  ∷ word (τ ∷ ά ∷ χ ∷ α ∷ []) "Phlm.1.15"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "Phlm.1.15"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "Phlm.1.15"
  ∷ word (τ ∷ ο ∷ ῦ ∷ τ ∷ ο ∷ []) "Phlm.1.15"
  ∷ word (ἐ ∷ χ ∷ ω ∷ ρ ∷ ί ∷ σ ∷ θ ∷ η ∷ []) "Phlm.1.15"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "Phlm.1.15"
  ∷ word (ὥ ∷ ρ ∷ α ∷ ν ∷ []) "Phlm.1.15"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "Phlm.1.15"
  ∷ word (α ∷ ἰ ∷ ώ ∷ ν ∷ ι ∷ ο ∷ ν ∷ []) "Phlm.1.15"
  ∷ word (α ∷ ὐ ∷ τ ∷ ὸ ∷ ν ∷ []) "Phlm.1.15"
  ∷ word (ἀ ∷ π ∷ έ ∷ χ ∷ ῃ ∷ ς ∷ []) "Phlm.1.15"
  ∷ word (ο ∷ ὐ ∷ κ ∷ έ ∷ τ ∷ ι ∷ []) "Phlm.1.16"
  ∷ word (ὡ ∷ ς ∷ []) "Phlm.1.16"
  ∷ word (δ ∷ ο ∷ ῦ ∷ ∙λ ∷ ο ∷ ν ∷ []) "Phlm.1.16"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "Phlm.1.16"
  ∷ word (ὑ ∷ π ∷ ὲ ∷ ρ ∷ []) "Phlm.1.16"
  ∷ word (δ ∷ ο ∷ ῦ ∷ ∙λ ∷ ο ∷ ν ∷ []) "Phlm.1.16"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ ὸ ∷ ν ∷ []) "Phlm.1.16"
  ∷ word (ἀ ∷ γ ∷ α ∷ π ∷ η ∷ τ ∷ ό ∷ ν ∷ []) "Phlm.1.16"
  ∷ word (μ ∷ ά ∷ ∙λ ∷ ι ∷ σ ∷ τ ∷ α ∷ []) "Phlm.1.16"
  ∷ word (ἐ ∷ μ ∷ ο ∷ ί ∷ []) "Phlm.1.16"
  ∷ word (π ∷ ό ∷ σ ∷ ῳ ∷ []) "Phlm.1.16"
  ∷ word (δ ∷ ὲ ∷ []) "Phlm.1.16"
  ∷ word (μ ∷ ᾶ ∷ ∙λ ∷ ∙λ ∷ ο ∷ ν ∷ []) "Phlm.1.16"
  ∷ word (σ ∷ ο ∷ ὶ ∷ []) "Phlm.1.16"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Phlm.1.16"
  ∷ word (ἐ ∷ ν ∷ []) "Phlm.1.16"
  ∷ word (σ ∷ α ∷ ρ ∷ κ ∷ ὶ ∷ []) "Phlm.1.16"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Phlm.1.16"
  ∷ word (ἐ ∷ ν ∷ []) "Phlm.1.16"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ῳ ∷ []) "Phlm.1.16"
  ∷ word (Ε ∷ ἰ ∷ []) "Phlm.1.17"
  ∷ word (ο ∷ ὖ ∷ ν ∷ []) "Phlm.1.17"
  ∷ word (μ ∷ ε ∷ []) "Phlm.1.17"
  ∷ word (ἔ ∷ χ ∷ ε ∷ ι ∷ ς ∷ []) "Phlm.1.17"
  ∷ word (κ ∷ ο ∷ ι ∷ ν ∷ ω ∷ ν ∷ ό ∷ ν ∷ []) "Phlm.1.17"
  ∷ word (π ∷ ρ ∷ ο ∷ σ ∷ ∙λ ∷ α ∷ β ∷ ο ∷ ῦ ∷ []) "Phlm.1.17"
  ∷ word (α ∷ ὐ ∷ τ ∷ ὸ ∷ ν ∷ []) "Phlm.1.17"
  ∷ word (ὡ ∷ ς ∷ []) "Phlm.1.17"
  ∷ word (ἐ ∷ μ ∷ έ ∷ []) "Phlm.1.17"
  ∷ word (ε ∷ ἰ ∷ []) "Phlm.1.18"
  ∷ word (δ ∷ έ ∷ []) "Phlm.1.18"
  ∷ word (τ ∷ ι ∷ []) "Phlm.1.18"
  ∷ word (ἠ ∷ δ ∷ ί ∷ κ ∷ η ∷ σ ∷ έ ∷ ν ∷ []) "Phlm.1.18"
  ∷ word (σ ∷ ε ∷ []) "Phlm.1.18"
  ∷ word (ἢ ∷ []) "Phlm.1.18"
  ∷ word (ὀ ∷ φ ∷ ε ∷ ί ∷ ∙λ ∷ ε ∷ ι ∷ []) "Phlm.1.18"
  ∷ word (τ ∷ ο ∷ ῦ ∷ τ ∷ ο ∷ []) "Phlm.1.18"
  ∷ word (ἐ ∷ μ ∷ ο ∷ ὶ ∷ []) "Phlm.1.18"
  ∷ word (ἐ ∷ ∙λ ∷ ∙λ ∷ ό ∷ γ ∷ α ∷ []) "Phlm.1.18"
  ∷ word (ἐ ∷ γ ∷ ὼ ∷ []) "Phlm.1.19"
  ∷ word (Π ∷ α ∷ ῦ ∷ ∙λ ∷ ο ∷ ς ∷ []) "Phlm.1.19"
  ∷ word (ἔ ∷ γ ∷ ρ ∷ α ∷ ψ ∷ α ∷ []) "Phlm.1.19"
  ∷ word (τ ∷ ῇ ∷ []) "Phlm.1.19"
  ∷ word (ἐ ∷ μ ∷ ῇ ∷ []) "Phlm.1.19"
  ∷ word (χ ∷ ε ∷ ι ∷ ρ ∷ ί ∷ []) "Phlm.1.19"
  ∷ word (ἐ ∷ γ ∷ ὼ ∷ []) "Phlm.1.19"
  ∷ word (ἀ ∷ π ∷ ο ∷ τ ∷ ί ∷ σ ∷ ω ∷ []) "Phlm.1.19"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "Phlm.1.19"
  ∷ word (μ ∷ ὴ ∷ []) "Phlm.1.19"
  ∷ word (∙λ ∷ έ ∷ γ ∷ ω ∷ []) "Phlm.1.19"
  ∷ word (σ ∷ ο ∷ ι ∷ []) "Phlm.1.19"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "Phlm.1.19"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Phlm.1.19"
  ∷ word (σ ∷ ε ∷ α ∷ υ ∷ τ ∷ ό ∷ ν ∷ []) "Phlm.1.19"
  ∷ word (μ ∷ ο ∷ ι ∷ []) "Phlm.1.19"
  ∷ word (π ∷ ρ ∷ ο ∷ σ ∷ ο ∷ φ ∷ ε ∷ ί ∷ ∙λ ∷ ε ∷ ι ∷ ς ∷ []) "Phlm.1.19"
  ∷ word (ν ∷ α ∷ ί ∷ []) "Phlm.1.20"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ έ ∷ []) "Phlm.1.20"
  ∷ word (ἐ ∷ γ ∷ ώ ∷ []) "Phlm.1.20"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "Phlm.1.20"
  ∷ word (ὀ ∷ ν ∷ α ∷ ί ∷ μ ∷ η ∷ ν ∷ []) "Phlm.1.20"
  ∷ word (ἐ ∷ ν ∷ []) "Phlm.1.20"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ῳ ∷ []) "Phlm.1.20"
  ∷ word (ἀ ∷ ν ∷ ά ∷ π ∷ α ∷ υ ∷ σ ∷ ό ∷ ν ∷ []) "Phlm.1.20"
  ∷ word (μ ∷ ο ∷ υ ∷ []) "Phlm.1.20"
  ∷ word (τ ∷ ὰ ∷ []) "Phlm.1.20"
  ∷ word (σ ∷ π ∷ ∙λ ∷ ά ∷ γ ∷ χ ∷ ν ∷ α ∷ []) "Phlm.1.20"
  ∷ word (ἐ ∷ ν ∷ []) "Phlm.1.20"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ῷ ∷ []) "Phlm.1.20"
  ∷ word (π ∷ ε ∷ π ∷ ο ∷ ι ∷ θ ∷ ὼ ∷ ς ∷ []) "Phlm.1.21"
  ∷ word (τ ∷ ῇ ∷ []) "Phlm.1.21"
  ∷ word (ὑ ∷ π ∷ α ∷ κ ∷ ο ∷ ῇ ∷ []) "Phlm.1.21"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "Phlm.1.21"
  ∷ word (ἔ ∷ γ ∷ ρ ∷ α ∷ ψ ∷ ά ∷ []) "Phlm.1.21"
  ∷ word (σ ∷ ο ∷ ι ∷ []) "Phlm.1.21"
  ∷ word (ε ∷ ἰ ∷ δ ∷ ὼ ∷ ς ∷ []) "Phlm.1.21"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "Phlm.1.21"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Phlm.1.21"
  ∷ word (ὑ ∷ π ∷ ὲ ∷ ρ ∷ []) "Phlm.1.21"
  ∷ word (ἃ ∷ []) "Phlm.1.21"
  ∷ word (∙λ ∷ έ ∷ γ ∷ ω ∷ []) "Phlm.1.21"
  ∷ word (π ∷ ο ∷ ι ∷ ή ∷ σ ∷ ε ∷ ι ∷ ς ∷ []) "Phlm.1.21"
  ∷ word (ἅ ∷ μ ∷ α ∷ []) "Phlm.1.22"
  ∷ word (δ ∷ ὲ ∷ []) "Phlm.1.22"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Phlm.1.22"
  ∷ word (ἑ ∷ τ ∷ ο ∷ ί ∷ μ ∷ α ∷ ζ ∷ έ ∷ []) "Phlm.1.22"
  ∷ word (μ ∷ ο ∷ ι ∷ []) "Phlm.1.22"
  ∷ word (ξ ∷ ε ∷ ν ∷ ί ∷ α ∷ ν ∷ []) "Phlm.1.22"
  ∷ word (ἐ ∷ ∙λ ∷ π ∷ ί ∷ ζ ∷ ω ∷ []) "Phlm.1.22"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "Phlm.1.22"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "Phlm.1.22"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "Phlm.1.22"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "Phlm.1.22"
  ∷ word (π ∷ ρ ∷ ο ∷ σ ∷ ε ∷ υ ∷ χ ∷ ῶ ∷ ν ∷ []) "Phlm.1.22"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "Phlm.1.22"
  ∷ word (χ ∷ α ∷ ρ ∷ ι ∷ σ ∷ θ ∷ ή ∷ σ ∷ ο ∷ μ ∷ α ∷ ι ∷ []) "Phlm.1.22"
  ∷ word (ὑ ∷ μ ∷ ῖ ∷ ν ∷ []) "Phlm.1.22"
  ∷ word (Ἀ ∷ σ ∷ π ∷ ά ∷ ζ ∷ ε ∷ τ ∷ α ∷ ί ∷ []) "Phlm.1.23"
  ∷ word (σ ∷ ε ∷ []) "Phlm.1.23"
  ∷ word (Ἐ ∷ π ∷ α ∷ φ ∷ ρ ∷ ᾶ ∷ ς ∷ []) "Phlm.1.23"
  ∷ word (ὁ ∷ []) "Phlm.1.23"
  ∷ word (σ ∷ υ ∷ ν ∷ α ∷ ι ∷ χ ∷ μ ∷ ά ∷ ∙λ ∷ ω ∷ τ ∷ ό ∷ ς ∷ []) "Phlm.1.23"
  ∷ word (μ ∷ ο ∷ υ ∷ []) "Phlm.1.23"
  ∷ word (ἐ ∷ ν ∷ []) "Phlm.1.23"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ῷ ∷ []) "Phlm.1.23"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "Phlm.1.23"
  ∷ word (Μ ∷ ᾶ ∷ ρ ∷ κ ∷ ο ∷ ς ∷ []) "Phlm.1.24"
  ∷ word (Ἀ ∷ ρ ∷ ί ∷ σ ∷ τ ∷ α ∷ ρ ∷ χ ∷ ο ∷ ς ∷ []) "Phlm.1.24"
  ∷ word (Δ ∷ η ∷ μ ∷ ᾶ ∷ ς ∷ []) "Phlm.1.24"
  ∷ word (Λ ∷ ο ∷ υ ∷ κ ∷ ᾶ ∷ ς ∷ []) "Phlm.1.24"
  ∷ word (ο ∷ ἱ ∷ []) "Phlm.1.24"
  ∷ word (σ ∷ υ ∷ ν ∷ ε ∷ ρ ∷ γ ∷ ο ∷ ί ∷ []) "Phlm.1.24"
  ∷ word (μ ∷ ο ∷ υ ∷ []) "Phlm.1.24"
  ∷ word (Ἡ ∷ []) "Phlm.1.25"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ ς ∷ []) "Phlm.1.25"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Phlm.1.25"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ο ∷ υ ∷ []) "Phlm.1.25"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "Phlm.1.25"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "Phlm.1.25"
  ∷ word (μ ∷ ε ∷ τ ∷ ὰ ∷ []) "Phlm.1.25"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Phlm.1.25"
  ∷ word (π ∷ ν ∷ ε ∷ ύ ∷ μ ∷ α ∷ τ ∷ ο ∷ ς ∷ []) "Phlm.1.25"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "Phlm.1.25"
  ∷ []

max_stars_repo_name: scott-fleischman/GreekGrammar

max_issues_repo_name: scott-fleischman/GreekGrammar

max_forks_repo_name: scott-fleischman/GreekGrammar


text:
-- {-# OPTIONS -v tc.cover:20 #-}

-- Andreas, 2017-01-18, issue #2407

-- If underscores are not preserved (issue #819),
-- the case split fails due to size constraints.

open import Common.Size

data D (i : Size) : (j : Size< ↑ i) → Set where

  c : ∀ (j : Size< ↑ i) (k : Size< ↑ j)
       → D i j
       → D j k
       → D i k

split-u : ∀ i (j : Size< ↑ i) → D i j → Set
split-u _ _ x = {!x!}  -- split on x

-- Expected: splitting on x succeeds with
--   split-u _ _ (c j k x x₁) = {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Level.NP
open import Type
open import Relation.Binary.Logical
open import Relation.Binary.PropositionalEquality

module Explore.Universe.Logical (X : ★) where

open import Explore.Universe.Type
open import Explore.Universe X
open import Explore.Core

module From⟦X⟧ (⟦X⟧ : ⟦★₀⟧ X X) where

  -- TODO _⟦≃⟧_ : (⟦Rel⟧ ⟦★₀⟧) ₀ _≃_ _≃_

  data ⟦U⟧ : ⟦★₁⟧ U U
  ⟦El⟧ : (⟦U⟧ ⟦→⟧ ⟦★₀⟧) El El

  data ⟦U⟧ where
    ⟦𝟘ᵁ⟧ : ⟦U⟧ 𝟘ᵁ 𝟘ᵁ
    ⟦𝟙ᵁ⟧ : ⟦U⟧ 𝟙ᵁ 𝟙ᵁ
    ⟦𝟚ᵁ⟧ : ⟦U⟧ 𝟚ᵁ 𝟚ᵁ
    _⟦×ᵁ⟧_ : ⟦Op₂⟧ {_} {_} {₁} ⟦U⟧ _×ᵁ_ _×ᵁ_
    _⟦⊎ᵁ⟧_ : ⟦Op₂⟧ {_} {_} {₁} ⟦U⟧ _⊎ᵁ_ _⊎ᵁ_
    ⟦Σᵁ⟧ : (⟨ u ∶ ⟦U⟧ ⟩⟦→⟧ (⟦El⟧ u ⟦→⟧ ⟦U⟧) ⟦→⟧ ⟦U⟧) Σᵁ Σᵁ
    ⟦Xᵁ⟧ : ⟦U⟧ Xᵁ Xᵁ
    -- ⟦≃ᵁ⟧ : (⟨ u ∶ ⟦U⟧ ⟩⟦→⟧ (⟨ A ∶ ⟦★₀⟧ ⟩⟦→⟧ ⟦El⟧ u ⟦≃⟧ A ⟦→⟧ ⟦U⟧)) ≃ᵁ ≃ᵁ

  ⟦El⟧ ⟦𝟘ᵁ⟧ = _≡_
  ⟦El⟧ ⟦𝟙ᵁ⟧ = _≡_
  ⟦El⟧ ⟦𝟚ᵁ⟧ = _≡_
  ⟦El⟧ (u₀ ⟦×ᵁ⟧ u₁) = ⟦El⟧ u₀ ⟦×⟧ ⟦El⟧ u₁
  ⟦El⟧ (u₀ ⟦⊎ᵁ⟧ u₁) = ⟦El⟧ u₀ ⟦⊎⟧ ⟦El⟧ u₁
  ⟦El⟧ (⟦Σᵁ⟧ u f) = ⟦Σ⟧ (⟦El⟧ u) λ x → ⟦El⟧ (f x)
  ⟦El⟧ ⟦Xᵁ⟧ = ⟦X⟧
  -- ⟦El⟧ (⟦≃ᵁ⟧ u A e) = A

  module From⟦Xᵉ⟧
           {⟦X⟧ : ⟦★₀⟧ X X}
           {ℓ₀ ℓ₁} ℓᵣ
           {Xᵉ : Explore X}
           (⟦Xᵉ⟧ : ⟦Explore⟧ {ℓ₀} {ℓ₁} ℓᵣ ⟦X⟧ Xᵉ Xᵉ) where
    open From⟦X⟧ ⟦X⟧ public

    ⟦explore⟧ : ∀ {u₀ u₁} (u : ⟦U⟧ u₀ u₁) → ⟦Explore⟧ {ℓ₀} {ℓ₁} ℓᵣ (⟦El⟧ u) (explore u₀) (explore u₁)
    ⟦explore⟧ ⟦𝟘ᵁ⟧        = ⟦𝟘ᵉ⟧ {ℓ₀} {ℓ₁} {ℓᵣ}
    ⟦explore⟧ ⟦𝟙ᵁ⟧        = ⟦𝟙ᵉ⟧ {ℓ₀} {ℓ₁} {ℓᵣ} {_≡_} {refl}
    ⟦explore⟧ ⟦𝟚ᵁ⟧        = ⟦𝟚ᵉ⟧ {ℓ₀} {ℓ₁} {ℓᵣ} {_≡_} {refl} {refl}
    ⟦explore⟧ (u₀ ⟦×ᵁ⟧ u₁) = ⟦explore×⟧ {ℓ₀} {ℓ₁} {ℓᵣ} (⟦explore⟧ u₀) (⟦explore⟧ u₁)
    ⟦explore⟧ (u₀ ⟦⊎ᵁ⟧ u₁) = ⟦explore⊎⟧ {ℓ₀} {ℓ₁} {ℓᵣ} (⟦explore⟧ u₀) (⟦explore⟧ u₁)
    ⟦explore⟧ (⟦Σᵁ⟧ u f)  = ⟦exploreΣ⟧ {ℓ₀} {ℓ₁} {ℓᵣ} (⟦explore⟧ u) (⟦explore⟧ ∘ f)
    ⟦explore⟧ ⟦Xᵁ⟧        = ⟦Xᵉ⟧
    -- ⟦explore⟧ (⟦≃ᵁ⟧ u A e) = {!⟦explore-iso⟧ e!}

{-
⟦U⟧-sound : ∀ {{_ : FunExt}} {x y} → ⟦U⟧ x y → x ≡ y
⟦U⟧-refl : ∀ x → ⟦U⟧ x x

{-
⟦El⟧-refl : ∀ x → {!⟦El⟧ x x!}
⟦El⟧-refl = {!!}
-}

⟦U⟧-sound ⟦𝟘ᵁ⟧ = refl
⟦U⟧-sound ⟦𝟙ᵁ⟧ = refl
⟦U⟧-sound ⟦𝟚ᵁ⟧ = refl
⟦U⟧-sound (u ⟦×ᵁ⟧ u₁) = ap₂ _×ᵁ_ (⟦U⟧-sound u) (⟦U⟧-sound u₁)
⟦U⟧-sound (u ⟦⊎ᵁ⟧ u₁) = ap₂ _⊎ᵁ_ (⟦U⟧-sound u) (⟦U⟧-sound u₁)
⟦U⟧-sound (⟦Σᵁ⟧ {u₀} {u₁} u {f₀} {f₁} fᵣ) = apd₂ Σᵁ (⟦U⟧-sound u) (tr-→ El (const U) (⟦U⟧-sound u) f₀ ∙ λ= (λ A → ap (λ z → z (f₀ (tr El (! ⟦U⟧-sound u) A))) (tr-const (⟦U⟧-sound u)) ∙ ⟦U⟧-sound (fᵣ {!!}))) -- (λ= (λ y → let foo = xᵣ {{!!}} {y} {!xᵣ!} in {!tr-→ El (const U) (⟦U⟧-sound u)!}))

⟦U⟧-refl 𝟘ᵁ = ⟦𝟘ᵁ⟧
⟦U⟧-refl 𝟙ᵁ = ⟦𝟙ᵁ⟧
⟦U⟧-refl 𝟚ᵁ = ⟦𝟚ᵁ⟧
⟦U⟧-refl (x ×ᵁ x₁) = ⟦U⟧-refl x ⟦×ᵁ⟧ ⟦U⟧-refl x₁
⟦U⟧-refl (x ⊎ᵁ x₁) = ⟦U⟧-refl x ⟦⊎ᵁ⟧ ⟦U⟧-refl x₁
⟦U⟧-refl (Σᵁ x f) = ⟦Σᵁ⟧ (⟦U⟧-refl x) (λ y → {!⟦U⟧-refl ?!})
-}

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
module Ord where

data Nat : Set where
  Z : Nat
  S : Nat -> Nat

data Ord : Set  where
  z : Ord
  lim : (Nat -> Ord) -> Ord

zp  : Ord -> Ord
zp z = z
zp (lim f) = lim (\x -> zp (f x))


text:
-- 2018-11-02, Jesper:
-- Problem reported by Martin Escardo
-- Example by Guillaume Brunerie
-- C-c C-s was generating postfix projections
-- even with --postfix-projections disabled.

open import Agda.Builtin.Equality

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _×_

postulate
  A B : Set
  p : A × B

eta : p ≡ ({!!} , snd p)
eta = refl

-- C-c C-s should fill the hole with 'fst p'.


text:
module Lib.IO where

open import Lib.List
open import Lib.Prelude

{-# IMPORT System.Environment #-}

FilePath = String

postulate
  IO        : Set -> Set
  getLine   : IO String
  putStrLn  : String -> IO Unit
  putStr    : String -> IO Unit
  bindIO    : {A B : Set} -> IO A -> (A -> IO B) -> IO B
  returnIO  : {A : Set} -> A -> IO A
  getArgs   : IO (List String)
  readFile  : FilePath -> IO String
  writeFile : FilePath -> String -> IO Unit

{-# BUILTIN IO IO #-}
{-# COMPILED_TYPE IO IO #-}

{-# COMPILED putStr putStr #-}
{-# COMPILED putStrLn putStrLn #-}
{-# COMPILED bindIO (\_ _ -> (>>=) :: IO a -> (a -> IO b) -> IO b) #-}
{-# COMPILED returnIO (\_ -> return :: a -> IO a) #-}
  -- we need to throw away the type argument to return and bind
  -- and resolve the overloading explicitly (since Alonzo
  -- output is sprinkled with unsafeCoerce#).
{-# COMPILED getLine getLine #-}
{-# COMPILED getArgs System.Environment.getArgs #-}
{-# COMPILED readFile readFile #-}
{-# COMPILED writeFile writeFile #-}

mapM : {A B : Set} -> (A -> IO B) -> List A -> IO (List B)
mapM f [] = returnIO []
mapM f (x :: xs) = bindIO (f x) \y -> bindIO (mapM f xs) \ys -> returnIO (y :: ys)

mapM₋ : {A : Set} -> (A -> IO Unit) -> List A -> IO Unit
mapM₋ f xs = bindIO (mapM f xs) \_ -> returnIO unit


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Instance.Nat where

-- Skeleton of FinSetoid as a Category

open import Level

open import Data.Fin.Base using (Fin; inject+; raise; splitAt; join)
open import Data.Fin.Properties
open import Data.Nat.Base using (ℕ; _+_)
open import Data.Sum using (inj₁; inj₂; [_,_]′)
open import Data.Sum.Properties
open import Relation.Binary.PropositionalEquality
  using (_≗_; _≡_; refl; sym; trans; cong; module ≡-Reasoning; inspect; [_])
open import Function using (id; _∘′_)

open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
open import Categories.Category.Cocartesian using (Cocartesian)
open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory)
open import Categories.Category.Core using (Category)
open import Categories.Category.Duality using (Cocartesian⇒coCartesian)
open import Categories.Object.Coproduct
open import Categories.Object.Duality using (Coproduct⇒coProduct)
open import Categories.Object.Product

Nat : Category 0ℓ 0ℓ 0ℓ
Nat = record
  { Obj = ℕ
  ; _⇒_ = λ m n → (Fin m → Fin n)
  ; _≈_ = _≗_
  ; id = id
  ; _∘_ = _∘′_
  ; assoc = λ _ → refl
  ; sym-assoc = λ _ → refl
  ; identityˡ = λ _ → refl
  ; identityʳ = λ _ → refl
  ; identity² = λ _ → refl
  ; equiv = record
    { refl = λ _ → refl
    ; sym = λ x≡y z → sym (x≡y z)
    ; trans = λ x≡y y≡z w → trans (x≡y w) (y≡z w)
    }
  ; ∘-resp-≈ = λ {_ _ _ f h g i} f≗h g≗i x → trans (f≗h (g x)) (cong h (g≗i x))
  }

-- For other uses, it is important to choose coproducts
-- in theory, it should be strictly associative... but it's not, and won't be for any choice.
Coprod : (m n : ℕ) → Coproduct Nat m n
Coprod m n = record
  { A+B = m + n
  ; i₁ = inject+ n
  ; i₂ = raise m
  ; [_,_] = λ l r z → [ l , r ]′ (splitAt m z)
  ; inject₁ = λ {_ f g} x → cong [ f , g ]′ (splitAt-inject+ m n x)
  ; inject₂ = λ {_ f g} x → cong [ f , g ]′ (splitAt-raise m n x)
  ; unique = uniq
  }
  where
    open ≡-Reasoning
    uniq : {o : ℕ} {h : Fin (m + n) → Fin o} {f : Fin m → Fin o} {g : Fin n → Fin o} →
      h ∘′ inject+ n ≗ f → h ∘′ raise m ≗ g → (λ z → [ f , g ]′ (splitAt m z)) ≗ h
    uniq {_} {h} {f} {g} h≗f h≗g w = begin
      [ f , g ]′ (splitAt m w)                         ≡⟨ [,]-cong (λ x → sym (h≗f x)) (λ x → sym (h≗g x)) (splitAt m w) ⟩
      [ h ∘′ inject+ n , h ∘′ raise m ]′ (splitAt m w) ≡˘⟨ [,]-∘-distr h (splitAt m w) ⟩
      h ([ inject+ n , raise m ]′ (splitAt m w))       ≡⟨ cong h (join-splitAt m n w) ⟩
      h w                                              ∎

Nat-Cocartesian : Cocartesian Nat
Nat-Cocartesian = record
  { initial = record
    { ⊥ = 0
    ; ⊥-is-initial = record
      { ! = λ ()
      ; !-unique = λ _ ()
      }
    }
  ; coproducts = record { coproduct = λ {m} {n} → Coprod m n }
  }

-- And Natop is what is used a lot, so record some things here too
Natop : Category 0ℓ 0ℓ 0ℓ
Natop = Category.op Nat

Natop-Product : (m n : ℕ) → Product Natop m n
Natop-Product m n = Coproduct⇒coProduct Nat (Coprod m n)

Natop-Cartesian : CartesianCategory 0ℓ 0ℓ 0ℓ
Natop-Cartesian = record
  { U = Natop
  ; cartesian = Cocartesian⇒coCartesian Nat Nat-Cocartesian
  }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
-- Path induction

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

module Experiment.PropositionalEq where

open import Level renaming (zero to lzero; suc to lsuc)
open import Relation.Binary.PropositionalEquality
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
open import Relation.Binary

private
  variable
    a c : Level
    A : Set a

-- HoTT 1.12.1
-- Path induction
PathInd : (C : (x y : A) → x ≡ y → Set c) →
          (∀ x → C x x refl) → ∀ x y (p : x ≡ y) → C x y p
PathInd C c x .x refl = c x

PathInd-refl : ∀ (C : (x y : A) → x ≡ y → Set c) (c : ∀ x → C x x refl) x →
               PathInd C c x x refl ≡ c x
PathInd-refl C c x = refl

-- Based path induction
BasedPathInd : (a : A) (C : ∀ x → a ≡ x → Set c) → C a refl →
               ∀ x (p : a ≡ x) → C x p
BasedPathInd a C c .a refl = c

BasedPathInd-refl : ∀ (a : A) (C : ∀ x → a ≡ x → Set c) (c : C a refl) →
                    BasedPathInd a C c a refl ≡ c
BasedPathInd-refl _ _ _ = refl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Characters
------------------------------------------------------------------------

module Data.Char where

open import Data.Nat using (ℕ)
import Data.Nat.Properties as NatProp
open import Data.Bool using (Bool; true; false)
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Binary
import Relation.Binary.On as On
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
open import Relation.Binary.PropositionalEquality.TrustMe

open import Data.String.Core using (String; primShowChar)
import Data.Char.Core as Core
open Core public using (Char)
open Core

show : Char → String
show = primShowChar

toNat : Char → ℕ
toNat = primCharToNat

-- Informative equality test.

_≟_ : Decidable {A = Char} _≡_
s₁ ≟ s₂ with primCharEquality s₁ s₂
... | true  = yes trustMe
... | false = no whatever
  where postulate whatever : _

-- Boolean equality test.
--
-- Why is the definition _==_ = primCharEquality not used? One reason
-- is that the present definition can sometimes improve type
-- inference, at least with the version of Agda that is current at the
-- time of writing: see unit-test below.

infix 4 _==_

_==_ : Char → Char → Bool
c₁ == c₂ = ⌊ c₁ ≟ c₂ ⌋

private

  -- The following unit test does not type-check (at the time of
  -- writing) if _==_ is replaced by primCharEquality.

  data P : (Char → Bool) → Set where
    p : (c : Char) → P (_==_ c)

  unit-test : P (_==_ 'x')
  unit-test = p _

setoid : Setoid _ _
setoid = PropEq.setoid Char

decSetoid : DecSetoid _ _
decSetoid = PropEq.decSetoid _≟_

-- An ordering induced by the toNat function.

strictTotalOrder : StrictTotalOrder _ _ _
strictTotalOrder = On.strictTotalOrder NatProp.strictTotalOrder toNat


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Convenient syntax for "equational reasoning" in multiple Setoids
------------------------------------------------------------------------

-- Example use:
--
--   open import Data.Maybe
--   import Relation.Binary.SetoidReasoning as SetR
--
--   begin⟨ S ⟩
--     x
--       ≈⟨ drop-just (begin⟨ setoid S ⟩
--          just x
--            ≈⟨ justx≈mz ⟩
--          mz
--            ≈⟨ mz≈justy ⟩
--          just y ∎) ⟩
--     y
--       ≈⟨ y≈z ⟩
--     z ∎

open import Relation.Binary.EqReasoning as EqR using (_IsRelatedTo_)
open import Relation.Binary
open import Relation.Binary.Core

open Setoid

module Relation.Binary.SetoidReasoning where

infix 1 begin⟨_⟩_
infixr 2 _≈⟨_⟩_ _≡⟨_⟩_
infix 2 _∎

begin⟨_⟩_ : ∀ {c l} (S : Setoid c l) → {x y : Carrier S} → _IsRelatedTo_ S x y → _≈_ S x y
begin⟨_⟩_ S p = EqR.begin_ S p

_∎ : ∀ {c l} {S : Setoid c l} → (x : Carrier S) → _IsRelatedTo_ S x x
_∎ {S = S} = EqR._∎ S

_≈⟨_⟩_ : ∀ {c l} {S : Setoid c l} → (x : Carrier S) → {y z : Carrier S} → _≈_ S x y → _IsRelatedTo_ S y z → _IsRelatedTo_ S x z
_≈⟨_⟩_ {S = S} = EqR._≈⟨_⟩_ S

_≡⟨_⟩_ : ∀ {c l} {S : Setoid c l} → (x : Carrier S) → {y z : Carrier S} → x ≡ y → _IsRelatedTo_ S y z → _IsRelatedTo_ S x z
_≡⟨_⟩_ {S = S} = EqR._≡⟨_⟩_ S


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

open import Base
open import Homotopy.Pushout
open import Homotopy.VanKampen.Guide

module Homotopy.VanKampen.Code {i} (d : pushout-diag i)
  (l : legend i (pushout-diag.C d)) where

  open pushout-diag d
  open legend l

  open import Homotopy.Truncation
  open import Homotopy.PathTruncation

  -- Code from A.
  import Homotopy.VanKampen.SplitCode d l as SC
  import Homotopy.VanKampen.Code.LemmaPackA d l as C
  -- Code from B. Code flipped.
  import Homotopy.VanKampen.SplitCode (pushout-diag-flip d) l as SCF
  import Homotopy.VanKampen.Code.LemmaPackA (pushout-diag-flip d) l as CF

  P : Set i
  P = pushout d

  module _ where
    -- Things that can be directly re-exported
    -- FIXME Ideally, this should be ‵SC'.
    -- Somehow that doesn′t work.
    open import Homotopy.VanKampen.SplitCode d l
      public using () renaming
        ( code            to a-code
        ; code-a          to a-code-a
        ; code-b          to a-code-b
        ; code-rec        to a-code-rec
        ; code-rec-nondep to a-code-rec-nondep
        ; code-is-set     to a-code-is-set
        ; code-a-is-set   to a-code-a-is-set
        ; code-b-is-set   to a-code-b-is-set
        )
    module _ {a₁ : A} where
      open import Homotopy.VanKampen.SplitCode d l a₁
        public using () renaming
          ( code-a-refl-refl  to a-code-a-refl-refl
          ; code-b-refl-refl  to a-code-b-refl-refl
          ; code-ab-swap      to a-code-ab-swap
          ; trans-a           to trans-a-code-a
          ; trans-ba          to trans-a-code-ba
          ; trans-ab          to trans-a-code-ab
          ; a⇒b               to aa⇒ab
          ; b⇒a               to ab⇒aa
          )

    a-a : ∀ {a₁} {a₂} → a₁ ≡₀ a₂ → a-code-a a₁ a₂
    a-a = SC.a _

    infixl 6 a-a
    syntax a-a co = ⟧a co

    a-ba : ∀ {a₁} {a₂} n → a-code-b a₁ (g $ loc n) → f (loc n) ≡₀ a₂ → a-code-a a₁ a₂
    a-ba = SC.ba _

    infixl 6 a-ba
    syntax a-ba n co p = co ab⟦ n ⟧a p

    a-ab : ∀ {a₁} {b₂} n → a-code-a a₁ (f $ loc n) → g (loc n) ≡₀ b₂ → a-code-b a₁ b₂
    a-ab = SC.ab _

    infixl 6 a-ab
    syntax a-ab n co p = co aa⟦ n ⟧b p

  module _ where
    -- Things that can be directly re-exported
    open import Homotopy.VanKampen.SplitCode (pushout-diag-flip d) l
      public using () renaming
        ( code-a          to b-code-b
        ; code-b          to b-code-a
        ; code-rec        to b-code-rec
        ; code-rec-nondep to b-code-rec-nondep
        ; code-a-is-set   to b-code-b-is-set
        ; code-b-is-set   to b-code-a-is-set
        )

    b-code : B → P → Set i
    b-code b = SCF.code b ◯ pushout-flip

    module _ {b₁ : B} where
      open import Homotopy.VanKampen.SplitCode (pushout-diag-flip d) l b₁
        public using () renaming
          ( code-a-refl-refl  to b-code-b-refl-refl
          ; code-b-refl-refl  to b-code-a-refl-refl
          ; code-ab-swap      to b-code-ba-swap
          ; trans-a           to trans-b-code-b
          ; trans-ba          to trans-b-code-ab
          ; trans-ab          to trans-b-code-ba
          ; a⇒b               to bb⇒ba
          ; b⇒a               to ba⇒bb
          )

    b-b : ∀ {b₁} {b₂} → b₁ ≡₀ b₂ → b-code-b b₁ b₂
    b-b = SCF.a _

    infixl 6 b-b
    syntax b-b co = ⟧b co

    b-ab : ∀ {b₁} {b₂} n → b-code-a b₁ (f $ loc n) → g (loc n) ≡₀ b₂ → b-code-b b₁ b₂
    b-ab = SCF.ba _

    infixl 6 b-ab
    syntax b-ab c co p = co ba⟦ c ⟧b p

    b-ba : ∀ {b₁} {a₂} n → b-code-b b₁ (g $ loc n) → f (loc n) ≡₀ a₂ → b-code-a b₁ a₂
    b-ba = SCF.ab _

    infixl 6 b-ba
    syntax b-ba c co p = co bb⟦ c ⟧a p

    b-code-is-set : ∀ b₁ p₂ → is-set (b-code b₁ p₂)
    b-code-is-set b₁ = SCF.code-is-set b₁ ◯ pushout-flip

  -- Tail flipping
  open import Homotopy.VanKampen.Code.LemmaPackA d l public
    using () renaming
      ( aa⇒ba to aa⇒ba
      ; ab⇒bb to ab⇒bb
      ; ap⇒bp to ap⇒bp
      )
  open import Homotopy.VanKampen.Code.LemmaPackA (pushout-diag-flip d) l public
    using () renaming
      ( aa⇒ba to bb⇒ab
      ; ab⇒bb to ba⇒aa
      )

  -- Tail drifting
  open import Homotopy.VanKampen.Code.LemmaPackB d l public
    using () renaming
      ( trans-q-code-a  to trans-q-a-code-a
      ; trans-!q-code-a to trans-!q-a-code-a
      ; trans-q-code-ba to trans-q-a-code-ba
      ; trans-q-code-ab to trans-q-a-code-ab
      )
  open import Homotopy.VanKampen.Code.LemmaPackB (pushout-diag-flip d) l public
    using () renaming
      ( trans-q-code-a  to trans-q-b-code-b
      ; trans-!q-code-a to trans-!q-b-code-b
      ; trans-q-code-ba to trans-q-b-code-ab
      ; trans-q-code-ab to trans-q-b-code-ba
      )

  bp⇒ap : ∀ n {p} → b-code (g $ loc n) p → a-code (f $ loc n) p
  bp⇒ap n {p} = transport
    (λ x → b-code (g $ loc n) p → a-code (f $ loc n) x)
    (pushout-flip-flip p)
    (CF.ap⇒bp n {pushout-flip p})

  private
    Laba : name → P → Set i
    Laba = λ n p → ∀ (co : a-code (f $ loc n) p) → bp⇒ap n {p} (ap⇒bp n {p} co) ≡ co
  private
    aba-glue-code : ∀ c {p} → Laba c p
  abstract
    aba-glue-code n {p} = pushout-rec (Laba n)
      (λ _ → C.aba-glue-code-a n)
      (λ _ → C.aba-glue-code-b n)
      (λ _ → funext λ _ → prop-has-all-paths (a-code-b-is-set (f $ loc n) _ _ _) _ _)
      p

  private
    Lbab : name → P → Set i
    Lbab = λ n p → ∀ (co : b-code (g $ loc n) p) → ap⇒bp n {p} (bp⇒ap n {p} co) ≡ co
  private
    bab-glue-code : ∀ n {p} → Lbab n p
  abstract
    bab-glue-code n {p} = pushout-rec (Lbab n)
      (λ _ → CF.aba-glue-code-b n)
      (λ _ → CF.aba-glue-code-a n)
      (λ _ → funext λ _ → prop-has-all-paths (b-code-b-is-set (g $ loc n) _ _ _) _ _)
      p

  private
    glue-code-loc : ∀ n p → a-code (f $ loc n) p ≃ b-code (g $ loc n) p
    glue-code-loc n p = ap⇒bp n {p} , iso-is-eq
      (ap⇒bp n {p}) (bp⇒ap n {p}) (bab-glue-code n {p}) (aba-glue-code n {p})

  private
    TapbpTa : ∀ n₁ n₂ (r : loc n₁ ≡ loc n₂) {a}
      → a-code-a (f $ loc n₂) a → Set i
    TapbpTa n₁ n₂ r {a} co =
        transport (λ x → b-code-a x a) (ap g r)
          (aa⇒ba n₁ {a} $ transport (λ x → a-code-a x a) (! $ ap f r) co)
      ≡ aa⇒ba n₂ {a} co

    TapbpTb : ∀ n₁ n₂ (r : loc n₁ ≡ loc n₂) {b}
      → a-code-b (f $ loc n₂) b → Set i
    TapbpTb n₁ n₂ r {b} co =
        transport (λ x → b-code-b x b) (ap g r)
          (ab⇒bb n₁ {b} $ transport (λ x → a-code-b x b) (! $ ap f r) co)
      ≡ ab⇒bb n₂ {b} co

    TapbpTp : ∀ n₁ n₂ (r : loc n₁ ≡ loc n₂) {p}
      → a-code (f $ loc n₂) p → Set i
    TapbpTp n₁ n₂ r {p} co =
        transport (λ x → b-code x p) (ap g r)
          (ap⇒bp n₁ {p} $ transport (λ x → a-code x p) (! $ ap f r) co)
      ≡ ap⇒bp n₂ {p} co

  private
    ap⇒bp-shift-split : ∀ n₁ n₂ r
      → (∀ {a₂} co → TapbpTa n₁ n₂ r {a₂} co)
      × (∀ {b₂} co → TapbpTb n₁ n₂ r {b₂} co)
  abstract
    ap⇒bp-shift-split n₁ n₂ r = a-code-rec (f $ loc n₂)
      (TapbpTa n₁ n₂ r)
      ⦃ λ _ → ≡-is-set $ b-code-a-is-set _ _ ⦄
      (TapbpTb n₁ n₂ r)
      ⦃ λ _ → ≡-is-set $ b-code-b-is-set _ _ ⦄
      (λ {a} p →
        transport (λ x → b-code-a x a) (ap g r)
          (aa⇒ba n₁ {a} $ transport (λ x → a-code-a x a) (! $ ap f r) $ ⟧a p)
            ≡⟨ ap (transport (λ x → b-code-a x a) (ap g r) ◯ aa⇒ba n₁ {a})
                  $ trans-!q-a-code-a (ap f r) p ⟩
        transport (λ x → b-code-a x a) (ap g r)
          (⟧b refl₀ bb⟦ n₁ ⟧a proj (ap f r) ∘₀ p)
            ≡⟨ trans-q-b-code-ba (ap g r) _ _ _ ⟩
        transport (λ x → b-code-b x (g $ loc n₁)) (ap g r) (⟧b refl₀)
          bb⟦ n₁ ⟧a proj (ap f r) ∘₀ p
            ≡⟨ ap (λ x → x bb⟦ n₁ ⟧a proj (ap f r) ∘₀ p) $ trans-q-b-code-b (ap g r) _ ⟩
        ⟧b proj (! (ap g r)) ∘₀ refl₀ bb⟦ n₁ ⟧a proj (ap f r) ∘₀ p
            ≡⟨ ap (λ x → ⟧b x bb⟦ n₁ ⟧a proj (ap f r) ∘₀ p) $ refl₀-right-unit _ ⟩
        ⟧b proj (! (ap g r)) bb⟦ n₁ ⟧a proj (ap f r) ∘₀ p
            ≡⟨ ! $ SCF.code-a-shift (g $ loc n₂) n₁ (proj (! (ap g r))) n₂ (proj r) p ⟩
        ⟧b proj (! (ap g r) ∘ ap g r) bb⟦ n₂ ⟧a p
            ≡⟨ ap (λ x → ⟧b proj x bb⟦ n₂ ⟧a p) $ opposite-left-inverse $ ap g r ⟩∎
        aa⇒ba n₂ {a} (⟧a p)
            ∎)
      (λ {a} n {co} pco p →
        transport (λ x → b-code-a x a) (ap g r)
          (aa⇒ba n₁ {a} $ transport (λ x → a-code-a x a) (! $ ap f r) $ co ab⟦ n ⟧a p)
            ≡⟨ ap (transport (λ x → b-code-a x a) (ap g r) ◯ aa⇒ba n₁ {a})
                  $ trans-q-a-code-ba (! $ ap f r) n co p ⟩
        transport (λ x → b-code-a x a) (ap g r)
          (ab⇒bb n₁ {g $ loc n} (transport (λ x → a-code-b x (g $ loc n)) (! $ ap f r) co) bb⟦ n ⟧a p)
            ≡⟨ trans-q-b-code-ba (ap g r) _ _ _ ⟩
        transport (λ x → b-code-b x (g $ loc n)) (ap g r)
          (ab⇒bb n₁ {g $ loc n} (transport (λ x → a-code-b x (g $ loc n)) (! $ ap f r) co)) bb⟦ n ⟧a p
            ≡⟨ ap (λ x → x bb⟦ n ⟧a p) pco ⟩∎
        ab⇒bb n₂ {g $ loc n} co bb⟦ n ⟧a p
            ∎)
      (λ {b} n {co} pco p →
        transport (λ x → b-code-b x b) (ap g r)
          (ab⇒bb n₁ {b} $ transport (λ x → a-code-b x b) (! $ ap f r) $ co aa⟦ n ⟧b p)
            ≡⟨ ap (transport (λ x → b-code-b x b) (ap g r) ◯ ab⇒bb n₁ {b})
                  $ trans-q-a-code-ab (! $ ap f r) n co p ⟩
        transport (λ x → b-code-b x b) (ap g r)
          (aa⇒ba n₁ {f $ loc n} (transport (λ x → a-code-a x (f $ loc n)) (! $ ap f r) co) ba⟦ n ⟧b p)
            ≡⟨ trans-q-b-code-ab (ap g r) _ _ _ ⟩
        transport (λ x → b-code-a x (f $ loc n)) (ap g r)
          (aa⇒ba n₁ {f $ loc n} (transport (λ x → a-code-a x (f $ loc n)) (! $ ap f r) co)) ba⟦ n ⟧b p
            ≡⟨ ap (λ x → x ba⟦ n ⟧b p) pco ⟩∎
        aa⇒ba n₂ {f $ loc n} co ba⟦ n ⟧b p
            ∎)
      (λ _ _ → prop-has-all-paths (b-code-a-is-set _ _ _ _) _ _)
      (λ _ _ → prop-has-all-paths (b-code-b-is-set _ _ _ _) _ _)
      (λ _ _ _ _ → prop-has-all-paths (b-code-a-is-set _ _ _ _) _ _)

  private
    ap⇒bp-shift : ∀ n₁ n₂ r {p} co → TapbpTp n₁ n₂ r {p} co
  abstract
    ap⇒bp-shift n₁ n₂ r {p} co =
      pushout-rec
        (λ p → ∀ co → TapbpTp n₁ n₂ r {p} co)
        (λ a → π₁ (ap⇒bp-shift-split n₁ n₂ r) {a})
        (λ b → π₂ (ap⇒bp-shift-split n₁ n₂ r) {b})
        (λ c → funext λ _ → prop-has-all-paths (b-code-is-set (g $ loc n₂) (right $ g c) _ _) _ _)
        p co

  glue-code-eq-route : ∀ p n₁ n₂ (r : loc n₁ ≡ loc n₂)
    → transport (λ c → a-code (f c) p ≃ b-code (g c) p) r (glue-code-loc n₁ p)
    ≡ glue-code-loc n₂ p
  abstract
    glue-code-eq-route p n₁ n₂ r = equiv-eq $ funext λ co →
      π₁ (transport (λ c → a-code (f c) p ≃ b-code (g c) p) r (glue-code-loc n₁ p)) co
        ≡⟨ ap (λ x → x co) $ app-trans
            (λ c → a-code (f c) p ≃ b-code (g c) p)
            (λ c → a-code (f c) p → b-code (g c) p)
            (λ _ → π₁)
            r
            (glue-code-loc n₁ p) ⟩
      transport (λ c → a-code (f c) p → b-code (g c) p) r (ap⇒bp n₁ {p}) co
        ≡⟨ trans-→ (λ c → a-code (f c) p) (λ c → b-code (g c) p) r (ap⇒bp n₁ {p}) co ⟩
      transport (λ c → b-code (g c) p) r (ap⇒bp n₁ {p} $ transport (λ c → a-code (f c) p) (! r) co)
        ≡⟨ ap (transport (λ c → b-code (g c) p) r ◯ ap⇒bp n₁ {p}) $ ! $ trans-ap (λ x → a-code x p) f (! r) co ⟩
      transport (λ c → b-code (g c) p) r (ap⇒bp n₁ {p} $ transport (λ x → a-code x p) (ap f (! r)) co)
        ≡⟨ ap (λ x → transport (λ c → b-code (g c) p) r $ ap⇒bp n₁ {p}
                    $ transport (λ x → a-code x p) x co)
              $ ap-opposite f r ⟩
      transport (λ c → b-code (g c) p) r (ap⇒bp n₁ {p} $ transport (λ x → a-code x p) (! $ ap f r) co)
        ≡⟨ ! $ trans-ap (λ x → b-code x p) g r _ ⟩
      transport (λ x → b-code x p) (ap g r) (ap⇒bp n₁ {p} $ transport (λ x → a-code x p) (! $ ap f r) co)
        ≡⟨ ap⇒bp-shift n₁ n₂ r {p} co ⟩∎
      ap⇒bp n₂ {p} co
        ∎

  glue-code-eq : ∀ c p → a-code (f c) p ≃ b-code (g c) p
  glue-code-eq c p = visit-fiber-rec l (λ c → a-code (f c) p ≃ b-code (g c) p)
    ⦃ λ c → ≃-is-set (a-code-is-set (f c) p) (b-code-is-set (g c) p) ⦄
    (λ n → glue-code-loc n p)
    (glue-code-eq-route p)
    c

  code : P → P → Set i
  code = pushout-rec-nondep (P → Set i) a-code b-code
    (λ c → funext λ p → eq-to-path $ glue-code-eq c p)

  open import HLevelBis
  abstract
    code-is-set : ∀ p₁ p₂ → is-set (code p₁ p₂)
    code-is-set = pushout-rec
      (λ p₁ → ∀ p₂ → is-set $ code p₁ p₂)
      a-code-is-set
      b-code-is-set
      (λ _ → prop-has-all-paths (Π-is-prop λ _ → is-set-is-prop) _ _)

  -- Useful lemma
  module _ {a₁ : A} where
    open import Homotopy.VanKampen.SplitCode d l a₁
      public using () renaming
        ( trans-code-glue-loc   to trans-a-code-glue-loc
        ; trans-code-!glue-loc  to trans-a-code-!glue-loc
        )

  abstract
    trans-b-code-glue-loc : ∀ {b₁} n₂ co → transport (b-code b₁) (glue $ loc n₂) co ≡ ba⇒bb n₂ co
    trans-b-code-glue-loc {b₁} n₂ co =
      transport (b-code b₁) (glue $ loc n₂) co
          ≡⟨ ! $ trans-ap (SCF.code b₁) pushout-flip (glue $ loc n₂) co ⟩
      transport (SCF.code b₁) (ap pushout-flip (glue $ loc n₂)) co
          ≡⟨ ap (λ x → transport (SCF.code b₁) x co)
                $ pushout-β-glue-nondep _ right left (! ◯ glue) (loc n₂) ⟩
      transport (SCF.code b₁) (! (glue $ loc n₂)) co
          ≡⟨ SCF.trans-code-!glue-loc b₁ n₂ co ⟩∎
      ba⇒bb n₂ co
          ∎

  abstract
    trans-b-code-!glue-loc : ∀ {b₁} n₂ co → transport (b-code b₁) (! (glue $ loc n₂)) co ≡ bb⇒ba n₂ co
    trans-b-code-!glue-loc {b₁} n₂ co =
      transport (b-code b₁) (! (glue $ loc n₂)) co
          ≡⟨ ! $ trans-ap (SCF.code b₁) pushout-flip (! (glue $ loc n₂)) co ⟩
      transport (SCF.code b₁) (ap pushout-flip (! (glue $ loc n₂))) co
          ≡⟨ ap (λ x → transport (SCF.code b₁) x co)
                $ pushout-β-!glue-nondep _ right left (! ◯ glue) (loc n₂) ⟩
      transport (SCF.code b₁) (! (! (glue $ loc n₂))) co
          ≡⟨ ap (λ x → transport (SCF.code b₁) x co)
                $ opposite-opposite $ glue $ loc n₂ ⟩
      transport (SCF.code b₁) (glue $ loc n₂) co
          ≡⟨ SCF.trans-code-glue-loc b₁ n₂ co ⟩∎
      bb⇒ba n₂ co
          ∎

  abstract
    trans-glue-code-loc : ∀ n {p} (co : a-code (f $ loc n) p)
      → transport (λ x → code x p) (glue $ loc n) co
      ≡ ap⇒bp n {p} co
    trans-glue-code-loc n {p} co =
        transport (λ x → code x p) (glue $ loc n) co
            ≡⟨ ! $ trans-ap (λ f → f p) code (glue $ loc n) co ⟩
        transport (λ f → f p) (ap code (glue $ loc n)) co
            ≡⟨ ap (λ x →  transport (λ f → f p) x co)
                $ pushout-β-glue-nondep (P → Set i) a-code b-code
                  (λ c → funext λ p → eq-to-path $ glue-code-eq c p)
                $ loc n ⟩
        transport (λ f → f p) (funext λ p → eq-to-path $ glue-code-eq (loc n) p) co
            ≡⟨ ! $ trans-ap (λ X → X) (λ f → f p)
                    (funext λ p → eq-to-path $ glue-code-eq (loc n) p) co ⟩
        transport (λ X → X) (happly (funext λ p → eq-to-path $ glue-code-eq (loc n) p) p) co
            ≡⟨ ap (λ x → transport (λ X → X) (x p) co)
                  $ happly-funext (λ p → eq-to-path $ glue-code-eq (loc n) p) ⟩
        transport (λ X → X) (eq-to-path $ glue-code-eq (loc n) p) co
            ≡⟨ trans-id-eq-to-path (glue-code-eq (loc n) p) co ⟩
        π₁ (glue-code-eq (loc n) p) co
            ≡⟨ ap (λ x → π₁ x co) $
                visit-fiber-β-loc l
                (λ c → a-code (f c) p ≃ b-code (g c) p)
                ⦃ λ c → ≃-is-set (a-code-is-set (f c) p) (b-code-is-set (g c) p) ⦄
                (λ n → glue-code-loc n p)
                (glue-code-eq-route p)
                n ⟩∎
        ap⇒bp n {p} co
            ∎

  abstract
    trans-!glue-code-loc : ∀ n {p} (co : b-code (g $ loc n) p)
      → transport (λ x → code x p) (! $ glue $ loc n) co
      ≡ bp⇒ap n {p} co
    trans-!glue-code-loc n {p} co =
      move!-transp-right (λ x → code x p) (glue $ loc n) co (bp⇒ap n {p} co)
        $ ! $
          transport (λ x → code x p) (glue $ loc n) (bp⇒ap n {p} co)
            ≡⟨ trans-glue-code-loc n {p} (bp⇒ap n {p} co) ⟩
          ap⇒bp n {p} (bp⇒ap n {p} co)
            ≡⟨ bab-glue-code n {p} co ⟩∎
          co
            ∎


text:
open import Prelude
open import core

module lemmas-consistency where
  -- type consistency is symmetric
  ~sym : {t1 t2 : typ} → t1 ~ t2 → t2 ~ t1
  ~sym TCRefl = TCRefl
  ~sym TCHole1 = TCHole2
  ~sym TCHole2 = TCHole1
  ~sym (TCArr p1 p2) = TCArr (~sym p1) (~sym p2)
  ~sym (TCProd h h₁) = TCProd (~sym h) (~sym h₁)

  -- type consistency isn't transitive
  not-trans : ((t1 t2 t3 : typ) → t1 ~ t2 → t2 ~ t3 → t1 ~ t3) → ⊥
  not-trans t with t (b ==> b) ⦇·⦈ b TCHole1 TCHole2
  ... | ()

  --  every pair of types is either consistent or not consistent
  ~dec : (t1 t2 : typ) → ((t1 ~ t2) + (t1 ~̸ t2))
    -- this takes care of all hole cases, so we don't consider them below
  ~dec _ ⦇·⦈ = Inl TCHole1
  ~dec ⦇·⦈ b = Inl TCHole2
  ~dec ⦇·⦈ (q ==> q₁) = Inl TCHole2
  ~dec ⦇·⦈ (q ⊗ q₁) = Inl TCHole2
    -- num cases
  ~dec b b = Inl TCRefl
  ~dec b (t2 ==> t3) = Inr ICBaseArr1
    -- arrow cases
  ~dec (t1 ==> t2) b = Inr ICBaseArr2
  ~dec (t1 ==> t2) (t3 ==> t4) with ~dec t1 t3 | ~dec t2 t4
  ... | Inl x | Inl y = Inl (TCArr x y)
  ... | Inl _ | Inr y = Inr (ICArr2 y)
  ... | Inr x | _     = Inr (ICArr1 x)
  ~dec b (t2 ⊗ t3) = Inr ICBaseProd1
  ~dec (t1 ==> t2) (t3 ⊗ t4) = Inr ICProdArr1
  ~dec (t1 ⊗ t2) b = Inr ICBaseProd2
  ~dec (t1 ⊗ t2) (t3 ==> t4) = Inr ICProdArr2
  ~dec (t1 ⊗ t2) (t3 ⊗ t4) with ~dec t1 t3 | ~dec t2 t4
  ~dec (t1 ⊗ t2) (t3 ⊗ t4) | Inl x | Inl x₁ = Inl (TCProd x x₁)
  ~dec (t1 ⊗ t2) (t3 ⊗ t4) | Inl x | Inr x₁ = Inr (ICProd2 x₁)
  ~dec (t1 ⊗ t2) (t3 ⊗ t4) | Inr x | Inl x₁ = Inr (ICProd1 x)
  ~dec (t1 ⊗ t2) (t3 ⊗ t4) | Inr x | Inr x₁ = Inr (ICProd1 x)

  -- no pair of types is both consistent and not consistent
  ~apart : {t1 t2 : typ} → (t1 ~̸ t2) → (t1 ~ t2) → ⊥
  ~apart ICBaseArr1 ()
  ~apart ICBaseArr2 ()
  ~apart (ICArr1 x) TCRefl = ~apart x TCRefl
  ~apart (ICArr1 x) (TCArr y y₁) = ~apart x y
  ~apart (ICArr2 x) TCRefl = ~apart x TCRefl
  ~apart (ICArr2 x) (TCArr y y₁) = ~apart x y₁
  ~apart ICBaseProd1 ()
  ~apart ICBaseProd2 ()
  ~apart ICProdArr1 ()
  ~apart ICProdArr2 ()
  ~apart (ICProd1 h) TCRefl = ~apart h TCRefl
  ~apart (ICProd1 h) (TCProd h₁ h₂) = ~apart h h₁
  ~apart (ICProd2 h) TCRefl = ~apart h TCRefl
  ~apart (ICProd2 h) (TCProd h₁ h₂) = ~apart h h₂

  ~apart-converse : (τ1 τ2 : typ) → (τ1 ~ τ2 → ⊥) → τ1 ~̸ τ2
  ~apart-converse τ1 τ2 ne with ~dec τ1 τ2
  ~apart-converse τ1 τ2 ne    | Inl h      = abort (ne h)
  ~apart-converse τ1 τ2 ne    | Inr h      = h

  ~decPair : (τ1 τ2 τ3 τ4 : typ) → ((τ1 ⊗ τ2) ~ (τ3 ⊗ τ4) → ⊥) → (τ1 ~ τ3 → ⊥) + (τ2 ~ τ4 → ⊥)
  ~decPair τ1 τ2 τ3 τ4 inc with ~apart-converse (τ1 ⊗ τ2) (τ3 ⊗ τ4) inc
  ~decPair τ1 τ2 τ3 τ4 inc    | ICProd1 h                                = Inl (~apart h)
  ~decPair τ1 τ2 τ3 τ4 inc    | ICProd2 h                                = Inr (~apart h)

  ~prod1 : ∀{τ1 τ2 τ3 τ4} → (τ1 ⊗ τ2) ~ (τ3 ⊗ τ4) → τ1 ~ τ3
  ~prod1 TCRefl = TCRefl
  ~prod1 (TCProd h1 h2) = h1

  ~prod2 : ∀{τ1 τ2 τ3 τ4} → (τ1 ⊗ τ2) ~ (τ3 ⊗ τ4) → τ2 ~ τ4
  ~prod2 TCRefl = TCRefl
  ~prod2 (TCProd h1 h2) = h2

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda


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

module Relation.Nullary.Discrete where

open import Relation.Nullary.Decidable
open import Path
open import Level

Discrete : Type a → Type a
Discrete A = (x y : A) → Dec (x ≡ y)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Andreas, 2017-10-04, issue #689, test case by stevana

-- {-# OPTIONS -v tc.data:50 #-}
-- {-# OPTIONS -v tc.force:100 #-}
-- {-# OPTIONS -v tc.constr:50 #-}
-- {-# OPTIONS -v tc.conv.sort:30 #-}
-- {-# OPTIONS -v tc.conv.nat:30 #-}

open import Agda.Primitive

data L {a} (A : Set a) : Set a where
  _∷_ : A → L A → L A

data S {a} {A : Set a} : L A → Set₁ where
  _∷_ : (x : A) → (xs : L A) → S (x ∷ xs)  -- x and xs are forced!

-- Should succeed without unsolved constraints.

-- There was a problem in the forcing analysis which I introduced
-- with apparently improper use of `noConstraints` (still do not know why)
-- for the Big/Small Forced argument analysis.
-- The latter one is obsolete and thus removed.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Data.Num.Injection where

open import Data.Num.Core

open import Data.Nat hiding (compare)
open import Data.Nat.Properties
open import Data.Nat.Properties.Simple
open import Data.Nat.Properties.Extra

open import Data.Fin as Fin
    using (Fin; fromℕ≤; inject≤)
    renaming (zero to z; suc to s)
open import Data.Fin.Properties
    using (toℕ-fromℕ≤; to-from; bounded; inject≤-lemma)
    renaming (toℕ-injective to Fin→ℕ-injective; _≟_ to _Fin≟_)
open import Data.Fin.Properties.Extra
open import Data.Sum
open import Data.Product
open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)

open import Function
open import Function.Injection
open Injection
-- open import Function.Equality using (_⟶_; _⟨$⟩_)
open import Relation.Nullary.Decidable
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open ≡-Reasoning
open ≤-Reasoning renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≈⟨_⟩_)
open DecTotalOrder decTotalOrder using (reflexive) renaming (refl to ≤-refl)
open StrictTotalOrder strictTotalOrder using (compare)

data InjCond : ℕ → ℕ → ℕ → Set where
    Ordinary  : ∀ {b d o} → (b≥d : b ≥ d) → (o≥1 : o ≥ 1) → InjCond b d o
    Digitless : ∀ {b d o}                 → (d≡0 : d ≡ 0) → InjCond b 0 o -- having no digits at all

data NonInjCond : ℕ → ℕ → ℕ → Set where
    Redundant : ∀ {b d o}                  → (d>b : d > b) → NonInjCond b d o -- having to many digits
    WithZeros : ∀ {b d o} → (o≡0 : o ≡ 0) → (d≢0 : d ≢ 0) → NonInjCond b d 0 -- with leading zeroes

data InjectionView : ℕ → ℕ → ℕ → Set where
    Inj    : ∀ {b d o} → InjCond    b d o → InjectionView b d o
    NonInj : ∀ {b d o} → NonInjCond b d o → InjectionView b d o

injectionView : (b d o : ℕ) → InjectionView b d o
injectionView b zero    zero    = Inj    (Digitless refl)
injectionView b (suc d) zero    = NonInj (WithZeros refl (λ ()))
injectionView b d       (suc o) with d ≤? b
injectionView b d       (suc o) | yes p = Inj    (Ordinary p (s≤s z≤n))
injectionView b d       (suc o) | no ¬p = NonInj (Redundant (≰⇒> ¬p))

IsInjective : ℕ → ℕ → ℕ → Set
IsInjective b d o with injectionView b d o
IsInjective b d o | Inj    _ = ⊤
IsInjective b d o | NonInj _ = ⊥

InjCond⇒IsInj : ∀ {b d o} → InjCond b d o → IsInjective b d o
InjCond⇒IsInj {b} {d} {o} cond with injectionView b d o
InjCond⇒IsInj _                  | Inj _ = tt
InjCond⇒IsInj (Ordinary b≥d o≥1) | NonInj (Redundant d>b) = contradiction b≥d (>⇒≰ d>b)
InjCond⇒IsInj (Ordinary b≥d ())  | NonInj (WithZeros o≡0 d≢0)
InjCond⇒IsInj (Digitless d≡0)    | NonInj (Redundant ())
InjCond⇒IsInj (Digitless d≡0)    | NonInj (WithZeros refl d≢0) = contradiction refl d≢0

-- InjCond⇒b≥1 : ∀ {b d o} → InjCond b (suc d) o → b ≥ 1
-- InjCond⇒b≥1 {zero}  (bijCond b≥d: o≥1:) = contradiction b≥d: (>⇒≰ (s≤s z≤n))
-- InjCond⇒b≥1 {suc b} (bijCond b≥d: o≥1:) = s≤s z≤n
--

NonInjCond⇏IsInj : ∀ {b d o} → NonInjCond b d o → ¬ IsInjective b d o
NonInjCond⇏IsInj {b} {d} {o} reason claim with injectionView b d o
NonInjCond⇏IsInj (Redundant d>b)     claim | Inj (Ordinary b≥d o≥1) = contradiction b≥d (>⇒≰ d>b)
NonInjCond⇏IsInj (Redundant ())      claim | Inj (Digitless d≡0)
NonInjCond⇏IsInj (WithZeros o≡0 d≢0) claim | Inj (Ordinary b≥d ())
NonInjCond⇏IsInj (WithZeros o≡0 d≢0) claim | Inj (Digitless d≡0) = contradiction refl d≢0
NonInjCond⇏IsInj reason              ()    | NonInj _

Digit-toℕ-injective : ∀ {d} o (x y : Fin d)
    → Digit-toℕ x o ≡ Digit-toℕ y o -- o + toℕ x ≡ o + toℕ y
    → x ≡ y
Digit-toℕ-injective {_} o x y eq =
    Fin→ℕ-injective         -- cancels `Fin.toℕ`
        $ cancel-+-left o    -- cancels `o +`
        $ eq

n∷-mono-strict : ∀ {b d o} (x y : Fin d) (xs ys : Num b d o)
    → InjCond b d o
    → toℕ xs < toℕ ys
    → toℕ (x ∷ xs) < toℕ (y ∷ ys)
n∷-mono-strict {b} {_} {o} () () xs ys (Digitless d≡0)    ⟦xs⟧<⟦ys⟧
n∷-mono-strict {b} {d} {o} x  y  xs ys (Ordinary b≥d o≥1) ⟦xs⟧<⟦ys⟧ =
    start
        suc (Digit-toℕ x o) + toℕ xs * b
    ≤⟨ +n-mono (toℕ xs * b) $
        start
            suc (Digit-toℕ x o)
        ≈⟨ sym (+-suc o (Fin.toℕ x)) ⟩
            -- push `o` to the left
            o + suc (Fin.toℕ x)
        ≤⟨ n+-mono o $
            start
                suc (Fin.toℕ x)
            ≤⟨ bounded x ⟩
                d
            ≤⟨ b≥d ⟩
                b
            ≤⟨ n≤m+n (Fin.toℕ y) b ⟩
                Fin.toℕ y + b
        □ ⟩
            o + (Fin.toℕ y + b)
        ≈⟨ sym (+-assoc o (Fin.toℕ y) b) ⟩
            Digit-toℕ y o + b
    □ ⟩
        Digit-toℕ y o + b + toℕ xs * b
    ≈⟨ +-assoc (Digit-toℕ y o) b (toℕ xs * b) ⟩
        Digit-toℕ y o + (b + toℕ xs * b)
    ≤⟨ n+-mono (Digit-toℕ y o) (*n-mono b ⟦xs⟧<⟦ys⟧) ⟩  -- replace `xs` with `ys`
        Digit-toℕ y o + toℕ ys * b
    □

∷ns-mono-strict : ∀ {b d o} (x y : Fin d) (xs ys : Num b d o)
    → toℕ xs ≡ toℕ ys
    → Digit-toℕ x o < Digit-toℕ y o
    → toℕ (x ∷ xs) < toℕ (y ∷ ys)
∷ns-mono-strict {b} {d} {o} x y xs ys ⟦xs⟧≡⟦ys⟧ ⟦x⟧<⟦y⟧ = start
        suc (Digit-toℕ x o + toℕ xs * b)
    ≈⟨ cong (λ w → suc (Digit-toℕ x o + w * b)) ⟦xs⟧≡⟦ys⟧ ⟩
        suc (Digit-toℕ x o + toℕ ys * b)
    ≤⟨ +n-mono (toℕ ys * b) ⟦x⟧<⟦y⟧ ⟩
        Digit-toℕ y o + toℕ ys * b
    □

toℕ-injective-⟦x∷xs⟧>0-lemma : ∀ {b d o}
    → o ≥ 1
    → (x : Fin d)
    → (xs : Num b d o)
    → toℕ (x ∷ xs) > 0
toℕ-injective-⟦x∷xs⟧>0-lemma {b} {d} {o} o≥1 x xs =
    start
        suc zero
    ≤⟨ o≥1 ⟩
        o
    ≤⟨ m≤m+n o (Fin.toℕ x) ⟩
        o + Fin.toℕ x
    ≤⟨ m≤m+n (o + Fin.toℕ x) (toℕ xs * b) ⟩
        o + Fin.toℕ x + toℕ xs * b
    □

toℕ-injective : ∀ {b d o}
    → {isInj : IsInjective b d o}
    → (xs ys : Num b d o)
    → toℕ xs ≡ toℕ ys
    → xs ≡ ys
toℕ-injective {b} {d} {o} xs ys eq with injectionView b d o
toℕ-injective                 ∙        ∙        eq | Inj (Ordinary b≥d o≥1) = refl
toℕ-injective                 ∙        (y ∷ ys) eq | Inj (Ordinary b≥d o≥1) = contradiction eq (<⇒≢ (toℕ-injective-⟦x∷xs⟧>0-lemma o≥1 y ys))
toℕ-injective                 (x ∷ xs) ∙        eq | Inj (Ordinary b≥d o≥1) = contradiction eq (>⇒≢ (toℕ-injective-⟦x∷xs⟧>0-lemma o≥1 x xs))
toℕ-injective {b} {zero} {o} (() ∷ xs) (y ∷ ys) eq | Inj cond
toℕ-injective {b} {suc d} {o} (x ∷ xs) (y ∷ ys) eq | Inj cond with compare (toℕ xs) (toℕ ys)
toℕ-injective {b} {suc d} {o} (x ∷ xs) (y ∷ ys) eq | Inj cond | tri< ⟦xs⟧<⟦ys⟧ _ _ = contradiction eq (<⇒≢ (n∷-mono-strict x y xs ys cond ⟦xs⟧<⟦ys⟧))
toℕ-injective {b} {suc d} {o} (x ∷ xs) (y ∷ ys) eq | Inj cond | tri≈ _ ⟦xs⟧≡⟦ys⟧ _ with compare (Digit-toℕ x o) (Digit-toℕ y o)
toℕ-injective {b} {suc d} {o} (x ∷ xs) (y ∷ ys) eq | Inj cond | tri≈ _ ⟦xs⟧≡⟦ys⟧ _ | tri< ⟦x⟧<⟦y⟧ _ _ = contradiction eq (<⇒≢ (∷ns-mono-strict x y xs ys ⟦xs⟧≡⟦ys⟧ ⟦x⟧<⟦y⟧))
toℕ-injective {b} {suc d} {o} (x ∷ xs) (y ∷ ys) eq | Inj cond | tri≈ _ ⟦xs⟧≡⟦ys⟧ _ | tri≈ _ ⟦x⟧≡⟦y⟧ _ = cong₂ _∷_ (Digit-toℕ-injective o x y ⟦x⟧≡⟦y⟧) (toℕ-injective {isInj = InjCond⇒IsInj cond} xs ys ⟦xs⟧≡⟦ys⟧)
toℕ-injective {b} {suc d} {o} (x ∷ xs) (y ∷ ys) eq | Inj cond | tri≈ _ ⟦xs⟧≡⟦ys⟧ _ | tri> _ _ ⟦x⟧>⟦y⟧ = contradiction eq (>⇒≢ (∷ns-mono-strict y x ys xs (sym ⟦xs⟧≡⟦ys⟧) ⟦x⟧>⟦y⟧))
toℕ-injective {b} {suc d} {o} (x ∷ xs) (y ∷ ys) eq | Inj cond | tri> _ _ ⟦xs⟧>⟦ys⟧ = contradiction eq (>⇒≢ ((n∷-mono-strict y x ys xs cond ⟦xs⟧>⟦ys⟧)))
toℕ-injective                 ∙        ∙        eq | Inj (Digitless d≡0) = refl
toℕ-injective                 ∙       (() ∷ ys) eq | Inj (Digitless d≡0)
toℕ-injective                 (() ∷ xs) ys      eq | Inj (Digitless d≡0)
toℕ-injective {isInj = ()}    xs        ys      eq | NonInj reason

InjCond⇒Injective : ∀ {b} {d} {o} → InjCond b d o → Injective (Num⟶ℕ b d o)
InjCond⇒Injective condition {x} {y} = toℕ-injective {isInj = InjCond⇒IsInj condition} x y

NonInjCond⇏Injective : ∀ {b} {d} {o} → NonInjCond b d o → ¬ (Injective (Num⟶ℕ b d o))
NonInjCond⇏Injective {zero} {zero}      (Redundant ()) claim
NonInjCond⇏Injective {zero} {suc d} {o} (Redundant d>b) claim =
    contradiction
        (claim
            {z ∷ ∙}
            {z ∷ z ∷ ∙}
            ⟦1∷∙⟧≡⟦1∷1∷∙⟧)
        (λ ())
    where   ⟦1∷∙⟧≡⟦1∷1∷∙⟧ : toℕ {zero} {suc d} {o} (z ∷ ∙) ≡ toℕ {zero} {suc d} {o} (z ∷ z ∷ ∙)
            ⟦1∷∙⟧≡⟦1∷1∷∙⟧ = cong (λ w → o + 0 + w) (sym (*-right-zero (o + 0 + 0)))
NonInjCond⇏Injective {suc b} {zero} (Redundant ()) claim
NonInjCond⇏Injective {suc b} {suc zero} (Redundant (s≤s ())) claim
NonInjCond⇏Injective {suc b} {suc (suc d)} {o} (Redundant d>b) claim =
    contradiction
        (claim
            {z ∷ s z ∷ ∙}
            {fromℕ≤ d>b ∷ z ∷ ∙}
            ⟦1∷2⟧≡⟦b+1∷1⟧)
        (λ ())
    where   ⟦1∷2⟧≡⟦b+1∷1⟧ : toℕ {suc b} {suc (suc d)} {o} (z ∷ s z ∷ ∙) ≡ toℕ {suc b} {suc (suc d)} {o} (fromℕ≤ {suc b} d>b ∷ z ∷ ∙)
            ⟦1∷2⟧≡⟦b+1∷1⟧ =
                begin
                    o + zero + (o + suc zero + zero) * suc b
                ≡⟨ cong (λ x → x + (o + suc zero + zero) * suc b) (+-right-identity o) ⟩
                    o + (o + suc zero + zero) * suc b
                ≡⟨ cong (λ x → o + (x + zero) * suc b) (+-suc o zero) ⟩
                    o + (suc (o + zero) + zero) * suc b
                ≡⟨ refl ⟩
                    o + (suc b + (o + zero + zero) * suc b)
                ≡⟨ sym (+-assoc o (suc b) ((o + zero + zero) * suc b)) ⟩
                    o + suc b + (o + zero + zero) * suc b
                ≡⟨ cong (λ x → o + x + (o + zero + zero) * suc b) (sym (toℕ-fromℕ≤ d>b)) ⟩
                    o + Fin.toℕ (fromℕ≤ d>b) + (o + zero + zero) * suc b
                ∎
NonInjCond⇏Injective {b} {zero} {_} (WithZeros o≡0 d≢0) claim = contradiction refl d≢0
NonInjCond⇏Injective {b} {suc d} {_} (WithZeros o≡0 d≢0) claim =
    contradiction
        (claim
            {z ∷ ∙}
            {∙}
            ⟦0∷∙⟧≡⟦∙⟧)
        (λ ())
    where   ⟦0∷∙⟧≡⟦∙⟧ : toℕ {b} {suc d} {0} (z ∷ ∙) ≡ toℕ {b} {suc d} {0} ∙
            ⟦0∷∙⟧≡⟦∙⟧ = refl

Injective? : ∀ b d o → Dec (Injective (Num⟶ℕ b d o))
Injective? b d o with injectionView b d o
Injective? b d o | Inj condition = yes (InjCond⇒Injective condition)
Injective? b d o | NonInj reason = no (NonInjCond⇏Injective reason)

-- begin
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ∎

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral