text:
module Numeral.Natural.Function.GreatestCommonDivisor.Proofs where

open import Data
open import Functional
open import Logic.Propositional
open import Numeral.Finite
open import Numeral.Natural
open import Numeral.Natural.Function.GreatestCommonDivisor
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.FlooredDivision
open import Numeral.Natural.Oper.FlooredDivision.Proofs.Inverse
open import Numeral.Natural.Oper.Modulo
open import Numeral.Natural.Relation.Divisibility
open import Numeral.Natural.Relation.Divisibility.Proofs
open import Numeral.Natural.Relation.Divisibility.Proofs.Modulo
open import Numeral.Natural.Relation.Order
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Relator
open import Structure.Relator.Properties
open import Structure.Operator
open import Structure.Operator.Properties
open import Syntax.Number
open import Syntax.Transitivity

private variable a b c d d₁ d₂ : ℕ

gcd-same : (gcd(a)(a) ≡ a)
gcd-same = [↔]-to-[→] Gcd-gcd-value (Gcd.intro₂ (reflexivity(_∣_)) (reflexivity(_∣_)) (const id))

instance
  gcd-identityₗ : Identityₗ(gcd)(𝟎)
  Identityₗ.proof gcd-identityₗ = [↔]-to-[→] Gcd-gcd-value (Gcd.intro₂ Div𝟎 (reflexivity(_∣_)) (const id))

instance
  gcd-identityᵣ : Identityᵣ(gcd)(𝟎)
  Identityᵣ.proof gcd-identityᵣ = [≡]-intro

instance
  gcd-absorberₗ : Absorberₗ(gcd)(1)
  Absorberₗ.proof gcd-absorberₗ{b} = [↔]-to-[→] (Gcd-gcd-value{_}{b}) (Gcd.intro₂ [1]-divides [1]-divides const)

instance
  gcd-absorberᵣ : Absorberᵣ(gcd)(1)
  Absorberᵣ.proof gcd-absorberᵣ{a} = [↔]-to-[→] (Gcd-gcd-value{a}{_}) (Gcd.intro₂ [1]-divides [1]-divides (const id))

instance
  gcd-commutativity : Commutativity(gcd)
  Commutativity.proof gcd-commutativity {x}{y} = [↔]-to-[→] (Gcd-gcd-value {x}{y}) (Gcd-swap Gcd-gcd)

instance
  gcd-associativity : Associativity(gcd)
  Associativity.proof gcd-associativity {x}{y}{z} = [↔]-to-[→] (Gcd-gcd-value) (assoc Gcd-gcd Gcd-gcd Gcd-gcd) where
    assoc : Gcd x y d₁ → Gcd y z d₂ → Gcd x d₂ d → Gcd d₁ z d
    assoc xyd₁ yzd₂ xd₂d =
      let d₁x   = Gcd.divisorₗ xyd₁
          d₁y   = Gcd.divisorᵣ xyd₁
          xyd₁m = Gcd.maximum₂ xyd₁
          d₂y   = Gcd.divisorₗ yzd₂
          d₂z   = Gcd.divisorᵣ yzd₂
          yzd₂m = Gcd.maximum₂ yzd₂
          dx    = Gcd.divisorₗ xd₂d
          dd₂   = Gcd.divisorᵣ xd₂d
          xd₂dm = Gcd.maximum₂ xd₂d
      in Gcd.intro₂
        (xyd₁m dx (dd₂ 🝖 d₂y))
        (dd₂ 🝖 d₂z)
        (\dd₁ dz → xd₂dm (dd₁ 🝖 d₁x) (xd₂dm (dd₁ 🝖 d₁x) (yzd₂m (dd₁ 🝖 d₁y) dz) 🝖 dd₂))

gcd-dividesₗ : (gcd(a)(b) ∣ a)
gcd-dividesₗ {a}{b} = Gcd.divisorₗ{a}{b} Gcd-gcd

gcd-dividesᵣ : (gcd(a)(b) ∣ b)
gcd-dividesᵣ {a}{b} = Gcd.divisorᵣ{a}{b} Gcd-gcd

gcd-divisors : (d ∣ a) → (d ∣ b) → (d ∣ gcd(a)(b))
gcd-divisors da db = Gcd.maximum₂ Gcd-gcd da db

gcd-of-mod : (gcd(a mod 𝐒(b))(𝐒(b)) ≡ gcd(a)(𝐒(b)))
gcd-of-mod{a}{b} = [↔]-to-[→] (Gcd-gcd-value{a mod 𝐒(b)}{𝐒(b)}) (p Gcd-gcd) where
  p : Gcd(a)(𝐒(b)) d → Gcd(a mod 𝐒(b))(𝐒(b)) d
  p abd =
    let da = Gcd.divisorₗ abd
        db = Gcd.divisorᵣ abd
        m  = Gcd.maximum₂ abd
    in Gcd.intro₂ ([↔]-to-[→] (divides-mod db) da) db (Dab ↦ Db ↦ m ([↔]-to-[←] (divides-mod Db) Dab) Db)

-- TODO: Is it neccessary to prove this? By gcd-dividesₗ and gcd-dividesᵣ, one get (gcd(a)(b) ∣ min(a)(b)) and the divisor is always smaller
-- gcd-min-order : (gcd(a)(b) ≤ min(a)(b))

gcd-with-[+] : (gcd(a + b)(b) ≡ gcd(a)(b))
gcd-with-[+] {a}{b} = [↔]-to-[→] Gcd-gcd-value (p Gcd-gcd) where
  p : Gcd(a)(b) d → Gcd(a + b)(b) d
  p abd =
    let da = Gcd.divisorₗ abd
        db = Gcd.divisorᵣ abd
        m  = Gcd.maximum₂ abd
    in Gcd.intro₂ (divides-with-[+] da db) db (Dab ↦ Db ↦ m ([↔]-to-[←] (divides-without-[+] Dab) Db) Db)

gcd-with₁-[⋅] : (gcd(a ⋅ b)(b) ≡ b)
gcd-with₁-[⋅] {a}{b} = [↔]-to-[→] (Gcd-gcd-value {a ⋅ b}{b}) (Gcd.intro₂ (divides-with-[⋅] {b}{a} ([∨]-introᵣ (reflexivity(_∣_)))) (reflexivity(_∣_)) (const id))

gcd-with-[⋅] : (gcd(a ⋅ c)(b ⋅ c) ≡ gcd(a)(b) ⋅ c)
gcd-with-[⋅] {a}{𝟎}   {b} = [≡]-intro
gcd-with-[⋅] {a}{𝐒(c)}{b} =
  gcd(a ⋅ 𝐒(c)) (b ⋅ 𝐒(c))                 🝖[ _≡_ ]-[ q ]-sym
  gcd(a ⋅ 𝐒(c)) (b ⋅ 𝐒(c)) ⌊/⌋ 𝐒(c) ⋅ 𝐒(c) 🝖[ _≡_ ]-[ congruence₂ₗ(_⋅_)(𝐒(c)) ([↔]-to-[→] Gcd-gcd-value (p{gcd(a ⋅ 𝐒(c))(b ⋅ 𝐒(c)) ⌊/⌋ 𝐒(c)} ([↔]-to-[←] Gcd-gcd-value (symmetry(_≡_) q)))) ]-sym
  gcd(a)(b) ⋅ 𝐒(c)                         🝖-end
  where
    p : Gcd a b d ← Gcd(a ⋅ 𝐒(c))(b ⋅ 𝐒(c))(d ⋅ 𝐒(c))
    p acbcdc =
      let dcac = Gcd.divisorₗ acbcdc
          dcbc = Gcd.divisorᵣ acbcdc
          m    = Gcd.maximum₂ acbcdc
      in Gcd.intro₂ (divides-without-[⋅]ᵣ-both {z = c} dcac) (divides-without-[⋅]ᵣ-both {z = c} dcbc) (\{D} → Da ↦ Db ↦ divides-without-[⋅]ᵣ-both {z = c} (m{D ⋅ 𝐒(c)} (divides-with-[⋅]ᵣ-both {z = 𝐒(c)} Da) (divides-with-[⋅]ᵣ-both {z = 𝐒(c)} Db)))

    q = [⋅][⌊/⌋]-inverseOperatorᵣ (gcd-divisors{𝐒(c)}{a ⋅ 𝐒(c)}{b ⋅ 𝐒(c)} (divides-with-[⋅] {𝐒(c)}{a} ([∨]-introᵣ (reflexivity(_∣_)))) (divides-with-[⋅]  {𝐒(c)}{b} ([∨]-introᵣ (reflexivity(_∣_)))))

gcd-0 : ((a ≡ 𝟎) ∧ (b ≡ 𝟎)) ↔ (gcd a b ≡ 𝟎)
gcd-0 = [↔]-intro l r where
  l : ((a ≡ 𝟎) ∧ (b ≡ 𝟎)) ← (gcd a b ≡ 𝟎)
  l {𝟎}   {𝟎}   p = [∧]-intro [≡]-intro [≡]-intro
  l {𝐒 a} {𝐒 b} p
    with intro zv _ ← [↔]-to-[←] (Gcd-gcd-value{𝐒(a)}{𝐒(b)}) p
    with () ← [0]-divides-not (zv 𝟎)

  r : ((a ≡ 𝟎) ∧ (b ≡ 𝟎)) → (gcd a b ≡ 𝟎)
  r {𝟎} {𝟎} _ = [≡]-intro

open import Logic.Classical
open import Logic.Propositional.Theorems
open import Numeral.Natural.Decidable
open import Numeral.Natural.Relation
open import Numeral.Natural.Relation.Proofs
open import Type.Properties.Decidable.Proofs

gcd-positive : (Positive(a) ∨ Positive(b)) ↔ Positive(gcd a b)
gcd-positive{a}{b} = [↔]-transitivity ([∨]-map-[↔] Positive-non-zero Positive-non-zero) ([↔]-transitivity ([↔]-symmetry ([¬]-preserves-[∧][∨] ⦃ decider-classical(a ≡ 𝟎) ⦄ ⦃ decider-classical(b ≡ 𝟎) ⦄)) ([↔]-transitivity ([¬]-unaryOperator (gcd-0 {a}{b})) ([↔]-symmetry Positive-non-zero)))

gcd-of-successor : ∀{n} → Gcd(n)(𝐒(n))(1)
gcd-of-successor = Gcd.intro₂ [1]-divides [1]-divides p where
  p : ∀{d n} → (d ∣ n) → (d ∣ 𝐒(n)) → (d ∣ 1)
  p Div𝟎 dsn = dsn
  p (Div𝐒 dn) dsn = p dn ([↔]-to-[→] (divides-without-[+] dsn) (reflexivity(_∣_)))

open import Logic.Propositional.Theorems
open import Numeral.Natural.Coprime
open import Numeral.Natural.Coprime.Proofs
open import Numeral.Natural.Oper.FlooredDivision.Proofs
open import Numeral.Natural.Oper.FlooredDivision.Proofs.Inverse
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Relation.Order.Proofs
open import Syntax.Implication

[⌊/⌋₀]-gcd-coprime : (Positive(a) ∨ Positive(b)) → Coprime(a ⌊/⌋₀ gcd(a)(b)) (b ⌊/⌋₀ gcd(a)(b))
[⌊/⌋₀]-gcd-coprime {a}{b} nz =
  let d = gcd(a)(b)
      D = gcd(a ⌊/⌋₀ d) (b ⌊/⌋₀ d)
      gcd-D = Gcd-gcd {a ⌊/⌋₀ d} {b ⌊/⌋₀ d}
      d-pos = [↔]-to-[→] Positive-greater-than-zero ([↔]-to-[→] gcd-positive nz)
  in
    • (
      Gcd.divisorₗ gcd-D ⇒
      (D ∣ (a ⌊/⌋₀ d))         ⇒-[ divides-with-[⋅]ᵣ-both {z = d} ]
      (D ⋅ d ∣ (a ⌊/⌋₀ d) ⋅ d) ⇒-[ substitute₂ᵣ(_∣_) ([⋅][⌊/⌋₀]-inverseOperatorᵣ d-pos (gcd-dividesₗ {b = b})) ]
      (D ⋅ d ∣ a)              ⇒-[ substitute₂ₗ(_∣_) (commutativity(_⋅_) {D}{d}) ]
      (d ⋅ D ∣ a)              ⇒-end
    )
    • (
      Gcd.divisorᵣ gcd-D ⇒
      (D ∣ (b ⌊/⌋₀ d))         ⇒-[ divides-with-[⋅]ᵣ-both {z = d} ]
      (D ⋅ d ∣ (b ⌊/⌋₀ d) ⋅ d) ⇒-[ substitute₂ᵣ(_∣_) ([⋅][⌊/⌋₀]-inverseOperatorᵣ d-pos gcd-dividesᵣ) ]
      (D ⋅ d ∣ b)              ⇒-[ substitute₂ₗ(_∣_) (commutativity(_⋅_) {D}{d}) ]
      (d ⋅ D ∣ b)              ⇒-end
    )
    ⇒₂-[ Gcd.maximum₂ Gcd-gcd ]
    ((d ⋅ D) ∣ d)                ⇒-[]
    ((d ⋅ D) ∣ (d ⋅ 1))          ⇒-[ divides-without-[⋅]ₗ-both' d-pos ]
    (D ∣ 1)                      ⇒-[ [1]-only-divides-[1] ]
    (D ≡ 1)                      ⇒-[ [↔]-to-[←] Coprime-gcd ]
    Coprime(a ⌊/⌋₀ d) (b ⌊/⌋₀ d) ⇒-end

[⌊/⌋]-gcd-coprime : (nz : Positive(a) ∨ Positive(b)) → Coprime((a ⌊/⌋ gcd(a)(b)) ⦃ [↔]-to-[→] gcd-positive nz ⦄) ((b ⌊/⌋ gcd(a)(b)) ⦃ [↔]-to-[→] gcd-positive nz ⦄)
[⌊/⌋]-gcd-coprime {a}{b} nz = substitute₂(Coprime)
  ([⌊/⌋][⌊/⌋₀]-equality ⦃ [↔]-to-[→] gcd-positive nz ⦄)
  ([⌊/⌋][⌊/⌋₀]-equality ⦃ [↔]-to-[→] gcd-positive nz ⦄)
  ([⌊/⌋₀]-gcd-coprime nz)


text:
open import Relation.Binary.Core

module TreeSort.Impl1.Correctness.Order  {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_)  where

open import BSTree _≤_
open import BSTree.Properties _≤_ trans≤
open import BTree {A}
open import Data.List
open import Data.Sum
open import Function using (_∘_)
open import List.Sorted _≤_
open import TreeSort.Impl1 _≤_ tot≤

lemma-insert-*⊴ : {x y : A}{t : BTree} → x ≤ y → t *⊴ y → insert x t *⊴ y
lemma-insert-*⊴ x≤y lelf = lend x≤y lelf
lemma-insert-*⊴ {x = x}{t = node z l r} x≤y (lend z≤y r≤y)
    with tot≤ x z
... | inj₁ x≤z = lend z≤y r≤y
... | inj₂ z≤x = lend z≤y (lemma-insert-*⊴ x≤y r≤y)

lemma-insert-⊴* : {x y : A}{t : BTree} → y ≤ x → y ⊴* t → y ⊴* insert x t
lemma-insert-⊴* y≤x gelf = gend y≤x gelf
lemma-insert-⊴* {x = x} {t = node z l r} y≤x (gend y≤z y≤l)
    with tot≤ x z
... | inj₁ x≤z = gend y≤z (lemma-insert-⊴* y≤x y≤l)
... | inj₂ z≤x = gend y≤z y≤l

lemma-insert-bst : {t : BTree}(x : A) → BSTree t → BSTree (insert x t)
lemma-insert-bst x slf = snd slf slf lelf gelf
lemma-insert-bst x (snd {x = y} sl sr l≤y y≤r)
    with tot≤ x y
... | inj₁ x≤y = snd (lemma-insert-bst x sl) sr (lemma-insert-*⊴ x≤y l≤y) y≤r
... | inj₂ y≤x = snd sl (lemma-insert-bst x sr) l≤y (lemma-insert-⊴* y≤x y≤r)

lemma-treeSort-bst : (xs : List A) → BSTree (treeSort xs)
lemma-treeSort-bst [] = slf
lemma-treeSort-bst (x ∷ xs) = lemma-insert-bst x (lemma-treeSort-bst xs)

theorem-treeSort-sorted : (xs : List A) → Sorted (flatten (treeSort xs))
theorem-treeSort-sorted = lemma-bst-sorted ∘ lemma-treeSort-bst

ext: agda

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module HighlightPositivity where

data A : Set where
  inA : (A -> A) -> A

data B : Set
data C : Set

data B where
  inB : (C -> B) -> B

data C where
  inC : B -> C

record D : Set where
  inductive
  field
    outD : D -> D

endo : Set -> Set
endo X = X -> X

data E : Set where
  inE : endo E -> E

data F (X : Set -> Set) : Set where
  inF : X (F X) -> F X

open import Agda.Builtin.Bool

data GU : Set
GT : Bool -> Set

data GU where
  inGU : ∀ b → GT b -> GU

GT false = Bool
GT true = GU -> Bool

open import Agda.Builtin.Equality

data H : Set where
  inH : ∀ f → f ≡ (λ (x : H) → x) -> H -- non-positive occurrence is
                                       -- in the implicit type of f

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
import Loop
import Loop.Bundles
import Loop.Definitions
import Loop.Properties
import Loop.Structures
import Magma
import Magma.Bundles
import Magma.Definitions
import Magma.Properties
import Magma.Structures
import Morphism.Structures
import Quasigroup
import Quasigroup.Bundles
import Quasigroup.Definitions
import Quasigroup.Properties
import Quasigroup.Structures


text:
module Lec3 where

open import CS410-Prelude

not : Two -> Two
not tt = ff
not ff = tt

data TwoTestable (b : Two) : (x : Two) -> Set where
  same : TwoTestable b b
  diff : TwoTestable b (not b)

twoTest : (b x : Two) -> TwoTestable b x
twoTest tt tt = same
twoTest tt ff = diff
twoTest ff tt = diff
twoTest ff ff = same

twoTest' : (b x : Two) -> TwoTestable b x
twoTest' = caseTwo (caseTwo same diff) (caseTwo diff same)

xor : Two -> Two -> Two
xor b x with twoTest b x
xor b .b       | same = ff
xor b .(not b) | diff = tt

xorHelp : (b x : Two) -> TwoTestable b x -> Two
xorHelp b .b       same = ff
xorHelp b .(not b) diff = tt

xor' : Two -> Two -> Two
xor' b x = xorHelp b x (twoTest b x)


text:
module _ (X : Set) where

open import Agda.Builtin.Equality

postulate
  A : Set

data D : Set where
  c : A → D

variable
  P : D → Set

postulate
  p : (f : ∀ x → P (c x)) (x y : A) → f x ≡ f y


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Prod where

open import Cubical.Data.Prod.Base public
open import Cubical.Data.Prod.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Issue462 where

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

postulate A : Set

record R (_≈_ _∼_ : A → A → Set) : Set where
  field
    ≈-refl      : (x : A) → x ≈ x
    ∼-reflexive : (x y : A) → x ≈ y → x ∼ y

  ∼-refl : (x : A) → x ∼ x
  ∼-refl x = ∼-reflexive x x (≈-refl x)

postulate
  _≈_    : A → A → Set
  ≈-refl : ((x : A) → x ≡ x) → (x : A) → x ≈ x
  ≈-irr  : (x : A) (p : x ≈ x) → p ≡ p

≡-r : R _≡_ _≡_
≡-r = record
  { ≈-refl      = ≡-refl
  ; ∼-reflexive = λ _ _ p → p
  }

≈-reflexive : (x y : A) → x ≡ y → x ≈ y
≈-reflexive .x .x (≡-refl x) = ≈-refl (R.∼-refl ≡-r) x

≈-r : R _≡_ _≈_
≈-r = record
  { ≈-refl      = ≡-refl
  ; ∼-reflexive = ≈-reflexive
  }

foo : A → Set₁
foo x with ≈-irr x (R.∼-refl ≈-r x)
foo x | _ = Set

-- The generated with function should not contain unsolved
-- meta-variables.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-

This file contains quotient groups

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.QuotientGroup where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Powerset
open import Cubical.Foundations.GroupoidLaws hiding (assoc)
open import Cubical.Data.Sigma
open import Cubical.HITs.SetQuotients.Base renaming (_/_ to _/s_)
open import Cubical.HITs.SetQuotients.Properties
open import Cubical.Relation.Binary.Base

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Subgroup

private
  variable
    ℓ : Level

module _ (G' : Group ℓ) (H' : Subgroup G') (Hnormal : isNormal H') where

  open BinaryRelation
  open isSubgroup (snd H')
  open GroupStr (snd G')
  open GroupTheory G'
  private
    G = ⟨ G' ⟩

  _~_ : G → G → Type ℓ
  x ~ y = x · inv y ∈ ⟪ H' ⟫

  isRefl~ : isRefl _~_
  isRefl~ x = subst-∈ ⟪ H' ⟫ (sym (·InvR x)) id-closed

  G/H : Type ℓ
  G/H = G /s _~_

  1/H : G/H
  1/H = [ 1g ]

  _·/H_ : G/H → G/H → G/H
  x ·/H y = setQuotBinOp isRefl~ isRefl~ _·_ rem x y
   where
   rem : (a a' b b' : G)
       → a · inv a' ∈ ⟪ H' ⟫
       → b · inv b' ∈ ⟪ H' ⟫
       → (a · b) · inv (a' · b') ∈ ⟪ H' ⟫
   rem a a' b b' haa' hbb' = subst-∈ ⟪ H' ⟫ (cong (_ ·_) (sym (invDistr _ _))) rem5
     where
     rem1 : (inv a' · a) · b · inv b' ∈ ⟪ H' ⟫
     rem1 = ·CommNormalSubgroup H' Hnormal
              (op-closed  hbb' (·CommNormalSubgroup H' Hnormal haa'))

     rem2 : ((inv a' · a) · b) · inv b' ∈ ⟪ H' ⟫
     rem2 = subst-∈ ⟪ H' ⟫ (·Assoc _ _ _) rem1

     rem3 : inv b' · (inv a' · a) · b ∈ ⟪ H' ⟫
     rem3 = ·CommNormalSubgroup H' Hnormal rem2

     rem4 : (inv b' · inv a') · (a · b) ∈ ⟪ H' ⟫
     rem4 = subst-∈ ⟪ H' ⟫ (cong (inv b' ·_) (sym (·Assoc _ _ _)) ∙ ·Assoc _ _ _) rem3

     rem5 : (a · b) · inv b' · inv a' ∈ ⟪ H' ⟫
     rem5 = ·CommNormalSubgroup H' Hnormal rem4

  inv/H : G/H → G/H
  inv/H = setQuotUnaryOp inv rem
    where
    rem : (a a' : G) → a · inv a' ∈ ⟪ H' ⟫ → inv a · inv (inv a') ∈ ⟪ H' ⟫
    rem a a' haa' = subst-∈ ⟪ H' ⟫ (cong (inv a ·_) (sym (invInv a'))) rem1
      where
      ha'a : a' · inv a ∈ ⟪ H' ⟫
      ha'a = subst-∈ ⟪ H' ⟫ (invDistr a (inv a') ∙ cong (_· inv a) (invInv a')) (inv-closed haa')

      rem1 : inv a · a' ∈ ⟪ H' ⟫
      rem1 = ·CommNormalSubgroup H' Hnormal ha'a

  ·/H-assoc : (a b c : G/H) → (a ·/H (b ·/H c)) ≡ ((a ·/H b) ·/H c)
  ·/H-assoc = elimProp3 (λ x y z → squash/ _ _) λ x y z → cong [_] (·Assoc x y z)

  ·/H-rid : (a : G/H) → (a ·/H 1/H) ≡ a
  ·/H-rid = elimProp (λ x → squash/ _ _) λ x → cong [_] (·IdR x)

  ·/H-invr : (a : G/H) → (a ·/H inv/H a) ≡ 1/H
  ·/H-invr = elimProp (λ x → squash/ _ _) λ x → cong [_] (·InvR x)

  asGroup : Group ℓ
  asGroup = makeGroup-right 1/H _·/H_ inv/H squash/ ·/H-assoc ·/H-rid ·/H-invr

_/_ : (G : Group ℓ) → (H : NormalSubgroup G) → Group ℓ
G / H = asGroup G (H .fst) (H .snd)

[_]/G : {G : Group ℓ} {H : NormalSubgroup G} → ⟨ G ⟩ → ⟨ G / H ⟩
[ x ]/G = [ x ]

-- Quotienting by a trivial subgroup
module _ {G' : Group ℓ} (H' : NormalSubgroup G')
         (contrH : (x y : fst G') → _~_ G' (fst H') (snd H') x y → x ≡ y) where
  private
    -- open isSubgroup (snd H')
    open GroupStr (snd G')
    open GroupTheory G'
    G = fst G'
    G/H' = fst (G' / H')

    Code : (g : G) → G/H' → hProp ℓ
    Code g =
      elim (λ _ → isSetHProp)
        (λ a → (g ≡ a) , is-set _ _)
        λ a b r → Σ≡Prop (λ _ → isPropIsProp) (cong (g ≡_) (contrH a b r))

    decode : (g : G) (x : G/H') → [ g ] ≡ x → Code g x .fst
    decode g x = J (λ x _ → Code g x .fst) refl

  trivialRel→elimPath : {g h : G} → Path G/H' [ g ] [ h ] → g ≡ h
  trivialRel→elimPath {g = g} {h = h} = decode g [ h ]

  trivialRelIso : GroupIso G' (G' / H')
  Iso.fun (fst trivialRelIso) g = [ g ]
  Iso.inv (fst trivialRelIso) =
    rec is-set (λ g → g) contrH
  Iso.rightInv (fst trivialRelIso) =
    elimProp (λ _ → squash/ _ _) λ _ → refl
  Iso.leftInv (fst trivialRelIso) _ = refl
  snd trivialRelIso =
    makeIsGroupHom λ _ _ → refl

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

module Relation.Nullary where

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module HBound  where

import Relation.Unary.PredicateTransformer  as PT
open import Relation.Unary
open import Level
open import Relation.Binary using (Rel; IsEquivalence; module IsEquivalence; Reflexive; Symmetric; Transitive)

open import  Category.Applicative

--naturalTrans : ∀ {a ℓ₁ ℓ₂ : Level } (ix : Set a )   (f : RU.Pred {a} ix ℓ₁ ) (g : RU.Pred {a} ix ℓ₂) -> Set (suc (ℓ₁ ∪  ℓ₂ ∪ a)  )
-- naturalTrans ix f g = ∀ (x : ix) -> f x  -> g x

-- indexed natural transformation as family predicates
-- note: this is not the most general notion of a natural transformation
NatIx : ∀ {i j k : Level } (a : Set k) (f : Pred a i) (g : Pred a j) -> Set ( j ⊔  i ⊔ k)
NatIx   a  f g =  ∀ ( x : a  ) -> (f x -> g x )

-- this is a simplified model of a homogenuous natural transformation
Nat : ∀ {i j }  -> ∀  { a : Set i} ->   Rel (Pred a j) (i ⊔ j )
Nat f g = forall x -> (f x -> g x )

{-
question: is using a formal model of categorical arrows useful here
-}
record NatFunctor {i j } {a : Set i} (t : Pred a j -> Pred a j) : Set ( i ⊔ suc j)  where
  field
       natMap : ∀ {f g} -> Nat f g -> Nat (t f) (t g )

-- record NatTraverseable


text:
module DayConvolution where

open import Library
open import Functors
open import Categories
open import Categories.Sets
open import MonoidalCat

-- first draft

ODay : ∀{l m}(M : Monoidal {l}{m})
       (F G : Fun (Monoidal.C M) (Sets {l})) ->
       Cat.Obj (Monoidal.C M) -> Set _
ODay M F G X =
  Σ Obj \Y -> Σ Obj \Z -> OMap F Y × OMap G Z × Hom X (OMap ⊗ (Y , Z))
  where open Monoidal M; open Cat C; open Fun

HDay : ∀{l m}(M : Monoidal {l}{m})
       (F G : Fun (Monoidal.C M) (Sets {l})) -> ∀{X X'} ->
       Cat.Hom (Monoidal.C M) X X' -> ODay M F G X' -> ODay M F G X
HDay M F G f (y , z , fy , gz , g) = y , z , fy , gz , comp g f
  where open Monoidal M; open Cat C

DayF : ∀{l m}(M : Monoidal {l}{m})
       (F G : Fun (Monoidal.C M) (Sets {l})) -> Fun ((Monoidal.C M) Op) Sets
DayF M F G = functor
  (ODay M F G)
  (HDay M F G)
  (\ {X} -> ext (\{ (y , z , fy , gz , g) ->
    cong (λ g → y , z , fy , gz , g) idr}))
  (\ {X Y Z h k} -> ext (\{ (y , z , fy , gz , g) ->
    cong (λ l → y , z , fy , gz , l) (sym ass)}))
  where open Monoidal M; open Cat C

-- subject to some additional conditions
-- forall h : y -> y'.
--   (y , F h fy' , gz , g) ~ (y' , z , fy' , gz , [h,id] . g)
--
-- forall k : z -> z'
--   (y , z , fy , G k gz' , g) ~ (y , z' , fy , gz' , [id,k] . g)

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Substitution lemmas
------------------------------------------------------------------------

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

module Data.Fin.Substitution.Lemmas where

import Category.Applicative.Indexed as Applicative
open import Data.Fin.Substitution
open import Data.Nat hiding (_⊔_)
open import Data.Fin using (Fin; zero; suc; lift)
open import Data.Vec
import Data.Vec.Properties as VecProp
open import Function as Fun using (_∘_; _$_)
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl; sym; cong; cong₂)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
  using (Star; ε; _◅_; _▻_)
open PropEq.≡-Reasoning
open import Level using (Level; _⊔_)
open import Relation.Unary using (Pred)

-- A lemma which does not refer to any substitutions.

lift-commutes : ∀ {n} k j (x : Fin (j + (k + n))) →
                lift j suc (lift j (lift k suc) x) ≡
                lift j (lift (suc k) suc) (lift j suc x)
lift-commutes k zero    x       = refl
lift-commutes k (suc j) zero    = refl
lift-commutes k (suc j) (suc x) = cong suc (lift-commutes k j x)

-- The modules below prove a number of substitution lemmas, on the
-- assumption that the underlying substitution machinery satisfies
-- certain properties.

record Lemmas₀ {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where
  field simple : Simple T

  open Simple simple

  extensionality : ∀ {m n} {ρ₁ ρ₂ : Sub T m n} →
                   (∀ x → lookup ρ₁ x ≡ lookup ρ₂ x) → ρ₁ ≡ ρ₂
  extensionality {ρ₁ = []}      {[]}       hyp = refl
  extensionality {ρ₁ = t₁ ∷ ρ₁} { t₂ ∷ ρ₂} hyp with hyp zero
  extensionality {ρ₁ = t₁ ∷ ρ₁} {.t₁ ∷ ρ₂} hyp | refl =
    cong (_∷_ t₁) (extensionality (hyp ∘ suc))

  id-↑⋆ : ∀ {n} k → id ↑⋆ k ≡ id {k + n}
  id-↑⋆ zero    = refl
  id-↑⋆ (suc k) = begin
    (id ↑⋆ k) ↑ ≡⟨ cong _↑ (id-↑⋆ k) ⟩
    id        ↑ ∎

  lookup-map-weaken-↑⋆ : ∀ {m n} k x {ρ : Sub T m n} →
                         lookup (map weaken ρ ↑⋆ k) x ≡
                         lookup ((ρ ↑) ↑⋆ k) (lift k suc x)
  lookup-map-weaken-↑⋆ zero    x           = refl
  lookup-map-weaken-↑⋆ (suc k) zero        = refl
  lookup-map-weaken-↑⋆ (suc k) (suc x) {ρ} = begin
    lookup (map weaken (map weaken ρ ↑⋆ k)) x        ≡⟨ VecProp.lookup-map x weaken (map weaken ρ ↑⋆ k) ⟩
    weaken (lookup (map weaken ρ ↑⋆ k) x)            ≡⟨ cong weaken (lookup-map-weaken-↑⋆ k x) ⟩
    weaken (lookup ((ρ ↑) ↑⋆ k) (lift k suc x))      ≡⟨ sym $ VecProp.lookup-map (lift k suc x) weaken ((ρ ↑) ↑⋆ k) ⟩
    lookup (map weaken ((ρ ↑) ↑⋆ k)) (lift k suc x)  ∎

record Lemmas₁ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where
  field lemmas₀ : Lemmas₀ T

  open Lemmas₀ lemmas₀
  open Simple simple

  field weaken-var : ∀ {n} {x : Fin n} → weaken (var x) ≡ var (suc x)

  lookup-map-weaken : ∀ {m n} x {y} {ρ : Sub T m n} →
                      lookup             ρ  x ≡ var      y →
                      lookup (map weaken ρ) x ≡ var (suc y)
  lookup-map-weaken x {y} {ρ} hyp = begin
    lookup (map weaken ρ) x  ≡⟨ VecProp.lookup-map x weaken ρ ⟩
    weaken (lookup ρ x)      ≡⟨ cong weaken hyp ⟩
    weaken (var y)           ≡⟨ weaken-var ⟩
    var (suc y)              ∎

  mutual

    lookup-id : ∀ {n} (x : Fin n) → lookup id x ≡ var x
    lookup-id zero    = refl
    lookup-id (suc x) = lookup-wk x

    lookup-wk : ∀ {n} (x : Fin n) → lookup wk x ≡ var (suc x)
    lookup-wk x = lookup-map-weaken x {ρ = id} (lookup-id x)

  lookup-↑⋆ : ∀ {m n} (f : Fin m → Fin n) {ρ : Sub T m n} →
              (∀ x → lookup ρ x ≡ var (f x)) →
              ∀ k x → lookup (ρ ↑⋆ k) x ≡ var (lift k f x)
  lookup-↑⋆ f         hyp zero    x       = hyp x
  lookup-↑⋆ f         hyp (suc k) zero    = refl
  lookup-↑⋆ f {ρ = ρ} hyp (suc k) (suc x) =
    lookup-map-weaken x {ρ = ρ ↑⋆ k} (lookup-↑⋆ f hyp k x)

  lookup-lift-↑⋆ : ∀ {m n} (f : Fin n → Fin m) {ρ : Sub T m n} →
                   (∀ x → lookup ρ (f x) ≡ var x) →
                   ∀ k x → lookup (ρ ↑⋆ k) (lift k f x) ≡ var x
  lookup-lift-↑⋆ f         hyp zero    x       = hyp x
  lookup-lift-↑⋆ f         hyp (suc k) zero    = refl
  lookup-lift-↑⋆ f {ρ = ρ} hyp (suc k) (suc x) =
    lookup-map-weaken (lift k f x) {ρ = ρ ↑⋆ k} (lookup-lift-↑⋆ f hyp k x)

  lookup-wk-↑⋆ : ∀ {n} k (x : Fin (k + n)) →
                 lookup (wk ↑⋆ k) x ≡ var (lift k suc x)
  lookup-wk-↑⋆ = lookup-↑⋆ suc lookup-wk

  lookup-wk-↑⋆-↑⋆ : ∀ {n} k j (x : Fin (j + (k + n))) →
                    lookup (wk ↑⋆ k ↑⋆ j) x ≡
                    var (lift j (lift k suc) x)
  lookup-wk-↑⋆-↑⋆ k = lookup-↑⋆ (lift k suc) (lookup-wk-↑⋆ k)

  lookup-sub-↑⋆ : ∀ {n t} k (x : Fin (k + n)) →
                  lookup (sub t ↑⋆ k) (lift k suc x) ≡ var x
  lookup-sub-↑⋆ = lookup-lift-↑⋆ suc lookup-id

  open Lemmas₀ lemmas₀ public

record Lemmas₂ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where
  field
    lemmas₁     : Lemmas₁ T
    application : Application T T

  open Lemmas₁ lemmas₁

  subst : Subst T
  subst = record { simple = simple; application = application }

  open Subst subst

  field var-/ : ∀ {m n x} {ρ : Sub T m n} → var x / ρ ≡ lookup ρ x

  suc-/-sub : ∀ {n x} {t : T n} → var (suc x) / sub t ≡ var x
  suc-/-sub {x = x} {t} = begin
    var (suc x) / sub t     ≡⟨ var-/ ⟩
    lookup (sub t) (suc x)  ≡⟨ refl ⟩
    lookup id x             ≡⟨ lookup-id x ⟩
    var x                   ∎

  lookup-⊙ : ∀ {m n k} x {ρ₁ : Sub T m n} {ρ₂ : Sub T n k} →
             lookup (ρ₁ ⊙ ρ₂) x ≡ lookup ρ₁ x / ρ₂
  lookup-⊙ x {ρ₁} {ρ₂} = VecProp.lookup-map x (λ t → t / ρ₂) ρ₁

  lookup-⨀ : ∀ {m n} x (ρs : Subs T m n) →
             lookup (⨀ ρs) x ≡ var x /✶ ρs
  lookup-⨀ x ε                = lookup-id x
  lookup-⨀ x (ρ ◅ ε)          = sym var-/
  lookup-⨀ x (ρ ◅ (ρ′ ◅ ρs′)) = begin
    lookup (⨀ (ρ ◅ ρs)) x  ≡⟨ refl ⟩
    lookup (⨀ ρs ⊙ ρ) x    ≡⟨ lookup-⊙ x {ρ₁ = ⨀ (ρ′ ◅ ρs′)} ⟩
    lookup (⨀ ρs) x / ρ    ≡⟨ cong₂ _/_ (lookup-⨀ x (ρ′ ◅ ρs′)) refl ⟩
    var x /✶ ρs / ρ        ∎
    where ρs = ρ′ ◅ ρs′

  id-⊙ : ∀ {m n} {ρ : Sub T m n} → id ⊙ ρ ≡ ρ
  id-⊙ {ρ = ρ} = extensionality λ x → begin
    lookup (id ⊙ ρ) x  ≡⟨ lookup-⊙ x {ρ₁ = id} ⟩
    lookup  id x / ρ   ≡⟨ cong₂ _/_ (lookup-id x) refl ⟩
    var x        / ρ   ≡⟨ var-/ ⟩
    lookup ρ x         ∎

  lookup-wk-↑⋆-⊙ : ∀ {m n} k {x} {ρ : Sub T (k + suc m) n} →
                   lookup (wk ↑⋆ k ⊙ ρ) x ≡ lookup ρ (lift k suc x)
  lookup-wk-↑⋆-⊙ k {x} {ρ} = begin
    lookup (wk ↑⋆ k ⊙ ρ) x   ≡⟨ lookup-⊙ x {ρ₁ = wk ↑⋆ k} ⟩
    lookup (wk ↑⋆ k) x / ρ   ≡⟨ cong₂ _/_ (lookup-wk-↑⋆ k x) refl ⟩
    var (lift k suc x) / ρ   ≡⟨ var-/ ⟩
    lookup ρ (lift k suc x)  ∎

  wk-⊙-sub′ : ∀ {n} {t : T n} k → wk ↑⋆ k ⊙ sub t ↑⋆ k ≡ id
  wk-⊙-sub′ {t = t} k = extensionality λ x → begin
    lookup (wk ↑⋆ k ⊙ sub t ↑⋆ k) x     ≡⟨ lookup-wk-↑⋆-⊙ k ⟩
    lookup (sub t ↑⋆ k) (lift k suc x)  ≡⟨ lookup-sub-↑⋆ k x ⟩
    var x                               ≡⟨ sym (lookup-id x) ⟩
    lookup id x                         ∎

  wk-⊙-sub : ∀ {n} {t : T n} → wk ⊙ sub t ≡ id
  wk-⊙-sub = wk-⊙-sub′ zero

  var-/-wk-↑⋆ : ∀ {n} k (x : Fin (k + n)) →
                var x / wk ↑⋆ k ≡ var (lift k suc x)
  var-/-wk-↑⋆ k x = begin
    var x / wk ↑⋆ k     ≡⟨ var-/ ⟩
    lookup (wk ↑⋆ k) x  ≡⟨ lookup-wk-↑⋆ k x ⟩
    var (lift k suc x)  ∎

  wk-↑⋆-⊙-wk : ∀ {n} k j →
               wk {n} ↑⋆ k ↑⋆ j ⊙ wk ↑⋆ j ≡
               wk ↑⋆ j ⊙ wk ↑⋆ suc k ↑⋆ j
  wk-↑⋆-⊙-wk k j = extensionality λ x → begin
    lookup (wk ↑⋆ k ↑⋆ j ⊙ wk ↑⋆ j) x               ≡⟨ lookup-⊙ x {ρ₁ = wk ↑⋆ k ↑⋆ j} ⟩
    lookup (wk ↑⋆ k ↑⋆ j) x / wk ↑⋆ j               ≡⟨ cong₂ _/_ (lookup-wk-↑⋆-↑⋆ k j x) refl ⟩
    var (lift j (lift k suc) x) / wk ↑⋆ j           ≡⟨ var-/-wk-↑⋆ j (lift j (lift k suc) x) ⟩
    var (lift j suc (lift j (lift k suc) x))        ≡⟨ cong var (lift-commutes k j x) ⟩
    var (lift j (lift (suc k) suc) (lift j suc x))  ≡⟨ sym (lookup-wk-↑⋆-↑⋆ (suc k) j (lift j suc x)) ⟩
    lookup (wk ↑⋆ suc k ↑⋆ j) (lift j suc x)        ≡⟨ sym var-/ ⟩
    var (lift j suc x) / wk ↑⋆ suc k ↑⋆ j           ≡⟨ cong₂ _/_ (sym (lookup-wk-↑⋆ j x)) refl ⟩
    lookup (wk ↑⋆ j) x / wk ↑⋆ suc k ↑⋆ j           ≡⟨ sym (lookup-⊙ x {ρ₁ = wk ↑⋆ j}) ⟩
    lookup (wk ↑⋆ j ⊙ wk ↑⋆ suc k ↑⋆ j) x           ∎

  open Subst   subst   public hiding (simple; application)
  open Lemmas₁ lemmas₁ public

record Lemmas₃ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where
  field lemmas₂ : Lemmas₂ T

  open Lemmas₂ lemmas₂

  field
    /✶-↑✶ : ∀ {m n} (ρs₁ ρs₂ : Subs T m n) →
            (∀ k x → var x /✶ ρs₁ ↑✶ k ≡ var x /✶ ρs₂ ↑✶ k) →
            ∀ k t → t /✶ ρs₁ ↑✶ k ≡ t /✶ ρs₂ ↑✶ k

  /✶-↑✶′ : ∀ {m n} (ρs₁ ρs₂ : Subs T m n) →
           (∀ k → ⨀ (ρs₁ ↑✶ k) ≡ ⨀ (ρs₂ ↑✶ k)) →
           ∀ k t → t /✶ ρs₁ ↑✶ k ≡ t /✶ ρs₂ ↑✶ k
  /✶-↑✶′ ρs₁ ρs₂ hyp = /✶-↑✶ ρs₁ ρs₂ (λ k x → begin
    var x /✶ ρs₁ ↑✶ k        ≡⟨ sym (lookup-⨀ x (ρs₁ ↑✶ k)) ⟩
    lookup (⨀ (ρs₁ ↑✶ k)) x  ≡⟨ cong (Fun.flip lookup x) (hyp k) ⟩
    lookup (⨀ (ρs₂ ↑✶ k)) x  ≡⟨ lookup-⨀ x (ρs₂ ↑✶ k) ⟩
    var x /✶ ρs₂ ↑✶ k        ∎)

  id-vanishes : ∀ {n} (t : T n) → t / id ≡ t
  id-vanishes = /✶-↑✶′ (ε ▻ id) ε id-↑⋆ zero

  ⊙-id : ∀ {m n} {ρ : Sub T m n} → ρ ⊙ id ≡ ρ
  ⊙-id {ρ = ρ} = begin
    map (λ t → t / id) ρ  ≡⟨ VecProp.map-cong id-vanishes ρ ⟩
    map Fun.id         ρ  ≡⟨ VecProp.map-id ρ ⟩
    ρ                     ∎

  open Lemmas₂ lemmas₂ public hiding (wk-⊙-sub′)

record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where
  field lemmas₃ : Lemmas₃ T

  open Lemmas₃ lemmas₃

  field /-wk : ∀ {n} {t : T n} → t / wk ≡ weaken t

  private

    ↑-distrib′ : ∀ {m n k} {ρ₁ : Sub T m n} {ρ₂ : Sub T n k} →
                 (∀ t → t / ρ₂ / wk ≡ t / wk / ρ₂ ↑) →
                 (ρ₁ ⊙ ρ₂) ↑ ≡ ρ₁ ↑ ⊙ ρ₂ ↑
    ↑-distrib′ {ρ₁ = ρ₁} {ρ₂} hyp = begin
      (ρ₁ ⊙ ρ₂) ↑                             ≡⟨ refl ⟩
      var zero        ∷ map weaken (ρ₁ ⊙ ρ₂)  ≡⟨ cong₂ _∷_ (sym var-/) lemma ⟩
      var zero / ρ₂ ↑ ∷ map weaken ρ₁ ⊙ ρ₂ ↑  ≡⟨ refl ⟩
      ρ₁ ↑ ⊙ ρ₂ ↑                             ∎
      where
      lemma = begin
        map weaken (map (λ t → t / ρ₂) ρ₁)    ≡⟨ sym (VecProp.map-∘ _ _ _) ⟩
        map (λ t → weaken (t / ρ₂)) ρ₁        ≡⟨ VecProp.map-cong (λ t → begin
                                                   weaken (t / ρ₂)  ≡⟨ sym /-wk ⟩
                                                   t / ρ₂ / wk      ≡⟨ hyp t ⟩
                                                   t / wk / ρ₂ ↑    ≡⟨ cong₂ _/_ /-wk refl ⟩
                                                   weaken t / ρ₂ ↑  ∎) ρ₁ ⟩
        map (λ t → weaken t / ρ₂ ↑) ρ₁        ≡⟨ VecProp.map-∘ _ _ _ ⟩
        map (λ t → t / ρ₂ ↑) (map weaken ρ₁)  ∎

    ↑⋆-distrib′ : ∀ {m n o} {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} →
                  (∀ k t → t / ρ₂ ↑⋆ k / wk ≡ t / wk / ρ₂ ↑⋆ suc k) →
                  ∀ k → (ρ₁ ⊙ ρ₂) ↑⋆ k ≡ ρ₁ ↑⋆ k ⊙ ρ₂ ↑⋆ k
    ↑⋆-distrib′                hyp zero    = refl
    ↑⋆-distrib′ {ρ₁ = ρ₁} {ρ₂} hyp (suc k) = begin
      (ρ₁ ⊙ ρ₂) ↑⋆ suc k         ≡⟨ cong _↑ (↑⋆-distrib′ hyp k) ⟩
      (ρ₁ ↑⋆ k ⊙ ρ₂ ↑⋆ k) ↑      ≡⟨ ↑-distrib′ (hyp k) ⟩
      ρ₁ ↑⋆ suc k ⊙ ρ₂ ↑⋆ suc k  ∎

  map-weaken : ∀ {m n} {ρ : Sub T m n} → map weaken ρ ≡ ρ ⊙ wk
  map-weaken {ρ = ρ} = begin
    map weaken ρ          ≡⟨ VecProp.map-cong (λ _ → sym /-wk) ρ ⟩
    map (λ t → t / wk) ρ  ≡⟨ refl ⟩
    ρ ⊙ wk                ∎

  private

    ⊙-wk′ : ∀ {m n} {ρ : Sub T m n} k →
            ρ ↑⋆ k ⊙ wk ↑⋆ k ≡ wk ↑⋆ k ⊙ ρ ↑ ↑⋆ k
    ⊙-wk′ {ρ = ρ} k = sym (begin
      wk ↑⋆ k ⊙ ρ ↑ ↑⋆ k  ≡⟨ lemma ⟩
      map weaken ρ ↑⋆ k   ≡⟨ cong (λ ρ′ → ρ′ ↑⋆ k) map-weaken ⟩
      (ρ ⊙ wk) ↑⋆ k       ≡⟨ ↑⋆-distrib′ (λ k t →
                               /✶-↑✶′ (ε ▻ wk ↑⋆ k ▻ wk) (ε ▻ wk ▻ wk ↑⋆ suc k)
                                      (wk-↑⋆-⊙-wk k) zero t) k ⟩
      ρ ↑⋆ k ⊙ wk ↑⋆ k    ∎)
      where
      lemma = extensionality λ x → begin
        lookup (wk ↑⋆ k ⊙ ρ ↑ ↑⋆ k) x     ≡⟨ lookup-wk-↑⋆-⊙ k ⟩
        lookup (ρ ↑ ↑⋆ k) (lift k suc x)  ≡⟨ sym (lookup-map-weaken-↑⋆ k x) ⟩
        lookup (map weaken ρ ↑⋆ k) x      ∎

  ⊙-wk : ∀ {m n} {ρ : Sub T m n} → ρ ⊙ wk ≡ wk ⊙ ρ ↑
  ⊙-wk = ⊙-wk′ zero

  wk-commutes : ∀ {m n} {ρ : Sub T m n} t →
                t / ρ / wk ≡ t / wk / ρ ↑
  wk-commutes {ρ = ρ} = /✶-↑✶′ (ε ▻ ρ ▻ wk) (ε ▻ wk ▻ ρ ↑) ⊙-wk′ zero

  ↑⋆-distrib : ∀ {m n o} {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} →
               ∀ k → (ρ₁ ⊙ ρ₂) ↑⋆ k ≡ ρ₁ ↑⋆ k ⊙ ρ₂ ↑⋆ k
  ↑⋆-distrib = ↑⋆-distrib′ (λ _ → wk-commutes)

  /-⊙ : ∀ {m n k} {ρ₁ : Sub T m n} {ρ₂ : Sub T n k} t →
        t / ρ₁ ⊙ ρ₂ ≡ t / ρ₁ / ρ₂
  /-⊙ {ρ₁ = ρ₁} {ρ₂} t =
    /✶-↑✶′ (ε ▻ ρ₁ ⊙ ρ₂) (ε ▻ ρ₁ ▻ ρ₂) ↑⋆-distrib zero t

  ⊙-assoc : ∀ {m n k o}
              {ρ₁ : Sub T m n} {ρ₂ : Sub T n k} {ρ₃ : Sub T k o} →
            ρ₁ ⊙ (ρ₂ ⊙ ρ₃) ≡ (ρ₁ ⊙ ρ₂) ⊙ ρ₃
  ⊙-assoc {ρ₁ = ρ₁} {ρ₂} {ρ₃} = begin
    map (λ t → t / ρ₂ ⊙ ρ₃) ρ₁                  ≡⟨ VecProp.map-cong /-⊙ ρ₁ ⟩
    map (λ t → t / ρ₂ / ρ₃) ρ₁                  ≡⟨ VecProp.map-∘ _ _ _ ⟩
    map (λ t → t / ρ₃) (map (λ t → t / ρ₂) ρ₁)  ∎

  map-weaken-⊙-sub : ∀ {m n} {ρ : Sub T m n} {t} → map weaken ρ ⊙ sub t ≡ ρ
  map-weaken-⊙-sub {ρ = ρ} {t} = begin
    map weaken ρ ⊙ sub t  ≡⟨ cong₂ _⊙_ map-weaken refl ⟩
    ρ ⊙ wk ⊙ sub t        ≡⟨ sym ⊙-assoc ⟩
    ρ ⊙ (wk ⊙ sub t)      ≡⟨ cong (_⊙_ ρ) wk-⊙-sub ⟩
    ρ ⊙ id                ≡⟨ ⊙-id ⟩
    ρ                     ∎

  sub-⊙ : ∀ {m n} {ρ : Sub T m n} t → sub t ⊙ ρ ≡ ρ ↑ ⊙ sub (t / ρ)
  sub-⊙ {ρ = ρ} t = begin
    sub t ⊙ ρ                           ≡⟨ refl ⟩
    t / ρ ∷ id ⊙ ρ                      ≡⟨ cong (_∷_ (t / ρ)) id-⊙ ⟩
    t / ρ ∷ ρ                           ≡⟨ cong (_∷_ (t / ρ)) (sym map-weaken-⊙-sub) ⟩
    t / ρ ∷ map weaken ρ ⊙ sub (t / ρ)  ≡⟨ cong₂ _∷_ (sym var-/) refl ⟩
    ρ ↑ ⊙ sub (t / ρ)                   ∎

  suc-/-↑ : ∀ {m n} {ρ : Sub T m n} x →
            var (suc x) / ρ ↑ ≡ var x / ρ / wk
  suc-/-↑ {ρ = ρ} x = begin
    var (suc x) / ρ ↑        ≡⟨ var-/ ⟩
    lookup (map weaken ρ) x  ≡⟨ cong (Fun.flip lookup x) (map-weaken {ρ = ρ}) ⟩
    lookup (ρ ⊙ wk)       x  ≡⟨ lookup-⊙ x {ρ₁ = ρ} ⟩
    lookup ρ x / wk          ≡⟨ cong₂ _/_ (sym var-/) refl ⟩
    var x / ρ / wk           ∎

  open Lemmas₃ lemmas₃ public
    hiding (/✶-↑✶; /✶-↑✶′; wk-↑⋆-⊙-wk;
            lookup-wk-↑⋆-⊙; lookup-map-weaken-↑⋆)

-- For an example of how AppLemmas can be used, see
-- Data.Fin.Substitution.List.

record AppLemmas {ℓ₁ ℓ₂} (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
  field
    application : Application T₁ T₂
    lemmas₄     : Lemmas₄ T₂

  open Application application using (_/_; _/✶_)
  open Lemmas₄ lemmas₄
    using (id; _⊙_; wk; weaken; sub; _↑; ⨀) renaming (_/_ to _⊘_)

  field
    id-vanishes : ∀ {n} (t : T₁ n) → t / id ≡ t
    /-⊙         : ∀ {m n k} {ρ₁ : Sub T₂ m n} {ρ₂ : Sub T₂ n k} t →
                  t / ρ₁ ⊙ ρ₂ ≡ t / ρ₁ / ρ₂

  private module L₄ = Lemmas₄ lemmas₄

  /-⨀ : ∀ {m n} t (ρs : Subs T₂ m n) → t / ⨀ ρs ≡ t /✶ ρs
  /-⨀ t ε                = id-vanishes t
  /-⨀ t (ρ ◅ ε)          = refl
  /-⨀ t (ρ ◅ (ρ′ ◅ ρs′)) = begin
    t / ⨀ ρs ⊙ ρ  ≡⟨ /-⊙ t ⟩
    t / ⨀ ρs / ρ  ≡⟨ cong₂ _/_ (/-⨀ t (ρ′ ◅ ρs′)) refl ⟩
    t /✶ ρs / ρ   ∎
    where ρs = ρ′ ◅ ρs′

  ⨀→/✶ : ∀ {m n} (ρs₁ ρs₂ : Subs T₂ m n) →
         ⨀ ρs₁ ≡ ⨀ ρs₂ → ∀ t → t /✶ ρs₁ ≡ t /✶ ρs₂
  ⨀→/✶ ρs₁ ρs₂ hyp t = begin
    t /✶ ρs₁   ≡⟨ sym (/-⨀ t ρs₁) ⟩
    t / ⨀ ρs₁  ≡⟨ cong (_/_ t) hyp ⟩
    t / ⨀ ρs₂  ≡⟨ /-⨀ t ρs₂ ⟩
    t /✶ ρs₂   ∎

  wk-commutes : ∀ {m n} {ρ : Sub T₂ m n} t →
                t / ρ / wk ≡ t / wk / ρ ↑
  wk-commutes {ρ = ρ} = ⨀→/✶ (ε ▻ ρ ▻ wk) (ε ▻ wk ▻ ρ ↑) L₄.⊙-wk

  sub-commutes : ∀ {m n} {t′} {ρ : Sub T₂ m n} t →
                 t / sub t′ / ρ ≡ t / ρ ↑ / sub (t′ ⊘ ρ)
  sub-commutes {t′ = t′} {ρ} =
    ⨀→/✶ (ε ▻ sub t′ ▻ ρ) (ε ▻ ρ ↑ ▻ sub (t′ ⊘ ρ)) (L₄.sub-⊙ t′)

  wk-sub-vanishes : ∀ {n t′} (t : T₁ n) → t / wk / sub t′ ≡ t
  wk-sub-vanishes {t′ = t′} = ⨀→/✶ (ε ▻ wk ▻ sub t′) ε L₄.wk-⊙-sub

  /-weaken : ∀ {m n} {ρ : Sub T₂ m n} t → t / map weaken ρ ≡ t / ρ / wk
  /-weaken {ρ = ρ} = ⨀→/✶ (ε ▻ map weaken ρ) (ε ▻ ρ ▻ wk) L₄.map-weaken

  open Application application public
  open L₄ public
    hiding (application; _⊙_; _/_; _/✶_;
            id-vanishes; /-⊙; wk-commutes)

record Lemmas₅ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where
  field lemmas₄ : Lemmas₄ T

  private module L₄ = Lemmas₄ lemmas₄

  appLemmas : AppLemmas T T
  appLemmas = record
    { application = L₄.application
    ; lemmas₄     = lemmas₄
    ; id-vanishes = L₄.id-vanishes
    ; /-⊙         = L₄./-⊙
    }

  open AppLemmas appLemmas public hiding (lemmas₄)

------------------------------------------------------------------------
-- Instantiations and code for facilitating instantiations

-- Lemmas about variable substitutions (renamings).

module VarLemmas where

  open VarSubst

  lemmas₃ : Lemmas₃ Fin
  lemmas₃ = record
    { lemmas₂ = record
      { lemmas₁ = record
        { lemmas₀ = record
          { simple = simple
          }
        ; weaken-var = refl
        }
      ; application = application
      ; var-/       = refl
      }
    ; /✶-↑✶ = λ _ _ hyp → hyp
    }

  private module L₃ = Lemmas₃ lemmas₃

  lemmas₅ : Lemmas₅ Fin
  lemmas₅ = record
    { lemmas₄ = record
      { lemmas₃ = lemmas₃
      ; /-wk    = L₃.lookup-wk _
      }
    }

  open Lemmas₅ lemmas₅ public hiding (lemmas₃)

-- Lemmas about "term" substitutions.

record TermLemmas (T : ℕ → Set) : Set₁ where
  field
    termSubst : TermSubst T

  open TermSubst termSubst

  field
    app-var : ∀ {T′} {lift : Lift T′ T} {m n x} {ρ : Sub T′ m n} →
              app lift (var x) ρ ≡ Lift.lift lift (lookup ρ x)
    /✶-↑✶   : ∀ {T₁ T₂} {lift₁ : Lift T₁ T} {lift₂ : Lift T₂ T} →
              let open Lifted lift₁
                    using () renaming (_↑✶_ to _↑✶₁_; _/✶_ to _/✶₁_)
                  open Lifted lift₂
                    using () renaming (_↑✶_ to _↑✶₂_; _/✶_ to _/✶₂_)
              in
              ∀ {m n} (ρs₁ : Subs T₁ m n) (ρs₂ : Subs T₂ m n) →
              (∀ k x → var x /✶₁ ρs₁ ↑✶₁ k ≡ var x /✶₂ ρs₂ ↑✶₂ k) →
              ∀ k t → t /✶₁ ρs₁ ↑✶₁ k ≡ t /✶₂ ρs₂ ↑✶₂ k

  private module V = VarLemmas

  lemmas₃ : Lemmas₃ T
  lemmas₃ = record
    { lemmas₂ = record
      { lemmas₁ = record
        { lemmas₀ = record
          { simple = simple
          }
        ; weaken-var = λ {_ x} → begin
            var x /Var V.wk      ≡⟨ app-var ⟩
            var (lookup V.wk x)  ≡⟨ cong var (V.lookup-wk x) ⟩
            var (suc x)          ∎
        }
      ; application = Subst.application subst
      ; var-/       = app-var
      }
    ; /✶-↑✶ = /✶-↑✶
    }

  private module L₃ = Lemmas₃ lemmas₃

  lemmas₅ : Lemmas₅ T
  lemmas₅ = record
    { lemmas₄ = record
      { lemmas₃ = lemmas₃
      ; /-wk    = λ {_ t} → begin
          t / wk       ≡⟨ /✶-↑✶ (ε ▻ wk) (ε ▻ V.wk)
                            (λ k x → begin
                               var x / wk ↑⋆ k                 ≡⟨ L₃.var-/-wk-↑⋆ k x ⟩
                               var (lift k suc x)              ≡⟨ cong var (sym (V.var-/-wk-↑⋆ k x)) ⟩
                               var (lookup (V._↑⋆_ V.wk k) x)  ≡⟨ sym app-var ⟩
                               var x /Var V._↑⋆_ V.wk k        ∎)
                            zero t ⟩
          t /Var V.wk  ≡⟨⟩
          weaken t     ∎
      }
    }

  open Lemmas₅ lemmas₅ public hiding (lemmas₃)


text:
open import eq
open import bool
open import bool-relations using (transitive; total)
open import maybe
open import nat
open import nat-thms       using (≤-trans; ≤-total)
open import product

module z05-01-bst-test where

open import bool-relations _≤_ hiding (transitive; total)

import z05-01-bst as BST
open   BST nat _≤_ (λ {x} {y} {z} → ≤-trans {x} {y} {z})
                   (λ {x} {y}     → ≤-total {x} {y})

empty : bst 0 0
empty = bst-leaf refl

_ : bst-search 0 empty ≡ nothing
_ = refl

_ : bst-insert 5 empty ≡ bst-node 5 (bst-leaf refl) (bst-leaf refl) refl refl
_ = refl

bst-5 : bst 0 5
bst-5 = bst-insert 5 empty

_ : maybe (Σ ℕ (λ z → (5 < z || 5 =ℕ z) && (z < 5 || z =ℕ 5) ≡ tt))
_ = bst-search 5 bst-5

_ : bst-insert 9 bst-5 ≡ bst-node 5 (bst-leaf refl)
                           (bst-node 9 (bst-leaf refl) (bst-leaf refl) refl refl) refl refl
_ = refl

_ : bst 0 9
_ = bst-insert 9 bst-5

_ : bst 0 5
_ = bst-dec-lb {0} {0} {5} (bst-leaf refl) refl

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
module Data.TreeRep where

open import Prelude hiding (_>>=_) renaming (_>>=′_ to _>>=_)
open import Container.Traversable
open import Builtin.Reflection
open import Builtin.Float

data Leaf : Set where
  char   : Char → Leaf
  string : String → Leaf
  float  : Float → Leaf
  name   : Name → Leaf

data TreeRep : Set where
  leaf : Leaf → TreeRep
  node : Nat → List TreeRep → TreeRep

--- Eq instance ---

private
  leaf-char-inj : ∀ {x y} → Leaf.char x ≡ char y → x ≡ y
  leaf-char-inj refl = refl

  leaf-string-inj : ∀ {x y} → Leaf.string x ≡ string y → x ≡ y
  leaf-string-inj refl = refl

  leaf-float-inj : ∀ {x y} → Leaf.float x ≡ float y → x ≡ y
  leaf-float-inj refl = refl

  leaf-name-inj : ∀ {x y} → Leaf.name x ≡ name y → x ≡ y
  leaf-name-inj refl = refl

  leaf-inj : ∀ {x y} → leaf x ≡ leaf y → x ≡ y
  leaf-inj refl = refl

  node-inj₁ : ∀ {x y z w} → node x z ≡ node y w → x ≡ y
  node-inj₁ refl = refl

  node-inj₂ : ∀ {x y z w} → node x z ≡ node y w → z ≡ w
  node-inj₂ refl = refl

  eq-leaf : (x y : Leaf) → Dec (x ≡ y)
  eq-leaf (char x) (char x₁) = decEq₁ leaf-char-inj (x == x₁)
  eq-leaf (string x) (string x₁) = decEq₁ leaf-string-inj (x == x₁)
  eq-leaf (float x) (float x₁) = decEq₁ leaf-float-inj (x == x₁)
  eq-leaf (name x) (name x₁) = decEq₁ leaf-name-inj (x == x₁)
  eq-leaf (char x) (string x₁) = no λ()
  eq-leaf (char x) (float x₁) = no λ()
  eq-leaf (char x) (name x₁) = no λ()
  eq-leaf (string x) (char x₁) = no λ()
  eq-leaf (string x) (float x₁) = no λ()
  eq-leaf (string x) (name x₁) = no λ()
  eq-leaf (float x) (char x₁) = no λ()
  eq-leaf (float x) (string x₁) = no λ()
  eq-leaf (float x) (name x₁) = no λ()
  eq-leaf (name x) (char x₁) = no λ()
  eq-leaf (name x) (string x₁) = no λ()
  eq-leaf (name x) (float x₁) = no λ()

instance
  EqLeaf : Eq Leaf
  _==_ {{EqLeaf}} = eq-leaf

private
  eq-tree  : (x y : TreeRep) → Dec (x ≡ y)
  eq-trees : (xs ys : List TreeRep) → Dec (xs ≡ ys)

  eq-tree (leaf x) (leaf x₁) = decEq₁ leaf-inj (x == x₁)
  eq-tree (leaf x) (node x₁ x₂) = no λ()
  eq-tree (node x x₁) (leaf x₂) = no λ()
  eq-tree (node x xs) (node y ys) = decEq₂ node-inj₁ node-inj₂ (x == y) (eq-trees xs ys)

  eq-trees [] [] = yes refl
  eq-trees [] (x ∷ ys) = no λ()
  eq-trees (x ∷ xs) [] = no λ()
  eq-trees (x ∷ xs) (y ∷ ys) = decEq₂ cons-inj-head cons-inj-tail (eq-tree x y) (eq-trees xs ys)

instance
  EqTree : Eq TreeRep
  _==_ {{EqTree}} = eq-tree

--- Ord instance ---

data LessLeaf : Leaf → Leaf → Set where
  char         : ∀ {x y} → x < y → LessLeaf (char x) (char y)
  string       : ∀ {x y} → x < y → LessLeaf (string x) (string y)
  float        : ∀ {x y} → x < y → LessLeaf (float x) (float y)
  name         : ∀ {x y} → x < y → LessLeaf (name x) (name y)
  char<string  : ∀ {x y} → LessLeaf (char x) (string y)
  char<float   : ∀ {x y} → LessLeaf (char x) (float y)
  char<name    : ∀ {x y} → LessLeaf (char x) (name y)
  string<float : ∀ {x y} → LessLeaf (string x) (float y)
  string<name  : ∀ {x y} → LessLeaf (string x) (name y)
  float<name   : ∀ {x y} → LessLeaf (float x) (name y)

private
  cmp-leaf : (a b : Leaf) → Comparison LessLeaf a b
  cmp-leaf (char x) (char x₁) = mapComparison char (compare x x₁)
  cmp-leaf (string x) (string x₁) = mapComparison string (compare x x₁)
  cmp-leaf (float x) (float x₁) = mapComparison float (compare x x₁)
  cmp-leaf (name x) (name x₁) = mapComparison name (compare x x₁)
  cmp-leaf (char x) (string x₁) = less char<string
  cmp-leaf (char x) (float x₁) = less char<float
  cmp-leaf (char x) (name x₁) = less char<name
  cmp-leaf (string x) (char x₁) = greater char<string
  cmp-leaf (string x) (float x₁) = less string<float
  cmp-leaf (string x) (name x₁) = less string<name
  cmp-leaf (float x) (char x₁) = greater char<float
  cmp-leaf (float x) (string x₁) = greater string<float
  cmp-leaf (float x) (name x₁) = less float<name
  cmp-leaf (name x) (char x₁) = greater char<name
  cmp-leaf (name x) (string x₁) = greater string<name
  cmp-leaf (name x) (float x₁) = greater float<name

instance
  OrdLeaf : Ord Leaf
  OrdLeaf = defaultOrd cmp-leaf

  OrdLawsLeaf : Ord/Laws Leaf
  Ord/Laws.super OrdLawsLeaf = it
  less-antirefl {{OrdLawsLeaf}} (char   lt) = less-antirefl {A = Nat      } lt
  less-antirefl {{OrdLawsLeaf}} (string lt) = less-antirefl {A = List Char} lt
  less-antirefl {{OrdLawsLeaf}} (float  lt) = less-antirefl {A = Float    } lt
  less-antirefl {{OrdLawsLeaf}} (name   lt) = less-antirefl {A = Name     } lt
  less-trans {{OrdLawsLeaf}} (char   lt) (char   lt₁) = char   (less-trans {A = Nat      } lt lt₁)
  less-trans {{OrdLawsLeaf}} (string lt) (string lt₁) = string (less-trans {A = List Char} lt lt₁)
  less-trans {{OrdLawsLeaf}} (float  lt) (float  lt₁) = float  (less-trans {A = Float    } lt lt₁)
  less-trans {{OrdLawsLeaf}} (name   lt) (name   lt₁) = name   (less-trans {A = Name     } lt lt₁)
  less-trans {{OrdLawsLeaf}} (char   lt) char<string  = char<string
  less-trans {{OrdLawsLeaf}} (char   lt) char<float   = char<float
  less-trans {{OrdLawsLeaf}} (char   lt) char<name    = char<name
  less-trans {{OrdLawsLeaf}} (string lt) string<float = string<float
  less-trans {{OrdLawsLeaf}} (string lt) string<name  = string<name
  less-trans {{OrdLawsLeaf}} (float  lt) float<name   = float<name
  less-trans {{OrdLawsLeaf}} char<string  (string lt) = char<string
  less-trans {{OrdLawsLeaf}} char<string string<float = char<float
  less-trans {{OrdLawsLeaf}} char<string  string<name = char<name
  less-trans {{OrdLawsLeaf}} char<float   (float lt)  = char<float
  less-trans {{OrdLawsLeaf}} char<float   float<name  = char<name
  less-trans {{OrdLawsLeaf}} char<name    (name lt)   = char<name
  less-trans {{OrdLawsLeaf}} string<float (float lt)  = string<float
  less-trans {{OrdLawsLeaf}} string<float float<name  = string<name
  less-trans {{OrdLawsLeaf}} string<name  (name lt)   = string<name
  less-trans {{OrdLawsLeaf}} float<name   (name lt)   = float<name

data LessTree : TreeRep → TreeRep → Set where
  leaf      : ∀ {x y} → x < y → LessTree (leaf x) (leaf y)
  leaf<node : ∀ {x y ys} → LessTree (leaf x) (node y ys)
  tag<      : ∀ {x y xs ys} → x < y → LessTree (node x xs) (node y ys)
  children< : ∀ {x xs ys} → LessList LessTree xs ys → LessTree (node x xs) (node x ys)

private
  cmp-tree  : ∀ x y → Comparison LessTree x y
  cmp-trees : ∀ xs ys → Comparison (LessList LessTree) xs ys

  cmp-tree (leaf x) (leaf y) = mapComparison leaf (compare x y)
  cmp-tree (leaf _) (node _ _) = less leaf<node
  cmp-tree (node _ _) (leaf _) = greater leaf<node
  cmp-tree (node x xs) (node  y ys)  with compare x y
  cmp-tree (node x xs) (node  y ys)  | less    x<y = less (tag< x<y)
  cmp-tree (node x xs) (node  y ys)  | greater x>y = greater (tag< x>y)
  cmp-tree (node x xs) (node .x ys)  | equal refl with cmp-trees xs ys
  cmp-tree (node x xs) (node .x ys)  | equal refl | less    lt = less (children< lt)
  cmp-tree (node x xs) (node .x .xs) | equal refl | equal refl = equal refl
  cmp-tree (node x xs) (node .x ys)  | equal refl | greater gt = greater (children< gt)

  cmp-trees [] [] = equal refl
  cmp-trees []       (x ∷ ys) = less nil<cons
  cmp-trees (x ∷ xs) []       = greater nil<cons
  cmp-trees (x ∷ xs) (y ∷ ys) = compareCons (cmp-tree x y) (cmp-trees xs ys)

instance
  OrdTree : Ord TreeRep
  OrdTree = defaultOrd cmp-tree

private
  antirefl  : {t : TreeRep} → t < t → ⊥
  antirefls : {ts : List TreeRep} → ts < ts → ⊥
  antirefl  (leaf lt)      = less-antirefl {A = Leaf} lt
  antirefl  (tag< lt)      = less-antirefl {A = Nat} lt
  antirefl  (children< lt) = antirefls lt
  antirefls (head< lt)     = antirefl lt
  antirefls (tail< lt)     = antirefls lt

  ltrans  : {s t u : TreeRep} → s < t → t < u → s < u
  ltranss : {ss ts us : List TreeRep} → ss < ts → ts < us → ss < us
  ltrans (leaf lt)      (leaf lt₁)      = leaf (less-trans {A = Leaf} lt lt₁)
  ltrans (leaf lt)      leaf<node       = leaf<node
  ltrans leaf<node      (tag< lt)       = leaf<node
  ltrans leaf<node      (children< lt)  = leaf<node
  ltrans (tag< lt)      (tag< lt₁)      = tag< (less-trans {A = Nat} lt lt₁)
  ltrans (tag< lt)      (children< lt₁) = tag< lt
  ltrans (children< lt) (tag< lt₁)      = tag< lt₁
  ltrans (children< lt) (children< lt₁) = children< (ltranss lt lt₁)
  ltranss nil<cons      (head< lt)      = nil<cons
  ltranss nil<cons      (tail< lt₁)     = nil<cons
  ltranss (head< lt)    (head< lt₁)     = head< (ltrans lt lt₁)
  ltranss (head< lt)    (tail< lt₁)     = head< lt
  ltranss (tail< lt)    (head< lt₁)     = head< lt₁
  ltranss (tail< lt)    (tail< lt₁)     = tail< (ltranss lt lt₁)

instance
  OrdLawsTree : Ord/Laws TreeRep
  Ord/Laws.super OrdLawsTree = it
  less-antirefl {{OrdLawsTree}} = antirefl
  less-trans    {{OrdLawsTree}} = ltrans

--- Encoding types as trees ---

record TreeEncoding {a} (A : Set a) : Set a where
  constructor treeEncoding
  field
    treeEncode : A → TreeRep
    treeDecode : TreeRep → Maybe A
    isTreeEmbedding : ∀ x → treeDecode (treeEncode x) ≡ just x

open TreeEncoding {{...}} public

module _ {a} {A : Set a} {{_ : TreeEncoding A}} where
  private
    encode-injective : (x y : A) → treeEncode x ≡ treeEncode y → x ≡ y
    encode-injective x y eq = eraseEquality $ just-inj $
      isTreeEmbedding x ʳ⟨≡⟩ cong treeDecode eq ⟨≡⟩ isTreeEmbedding y

    decTreeEq : (x y : A) → Dec (x ≡ y)
    decTreeEq x y with treeEncode x == treeEncode y
    decTreeEq x y | yes eq = yes (encode-injective x y eq)
    decTreeEq x y | no !eq = no λ x=y → !eq (cong treeEncode x=y)

  EqByTreeEncoding : Eq A
  _==_ {{EqByTreeEncoding}} = decTreeEq

  data LessEncoding (x y : A) : Set a where
    less-enc : treeEncode x < treeEncode y → LessEncoding x y

  OrdByTreeEncoding : Ord A
  OrdByTreeEncoding = defaultOrd λ x y → injectComparison (encode-injective _ _) less-enc $
                                          (compare on treeEncode) x y

  OrdLawsByTreeEncoding : Ord/Laws A
  Ord/Laws.super OrdLawsByTreeEncoding = OrdByTreeEncoding
  less-antirefl {{OrdLawsByTreeEncoding}} (less-enc lt) = less-antirefl {A = TreeRep} lt
  less-trans    {{OrdLawsByTreeEncoding}} (less-enc lt) (less-enc lt₁) = less-enc (less-trans {A = TreeRep} lt lt₁)

--- Encodings for standard types ---

instance
  EncodeNat : TreeEncoding Nat
  EncodeNat = treeEncoding enc dec (λ _ → refl)
    where
      enc : Nat → TreeRep
      enc n = node n []

      dec : TreeRep → Maybe Nat
      dec (node n _) = just n
      dec (leaf _) = nothing

  EncodeBool : TreeEncoding Bool
  EncodeBool = treeEncoding enc dec emb
    where
      enc : Bool → TreeRep
      enc false = node 0 []
      enc true = node 1 []

      dec : TreeRep → Maybe Bool
      dec (node 0 _) = just false
      dec _          = just true

      emb : ∀ b → dec (enc b) ≡ just b
      emb false = refl
      emb true  = refl

  EncodeMaybe : ∀ {a} {A : Set a} {{_ : TreeEncoding A}} → TreeEncoding (Maybe A)
  EncodeMaybe {A = A} = treeEncoding enc dec emb
    where
      enc : Maybe A → TreeRep
      enc nothing  = node 0 []
      enc (just x) = node 1 [ treeEncode x ]

      dec : TreeRep → Maybe (Maybe A)
      dec (node 0 _)       = just nothing
      dec (node _ (x ∷ _)) = just <$> treeDecode x
      dec _                = nothing

      emb : ∀ x → dec (enc x) ≡ just x
      emb nothing  = refl
      emb (just x) = just =$= isTreeEmbedding x

  EncodeSigma : ∀ {a b} {A : Set a} {B : A → Set b}
                  {{EncA : TreeEncoding A}} {{EncB : ∀ {x} → TreeEncoding (B x)}} →
                  TreeEncoding (Σ A B)
  EncodeSigma {A = A} {B = B} = treeEncoding enc dec emb
    where
      enc : Σ A B → TreeRep
      enc (x , y) = node 0 (treeEncode x ∷ treeEncode y ∷ [])

      dec : TreeRep → Maybe (Σ A B)
      dec (node _ (x ∷ y ∷ _)) = do
        x ← treeDecode x ofType Maybe A
        y ← treeDecode y
        just (x , y)
      dec _ = nothing

      emb : ∀ x → dec (enc x) ≡ just x
      emb (x , y) rewrite isTreeEmbedding x | isTreeEmbedding y = refl

  EncodeList : ∀ {a} {A : Set a} {{_ : TreeEncoding A}} → TreeEncoding (List A)
  treeEncode {{EncodeList}} xs          = node 0 (map treeEncode xs)
  treeDecode {{EncodeList}} (node _ xs) = traverse′ treeDecode xs
  treeDecode {{EncodeList}} _           = nothing
  isTreeEmbedding {{EncodeList}} []       = refl
  isTreeEmbedding {{EncodeList}} (x ∷ xs) = _∷_ =$= isTreeEmbedding x =*= isTreeEmbedding xs

--- Example ---

-- private
--   data TestData : Set where
--     cA : TestData → TestData
--     cB : TestData → TestData → TestData
--     cC : TestData
--     cD : TestData → TestData → TestData

--   private
--     encodeTest : TestData → TreeRep
--     encodeTest (cA x)   = node 0 (encodeTest x ∷ [])
--     encodeTest (cB x y) = node 1 (encodeTest x ∷ encodeTest y ∷ [])
--     encodeTest cC       = node 2 []
--     encodeTest (cD x y) = node 3 (encodeTest x ∷ encodeTest y ∷ [])

--     decodeTest : TreeRep → Maybe TestData
--     decodeTest (leaf _) = nothing
--     decodeTest (node 0 (x ∷ []))     = cA <$> decodeTest x
--     decodeTest (node 1 (x ∷ y ∷ [])) = cB <$> decodeTest x <*> decodeTest y
--     decodeTest (node 2 [])           = just cC
--     decodeTest (node 3 (x ∷ y ∷ [])) = cD <$> decodeTest x <*> decodeTest y
--     decodeTest _ = nothing

--     embeddingTest : ∀ x → decodeTest (encodeTest x) ≡ just x
--     embeddingTest (cA x)   = cA =$= embeddingTest x
--     embeddingTest (cB x y) = cB =$= embeddingTest x =*= embeddingTest y
--     embeddingTest cC       = refl
--     embeddingTest (cD x y) = cD =$= embeddingTest x =*= embeddingTest y

--   instance
--     EncodeTest : TreeEncoding TestData
--     EncodeTest = record { treeEncode      = encodeTest
--                         ; treeDecode      = decodeTest
--                         ; isTreeEmbedding = embeddingTest }

--     EqTest : Eq TestData
--     EqTest = EqByTreeEncoding

--     OrdTest : Ord TestData
--     OrdTest = OrdByTreeEncoding

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
module _ where

open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.Unit
open import Agda.Builtin.List
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Bool

_>>_ : {A B : Set} → TC A → TC B → TC B
m >> m₁ = m >>= λ _ → m₁

data Fin : Nat → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)

macro
  reflectAndCheck : ∀ {a} {A : Set a} → A → Term → TC ⊤
  reflectAndCheck {A = A} x hole = withNormalisation true do
    `x  ← quoteTC x
    `A  ← quoteTC A
    ``x ← checkType `x `A >>= quoteTC
    unify hole ``x

  quoteUnquote : ∀ {a} {A : Set a} → A → Term → TC ⊤
  quoteUnquote x hole = withNormalisation true do
    `x ← quoteTC x
    unify hole `x

module _ (n : Nat) (A : Set) (m : Nat) (j : Fin m) where

  plam₁ : Fin n → Fin m
  plam₁ = λ where zero → j; (suc i) → j

  `plam₁ : Term
  `plam₁ = reflectAndCheck plam₁

  plam₁′ : Fin n → Fin m
  plam₁′ = quoteUnquote plam₁

  refined₁ : n ≡ suc m → Nat
  refined₁ refl = 0
    where
      plam : Fin n → Fin m
      plam = λ where zero → j; (suc i) → i

      `plam : Term
      `plam = reflectAndCheck plam

      plam′ : Fin n → Fin m
      plam′ = quoteUnquote plam

  refined₂ : m ≡ suc n → Nat
  refined₂ refl = 0
    where
      plam : Fin n → Fin m
      plam = λ where zero → j; (suc i) → suc (suc i)

      `plam : Term
      `plam = reflectAndCheck plam

      plam′ : Fin n → Fin m
      plam′ = quoteUnquote plam


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

open import Definition.Typed.EqualityRelation

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

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.MaybeEmbed

open import Tools.Product
open import Tools.Empty

import Definition.LogicalRelation.Weakening as wkLR
import Tools.PropositionalEquality as PE
import Data.Nat as Nat

-- Validity of the universe type.
U¹ᵛ : ∀ {Γ rU l} → (ι ¹ <∞ l) → ([Γ] : ⊩ᵛ Γ)
      → Γ ⊩ᵛ⟨ l ⟩ Univ rU ¹ ^ [ ! , ∞ ] / [Γ]
U¹ᵛ {Γ} {rU} ∞< [Γ] ⊢Δ [σ] =
  Ugen ⊢Δ , (λ [σ′] [σ≡σ′] → id (Uⱼ ⊢Δ))

U⁰ᵛ : ∀ {Γ rU l' l} → (⁰ ≤ l') → (ι l' <∞ l) → ([Γ] : ⊩ᵛ Γ)
      → Γ ⊩ᵛ⟨ l ⟩ Univ rU ⁰ ^ [ ! , ι ¹ ] / [Γ]
U⁰ᵛ {Γ} {rU} (<is≤ 0<1) ∞< [Γ] ⊢Δ [σ] = emb ∞< (Uᵣ (Uᵣ rU ⁰ emb< PE.refl [[ Ugenⱼ ⊢Δ , Ugenⱼ ⊢Δ , id (Ugenⱼ ⊢Δ) ]])) , (λ [σ′] [σ≡σ′] → id (Ugenⱼ ⊢Δ))
U⁰ᵛ {Γ} {rU} (≡is≤ PE.refl) l< [Γ] ⊢Δ [σ] =
  Uᵣ (Uᵣ rU ⁰ l< PE.refl [[ Ugenⱼ ⊢Δ , Ugenⱼ ⊢Δ , id (Ugenⱼ ⊢Δ) ]])
  , (λ [σ′] [σ≡σ′] → id (Ugenⱼ ⊢Δ))

Uᵛgen : ∀ {Γ rU lU lU' l} → (lU ≤ lU') → (ι lU' <∞ l) → ([Γ] : ⊩ᵛ Γ)
     → Γ ⊩ᵛ⟨ l ⟩ Univ rU lU ^ [ ! , next lU ] / [Γ]
Uᵛgen {lU = ⁰} = U⁰ᵛ
Uᵛgen {lU = ¹} (≡is≤ PE.refl) = U¹ᵛ

Uᵛ : ∀ {Γ rU lU l} → (ι lU <∞ l) → ([Γ] : ⊩ᵛ Γ)
     → Γ ⊩ᵛ⟨ l ⟩ Univ rU lU ^ [ ! , next lU ] / [Γ]
Uᵛ = Uᵛgen (≡is≤ PE.refl)

Uᵗᵛ₁ :  ∀ {Γ rU} → (⊢Γ : ⊢ Γ) → Γ ⊩⟨ ∞ ⟩ Univ rU ⁰ ∷ Univ ! ¹ ^ [ ! , ∞ ] / Ugen ⊢Γ
Uᵗᵛ₁ {Γ} {rU} ⊢Γ = Uₜ (Univ rU ⁰) (idRedTerm:*: (univ 0<1 ⊢Γ)) Uₙ (≅-U⁰refl ⊢Γ)
                                  (λ σ ⊢Δ₁ → Uᵣ′ (Univ rU ⁰) (ι ¹) rU ⁰ emb< PE.refl (idRed:*: (Ugenⱼ ⊢Δ₁)))

Uᵗᵛ : ∀ {Γ rU} → ([Γ] : ⊩ᵛ Γ) → Γ ⊩ᵛ⟨ ∞ ⟩ Univ rU ⁰ ∷ Univ ! ¹ ^ [ ! , ∞ ] / [Γ] / Uᵛ ∞< [Γ]
Uᵗᵛ {Γ} {rU} [Γ] = λ ⊢Δ [σ] → Uᵗᵛ₁ ⊢Δ
                            , λ [σ′] [σ≡σ′] → Uₜ₌ (Uᵗᵛ₁ ⊢Δ) (Uᵗᵛ₁ ⊢Δ) (≅-U⁰refl ⊢Δ) λ [ρ] ⊢Δ → id (Ugenⱼ ⊢Δ)

-- Valid terms of type U are valid types.
univᵛ : ∀ {A Γ rU lU lU' l} ([Γ] : ⊩ᵛ Γ)
        (lU< : lU ≤ lU')
        ([U] : Γ ⊩ᵛ⟨ l ⟩ Univ rU lU ^ [ ! , next lU ] / [Γ])
      → Γ ⊩ᵛ⟨ l ⟩ A ∷ Univ rU lU ^ [ ! , next lU ] / [Γ] / [U]
      → Γ ⊩ᵛ⟨ ι lU' ⟩ A ^ [ rU , ι lU ] / [Γ]
univᵛ {lU = lU} {l = l} [Γ] lU< [U] [A] ⊢Δ [σ] =
  let [A]₁ = irrelevance-≤ lU< (univEq (proj₁ ([U] ⊢Δ [σ])) (proj₁ ([A] ⊢Δ [σ]))) in
  [A]₁ , λ [σ′] [σ≡σ′] → univEqEq (proj₁ ([U] ⊢Δ [σ])) [A]₁
                                  ((proj₂ ([A] ⊢Δ [σ])) [σ′] [σ≡σ′])

-- Valid term equality of type U is valid type equality.
univEqᵛ : ∀ {A B Γ rU lU l l′} ([Γ] : ⊩ᵛ Γ)
          ([U] : Γ ⊩ᵛ⟨ l′ ⟩ Univ rU lU ^ [ ! , next lU ] / [Γ])
          ([A] : Γ ⊩ᵛ⟨ l ⟩ A ^ [ rU , ι lU ] / [Γ])
        → Γ ⊩ᵛ⟨ l′ ⟩ A ≡ B ∷ Univ rU lU ^ [ ! , next lU ] / [Γ] / [U]
        → Γ ⊩ᵛ⟨ l ⟩ A ≡ B ^ [ rU , ι lU ] / [Γ] / [A]
univEqᵛ {A} [Γ] [U] [A] [t≡u] ⊢Δ [σ] =
  univEqEq (proj₁ ([U] ⊢Δ [σ])) (proj₁ ([A] ⊢Δ [σ])) ([t≡u] ⊢Δ [σ])

univᵗᵛ : ∀ {Γ A t r l′}  ([Γ] : ⊩ᵛ Γ)
       → ([U] : Γ ⊩ᵛ⟨ ∞ ⟩ Univ r l′ ^ [ ! , next l′ ] / [Γ] )
       → ([A] : Γ ⊩ᵛ⟨ ∞ ⟩ A ∷ Univ r l′ ^ [ ! , next l′ ] / [Γ] / [U])
       → Γ ⊩ᵛ⟨ ∞ ⟩ t ∷ A ^ [ r , ι l′ ] / [Γ] / maybeEmbᵛ {A = A} [Γ] (univᵛ {A = A} [Γ] (≡is≤ PE.refl) [U] [A])
       → Γ ⊩ᵛ⟨ ι l′ ⟩ t ∷ A ^ [ r , ι l′ ] / [Γ] / univᵛ {A = A} [Γ] (≡is≤ PE.refl) [U] [A]
univᵗᵛ {Γ} {A} {t} {r} {⁰} [Γ] [U] [A] [t] ⊢Δ [σ] =
  univEqTerm (proj₁ ([U] ⊢Δ [σ])) (proj₁ ([A] ⊢Δ [σ])) (proj₁ ([t] ⊢Δ [σ])) ,
  λ [σ′] [σ≡σ′] → univEqEqTerm (proj₁ ([U] ⊢Δ [σ])) (proj₁ ([A] ⊢Δ [σ])) (proj₁ ([t] ⊢Δ [σ])) (proj₂ ([t] ⊢Δ [σ]) [σ′] [σ≡σ′])
univᵗᵛ {Γ} {A} {t} {r} {¹} [Γ] [U] [A] [t] ⊢Δ [σ] =
  univEqTerm (proj₁ ([U] ⊢Δ [σ])) (proj₁ ([A] ⊢Δ [σ])) (proj₁ ([t] ⊢Δ [σ])) ,
  λ [σ′] [σ≡σ′] → univEqEqTerm (proj₁ ([U] ⊢Δ [σ])) (proj₁ ([A] ⊢Δ [σ])) (proj₁ ([t] ⊢Δ [σ])) (proj₂ ([t] ⊢Δ [σ]) [σ′] [σ≡σ′])

un-univᵛ : ∀ {A Γ r l} ([Γ] : ⊩ᵛ Γ)
        ([U] : Γ ⊩ᵛ⟨ next l ⟩ Univ r l ^ [ ! , next l ] / [Γ])
      → Γ ⊩ᵛ⟨ ι l ⟩ A ^ [ r , ι l ] / [Γ]
      → Γ ⊩ᵛ⟨ next l ⟩ A ∷ Univ r l ^ [ ! , next l ] / [Γ] / [U]
un-univᵛ {l = l} [Γ] [U] [A] = λ ⊢Δ [σ] →
  irrelevanceTerm (Ugen (wf (escape (proj₁ ([A] ⊢Δ [σ])))))  (proj₁ ([U] ⊢Δ [σ])) (un-univEq (proj₁ ([A] ⊢Δ [σ]))) ,
  λ [σ′] [σ≡σ′] → irrelevanceEqTerm (Ugen (wf (escape (proj₁ ([A] ⊢Δ [σ]))))) (proj₁ ([U] ⊢Δ [σ])) (un-univEqEq (proj₁ ([A] ⊢Δ [σ])) (proj₁ ([A] ⊢Δ [σ′])) (proj₂ ([A] ⊢Δ [σ]) [σ′] [σ≡σ′]))

un-univEqᵛ : ∀ {A B Γ r l} ([Γ] : ⊩ᵛ Γ)
        ([U] : Γ ⊩ᵛ⟨ next l ⟩ Univ r l ^ [ ! , next l ] / [Γ])
      → ([A] : Γ ⊩ᵛ⟨ ι l ⟩ A ^ [ r , ι l ] / [Γ])
      → ([B] : Γ ⊩ᵛ⟨ ι l ⟩ B ^ [ r , ι l ] / [Γ])
      → Γ ⊩ᵛ⟨ ι l ⟩ A ≡ B ^ [ r , ι l ] / [Γ] / [A]
      → Γ ⊩ᵛ⟨ next l ⟩ A ≡ B ∷ Univ r l ^ [ ! , next l ] / [Γ] / [U]
un-univEqᵛ {l = l} [Γ] [U] [A] [B] [A≡B] = λ ⊢Δ [σ] →
  irrelevanceEqTerm (Ugen (wf (escape (proj₁ ([A] ⊢Δ [σ])))))  (proj₁ ([U] ⊢Δ [σ])) (un-univEqEq (proj₁ ([A] ⊢Δ [σ])) (proj₁ ([B] ⊢Δ [σ])) ([A≡B] ⊢Δ [σ]))

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


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

open import HoTT
open import cohomology.Theory
open import groups.ExactSequence
open import groups.Exactness
open import groups.HomSequence
open import groups.KernelImageUniqueFactorization
import cw.cohomology.GridPtdMap as GPM

open import cw.CW

module cw.cohomology.HigherCohomologyGroups {i} (OT : OrdinaryTheory i)
  {n} (⊙skel : ⊙Skeleton {i} (S (S (S n)))) (ac : ⊙has-cells-with-choice 0 ⊙skel i) where

private
  Sn≤SSSn : S n ≤ S (S (S n))
  Sn≤SSSn = lteSR lteS

  n≤SSn : n ≤ S (S n)
  n≤SSn = lteSR lteS

  n≤SSSn : n ≤ S (S (S n))
  n≤SSSn = lteSR (lteSR lteS)

  ⊙skel₋₁ = ⊙cw-init ⊙skel
  ac₋₁ = ⊙init-has-cells-with-choice ⊙skel ac

  ⊙skel₋₂ = ⊙cw-init ⊙skel₋₁

  ⊙skel₋₃ = ⊙cw-take n≤SSSn ⊙skel
  ac₋₃ = ⊙take-has-cells-with-choice n≤SSSn ⊙skel ac

open OrdinaryTheory OT
open import cw.cohomology.HigherCoboundaryGrid OT
open import cw.cohomology.Descending OT
open import cw.cohomology.InnerGrid OT (ℕ-to-ℤ (S (S n)))
  (⊙cw-incl-last ⊙skel₋₂)
  (⊙cw-incl-last ⊙skel₋₁)
  (⊙cw-incl-last ⊙skel)
open import cw.cohomology.WedgeOfCells OT
open import cw.cohomology.HigherCoboundary OT ⊙skel
import cw.cohomology.HigherCoboundary OT ⊙skel₋₁ as LC
import cw.cohomology.GridLongExactSequence cohomology-theory as GLES

{-
              H          apex
   Coker ≃ C(X₂/X₀)<---C(X₃/X₀) ≃ C(X)
              ^           ^
              |           |
              |           |
           C(X₂/X₁)<---C(X₃/X₁) ≃ Ker
             WoC          G

    WoC := Wedges of Cells
-}

private
  C-apex : Group i
  C-apex = C (ℕ-to-ℤ (S (S n))) (⊙Cofiber (⊙cw-incl-tail n≤SSSn ⊙skel))

  open import cohomology.LongExactSequence cohomology-theory
    (ℕ-to-ℤ (S n)) (⊙cw-incl-tail n≤SSSn ⊙skel)

  C-apex-iso-C-cw : C-apex ≃ᴳ C (ℕ-to-ℤ (S (S n))) ⊙⟦ ⊙skel ⟧
  C-apex-iso-C-cw = Exact2.G-trivial-and-L-trivial-implies-H-iso-K
    (exact-seq-index 1 C-cofiber-exact-seq)
    (exact-seq-index 2 C-cofiber-exact-seq)
    (C-cw-at-higher ⊙skel₋₃ ltS ac₋₃)
    (C-cw-at-higher ⊙skel₋₃ (ltSR ltS) ac₋₃)

  G : Group i
  G = C (ℕ-to-ℤ (S (S n))) (⊙Cofiber (⊙cw-incl-tail Sn≤SSSn ⊙skel))

  G-iso-Ker : G ≃ᴳ Ker.grp cw-co∂-last
  G-iso-Ker = Ker-cw-co∂-last ⊙skel ac

  H : Group i
  H = C (ℕ-to-ℤ (S (S n))) (⊙Cofiber (⊙cw-incl-tail n≤SSn ⊙skel₋₁))

  Coker-iso-H : LC.CokerCo∂ ≃ᴳ H
  Coker-iso-H = Coker-cw-co∂-last ⊙skel₋₁ ac₋₁

  module GLES-top = GLES (ℕ-to-ℤ (S n))
    (⊙cw-incl-nth Sn≤SSSn ⊙skel) (⊙cw-incl-tail Sn≤SSSn ⊙skel)
  module GPM-top = GPM
    (⊙cw-incl-nth Sn≤SSSn ⊙skel) (⊙cw-incl-tail Sn≤SSSn ⊙skel)

  G-to-C-apex : G →ᴳ C-apex
  G-to-C-apex = C-fmap (ℕ-to-ℤ (S (S n))) GPM-top.Z/X-to-Z/Y

  abstract
    G-to-C-apex-is-surj : is-surjᴳ G-to-C-apex
    G-to-C-apex-is-surj = Exact.K-trivial-implies-φ-is-surj
      (exact-seq-index 2 GLES-top.C-grid-cofiber-exact-seq)
      (CXₙ/Xₙ₋₁->-is-trivial ⊙skel₋₂ ltS (⊙take-has-cells-with-choice Sn≤SSSn ⊙skel ac))

  module GLES-right = GLES (ℕ-to-ℤ (S n))
    (⊙cw-incl-tail n≤SSn ⊙skel₋₁) (⊙cw-incl-last ⊙skel)
  module GPM-right = GPM
    (⊙cw-incl-tail n≤SSn ⊙skel₋₁) (⊙cw-incl-last ⊙skel)

  C-apex-to-H : C-apex →ᴳ H
  C-apex-to-H = C-fmap (ℕ-to-ℤ (S (S n))) GPM-right.Y/X-to-Z/X

  abstract
    C-apex-to-H-is-inj : is-injᴳ C-apex-to-H
    C-apex-to-H-is-inj = Exact.G-trivial-implies-ψ-is-inj
      (exact-seq-index 2 GLES-right.C-grid-cofiber-exact-seq)
      (CXₙ/Xₙ₋₁-<-is-trivial ⊙skel ltS ac)

  C-WoC : Group i
  C-WoC = C (ℕ-to-ℤ (S (S n))) (⊙Cofiber (⊙cw-incl-last ⊙skel₋₁))

  G-to-C-WoC : G →ᴳ C-WoC
  G-to-C-WoC = C-fmap (ℕ-to-ℤ (S (S n)))
    (GPM.Y/X-to-Z/X (⊙cw-incl-last ⊙skel₋₁) (⊙cw-incl-last ⊙skel))

  C-WoC-to-H : C-WoC →ᴳ H
  C-WoC-to-H = C-fmap (ℕ-to-ℤ (S (S n)))
    (GPM.Z/X-to-Z/Y (⊙cw-incl-nth Sn≤SSSn ⊙skel) (⊙cw-incl-last ⊙skel₋₁))

open import groups.KernelImage cw-co∂-last LC.cw-co∂-last
  (CXₙ/Xₙ₋₁-is-abelian ⊙skel₋₁ (ℕ-to-ℤ (S (S n))))

C-cw-iso-ker/im : C (ℕ-to-ℤ (S (S n))) ⊙⟦ ⊙skel ⟧ ≃ᴳ Ker/Im
C-cw-iso-ker/im = lemma ∘eᴳ C-apex-iso-C-cw ⁻¹ᴳ where
  lemma : C-apex ≃ᴳ Ker/Im
  lemma = H-iso-Ker/Im
    cw-co∂-last LC.cw-co∂-last
    (CXₙ/Xₙ₋₁-is-abelian ⊙skel₋₁ (ℕ-to-ℤ (S (S n))))
    φ₁ φ₁-is-surj φ₂ φ₂-is-inj lemma-comm
    where
      φ₁ = G-to-C-apex ∘ᴳ GroupIso.g-hom G-iso-Ker
      abstract
        φ₁-is-surj : is-surjᴳ φ₁
        φ₁-is-surj = ∘-is-surj G-to-C-apex-is-surj (equiv-is-surj (GroupIso.g-is-equiv G-iso-Ker))

      φ₂ = GroupIso.g-hom Coker-iso-H ∘ᴳ C-apex-to-H
      abstract
        φ₂-is-inj : is-injᴳ φ₂
        φ₂-is-inj = ∘-is-inj (equiv-is-inj (GroupIso.g-is-equiv Coker-iso-H)) C-apex-to-H-is-inj

      abstract
        lemma-comm : ∀ g →
             GroupIso.g Coker-iso-H (GroupHom.f (C-apex-to-H ∘ᴳ G-to-C-apex) (GroupIso.g G-iso-Ker g))
          == q[ fst g ]
        lemma-comm g =
          GroupIso.g Coker-iso-H (GroupHom.f C-apex-to-H (GroupHom.f G-to-C-apex (GroupIso.g G-iso-Ker g)))
            =⟨ ap (GroupIso.g Coker-iso-H) (! (C-inner-grid-commutes □$ᴳ GroupIso.g G-iso-Ker g)) ⟩
          GroupIso.g Coker-iso-H (GroupHom.f C-WoC-to-H (GroupHom.f G-to-C-WoC (GroupIso.g G-iso-Ker g)))
            =⟨ ap (GroupIso.g Coker-iso-H ∘ GroupHom.f C-WoC-to-H ∘ fst) (GroupIso.f-g G-iso-Ker g) ⟩
          GroupIso.g Coker-iso-H (GroupHom.f C-WoC-to-H (fst g))
            =⟨ GroupIso.g-f Coker-iso-H q[ fst g ] ⟩
          q[ fst g ]
            =∎

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module PiNF-algebra where

open import Data.Product hiding (map)
open import Level
open import Relation.Binary.Core
open import Algebra
import Algebra.FunctionProperties as FunctionProperties
open import Algebra.FunctionProperties.Core
open import Algebra.Structures

open import PiNF-syntax

------------------------------------------------------------------------------
-- Establish that Pi syntactically is a commutative semiring

⟷IsEquivalence : IsEquivalence _⟷_
⟷IsEquivalence = record {
    refl = id⟷ ;
    sym = sym  ;
    trans = _◎_
  }

+IsSemigroup : IsSemigroup _⟷_ PLUS
+IsSemigroup = record {
    isEquivalence = ⟷IsEquivalence ;
    assoc = λ x y z → assocr₊ {x} {y} {z} ;
    ∙-cong = _⊕_
  }

+0IsMonoid : IsMonoid _⟷_ PLUS ZERO
+0IsMonoid = record {
    isSemigroup = +IsSemigroup ;
    identity = ((λ x → unite₊ {x}) ,
                (λ x → swap₊ ◎ unite₊ {x}))
  }

+0IsCommutativeMonoid : IsCommutativeMonoid _⟷_ PLUS ZERO
+0IsCommutativeMonoid = record {
    isSemigroup = +IsSemigroup ;
    identityˡ = λ x → unite₊ {x} ;
    comm = λ x y → swap₊ {x} {y}
  }

+0CommutativeMonoid : CommutativeMonoid _ _
+0CommutativeMonoid = record {
  Carrier = B ;
  _≈_ = _⟷_ ;
  _∙_ = PLUS ;
  ε = ZERO ;
  isCommutativeMonoid = +0IsCommutativeMonoid
  }

--

⋆IsSemigroup : IsSemigroup _⟷_ TIMES
⋆IsSemigroup = record {
    isEquivalence = ⟷IsEquivalence ;
    assoc = λ x y z → assocr⋆ {x} {y} {z} ;
    ∙-cong = _⊗_
  }

⋆1IsMonoid : IsMonoid _⟷_ TIMES ONE
⋆1IsMonoid = record {
    isSemigroup = ⋆IsSemigroup ;
    identity = ((λ x → unite⋆ {x}) ,
                (λ x → swap⋆ ◎ unite⋆ {x}))
  }

⋆1IsCommutativeMonoid : IsCommutativeMonoid _⟷_ TIMES ONE
⋆1IsCommutativeMonoid = record {
    isSemigroup = ⋆IsSemigroup ;
    identityˡ = λ x → unite⋆ {x} ;
    comm = λ x y → swap⋆ {x} {y}
  }

⋆1CommutativeMonoid : CommutativeMonoid _ _
⋆1CommutativeMonoid = record {
  Carrier = B ;
  _≈_ = _⟷_ ;
  _∙_ = TIMES ;
  ε = ONE ;
  isCommutativeMonoid = ⋆1IsCommutativeMonoid
  }

record IsCommutativeSemiringWithoutAnnihilatingZero
         {a ℓ} {A : Set a} (≈ : Rel A ℓ)
         (+ * : Op₂ A) (0# 1# : A)
       : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    +-isCommutativeMonoid : IsCommutativeMonoid ≈ + 0#
    *-isCommutativeMonoid : IsCommutativeMonoid ≈ * 1#
    distrib               : * DistributesOver +

record CommutativeSemiringWithoutAnnihilatingZero c ℓ : Set (suc (c ⊔ ℓ)) where
  field
    Carrier : Set c
    _≈_ : Rel Carrier ℓ
    _+_ : Op₂ Carrier
    _*_ : Op₂ Carrier
    0# : Carrier
    1# : Carrier
    isCommutativeSemiringWithoutAnnihilatingZero :
      IsCommutativeSemiringWithoutAnnihilatingZero _≈_ _+_ _*_ 0# 1#

B-isCommutativeSemiringWithoutAnnihilatingZero
    : IsCommutativeSemiringWithoutAnnihilatingZero _⟷_ PLUS TIMES ZERO ONE
B-isCommutativeSemiringWithoutAnnihilatingZero = record {
    +-isCommutativeMonoid = +0IsCommutativeMonoid ;
    *-isCommutativeMonoid = ⋆1IsCommutativeMonoid ;
    distrib = ( (λ x y z → dist' {x} {y} {z}) ,
                (λ x y z → dist {y} {z} {x} ))
    }

------------------------------------------------------------------------------
-- Establish that Pi+negatives+fractionals syntactically is a meadow

+0-IsGroup : IsGroup _⟷_ PLUS ZERO NEG
+0-IsGroup = record {
  isMonoid = +0IsMonoid ;
  inverse = ( (λ x → swap₊ ◎ ε₊ {x}) ,
              (λ x → ε₊ {x}) );
  ⁻¹-cong = neg
  }

+0-IsAbelianGroup : IsAbelianGroup _⟷_ PLUS ZERO NEG
+0-IsAbelianGroup = record {
    isGroup = +0-IsGroup ;
    comm = λ x y → swap₊ {x} {y}
  }

B-IsRing : IsRing _⟷_ PLUS TIMES NEG ZERO ONE
B-IsRing = record {
    +-isAbelianGroup = +0-IsAbelianGroup ;
    *-isMonoid = ⋆1IsMonoid ;
    distrib = ( (λ x y z → dist' {x} {y} {z}) ,
                (λ x y z → dist {y} {z} {x} ))
  }

B-IsCommutativeRing : IsCommutativeRing _⟷_ PLUS TIMES NEG ZERO ONE
B-IsCommutativeRing = record {
    isRing = B-IsRing ;
    *-comm = λ x y → swap⋆ {x} {y}
  }

--

B-CommutativeRing : CommutativeRing _ _
B-CommutativeRing = record {
    Carrier = B ;
    _≈_ = _⟷_ ;
    _+_ = PLUS ;
    _*_ = TIMES ;
    -_ = NEG ;
    0# = ZERO ;
    1# = ONE ;
    isCommutativeRing = B-IsCommutativeRing
  }

--

record IsMeadow
         {a ℓ} {A : Set a} (≈ : Rel A ℓ)
         (+ * : Op₂ A) (- r : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    +*-isCommutativeRing : IsCommutativeRing ≈ + * - 0# 1#
    *-refl-l : ∀ x → ≈ (r (r x)) x
    *-refl-r : ∀ x → ≈ x (r (r x))
    *-ril-l : ∀ x → ≈ (* x (* x (r x))) x
    *-ril-r : ∀ x → ≈ x (* x (* x (r x)))
    r-cong : ∀ x y → ≈ x y → ≈ (r x) (r y)

record Meadow c ℓ : Set (suc (c ⊔ ℓ)) where
  field
    Carrier : Set c
    _≈_ : Rel Carrier ℓ
    _+_ : Op₂ Carrier
    _*_ : Op₂ Carrier
    -_ : Op₁ Carrier
    r  : Op₁ Carrier
    0# : Carrier
    1# : Carrier
    isMeadow : IsMeadow _≈_ _+_ _*_ -_ r 0# 1#

B-/IsMeadow : IsMeadow _⟷_ PLUS TIMES NEG RECIP ZERO ONE
B-/IsMeadow = record {
    +*-isCommutativeRing = B-IsCommutativeRing ;
    *-refl-l = λ x → refe⋆ {x} ;
    *-refl-r = λ x → sym (refe⋆ {x}) ;
    *-ril-l = λ x → sym (rili⋆ {x}) ;
    *-ril-r = λ x → rili⋆ {x} ;
    r-cong = λ x y → recip {x} {y}
  }

B-/Meadow : Meadow _ _
B-/Meadow = record {
    Carrier = B ;
    _≈_ = _⟷_ ;
    _+_ = PLUS ;
    _*_ = TIMES ;
    -_ = NEG ;
    r  = RECIP ;
    0# = ZERO ;
    1# = ONE ;
    isMeadow = B-/IsMeadow
  }

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
open import Nat
open import Prelude

module core where
  -- types
  data τ̇ : Set where
    num  : τ̇
    ⦇-⦈ : τ̇
    _==>_ : τ̇ → τ̇ → τ̇

  -- expressions, prefixed with a · to distinguish name clashes with agda
  -- built-ins
  data ė : Set where
    _·:_  : ė → τ̇ → ė
    X     : Nat → ė
    ·λ    : Nat → ė → ė
    N     : Nat → ė
    _·+_  : ė → ė → ė
    ⦇-⦈  : ė
    ⦇⌜_⌟⦈ : ė → ė
    _∘_   : ė → ė → ė

  ---- contexts and some operations on them

  -- variables are named with naturals in ė. therefore we represent
  -- contexts as functions from names for variables (nats) to possible
  -- bindings.
  ·ctx : Set
  ·ctx = Nat → Maybe τ̇

  -- convenient shorthand for the (unique up to fun. ext.) empty context
  ∅ : ·ctx
  ∅ _ = None

  -- add a new binding to the context, clobbering anything that might have
  -- been there before.
  _,,_ : ·ctx → (Nat × τ̇) → ·ctx
  (Γ ,, (x , t)) y with natEQ x y
  (Γ ,, (x , t)) .x | Inl refl = Some t
  (Γ ,, (x , t)) y  | Inr neq  = Γ y

  -- membership, or presence, in a context
  _∈_ : (p : Nat × τ̇) → (Γ : ·ctx) → Set
  (x , t) ∈ Γ = (Γ x) == Some t

  -- apartness for contexts, so that we can follow barendregt's convention
  _#_ : (n : Nat) → (Γ : ·ctx) → Set
  x # Γ = (Γ x) == None

  -- without: remove a variable from a context
  _/_ : ·ctx → Nat → ·ctx
  (Γ / x) y with natEQ x y
  (Γ / x) .x | Inl refl = None
  (Γ / x) y  | Inr neq  = Γ y

  -- the type consistency judgement
  data _~_ : (t1 : τ̇) → (t2 : τ̇) → Set where
    TCRefl : {t : τ̇} → t ~ t
    TCHole1 : {t : τ̇} → t ~ ⦇-⦈
    TCHole2 : {t : τ̇} → ⦇-⦈ ~ t
    TCArr : {t1 t2 t1' t2' : τ̇} →
               t1 ~ t1' →
               t2 ~ t2' →
               (t1 ==> t2) ~ (t1' ==> t2')

  -- type inconsistency. a judgmental version and associated proofs are in
  -- judgemental-inconsistency.agda. each definition implies the other, but
  -- the two are isomorphic only if you treat proofs of inconsistency at
  -- arrow types as being proof-irrelevant---that is, if you don't
  -- distinguish between cases where the inconsistency between a pair of
  -- function types stems from the domain, range, or both. we use the form
  -- below throughout the rest of the development because we do not care to
  -- make that distinction.
  _~̸_ : τ̇ → τ̇ → Set
  t1 ~̸ t2 = (t1 ~ t2) → ⊥

  --- matching for arrows
  data _▸arr_ : τ̇ → τ̇ → Set where
    MAHole : ⦇-⦈ ▸arr (⦇-⦈ ==> ⦇-⦈)
    MAArr  : {t1 t2 : τ̇} → (t1 ==> t2) ▸arr (t1 ==> t2)

  -- matching produces unique answers
  matcharrunicity : ∀{ t t2 t3 } →
                 t ▸arr t2 →
                 t ▸arr t3 →
                 t2 == t3
  matcharrunicity MAHole MAHole = refl
  matcharrunicity MAArr MAArr = refl

  -- if a type matches, then it's consistent with the least restrictive
  -- function type
  matchconsist : ∀{t t'} →
                 t ▸arr t' →
                 t ~ (⦇-⦈ ==> ⦇-⦈)
  matchconsist MAHole = TCHole2
  matchconsist MAArr = TCArr TCHole1 TCHole1

  matchnotnum : ∀{t1 t2} → num ▸arr (t1 ==> t2) → ⊥
  matchnotnum ()

  -- bidirectional type checking judgements for ė
  mutual
    -- synthesis
    data _⊢_=>_ : (Γ : ·ctx) → (e : ė) → (t : τ̇) → Set where
      SAsc    : {Γ : ·ctx} {e : ė} {t : τ̇} →
                 Γ ⊢ e <= t →
                 Γ ⊢ (e ·: t) => t
      SVar    : {Γ : ·ctx} {t : τ̇} {n : Nat} →
                 (n , t) ∈ Γ →
                 Γ ⊢ X n => t
      SAp     : {Γ : ·ctx} {e1 e2 : ė} {t t' t2 : τ̇} →
                 Γ ⊢ e1 => t →
                 t ▸arr (t2 ==> t') →
                 Γ ⊢ e2 <= t2 →
                 Γ ⊢ (e1 ∘ e2) => t'
      SNum    :  {Γ : ·ctx} {n : Nat} →
                 Γ ⊢ N n => num
      SPlus   : {Γ : ·ctx} {e1 e2 : ė}  →
                 Γ ⊢ e1 <= num →
                 Γ ⊢ e2 <= num →
                 Γ ⊢ (e1 ·+ e2) => num
      SEHole  : {Γ : ·ctx} → Γ ⊢ ⦇-⦈ => ⦇-⦈
      SNEHole : {Γ : ·ctx} {e : ė} {t : τ̇} →
                 Γ ⊢ e => t →
                 Γ ⊢ ⦇⌜ e ⌟⦈ => ⦇-⦈

    -- analysis
    data _⊢_<=_ : (Γ : ·ctx) → (e : ė) → (t : τ̇) → Set where
      ASubsume : {Γ : ·ctx} {e : ė} {t t' : τ̇} →
                 Γ ⊢ e => t' →
                 t ~ t' →
                 Γ ⊢ e <= t
      ALam : {Γ : ·ctx} {e : ė} {t t1 t2 : τ̇} {x : Nat} →
                 x # Γ →
                 t ▸arr (t1 ==> t2) →
                 (Γ ,, (x , t1)) ⊢ e <= t2 →
                 Γ ⊢ (·λ x e) <= t

  ----- some theorems about the rules and judgement presented so far.

  -- a variable is apart from any context from which it is removed
  aar : (Γ : ·ctx) (x : Nat) → x # (Γ / x)
  aar Γ x with natEQ x x
  aar Γ x | Inl refl = refl
  aar Γ x | Inr x≠x  = abort (x≠x refl)

  -- contexts give at most one binding for each variable
  ctxunicity : {Γ : ·ctx} {n : Nat} {t t' : τ̇} →
               (n , t) ∈ Γ →
               (n , t') ∈ Γ →
               t == t'
  ctxunicity {n = n} p q with natEQ n n
  ctxunicity p q | Inl refl = someinj (! p · q)
  ctxunicity _ _ | Inr x≠x = abort (x≠x refl)

  -- type consistency is symmetric
  ~sym : {t1 t2 : τ̇} → t1 ~ t2 → t2 ~ t1
  ~sym TCRefl = TCRefl
  ~sym TCHole1 = TCHole2
  ~sym TCHole2 = TCHole1
  ~sym (TCArr p1 p2) = TCArr (~sym p1) (~sym p2)

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

  -- if the domain or codomain of a pair of arrows isn't consistent, the
  -- whole arrow isn't consistent.
  lemarr1 : {t1 t2 t3 t4 : τ̇} → (t1 ~ t3 → ⊥) → (t1 ==> t2) ~ (t3 ==> t4)  → ⊥
  lemarr1 v TCRefl = v TCRefl
  lemarr1 v (TCArr p _) = v p

  lemarr2 : {t1 t2 t3 t4 : τ̇} → (t2 ~ t4 → ⊥) → (t1 ==> t2) ~ (t3 ==> t4) →  ⊥
  lemarr2 v TCRefl = v TCRefl
  lemarr2 v (TCArr _ p) = v p

  --  every pair of types is either consistent or not consistent
  ~dec : (t1 t2 : τ̇) → ((t1 ~ t2) + (t1 ~̸ t2))
    -- this takes care of all hole cases, so we don't consider them below
  ~dec _ ⦇-⦈ = Inl TCHole1
  ~dec ⦇-⦈ _ = Inl TCHole2
    -- num cases
  ~dec num num = Inl TCRefl
  ~dec num (t2 ==> t3) = Inr (λ ())
    -- arrow cases
  ~dec (t1 ==> t2) num = Inr (λ ())
  ~dec (t1 ==> t2) (t3 ==> t4) with ~dec t1 t3 | ~dec t2 t4
  ... | Inl x | Inl y = Inl (TCArr x y)
  ... | Inl _ | Inr y = Inr (lemarr2 y)
  ... | Inr x | _     = Inr (lemarr1 x)

  -- theorem: no pair of types is both consistent and not consistent. this
  -- is immediate from our encoding of the ~̸ judgement in the formalism
  -- here; in the exact mathematics presented in the paper, this would
  -- require induction to relate the two judgements.
  ~apart : {t1 t2 : τ̇} → (t1 ~̸ t2) → (t1 ~ t2) → ⊥
  ~apart v p = v p

  -- synthesis only produces equal types. note that there is no need for an
  -- analagous theorem for analytic positions because we think of
  -- the type as an input
  synthunicity : {Γ : ·ctx} {e : ė} {t t' : τ̇} →
                  (Γ ⊢ e => t)
                → (Γ ⊢ e => t')
                → t == t'
  synthunicity (SAsc _) (SAsc _) = refl
  synthunicity {Γ = G} (SVar in1) (SVar in2) = ctxunicity {Γ = G} in1 in2
  synthunicity (SAp D1 MAHole b) (SAp D2 MAHole y) = refl
  synthunicity (SAp D1 MAHole b) (SAp D2 MAArr y) with synthunicity D1 D2
  ... | ()
  synthunicity (SAp D1 MAArr b) (SAp D2 MAHole y) with synthunicity D1 D2
  ... | ()
  synthunicity (SAp D1 MAArr b) (SAp D2 MAArr y) with synthunicity D1 D2
  ... | refl = refl
  synthunicity SNum SNum = refl
  synthunicity (SPlus _ _ ) (SPlus _ _ ) = refl
  synthunicity SEHole SEHole = refl
  synthunicity (SNEHole _) (SNEHole _) = refl

  ----- the zippered form of the forms above and the rules for actions on them

  -- those types without holes anywhere
  tcomplete : τ̇ → Set
  tcomplete num         = ⊤
  tcomplete ⦇-⦈        = ⊥
  tcomplete (t1 ==> t2) = (tcomplete t1) × (tcomplete t2)

  -- similarly to the complete types, the complete expressions
  ecomplete : ė → Set
  ecomplete (e1 ·: t)  = ecomplete e1 × tcomplete t
  ecomplete (X _)      = ⊤
  ecomplete (·λ _ e1)  = ecomplete e1
  ecomplete (N x)      = ⊤
  ecomplete (e1 ·+ e2) = ecomplete e1 × ecomplete e2
  ecomplete ⦇-⦈       = ⊥
  ecomplete ⦇⌜ e1 ⌟⦈   = ⊥
  ecomplete (e1 ∘ e2)  = ecomplete e1 × ecomplete e2

  -- zippered form of types
  data τ̂ : Set where
    ▹_◃  : τ̇ → τ̂
    _==>₁_ : τ̂ → τ̇ → τ̂
    _==>₂_ : τ̇ → τ̂ → τ̂

  -- zippered form of expressions
  data ê : Set where
    ▹_◃   : ė → ê
    _·:₁_ : ê → τ̇ → ê
    _·:₂_ : ė → τ̂ → ê
    ·λ    : Nat → ê → ê
    _∘₁_  : ê → ė → ê
    _∘₂_  : ė → ê → ê
    _·+₁_ : ê → ė → ê
    _·+₂_ : ė → ê → ê
    ⦇⌜_⌟⦈ : ê → ê

  -- erasure of cursor for types and expressions, judgementally. see
  -- jugemental-erase.agda for an argument that this defines an isomorphic
  -- object to the direct metafunction provided in the text of the paper
  data erase-t : τ̂ → τ̇ → Set where
    ETTop  : ∀{t} → erase-t (▹ t ◃) t
    ETArrL : ∀{t1 t1' t2} → erase-t t1 t1' → erase-t (t1 ==>₁ t2) (t1' ==> t2)
    ETArrR : ∀{t1 t2 t2'} → erase-t t2 t2' → erase-t (t1 ==>₂ t2) (t1 ==> t2')

  data erase-e : ê → ė → Set where
    EETop   : ∀{x}         → erase-e (▹ x ◃) x
    EEAscL  : ∀{e e' t}    → erase-e e e'   → erase-e (e ·:₁ t) (e' ·: t)
    EEAscR  : ∀{e t t'}    → erase-t t t'   → erase-e (e ·:₂ t) (e ·: t')
    EELam   : ∀{x e e'}    → erase-e e e'   → erase-e (·λ x e) (·λ x e')
    EEApL   : ∀{e1 e1' e2} → erase-e e1 e1' → erase-e (e1 ∘₁ e2) (e1' ∘ e2)
    EEApR   : ∀{e1 e2 e2'} → erase-e e2 e2' → erase-e (e1 ∘₂ e2) (e1 ∘ e2')
    EEPlusL : ∀{e1 e1' e2} → erase-e e1 e1' → erase-e (e1 ·+₁ e2) (e1' ·+ e2)
    EEPlusR : ∀{e1 e2 e2'} → erase-e e2 e2' → erase-e (e1 ·+₂ e2) (e1 ·+ e2')
    EENEHole : ∀{e e'}     → erase-e e e'   → erase-e ⦇⌜ e ⌟⦈  ⦇⌜ e' ⌟⦈

  -- the three grammars that define actions
  data direction : Set where
    child : Nat → direction
    parent : direction

  data shape : Set where
    arrow : shape
    num   : shape
    asc   : shape
    var   : Nat → shape
    lam   : Nat → shape
    ap    : shape
    numlit : Nat → shape
    plus  : shape
    nehole : shape

  data action : Set where
    move : direction → action
    construct : shape → action
    del : action
    finish : action

  -- type actions
  data _+_+>_ : (t : τ̂) → (α : action) → (t' : τ̂) → Set where
    TMArrChild1 : {t1 t2 : τ̇} →
               ▹ t1 ==> t2 ◃ + move (child 1) +> (▹ t1 ◃ ==>₁ t2)
    TMArrChild2 : {t1 t2 : τ̇} →
               ▹ t1 ==> t2 ◃ + move (child 2) +> (t1 ==>₂ ▹ t2 ◃)
    TMArrParent1 : {t1 t2 : τ̇} →
               (▹ t1 ◃ ==>₁ t2) + move parent +> ▹ t1 ==> t2 ◃
    TMArrParent2 : {t1 t2 : τ̇} →
               (t1 ==>₂ ▹ t2 ◃) + move parent +> ▹ t1 ==> t2 ◃
    TMDel     : {t : τ̇} →
                (▹ t ◃) + del +> (▹ ⦇-⦈ ◃)
    TMConArrow  : {t : τ̇} →
                (▹ t ◃) + construct arrow +> (t ==>₂ ▹ ⦇-⦈ ◃)
    TMConNum  : (▹ ⦇-⦈ ◃) + construct num +> (▹ num ◃)
    TMArrZip1 : {t1 t1' : τ̂} {t2 : τ̇} {α : action} →
                (t1 + α +> t1') →
                ((t1 ==>₁ t2) + α +> (t1' ==>₁ t2))
    TMArrZip2 : {t2 t2' : τ̂} {t1 : τ̇} {α : action} →
                (t2 + α +> t2') →
                ((t1 ==>₂ t2) + α +> (t1 ==>₂ t2'))

  -- expression movement
  data _+_+>e_ : (e : ê) → (α : action) → (e' : ê) → Set where
    -- rules for ascriptions
    EMAscChild1 : {e : ė} {t : τ̇} →
              (▹ e ·: t ◃) + move (child 1) +>e (▹ e ◃ ·:₁ t)
    EMAscChild2 : {e : ė} {t : τ̇} →
              (▹ e ·: t ◃) + move (child 2) +>e (e  ·:₂ ▹ t ◃)
    EMAscParent1 : {e : ė} {t : τ̇} →
              (▹ e ◃ ·:₁ t) + move parent +>e (▹ e ·: t ◃)
    EMAscParent2 : {e : ė} {t : τ̇} →
              (e ·:₂ ▹ t ◃) + move parent +>e (▹ e ·: t ◃)
    -- rules for lambdas
    EMLamChild1 : {e : ė} {x : Nat} →
              ▹ (·λ x e) ◃ + move (child 1) +>e ·λ x (▹ e ◃)
    EMLamParent : {e : ė} {x : Nat} →
               ·λ x (▹ e ◃) + move parent +>e ▹ (·λ x e) ◃
    -- rules for 2-ary constructors
    EMPlusChild1 : {e1 e2 : ė} →
               (▹ e1 ·+ e2 ◃) + move (child 1) +>e (▹ e1 ◃ ·+₁ e2)
    EMPlusChild2 : {e1 e2 : ė} →
               (▹ e1 ·+ e2 ◃) + move (child 2) +>e (e1 ·+₂ ▹ e2 ◃)
    EMPlusParent1 : {e1 e2 : ė} →
               (▹ e1 ◃ ·+₁ e2) + move parent +>e (▹ e1 ·+ e2 ◃)
    EMPlusParent2 : {e1 e2 : ė} →
               (e1 ·+₂ ▹ e2 ◃) + move parent +>e (▹ e1 ·+ e2 ◃)

    EMApChild1 : {e1 e2 : ė} →
               (▹ e1 ∘ e2 ◃) + move (child 1)+>e (▹ e1 ◃ ∘₁ e2)
    EMApChild2 : {e1 e2 : ė} →
               (▹ e1 ∘ e2 ◃) + move (child 2) +>e (e1 ∘₂ ▹ e2 ◃)
    EMApParent1 : {e1 e2 : ė} →
               (▹ e1 ◃ ∘₁ e2) + move parent +>e (▹ e1 ∘ e2 ◃)
    EMApParent2 : {e1 e2 : ė} →
               (e1 ∘₂ ▹ e2 ◃) + move parent +>e (▹ e1 ∘ e2 ◃)

    -- rules for non-empty holes
    EMNEHoleChild1 : {e : ė} →
               (▹ ⦇⌜ e ⌟⦈ ◃) + move (child 1) +>e ⦇⌜ ▹ e ◃ ⌟⦈
    EMNEHoleParent : {e : ė} →
                ⦇⌜ ▹ e ◃ ⌟⦈ + move parent +>e (▹ ⦇⌜ e ⌟⦈ ◃)

  mutual
  -- synthetic action expressions
    data _⊢_=>_~_~>_=>_ : (Γ : ·ctx) → (e1 : ê) → (t1 : τ̇)
                        → (α : action) → (e2 : ê) → (t2 : τ̇) → Set where
      SAMove : {δ : direction} {e e' : ê} {Γ : ·ctx} {t : τ̇} →
                (e + move δ +>e e') →
                Γ ⊢ e => t ~ move δ ~> e' => t
      SADel : {Γ : ·ctx} {e : ė} {t : τ̇} →
                Γ ⊢ ▹ e ◃ => t ~ del ~> ▹ ⦇-⦈ ◃ => ⦇-⦈
      SAConAsc : {Γ : ·ctx} {e : ė} {t : τ̇} →
                Γ ⊢ ▹ e ◃ => t ~ construct asc ~> (e ·:₂ ▹ t ◃ ) => t
      SAConVar : {Γ : ·ctx} {x : Nat} {t : τ̇} →
                (p : (x , t) ∈ Γ) →
                Γ ⊢ ▹ ⦇-⦈ ◃ => ⦇-⦈ ~ construct (var x) ~> ▹ X x ◃ => t
      SAConLam : {Γ : ·ctx} {x : Nat} →
               (x # Γ) →
                Γ ⊢ ▹ ⦇-⦈ ◃ => ⦇-⦈ ~ construct (lam x) ~>
                   ((·λ x ⦇-⦈) ·:₂ (▹ ⦇-⦈ ◃ ==>₁ ⦇-⦈)) => (⦇-⦈ ==> ⦇-⦈)
      SAConApArr : {Γ : ·ctx} {t t1 t2 : τ̇} {e : ė} →
                t ▸arr (t1 ==> t2) →
                Γ ⊢ ▹ e ◃ => t ~ construct ap ~>  e ∘₂ ▹ ⦇-⦈ ◃ => t2
      SAConApOtw : {Γ : ·ctx} {t : τ̇} {e : ė} →
                (t ~̸ (⦇-⦈ ==> ⦇-⦈)) →
                Γ ⊢ ▹ e ◃ => t ~ construct ap ~> ⦇⌜ e ⌟⦈ ∘₂ ▹ ⦇-⦈ ◃ => ⦇-⦈
      SAConNumlit : {Γ : ·ctx} {n : Nat} →
                Γ ⊢ ▹ ⦇-⦈ ◃ => ⦇-⦈ ~ construct (numlit n) ~> ▹ N n ◃ => num
      SAConPlus1 : {Γ : ·ctx} {e : ė} {t : τ̇} →
                (t ~ num) →
                Γ ⊢ ▹ e ◃ => t ~ construct plus ~> e ·+₂ ▹ ⦇-⦈ ◃  => num
      SAConPlus2 : {Γ : ·ctx} {e : ė} {t : τ̇} →
                (t ~̸ num) →
                Γ ⊢ ▹ e ◃ => t ~ construct plus ~> ⦇⌜ e ⌟⦈ ·+₂ ▹ ⦇-⦈ ◃  => num
      SAConNEHole : {Γ : ·ctx} {e : ė} {t : τ̇} →
                  Γ ⊢ ▹ e ◃ => t ~ construct nehole ~> ⦇⌜ ▹ e ◃ ⌟⦈ => ⦇-⦈
      SAFinish : {Γ : ·ctx} {e : ė} {t : τ̇} →
                 (Γ ⊢ e => t) →
                 Γ ⊢ ▹ ⦇⌜ e ⌟⦈ ◃ => ⦇-⦈ ~ finish ~> ▹ e ◃ => t
      SAZipAsc1 : {Γ : ·ctx} {e e' : ê} {α : action} {t : τ̇} →
                  (Γ ⊢ e ~ α ~> e' ⇐ t) →
                  Γ ⊢ (e ·:₁ t) => t ~ α ~> (e' ·:₁ t) => t
      SAZipAsc2 : {Γ : ·ctx} {e : ė} {α : action} {t t' : τ̂} {t◆ t'◆ : τ̇} →
                  (t + α +> t') →
                  (erase-t t' t'◆) →
                  (erase-t t t◆) →
                  (Γ ⊢ e <= t'◆) →
                  Γ ⊢ (e ·:₂ t) => t◆ ~ α ~> (e ·:₂ t') => t'◆
      SAZipApArr : {Γ : ·ctx} {t t1 t2 t3 t4 : τ̇} {α : action} {eh eh' : ê} {e eh◆ : ė} →
                 (t ▸arr (t3 ==> t4)) →
                 (erase-e eh eh◆) →
                 (Γ ⊢ (eh◆) => t2) →
                 (Γ ⊢ eh => t2 ~ α ~> eh' => t) →
                 (Γ ⊢ e <= t3) →
                 Γ ⊢ (eh ∘₁ e) => t1 ~ α ~> (eh' ∘₁ e) => t4
      SAZipApAna : {Γ : ·ctx} {t' t2 t : τ̇} {e : ė} {eh eh' : ê} {α : action} →
                 (t' ▸arr (t2 ==> t)) →
                 (Γ ⊢ e => t') →
                 (Γ ⊢ eh ~ α ~> eh' ⇐ t2) →
                 Γ ⊢ (e ∘₂ eh) => t ~ α ~> (e ∘₂ eh') => t
      SAZipPlus1 : {Γ : ·ctx} {e : ė} {eh eh' : ê} {α : action} →
                   (Γ ⊢ eh ~ α ~> eh' ⇐ num) →
                   Γ ⊢ (eh ·+₁ e) => num ~ α ~> (eh' ·+₁ e) => num
      SAZipPlus2 : {Γ : ·ctx} {e : ė} {eh eh' : ê} {α : action} →
                   (Γ ⊢ eh ~ α ~> eh' ⇐ num) →
                   Γ ⊢ (e ·+₂ eh) => num ~ α ~> (e ·+₂ eh') => num
      SAZipHole : {Γ : ·ctx} {e e' : ê} {t t' : τ̇} {α : action} {e◆ : ė} →
                   (erase-e e e◆) →
                   (Γ ⊢ e◆ => t) →
                   (Γ ⊢ e => t ~ α ~> e' => t') →
                   Γ ⊢ ⦇⌜ e ⌟⦈ => ⦇-⦈ ~ α ~>  ⦇⌜ e' ⌟⦈ => ⦇-⦈

    -- analytic action expressions
    data _⊢_~_~>_⇐_ : (Γ : ·ctx) → (e : ê) → (α : action) →
                      (e' : ê) → (t : τ̇) → Set where
      AASubsume : {Γ : ·ctx} {e e' : ê} {t t' t'' : τ̇} {α : action} {e◆ : ė} →
                  (erase-e e e◆) →
                  (Γ ⊢ e◆ => t') →
                  (Γ ⊢ e => t' ~ α ~> e' => t'') →
                  (t ~ t'') →
                  Γ ⊢ e ~ α ~> e' ⇐ t
      AAMove : {e e' : ê} {δ : direction} {Γ : ·ctx} {t : τ̇} →
                  (e + move δ +>e e') →
                  Γ ⊢ e ~ move δ ~> e' ⇐ t
      AADel : {e : ė} {Γ : ·ctx} {t : τ̇} →
                 Γ ⊢ ▹ e ◃ ~ del ~> ▹ ⦇-⦈ ◃ ⇐ t
      AAConAsc : {Γ : ·ctx} {e : ė} {t : τ̇} →
                 Γ ⊢ ▹ e ◃ ~ construct asc ~> (e ·:₂ ▹ t ◃) ⇐ t
      AAConVar : {Γ : ·ctx} {t t' : τ̇} {x : Nat} →
                 (t ~̸ t') →
                 (p : (x , t') ∈ Γ) →
                 Γ ⊢ ▹ ⦇-⦈ ◃ ~ construct (var x) ~> ⦇⌜ ▹ X x ◃ ⌟⦈ ⇐ t
      AAConLam1 : {Γ : ·ctx} {x : Nat} {t t1 t2 : τ̇} →
                  (x # Γ) →
                  (t ▸arr (t1 ==> t2)) →
                  Γ ⊢ ▹ ⦇-⦈ ◃ ~ construct (lam x) ~>
                      ·λ x (▹ ⦇-⦈ ◃) ⇐ t
      AAConLam2 : {Γ : ·ctx} {x : Nat} {t : τ̇} →
                  (x # Γ) →
                  (t ~̸ (⦇-⦈ ==> ⦇-⦈)) →
                  Γ ⊢ ▹ ⦇-⦈ ◃ ~ construct (lam x) ~>
                      ⦇⌜ ·λ x ⦇-⦈ ·:₂ (▹ ⦇-⦈ ◃ ==>₁ ⦇-⦈) ⌟⦈ ⇐ t
      AAConNumlit : {Γ : ·ctx} {t : τ̇} {n : Nat} →
                    (t ~̸ num) →
                    Γ ⊢ ▹ ⦇-⦈ ◃ ~ construct (numlit n) ~> ⦇⌜ ▹ (N n) ◃ ⌟⦈ ⇐ t
      AAFinish : {Γ : ·ctx} {e : ė} {t : τ̇} →
                 (Γ ⊢ e <= t) →
                 Γ ⊢ ▹ ⦇⌜ e ⌟⦈ ◃ ~ finish ~> ▹ e ◃ ⇐ t
      AAZipLam : {Γ : ·ctx} {x : Nat} {t t1 t2 : τ̇} {e e' : ê} {α : action} →
                 x # Γ →
                 (t ▸arr (t1 ==> t2)) →
                 ((Γ ,, (x , t1)) ⊢ e ~ α ~> e' ⇐ t2) →
                 Γ ⊢ (·λ x e) ~ α ~> (·λ x e') ⇐ t


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

module Properties.DecSubtyping where

open import Agda.Builtin.Equality using (_≡_; refl)
open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
open import Luau.FunctionTypes using (src; srcⁿ; tgt)
open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_)
open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
open import Properties.Contradiction using (CONTRADICTION; ¬)
open import Properties.Functions using (_∘_)
open import Properties.Subtyping using (<:-refl; <:-trans; ≮:-trans-<:; <:-trans-≮:; <:-never; <:-unknown; <:-∪-left; <:-∪-right; <:-∪-lub;  ≮:-∪-left; ≮:-∪-right; <:-∩-left; <:-∩-right; <:-∩-glb;  ≮:-∩-left; ≮:-∩-right; dec-language; scalar-<:; <:-everything; <:-function; ≮:-function-left; ≮:-function-right)
open import Properties.TypeNormalization using (FunType; Normal; never; unknown; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:)
open import Properties.FunctionTypes using (fun-¬scalar; ¬fun-scalar; fun-function; src-unknown-≮:; tgt-never-≮:; src-tgtᶠ-<:)
open import Properties.Equality using (_≢_)

-- Honest this terminates, since src and tgt reduce the depth of nested arrows
{-# TERMINATING #-}
dec-subtypingˢⁿ : ∀ {T U} → Scalar T → Normal U → Either (T ≮: U) (T <: U)
dec-subtypingᶠ : ∀ {T U} → FunType T → FunType U → Either (T ≮: U) (T <: U)
dec-subtypingᶠⁿ : ∀ {T U} → FunType T → Normal U → Either (T ≮: U) (T <: U)
dec-subtypingⁿ : ∀ {T U} → Normal T → Normal U → Either (T ≮: U) (T <: U)
dec-subtyping : ∀ T U → Either (T ≮: U) (T <: U)

dec-subtypingˢⁿ T U with dec-language _ (scalar T)
dec-subtypingˢⁿ T U | Left p = Left (witness (scalar T) (scalar T) p)
dec-subtypingˢⁿ T U | Right p = Right (scalar-<: T p)

dec-subtypingᶠ {T = T} _ (U ⇒ V) with dec-subtypingⁿ U (normal (src T)) | dec-subtypingⁿ (normal (tgt T)) V
dec-subtypingᶠ {T = T} _ (U ⇒ V) | Left p | q = Left (≮:-trans-<: (src-unknown-≮: (≮:-trans-<: p (<:-normalize (src T)))) (<:-function <:-refl <:-unknown))
dec-subtypingᶠ {T = T} _ (U ⇒ V) | Right p | Left q = Left (≮:-trans-<: (tgt-never-≮: (<:-trans-≮: (normalize-<: (tgt T)) q)) (<:-trans (<:-function <:-never <:-refl) <:-∪-right))
dec-subtypingᶠ T (U ⇒ V) | Right p | Right q = Right (src-tgtᶠ-<: T (<:-trans p (normalize-<: _)) (<:-trans (<:-normalize _) q))

dec-subtypingᶠ T (U ∩ V) with dec-subtypingᶠ T U | dec-subtypingᶠ T V
dec-subtypingᶠ T (U ∩ V) | Left p | q = Left (≮:-∩-left p)
dec-subtypingᶠ T (U ∩ V) | Right p | Left q = Left (≮:-∩-right q)
dec-subtypingᶠ T (U ∩ V) | Right p | Right q = Right (<:-∩-glb p q)

dec-subtypingᶠⁿ T never = Left (witness function (fun-function T) never)
dec-subtypingᶠⁿ T unknown = Right <:-unknown
dec-subtypingᶠⁿ T (U ⇒ V) = dec-subtypingᶠ T (U ⇒ V)
dec-subtypingᶠⁿ T (U ∩ V) = dec-subtypingᶠ T (U ∩ V)
dec-subtypingᶠⁿ T (U ∪ V) with dec-subtypingᶠⁿ T U
dec-subtypingᶠⁿ T (U ∪ V) | Left (witness t p q) = Left (witness t p (q , ¬fun-scalar V T p))
dec-subtypingᶠⁿ T (U ∪ V) | Right p = Right (<:-trans p <:-∪-left)

dec-subtypingⁿ never U = Right <:-never
dec-subtypingⁿ unknown unknown = Right <:-refl
dec-subtypingⁿ unknown U with dec-subtypingᶠⁿ (never ⇒ unknown) U
dec-subtypingⁿ unknown U | Left p = Left (<:-trans-≮: <:-unknown p)
dec-subtypingⁿ unknown U | Right p₁ with dec-subtypingˢⁿ number U
dec-subtypingⁿ unknown U | Right p₁ | Left p = Left (<:-trans-≮: <:-unknown p)
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ with dec-subtypingˢⁿ string U
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Left p = Left (<:-trans-≮: <:-unknown p)
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ with dec-subtypingˢⁿ nil U
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Left p = Left (<:-trans-≮: <:-unknown p)
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Right p₄ with dec-subtypingˢⁿ boolean U
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Right p₄ | Left p = Left (<:-trans-≮: <:-unknown p)
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Right p₄ | Right p₅ = Right (<:-trans <:-everything (<:-∪-lub p₁ (<:-∪-lub p₂ (<:-∪-lub p₃ (<:-∪-lub p₄ p₅)))))
dec-subtypingⁿ (S ⇒ T) U = dec-subtypingᶠⁿ (S ⇒ T) U
dec-subtypingⁿ (S ∩ T) U = dec-subtypingᶠⁿ (S ∩ T) U
dec-subtypingⁿ (S ∪ T) U with dec-subtypingⁿ S U | dec-subtypingˢⁿ T U
dec-subtypingⁿ (S ∪ T) U | Left p | q = Left (≮:-∪-left p)
dec-subtypingⁿ (S ∪ T) U | Right p | Left q = Left (≮:-∪-right q)
dec-subtypingⁿ (S ∪ T) U | Right p | Right q = Right (<:-∪-lub p q)

dec-subtyping T U with dec-subtypingⁿ (normal T) (normal U)
dec-subtyping T U | Left p = Left (<:-trans-≮: (normalize-<: T) (≮:-trans-<: p (<:-normalize U)))
dec-subtyping T U | Right p = Right (<:-trans (<:-normalize T) (<:-trans p (normalize-<: U)))

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: TheGreatSageEqualToHeaven/luau

max_forks_repo_name: TheGreatSageEqualToHeaven/luau


text:
record category { ℓ₀ ℓ₁ } { k : Set ℓ₀ } (_⇒_ : k → k → Set ℓ₁) : Set (lsuc lzero ⊔ ℓ₀ ⊔ ℓ₁)
record groupoid { ℓ₀ ℓ₁ } { k : Set ℓ₀ } (_≈_ : k → k → Set ℓ₁) : Set (lsuc lzero ⊔ ℓ₀ ⊔ ℓ₁)
record groupoid { ℓ₀ ℓ₁ } { k } _≈_
  where
  coinductive
  field
    ⦃ cat ⦄ : category _≈_
  field
    symmetry : ∀ { x y } → x ≈ y → y ≈ x
record category { ℓ₀ ℓ₁ } { k } _⇒_
  where
  coinductive
  field
    id  : ∀ { a } → a ⇒ a
    _∘_ : ∀ { a b c } → b ⇒ c → a ⇒ b → a ⇒ c
  field
    _≈_ : { a b : k } → (f g : a ⇒ b) → Set
    ⦃ hom ⦄ : { a b : k } → groupoid { k = a ⇒ b } _≈_
  field
    lunit : ∀ { a b }     { x : a ⇒ b }                             → (id ∘ x) ≈ x
    runit : ∀ { a b }     { x : a ⇒ b }                             → (x ∘ id) ≈ x
    assoc : ∀ { a b c d } { x : c ⇒ d } { y : b ⇒ c } { z : a ⇒ b } → (x ∘ (y ∘ z)) ≈ ((x ∘ y) ∘ z)
open category ⦃ ... ⦄
open groupoid ⦃ ... ⦄


text:
module Data.List.Membership.Propositional.Instances where

open import Data.List using (List; _∷_)
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.List.Membership.Propositional using (_∈_)

open import Relation.Binary.PropositionalEquality using (refl)

open import Level using (Level)

private
  variable
    a : Level
    A : Set a
    x y : A
    xs : List A

instance
  ⦃here⦄ : x ∈ x ∷ xs
  ⦃here⦄ = here refl

  ⦃there⦄ : ⦃ x ∈ xs ⦄ → x ∈ y ∷ xs
  ⦃there⦄ ⦃ x∈xs ⦄ = there x∈xs

max_stars_repo_name: johnyob/agda-union

max_issues_repo_name: johnyob/agda-union

max_forks_repo_name: johnyob/agda-union