text:
module bools where

open import lib

----------------------------------------------------------------------
-- these problems are about the nand operator, also known as the Scheffer stroke
----------------------------------------------------------------------
nand-not : ∀ (b : 𝔹) → ~ b ≡ b nand b
nand-not tt = refl
nand-not ff = refl

nand-or : ∀ (b1 b2 : 𝔹) → b1 || b2 ≡ (b1 nand b1) nand (b2 nand b2)
nand-or tt tt = refl
nand-or tt ff = refl
nand-or ff tt = refl
nand-or ff ff = refl

nand-and : ∀ (b1 b2 : 𝔹) → b1 && b2 ≡ (b1 nand b2) nand (b1 nand b2)
nand-and tt tt = refl
nand-and tt ff = refl
nand-and ff tt = refl
nand-and ff ff = refl

nand-imp : ∀ (b1 b2 : 𝔹) → b1 imp b2 ≡ b1 nand (b2 nand b2)
nand-imp tt tt = refl
nand-imp tt ff = refl
nand-imp ff tt = refl
nand-imp ff ff = refl

ite-not : ∀(A : Set)(x : 𝔹)(y : A)(z : A) → if x then y else z ≡ if ~ x then z else y
ite-not A tt y z = refl
ite-not A ff y z = refl

&&-distrib : ∀ x y z → x && (y || z) ≡ (x && y) || (x && z)
&&-distrib tt tt tt = refl
&&-distrib tt tt ff = refl
&&-distrib tt ff tt = refl
&&-distrib tt ff ff = refl
&&-distrib ff tt tt = refl
&&-distrib ff tt ff = refl
&&-distrib ff ff tt = refl
&&-distrib ff ff ff = refl

combK : ∀ x y → x imp (y imp x) ≡ tt
combK tt tt = refl
combK tt ff = refl
combK ff tt = refl
combK ff ff = refl

combS : ∀ x y z → (x imp (y imp z)) ≡ tt → (x imp y) ≡ tt → x ≡ tt → z ≡ tt
combS tt tt tt x₁ x₂ x₃ = refl


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

open import HoTT
open import cohomology.ChainComplex
open import cohomology.Theory
open import groups.KernelImage
open import cw.CW

module cw.cohomology.ReconstructedCochainComplex {i : ULevel} (OT : OrdinaryTheory i) where

  open OrdinaryTheory OT
  import cw.cohomology.TipAndAugment OT as TAA
  import cw.cohomology.TipCoboundary OT as TC
  import cw.cohomology.HigherCoboundary OT as HC
  open import cw.cohomology.WedgeOfCells OT

  cochain-template : ∀ {n} (⊙skel : ⊙Skeleton {i} n) {m}
    → Dec (m ≤ n) → AbGroup i
  cochain-template ⊙skel (inr _) = Lift-abgroup {j = i} Unit-abgroup
  cochain-template ⊙skel {m = 0} (inl 0≤n) = TAA.C2×CX₀-abgroup (⊙cw-take 0≤n ⊙skel) 0
  cochain-template ⊙skel {m = S m} (inl Sm≤n) = CXₙ/Xₙ₋₁-abgroup (⊙cw-take Sm≤n ⊙skel) (ℕ-to-ℤ (S m))

  cochain-is-abelian-template : ∀ {n} (⊙skel : ⊙Skeleton {i} n) {m} m≤n?
    → is-abelian (AbGroup.grp (cochain-template ⊙skel {m} m≤n?))
  cochain-is-abelian-template ⊙skel m≤n? = AbGroup.comm (cochain-template ⊙skel m≤n?)

  abstract
    private
      coboundary-first-template : ∀ {n} (⊙skel : ⊙Skeleton {i} n)
        → (0≤n : 0 ≤ n) (1≤n : 1 ≤ n)
        → ⊙cw-init (⊙cw-take 1≤n ⊙skel) == ⊙cw-take (≤-trans lteS 1≤n) ⊙skel
        → ⊙cw-take (≤-trans lteS 1≤n) ⊙skel == ⊙cw-take 0≤n ⊙skel
        → TAA.C2×CX₀ (⊙cw-take 0≤n ⊙skel) 0 →ᴳ CXₙ/Xₙ₋₁ (⊙cw-take 1≤n ⊙skel) 1
      coboundary-first-template ⊙skel 0≤n 1≤n path₀ path₁ =
           TC.cw-co∂-head (⊙cw-take 1≤n ⊙skel)
        ∘ᴳ transport!ᴳ (λ ⊙skel → TAA.C2×CX₀ ⊙skel 0) (path₀ ∙ path₁)

      coboundary-higher-template : ∀ {n} (⊙skel : ⊙Skeleton {i} n)
        → {m : ℕ} (Sm≤n : S m ≤ n) (SSm≤n : S (S m) ≤ n)
        → ⊙cw-init (⊙cw-take SSm≤n ⊙skel) == ⊙cw-take (≤-trans lteS SSm≤n) ⊙skel
        → ⊙cw-take (≤-trans lteS SSm≤n) ⊙skel == ⊙cw-take Sm≤n ⊙skel
        →  CXₙ/Xₙ₋₁ (⊙cw-take Sm≤n ⊙skel)  (ℕ-to-ℤ (S m))
        →ᴳ CXₙ/Xₙ₋₁ (⊙cw-take SSm≤n ⊙skel) (ℕ-to-ℤ (S (S m)))
      coboundary-higher-template ⊙skel {m} Sm≤n SSm≤n path₀ path₁ =
           HC.cw-co∂-last (⊙cw-take SSm≤n ⊙skel)
        ∘ᴳ transport!ᴳ (λ ⊙skel → CXₙ/Xₙ₋₁ ⊙skel (ℕ-to-ℤ (S m))) (path₀ ∙ path₁)

  coboundary-template : ∀ {n} (⊙skel : ⊙Skeleton {i} n)
    → {m : ℕ} (m≤n? : Dec (m ≤ n)) (Sm≤n? : Dec (S m ≤ n))
    →  AbGroup.grp (cochain-template ⊙skel m≤n?)
    →ᴳ AbGroup.grp (cochain-template ⊙skel Sm≤n?)
  coboundary-template ⊙skel _ (inr _) = cst-hom
  coboundary-template ⊙skel (inr m≰n) (inl Sm≤n) = ⊥-rec $ m≰n (≤-trans lteS Sm≤n)
  coboundary-template ⊙skel {m = 0} (inl 0≤n) (inl 1≤n) =
    coboundary-first-template ⊙skel 0≤n 1≤n (⊙cw-init-take 1≤n ⊙skel)
      (ap (λ 0≤n → ⊙cw-take 0≤n ⊙skel) (≤-has-all-paths (≤-trans lteS 1≤n) 0≤n))
  coboundary-template ⊙skel {m = S m} (inl Sm≤n) (inl SSm≤n) =
    coboundary-higher-template ⊙skel Sm≤n SSm≤n (⊙cw-init-take SSm≤n ⊙skel)
      (ap (λ Sm≤n → ⊙cw-take Sm≤n ⊙skel) (≤-has-all-paths (≤-trans lteS SSm≤n) Sm≤n))

  cochain-complex : ∀ {n} → ⊙Skeleton {i} n → CochainComplex i
  cochain-complex {n} ⊙skel = record {M} where
    module M where
      head : AbGroup i
      head = C-abgroup 0 (⊙Lift ⊙Bool)

      cochain : ℕ → AbGroup i
      cochain m = cochain-template ⊙skel (≤-dec m n)

      augment : C 0 (⊙Lift ⊙Bool) →ᴳ AbGroup.grp (cochain 0)
      augment = TAA.cw-coε (⊙cw-take (O≤ n) ⊙skel)

      coboundary : ∀ m → (AbGroup.grp (cochain m) →ᴳ AbGroup.grp (cochain (S m)))
      coboundary m = coboundary-template ⊙skel (≤-dec m n) (≤-dec (S m) n)

  {- Properties of coboundaries -}

  {- lemmas of paths -}
  private
    abstract
      path-lemma₀ : ∀ {n} (⊙skel : ⊙Skeleton {i} (S n)) {m} (m<n : m < n) (Sm<n : S m < n)
        →  ap (λ m≤Sn → ⊙cw-take m≤Sn ⊙skel) (≤-has-all-paths (≤-trans lteS (lteSR (inr Sm<n))) (lteSR (inr m<n)))
        == ap (λ m≤n → ⊙cw-take m≤n (⊙cw-init ⊙skel)) (≤-has-all-paths (≤-trans lteS (inr Sm<n)) (inr m<n))
      path-lemma₀ ⊙skel m<n Sm<n =
        ap (λ m≤Sn → ⊙cw-take m≤Sn ⊙skel) (≤-has-all-paths (≤-trans lteS (lteSR (inr Sm<n))) (lteSR (inr m<n)))
          =⟨ ap (ap (λ m≤Sn → ⊙cw-take m≤Sn ⊙skel)) (contr-has-all-paths (≤-is-prop _ _) _ _) ⟩
        ap (λ m≤Sn → ⊙cw-take m≤Sn ⊙skel) (ap (lteSR ∘ inr) (<-has-all-paths (<-trans ltS Sm<n) m<n))
          =⟨ ∘-ap (λ m≤Sn → ⊙cw-take m≤Sn ⊙skel) (lteSR ∘ inr) _ ⟩
        ap (λ Sm<n → ⊙cw-take (lteSR (inr Sm<n)) ⊙skel) (<-has-all-paths (<-trans ltS Sm<n) m<n)
          =⟨ ap-∘ (λ m≤n → ⊙cw-take m≤n (⊙cw-init ⊙skel)) inr _ ⟩
        ap (λ m≤n → ⊙cw-take m≤n (⊙cw-init ⊙skel)) (ap inr (<-has-all-paths (<-trans ltS Sm<n) m<n))
          =⟨ ap (ap (λ m≤n → ⊙cw-take m≤n (⊙cw-init ⊙skel))) (contr-has-all-paths (≤-is-prop _ _) _ _) ⟩
        ap (λ m≤n → ⊙cw-take m≤n (⊙cw-init ⊙skel)) (≤-has-all-paths (≤-trans lteS (inr Sm<n)) (inr m<n))
          =∎

      -- would be trivial with [≤-has-all-paths] defined with the set detection (issue #2003)
      path-lemma₁ : ∀ {n} (⊙skel : ⊙Skeleton {i} (S (S n)))
        →  ap (λ n≤SSn → ⊙cw-take n≤SSn ⊙skel) (≤-has-all-paths (lteSR lteS) (lteSR lteS))
        == ap (λ n≤Sn → ⊙cw-take n≤Sn (⊙cw-init ⊙skel)) (≤-has-all-paths lteS lteS)
      path-lemma₁ ⊙skel =
        ap (λ n≤SSn → ⊙cw-take n≤SSn ⊙skel) (≤-has-all-paths (lteSR lteS) (lteSR lteS))
          =⟨ ap (ap (λ n≤SSn → ⊙cw-take n≤SSn ⊙skel)) (contr-has-all-paths (≤-is-prop _ _) _ _) ⟩
        idp
          =⟨ ap (ap (λ n≤Sn → ⊙cw-take n≤Sn (⊙cw-init ⊙skel))) (contr-has-all-paths (≤-is-prop _ _) _ _) ⟩
        ap (λ n≤Sn → ⊙cw-take n≤Sn (⊙cw-init ⊙skel)) (≤-has-all-paths lteS lteS)
          =∎

      -- would be trivial with [≤-has-all-paths] defined with the set detection (issue #2003)
      path-lemma₂ : ∀ {n} (⊙skel : ⊙Skeleton {i} (S n))
        → ap (λ n≤Sn → ⊙cw-take n≤Sn ⊙skel) (≤-has-all-paths lteS lteS) == idp
      path-lemma₂ ⊙skel =
        ap (λ n≤Sn → ⊙cw-take n≤Sn ⊙skel) (≤-has-all-paths lteS lteS)
          =⟨ ap (ap (λ n≤Sn → ⊙cw-take n≤Sn ⊙skel)) (contr-has-all-paths (≤-is-prop _ _) _ _) ⟩
        idp
          =∎

  {- properties of coboundary-template -}
  abstract
    {- lemmas of the first coboundary -}
    coboundary-first-template-descend-from-far : ∀ {n} (⊙skel : ⊙Skeleton {i} (S n)) 0<n 1<n
      → coboundary-template {n = S n} ⊙skel {0} (inl (lteSR (inr 0<n))) (inl (lteSR (inr 1<n)))
        == coboundary-template {n = n} (⊙cw-init ⊙skel) (inl (inr 0<n)) (inl (inr 1<n))
    coboundary-first-template-descend-from-far ⊙skel 0<n 1<n =
      ap (coboundary-first-template ⊙skel (lteSR (inr 0<n)) (lteSR (inr 1<n)) (⊙cw-init-take (lteSR (inr 1<n)) ⊙skel))
        (path-lemma₀ ⊙skel 0<n 1<n)

    coboundary-first-template-descend-from-two : ∀ (⊙skel : ⊙Skeleton {i} 2)
      → coboundary-template {n = 2} ⊙skel (inl (lteSR lteS)) (inl lteS)
        == coboundary-template {n = 1} (⊙cw-init ⊙skel) (inl lteS) (inl lteE)
    coboundary-first-template-descend-from-two ⊙skel =
      ap (coboundary-first-template ⊙skel (lteSR lteS) lteS idp) (path-lemma₁ ⊙skel)

    coboundary-first-template-β : ∀ (⊙skel : ⊙Skeleton {i} 1)
      →  coboundary-template {n = 1} ⊙skel (inl lteS) (inl lteE)
      == TC.cw-co∂-head ⊙skel
    coboundary-first-template-β ⊙skel = group-hom= $
        ap (GroupHom.f ∘ coboundary-first-template ⊙skel lteS lteE idp) (path-lemma₂ ⊙skel)

    {- lemmas of higher coboundaries -}
    coboundary-higher-template-descend-from-far : ∀ {n} (⊙skel : ⊙Skeleton {i} (S n)) {m} Sm<n SSm<n
      → coboundary-template {n = S n} ⊙skel {m = S m} (inl (lteSR (inr Sm<n))) (inl (lteSR (inr SSm<n)))
        == coboundary-template {n = n} (⊙cw-init ⊙skel) {m = S m} (inl (inr Sm<n)) (inl (inr SSm<n))
    coboundary-higher-template-descend-from-far ⊙skel {m} Sm<n SSm<n =
      ap (coboundary-higher-template ⊙skel (lteSR (inr Sm<n)) (lteSR (inr SSm<n)) (⊙cw-init-take (lteSR (inr SSm<n)) ⊙skel))
        (path-lemma₀ ⊙skel Sm<n SSm<n)

    coboundary-higher-template-descend-from-one-above : ∀ {n} (⊙skel : ⊙Skeleton {i} (S (S (S n))))
      → coboundary-template {n = S (S (S n))} ⊙skel {m = S n} (inl (lteSR lteS)) (inl lteS)
        == coboundary-template {n = S (S n)} (⊙cw-init ⊙skel) {m = S n} (inl lteS) (inl lteE)
    coboundary-higher-template-descend-from-one-above ⊙skel =
      ap (coboundary-higher-template ⊙skel (lteSR lteS) lteS idp) (path-lemma₁ ⊙skel)

    coboundary-higher-template-β : ∀ {n} (⊙skel : ⊙Skeleton {i} (S (S n)))
      →  coboundary-template {n = S (S n)} ⊙skel {m = S n} (inl lteS) (inl lteE)
      == HC.cw-co∂-last ⊙skel
    coboundary-higher-template-β ⊙skel = group-hom= $
      ap (GroupHom.f ∘ coboundary-higher-template ⊙skel lteS lteE idp) (path-lemma₂ ⊙skel)

ext: agda

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module Cats.Util.Logic.Constructive where

open import Data.Empty public
  using (⊥ ; ⊥-elim)
open import Data.Product public
  using (_,_ ; ∃-syntax ; Σ-syntax)
  renaming (_×_ to _∧_ ; proj₁ to ∧-eliml ; proj₂ to ∧-elimr)
open import Data.Sum public
  using ()
  renaming (_⊎_ to _∨_ ; inj₁ to ∨-introl ; inj₂ to ∨-intror)
open import Data.Unit public
  using (⊤)
  renaming (tt to ⊤-intro)
open import Relation.Nullary public
  using (¬_)

-- De Morgan's constructive rules
module _ {p q} {P : Set p} {Q : Set q} where

  ¬∨¬→¬∧ : ¬ P ∨ ¬ Q → ¬ (P ∧ Q)
  ¬∨¬→¬∧ (∨-introl ¬p) (p , _) = ¬p p
  ¬∨¬→¬∧ (∨-intror ¬q) (_ , q) = ¬q q

  ¬∨→¬∧¬ : ¬ (P ∨ Q) → ¬ P ∧ ¬ Q
  ¬∨→¬∧¬ ¬p∨q = (λ p → ¬p∨q (∨-introl p)) , (λ q → ¬p∨q (∨-intror q))

  ¬∧¬→¬∨ : ¬ P ∧ ¬ Q → ¬ (P ∨ Q)
  ¬∧¬→¬∨ (¬p , _) (∨-introl p) = ¬p p
  ¬∧¬→¬∨ (_ , ¬q) (∨-intror q) = ¬q q

-- Quantifiers and negation
module _ {u p} {U : Set u} {P : U → Set p} where

  ¬∃→∀¬ : ¬ (∃[ u ] (P u)) → ∀ u → ¬ P u
  ¬∃→∀¬ ¬∃ u pu = ¬∃ (u , pu)

  ∀¬→¬∃ : (∀ u → ¬ (P u)) → ¬ (∃[ u ] (P u))
  ∀¬→¬∃ ∀¬ (u , pu) = ∀¬ u pu

  ∃¬→¬∀ : ∃[ u ] (¬ P u) → ¬ (∀ u → P u)
  ∃¬→¬∀ (u , ¬pu) ∀upu = ¬pu (∀upu u)

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Instances.DiffInt where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Int.MoreInts.DiffInt renaming ( _+_ to _+ℤ_ ; _-_ to _-ℤ_)

open import Cubical.Algebra.Group.Base

open import Cubical.HITs.SetQuotients

open GroupStr

ℤGroup : Group₀
fst ℤGroup = ℤ
1g (snd ℤGroup) = [ 0 , 0 ]
_·_ (snd ℤGroup) = _+ℤ_
inv (snd ℤGroup) = -ℤ_
isGroup (snd ℤGroup) = makeIsGroup
                       ℤ-isSet
                       +ℤ-assoc
                       (λ x → zero-identityʳ 0 x)
                       (λ x → zero-identityˡ 0 x)
                       -ℤ-invʳ
                       -ℤ-invˡ

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Groups.Groups
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Numbers.Naturals.Naturals
open import Setoids.Setoids
open import Functions.Definition
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Rings.Homomorphisms.Definition

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Rings.Homomorphisms.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+A_ _*A_ : A → A → A} (R : Ring S _+A_ _*A_) where

open import Groups.Homomorphisms.Lemmas2 (Ring.additiveGroup R)

imageRing : {c d : _} {B : Set c} {T : Setoid {c} {d} B} {_+B_ : B → B → B} {_*B_ : B → B → B} → (f : A → B) → SetoidSurjection S T f → ({x y : A} → Setoid._∼_ T (f (x +A y)) ((f x) +B (f y))) → ({x y : A} → Setoid._∼_ T (f (x *A y)) ((f x) *B (f y))) → ({x y m n : B} → Setoid._∼_ T x m → Setoid._∼_ T y n → Setoid._∼_ T (x +B y) (m +B n)) → ({x y m n : B} → Setoid._∼_ T x m → Setoid._∼_ T y n → Setoid._∼_ T (x *B y) (m *B n)) → Ring T _+B_ _*B_
Ring.additiveGroup (imageRing f surj respects+ respects* +wd *wd) = imageGroup f surj respects+ +wd
Ring.*WellDefined (imageRing f surj respects+ respects* +wd *wd) = *wd
Ring.1R (imageRing f surj respects+ respects* +wd *wd) = f (Ring.1R R)
Ring.groupIsAbelian (imageRing {T = T} f record { surjective = surjective ; wellDefined = wellDefined } respects+ respects* +wd *wd) {a} {b} with surjective {a}
... | x , fx=a with surjective {b}
... | y , fy=b = transitive (+wd (symmetric fx=a) (symmetric fy=b)) (transitive (transitive (symmetric respects+) (transitive (wellDefined (Ring.groupIsAbelian R)) respects+)) (+wd fy=b fx=a))
  where
    open Setoid T
    open Equivalence eq
Ring.*Associative (imageRing {T = T} f record { surjective = surjective ; wellDefined = wellDefined } respects+ respects* +wd *wd) {a} {b} {c} with surjective {a}
... | x , fx=a with surjective {b}
... | y , fy=b with surjective {c}
... | z , fz=c = transitive (*wd (symmetric fx=a) (transitive (*wd (symmetric fy=b) (symmetric fz=c)) (symmetric respects*))) (transitive (transitive (symmetric respects*) (transitive (wellDefined (Ring.*Associative R)) respects*)) (*wd (transitive respects* (*wd fx=a fy=b)) fz=c))
  where
    open Setoid T
    open Equivalence eq
Ring.*Commutative (imageRing {T = T} f record { surjective = surjective ; wellDefined = wellDefined } respects+ respects* +wd *wd) {a} {b} with surjective {a}
... | x , fx=a with surjective {b}
... | y , fy=b = transitive (*wd (symmetric fx=a) (symmetric fy=b)) (transitive (transitive (symmetric respects*) (transitive (wellDefined (Ring.*Commutative R)) respects*)) (*wd fy=b fx=a))
  where
    open Setoid T
    open Equivalence eq
Ring.*DistributesOver+ (imageRing {T = T} f record { surjective = surjective ; wellDefined = wellDefined } respects+ respects* +wd *wd) {a} {b} {c} with surjective {a}
... | x , fx=a with surjective {b}
... | y , fy=b with surjective {c}
... | z , fz=c = transitive (*wd (symmetric fx=a) (+wd (symmetric fy=b) (symmetric fz=c))) (transitive (transitive (transitive (*wd reflexive (symmetric respects+)) (symmetric respects*)) (transitive (transitive (wellDefined (Ring.*DistributesOver+ R)) respects+) (+wd respects* respects*))) (+wd (*wd fx=a fy=b) (*wd fx=a fz=c)))
  where
    open Setoid T
    open Equivalence eq
Ring.identIsIdent (imageRing {T = T} f record { wellDefined = wellDefined ; surjective = surjective } respects+ respects* +wd *wd) {b} with surjective {b}
Ring.identIsIdent (imageRing {T = T} f record { wellDefined = wellDefined ; surjective = surjective } respects+ respects* +wd *wd) {b} | a , fa=b = transitive (transitive (*wd reflexive (symmetric fa=b)) (transitive (symmetric respects*) (wellDefined (Ring.identIsIdent R)))) fa=b
  where
    open Setoid T
    open Equivalence eq

homToImageRing : {c d : _} {B : Set c} {T : Setoid {c} {d} B} {_+B_ : B → B → B} {_*B_ : B → B → B} → (f : A → B) → (surj : SetoidSurjection S T f) → (respects+ : {x y : A} → Setoid._∼_ T (f (x +A y)) ((f x) +B (f y))) → (respects* : {x y : A} → Setoid._∼_ T (f (x *A y)) ((f x) *B (f y))) → (+wd : {x y m n : B} → Setoid._∼_ T x m → Setoid._∼_ T y n → Setoid._∼_ T (x +B y) (m +B n)) → (*wd : {x y m n : B} → Setoid._∼_ T x m → Setoid._∼_ T y n → Setoid._∼_ T (x *B y) (m *B n)) → RingHom R (imageRing f surj respects+ respects* +wd *wd) f
RingHom.preserves1 (homToImageRing {T = T} f surj respects+ respects* +wd *wd) = reflexive
  where
    open Setoid T
    open Equivalence eq
RingHom.ringHom (homToImageRing f surj respects+ respects* +wd *wd) = respects*
RingHom.groupHom (homToImageRing f surj respects+ respects* +wd *wd) = homToImageGroup f surj respects+ +wd


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

module Issue166NotSized where

postulate
  Size : Set
  ↑_   : Size → Size
  ∞    : Size

-- {-# BUILTIN SIZE    Size #-}
-- {-# BUILTIN SIZESUC ↑_   #-}
-- {-# BUILTIN SIZEINF ∞    #-}

data ⊥ : Set where

module M (A : Set) where

  data SizedNat : {i : Size} → Set where
    zero : {i : Size} → SizedNat {↑ i}
    suc  : {i : Size} → SizedNat {i} → SizedNat {↑ i}

open M ⊥

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
------------------------------------------------------------------------
-- Total parser combinators (very short version)
-- Nils Anders Danielsson
------------------------------------------------------------------------

module Short where

open import Category.Monad
open import Coinduction
open import Data.Bool
import Data.BoundedVec.Inefficient as BoundedVec
open import Data.Char
import Data.Colist as Colist
open import Data.List as List
open import Data.Maybe
open import Data.Nat
open import Data.Nat.Show
open import Data.String using (Costring)
open import Function
open import IO hiding (return) renaming (_>>=_ to _>>=IO_)
open import Relation.Nullary.Decidable

open RawMonadPlus List.monadPlus using () renaming (_>>=_ to _>>=′_)

infix  7 _⋆ _+
infixl 6 _>>=_ _>>=app_
infixl 5 _∣_

------------------------------------------------------------------------
-- Helper functions

flatten : {A : Set} → Maybe (List A) → List A
flatten nothing   = []
flatten (just xs) = xs

app : {A B : Set} → Maybe (A → List B) → A → List B
app nothing  x = []
app (just f) x = f x

_>>=app_ : {A B : Set} → List A → Maybe (A → List B) → List B
xs >>=app nothing = []
xs >>=app just f  = xs >>=′ f

------------------------------------------------------------------------
-- Parsers

mutual

  data Parser : (R : Set) → List R → Set₁ where
    return : ∀ {R} (x : R) → Parser R [ x ]
    fail   : ∀ {R} → Parser R []
    token  : Parser Char []
    _∣_    : ∀ {R xs₁ xs₂}
             (p₁ : Parser R  xs₁       )
             (p₂ : Parser R         xs₂) →
                   Parser R (xs₁ ++ xs₂)
    _>>=_  : ∀ {R₁ R₂ xs} {f : Maybe (R₁ → List R₂)}
             (p₁ :            ∞⟨ f  ⟩Parser R₁ (flatten xs)           )
             (p₂ : (x : R₁) → ∞⟨ xs ⟩Parser R₂               (app f x)) →
                                     Parser R₂ (flatten xs >>=app f)

  ∞⟨_⟩Parser : {R₂ : Set} → Maybe R₂ → (R₁ : Set) → List R₁ → Set₁
  ∞⟨ nothing ⟩Parser R₁ xs = ∞ (Parser R₁ xs)
  ∞⟨ just _  ⟩Parser R₁ xs =    Parser R₁ xs

------------------------------------------------------------------------
-- Derived combinators

sat : ∀ {R} → (Char → Maybe R) → Parser R []
sat {R} p = token >>= (ok ∘ p)
  where
  ok-index : Maybe R → List R
  ok-index nothing  = []
  ok-index (just x) = [ x ]

  ok : (x : Maybe R) → Parser R (ok-index x)
  ok nothing  = fail
  ok (just x) = return x

tok : Char → Parser Char []
tok t = sat (λ t′ → if t == t′ then just t′ else nothing)

return⋆ : ∀ {R} (xs : List R) → Parser R xs
return⋆ []       = fail
return⋆ (x ∷ xs) = return x ∣ return⋆ xs

mutual

  _⋆ : ∀ {R} → Parser R [] → Parser (List R) _
  p ⋆ = return [] ∣ p +

  _+ : ∀ {R} → Parser R [] → Parser (List R) _
  p + = p               >>= λ x  → ♯ (
        p ⋆             >>= λ xs →
        return (x ∷ xs)              )

digit = sat (λ t → if in-range t then just (to-number t) else nothing)
  where
  in-range : Char → Bool
  in-range t = ⌊ toNat '0' ≤? toNat  t  ⌋ ∧
               ⌊ toNat  t  ≤? toNat '9' ⌋

  to-number : Char → ℕ
  to-number t = toNat t ∸ toNat '0'

number = digit + >>= return ∘ foldl (λ n d → 10 * n + d) 0

------------------------------------------------------------------------
-- Parser interpreter

delayed? : ∀ {R R′ xs} {m : Maybe R′} → ∞⟨ m ⟩Parser R xs → Maybe R′
delayed? {m = m} _ = m

delayed?′ : ∀ {R₁ R₂ R′ : Set} {m : Maybe R′} {f : R₁ → List R₂} →
            ((x : R₁) → ∞⟨ m ⟩Parser R₂ (f x)) → Maybe R′
delayed?′ {m = m} _ = m

∂-initial : ∀ {R xs} → Parser R xs → Char → List R
∂-initial (return x)  t = []
∂-initial fail        t = []
∂-initial token       t = [ t ]
∂-initial (p₁ ∣ p₂)   t = ∂-initial p₁ t ++ ∂-initial p₂ t
∂-initial (p₁ >>= p₂) t with delayed? p₁ | delayed?′ p₂
... | just f  | nothing =  ∂-initial p₁ t >>=′ f
... | just f  | just xs = (∂-initial p₁ t >>=′ f) ++
                          (xs >>=′ λ x → ∂-initial (p₂ x) t)
... | nothing | nothing = []
... | nothing | just xs =  xs >>=′ λ x → ∂-initial (p₂ x) t

∂ : ∀ {R xs} (p : Parser R xs) (t : Char) → Parser R (∂-initial p t)
∂ (return x)  t = fail
∂ fail        t = fail
∂ token       t = return t
∂ (p₁ ∣ p₂)   t = ∂ p₁ t ∣ ∂ p₂ t
∂ (p₁ >>= p₂) t with delayed? p₁ | delayed?′ p₂
... | just f  | nothing = ∂ p₁ t >>= (λ x → ♭ (p₂ x))
... | just f  | just xs = ∂ p₁ t >>= (λ x →    p₂ x)
                        ∣ return⋆ xs >>= λ x → ∂ (p₂ x) t
... | nothing | nothing = ♯ ∂ (♭ p₁) t >>= (λ x → ♭ (p₂ x))
... | nothing | just xs = ♯ ∂ (♭ p₁) t >>= (λ x →    p₂ x)
                        ∣ return⋆ xs >>= λ x → ∂ (p₂ x) t

parse : ∀ {R xs} → Parser R xs → List Char → List R
parse {xs = xs} p []      = xs
parse           p (t ∷ s) = parse (∂ p t) s

------------------------------------------------------------------------
-- Example

data Expr : Set where
  num   : (n : ℕ)        → Expr
  plus  : (e₁ e₂ : Expr) → Expr
  times : (e₁ e₂ : Expr) → Expr

⟦_⟧ : Expr → ℕ
⟦ num n       ⟧ = n
⟦ plus  e₁ e₂ ⟧ = ⟦ e₁ ⟧ + ⟦ e₂ ⟧
⟦ times e₁ e₂ ⟧ = ⟦ e₁ ⟧ * ⟦ e₂ ⟧

mutual

  term   = factor
         ∣ ♯ term               >>= λ e₁ →
           tok '+'              >>= λ _  →
           factor               >>= λ e₂ →
           return (plus e₁ e₂)

  factor = atom
         ∣ ♯ factor             >>= λ e₁ →
           tok '*'              >>= λ _  →
           atom                 >>= λ e₂ →
           return (times e₁ e₂)

  atom   = (number >>= return ∘ num)
         ∣ tok '('              >>= λ _  →
           ♯ term               >>= λ e  →
           tok ')'              >>= λ _  →
           return e

------------------------------------------------------------------------
-- IO

toList : Costring → List Char
toList = BoundedVec.toList ∘ Colist.take 100000

main = run $
  ♯ getContents >>=IO λ s → ♯
  let s′ = takeWhile (not ∘ _==_ '\n') $ toList s
      es = parse term s′ in
  mapM′ (putStrLn ∘ show ∘ ⟦_⟧) (Colist.fromList es)

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A solver that uses reflection to automatically obtain and solve
-- equations over rings.
------------------------------------------------------------------------

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

module Tactic.RingSolver where

open import Agda.Builtin.Reflection

open import Algebra
open import Data.Fin   as Fin   using (Fin)
open import Data.Vec   as Vec   using (Vec; _∷_; [])
open import Data.List  as List  using (List; _∷_; [])
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing; fromMaybe)
open import Data.Nat            using (ℕ; suc; zero; _<ᵇ_)
open import Data.Nat.Reflection using (toTerm; toFinTerm)
open import Data.Bool           using (Bool; if_then_else_; true; false)
open import Data.Unit           using (⊤)
open import Data.String         using (String)
open import Data.Product        using (_,_)
open import Function
open import Reflection.Argument
open import Reflection.Term
open import Reflection.TypeChecking.MonadSyntax

open import Tactic.RingSolver.NonReflective renaming (solve to solve-fn)
open import Tactic.RingSolver.Core.AlmostCommutativeRing
open import Tactic.RingSolver.Core.NatSet as NatSet
open import Tactic.RingSolver.Core.ReflectionHelp

open AlmostCommutativeRing

------------------------------------------------------------------------
-- Processing
------------------------------------------------------------------------

private
  record RingNames : Set where
    constructor +⇒_*⇒_^⇒_-⇒_
    field
      +′ *′ ^′ -′ : Maybe Name

  checkIsRing : Term → TC Term
  checkIsRing ring = checkType ring (def (quote AlmostCommutativeRing) (2 ⋯⟨∷⟩ []))

  getVariableIDs : Term → Maybe NatSet
  getVariableIDs = go []
    where
    go : NatSet → Term → Maybe NatSet
    go t (con (quote List._∷_) (_ ∷ _ ∷ var i [] ⟨∷⟩ xs ⟨∷⟩ _)) = go (insert i t) xs
    go t (con (quote List.List.[]) _)                           = just t
    go _ _                                                      = nothing

  module OverRing (ring : Term) where

    -- Takes the name of a function that takes the ring as it's first
    -- explicit argument and the terms of it's arguments and inserts
    -- the required ring arguments
    --   e.g. "_+_" $ʳ xs = "_+_ {_} {_} ring xs"
    _$ʳ_ : Name → Args Term → Term
    nm $ʳ args = def nm (2 ⋯⟅∷⟆ ring ⟨∷⟩ args)

    checkIsListOfVariables : Term → TC Term
    checkIsListOfVariables xs =
      checkType xs (def (quote List) (1 ⋯⟅∷⟆ (quote Carrier $ʳ []) ⟨∷⟩ [])) >>= normalise

    getFieldName : Name → TC (Maybe Name)
    getFieldName nm = normalise (nm $ʳ []) <&> λ where
      (def f args) → just f
      _            → nothing

    getRingOperatorNames : TC RingNames
    getRingOperatorNames = ⦇
      +⇒ getFieldName (quote _+_)
      *⇒ getFieldName (quote _*_)
      ^⇒ getFieldName (quote _^_)
      -⇒ getFieldName (quote -_)
      ⦈

    module _ (nms : RingNames) (numVars : ℕ) where
      open RingNames nms

      -- This function applies the hidden arguments that the constructors
      -- that Expr needs. The first is the universe level, the second is the
      -- type it contains, and the third is the number of variables it's
      -- indexed by. All three of these could likely be inferred, but to
      -- make things easier we supply the third because we know it.
      _$ᵉ_ : Name → List (Arg Term) → Term
      e $ᵉ xs = con e (1 ⋯⟅∷⟆ quote Carrier $ʳ [] ⟅∷⟆ toTerm numVars ⟅∷⟆ xs)

      -- A constant expression.
      Κ′ : Term → Term
      Κ′ x = quote Κ $ᵉ (x ⟨∷⟩ [])

      _⇓≟_ : Maybe Name → Name → Bool
      nothing ⇓≟ _ = false
      just x  ⇓≟ y = primQNameEquality x y
      {-# INLINE _⇓≟_ #-}

      module ToExpr (Ι′ : ℕ → Maybe Term) where
        mutual
          -- Application of a ring operator often doesn't have a type as
          -- simple as "Carrier → Carrier → Carrier": there may be hidden
          -- arguments, etc. Here, we do our best to handle those cases,
          -- by just taking the last two explicit arguments.
          E⟨_⟩₂ : Name → List (Arg Term) → Term
          E⟨ nm ⟩₂ (x ⟨∷⟩ y ⟨∷⟩ []) = nm $ᵉ (E x ⟨∷⟩ E y ⟨∷⟩ [])
          E⟨ nm ⟩₂ (x ∷ xs)         = E⟨ nm ⟩₂ xs
          E⟨ nm ⟩₂ _                = unknown

          E⟨_⟩₁ : Name → List (Arg Term) → Term
          E⟨ nm ⟩₁ (x ⟨∷⟩ []) = nm $ᵉ (E x ⟨∷⟩ [])
          E⟨ nm ⟩₁ (x ∷ xs)   = E⟨ nm ⟩₁ xs
          E⟨ _  ⟩₁ _          = unknown

          E⟨^⟩ : List (Arg Term) → Term
          E⟨^⟩ (x ⟨∷⟩ y ⟨∷⟩ []) = quote _⊛_ $ᵉ (E x ⟨∷⟩ y ⟨∷⟩ [])
          E⟨^⟩ (x ∷ xs)         = E⟨^⟩ xs
          E⟨^⟩ _                = unknown

          -- When trying to figure out the shape of an expression, one of
          -- the difficult tasks is recognizing where constants in the
          -- underlying ring are used. If we were only dealing with ℕ, we
          -- might look for its constructors: however, we want to deal with
          -- arbitrary types which implement AlmostCommutativeRing. If the
          -- Term type contained type information we might be able to
          -- recognize it there, but it doesn't.
          --
          -- We're in luck, though, because all other cases in the following
          -- function *are* recognizable. As a result, the "catch-all" case
          -- will just assume that it has a constant expression.
          E : Term → Term
          -- Recognise the ring's fields
          E (def (quote _+_) xs) = E⟨ quote _⊕_ ⟩₂ xs
          E (def (quote _*_) xs) = E⟨ quote _⊗_ ⟩₂ xs
          E (def (quote _^_) xs) = E⟨^⟩ xs
          E (def (quote -_)  xs) = E⟨ quote ⊝_ ⟩₁ xs
          -- Recognise the underlying implementation of the ring's fields
          E (def nm          xs) = if +′ ⇓≟ nm then E⟨ quote _⊕_ ⟩₂ xs else
                                   if *′ ⇓≟ nm then E⟨ quote _⊗_ ⟩₂ xs else
                                   if ^′ ⇓≟ nm then E⟨^⟩ xs else
                                   if -′ ⇓≟ nm then E⟨ quote ⊝_ ⟩₁ xs else
                                   Κ′ (def nm xs)
          -- Variables
          E v@(var x _)          = fromMaybe (Κ′ v) (Ι′ x)
          -- Special case to recognise "suc" for naturals
          E (con (quote ℕ.suc) (x ⟨∷⟩ [])) = quote _⊕_ $ᵉ (Κ′ (toTerm 1) ⟨∷⟩ E x ⟨∷⟩ [])
          E t                    = Κ′ t

      callSolver : Vec String numVars → Term → Term → Args Type
      callSolver nms lhs rhs =
          2 ⋯⟅∷⟆ ring ⟨∷⟩ toTerm numVars ⟨∷⟩
          vlams nms (quote _⊜_  $ʳ (toTerm numVars ⟨∷⟩ E lhs ⟨∷⟩ E rhs ⟨∷⟩ [])) ⟨∷⟩
          hlams nms (quote refl $ʳ (1 ⋯⟅∷⟆ [])) ⟨∷⟩
          []
        where
        Ι′ : ℕ → Maybe Term
        Ι′ i = if i <ᵇ numVars then just (var i []) else nothing
        open ToExpr Ι′

      constructSoln : NatSet → Term → Term → Term
      constructSoln t lhs rhs =
          quote trans $ʳ (3 ⋯⟅∷⟆
            quote sym $ʳ (2 ⋯⟅∷⟆
              quote Ops.correct $ʳ (1 ⋯⟅∷⟆ E lhs ⟨∷⟩ ρ ⟨∷⟩ []) ⟨∷⟩ [])
            ⟨∷⟩
            (quote Ops.correct $ʳ (1 ⋯⟅∷⟆ E rhs ⟨∷⟩ ρ ⟨∷⟩ [])) ⟨∷⟩
            [])
        where
        Ι′ : ℕ → Maybe Term
        Ι′ i = Maybe.map (λ x → quote Ι $ᵉ (toFinTerm x ⟨∷⟩ [])) (lookup i t)

        open ToExpr Ι′
        ρ : Term
        ρ = curriedTerm t

------------------------------------------------------------------------
-- Macros
------------------------------------------------------------------------

-- This is the main macro which solves for equations in which the variables
-- are universally quantified over:
--
--   lemma : ∀ x y → x + y ≈ y + x
--   lemma = solve-∀ TypeRing
--
-- where TypRing is your implementation of AlmostCommutativeRing. (Find some
-- example implementations in Polynomial.Solver.Ring.AlmostCommutativeRing.Instances).

solve-∀-macro : Name → Term → TC ⊤
solve-∀-macro ring hole = do
  ring′ ← checkIsRing (def ring [])
  commitTC
  let open OverRing ring′
  operatorNames ← getRingOperatorNames
  hole′ ← inferType hole >>= reduce
  let variables , k , equation = underPi hole′
  just (lhs ∷ rhs ∷ []) ← pure (getArgs 2 equation)
    where nothing → typeError (strErr "Malformed call to solve." ∷
                               strErr "Expected target type to be like: ∀ x y → x + y ≈ y + x." ∷
                               strErr "Instead: " ∷
                               termErr hole′ ∷
                               [])
  unify hole (def (quote solve-fn) (callSolver operatorNames variables k lhs rhs))

macro
  solve-∀ : Name → Term → TC ⊤
  solve-∀ = solve-∀-macro

-- Use this macro when you want to solve something *under* a lambda. For example:
-- say you have a long proof, and you just want the solver to deal with an
-- intermediate step. Call it like so:
--
--   lemma₃ : ∀ x y → x + y * 1 + 3 ≈ 2 + 1 + y + x
--   lemma₃ x y = begin
--     x + y * 1 + 3 ≈⟨ +-comm x (y * 1) ⟨ +-cong ⟩ refl ⟩
--     y * 1 + x + 3 ≈⟨ solve (x ∷ y ∷ []) Int.ring ⟩
--     3 + y + x     ≡⟨ refl ⟩
--     2 + 1 + y + x ∎
--
-- The first argument is the free variables, and the second is the
-- ring implementation (as before).
--
-- One thing to note here is that we need to be able to infer *both* sides of
-- the equality, which the normal equaltional reasoning combinators don't let you
-- do. You'll need the combinators defined in Relation.Binary.Reasoning.Inference.
-- These are just as powerful as the others, but have slightly better inference properties.

solve-macro : Term → Name → Term → TC ⊤
solve-macro i ring hole = do
  ring′ ← checkIsRing (def ring [])
  commitTC
  let open OverRing ring′
  operatorNames ← getRingOperatorNames
  listOfVariables′ ← checkIsListOfVariables i
  commitTC
  hole′ ← inferType hole >>= reduce
  just vars′ ← pure (getVariableIDs listOfVariables′)
    where nothing → typeError (strErr "Malformed call to solve." ∷
                               strErr "First argument should be a list of free variables." ∷
                               strErr "Instead: " ∷
                               termErr listOfVariables′ ∷
                               [])
  just (lhs ∷ rhs ∷ []) ← pure (getArgs 2 hole′)
    where nothing → typeError (strErr "Malformed call to solve." ∷
                               strErr "First argument should be a list of free variables." ∷
                               strErr "Instead: " ∷
                               termErr hole′ ∷
                               [])
  unify hole (constructSoln operatorNames (List.length vars′) vars′ lhs rhs)

macro
  solve : Term → Name → Term → TC ⊤
  solve = solve-macro


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

open import homotopy.3x3.Common
open import homotopy.3x3.PushoutPushout
open import homotopy.3x3.Transpose

module homotopy.JoinAssoc3x3 {i} (A B C : Type i) where

open M using (Pushout^2)

join-assoc-span^2 : Span^2 {i}
join-assoc-span^2 =
  span^2 A (A × C) (A × C) (A × B) ((A × B) × C) (A × C) B (B × C) C
         fst (idf _) fst (λ u → fst (fst u) , snd u) fst snd fst snd (λ u → fst (fst u) , snd u) (λ u → snd (fst u) , snd u) (idf _) snd
         (λ _ → idp) (λ _ → idp) (λ _ → idp) (λ _ → idp)

open import homotopy.3x3.Commutes join-assoc-span^2 as PP

module _ (A B : Type i) (f : B → A) where

  lemma3-fun : Pushout (span A B B f (idf _)) → A
  lemma3-fun = Lemma3Fun.f  module _ where

    module Lemma3Fun = PushoutRec (idf _) f (λ _ → idp)

  lemma3-eq : (x : Pushout (span A B B f (idf _))) → left (lemma3-fun x) == x
  lemma3-eq = Pushout-elim (λ _ → idp) glue (λ b → ↓-∘=idf-in left lemma3-fun (idp,=□idp,-in idp ∙□-i/ idp / ! (ap (ap left) (Lemma3Fun.glue-β b)) /))

  lemma3 : Pushout (span A B B f (idf _)) ≃ A
  lemma3 = equiv lemma3-fun left (λ _ → idp) lemma3-eq

module _ (A B : Type i) (f : B → A) where

  lemma3'-fun : Pushout (span B A B (idf _) f) → A
  lemma3'-fun = Lemma3'Fun.f  module _ where

    module Lemma3'Fun = PushoutRec f (idf _) (λ _ → idp)

  lemma3'-eq : (x : Pushout (span B A B (idf _) f)) → right (lemma3'-fun x) == x
  lemma3'-eq = ! ∘ (Pushout-elim glue (λ _ → idp) (λ b → ↓-idf=∘-in right lemma3'-fun (,idp=□,idp-in idp ∙□-i/ ap (ap right) (Lemma3'Fun.glue-β b) / idp /)))

  lemma3' : Pushout (span B A B (idf _) f) ≃ A
  lemma3' = equiv lemma3'-fun right (λ _ → idp) lemma3'-eq

module _ (X Y Z T : Type i) (f : Z → X) (g : Z → Y) where

  private
    P1 : Type i
    P1 = Pushout (span X Y Z f g)

    P2 : Type i
    P2 = Pushout (span (X × T) (Y × T) (Z × T) (λ u → (f (fst u) , snd u)) (λ u → (g (fst u) , snd u)))

  lemma4 : P2 ≃ (P1 × T)
  lemma4 = equiv to from to-from from-to  module Lemma4 where

    to : P2 → P1 × T
    to = To.f  module _ where

      module To = PushoutRec (λ u → (left (fst u) , snd u)) (λ u → (right (fst u) , snd u)) (λ u → pair×= (glue (fst u)) idp)

    from-curr : T → (P1 → P2)
    from-curr t = FromCurr.f  module _ where

      module FromCurr = PushoutRec {D = P2} (λ x → left (x , t)) (λ y → right (y , t)) (λ z → glue (z , t))

    from : P1 × T → P2
    from (x , t) = from-curr t x

    to-from : (u : P1 × T) → to (from u) == u
    to-from (x , t) = to-from-curr t x  where

      ap-idf,×cst : ∀ {i j} {A : Type i} {B : Type j}
        {x y : A} (p : x == y) {b : B}
        → ap (λ v → v , b) p == pair×= p idp
      ap-idf,×cst idp = idp

      to-from-curr : (t : T) (x : P1) → to (from-curr t x) == (x , t)
      to-from-curr t = Pushout-elim (λ _ → idp) (λ _ → idp) (λ z → ↓-='-in (ap-idf,×cst (glue z) ∙ ! (To.glue-β (z , t)) ∙ ! (ap (ap to) (FromCurr.glue-β t z)) ∙ ∘-ap to (from-curr t) (glue z)))

    from-to : (u : P2) → from (to u) == u
    from-to = Pushout-elim (λ _ → idp) (λ _ → idp) (λ c → ↓-∘=idf-in from to (! (ap (ap from) (To.glue-β c) ∙ ap-pair×= from (glue (fst c)) ∙ FromCurr.glue-β (snd c) (fst c))))  where

      ap-pair×= : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (f : A × B → C)
        {a a' : A} (p : a == a') {b : B}
        → ap f (pair×= p idp) == ap (λ a → f (a , b)) p
      ap-pair×= f {a = a} {a' = .a} idp = idp

module _ (X Y T : Type i) where

  private
    P1 : Type i
    P1 = Pushout (span X Y (X × Y) fst snd)

    P2 : Type i
    P2 = Pushout (span (T × X) (T × Y) ((T × X) × Y) fst (λ u → (fst (fst u) , snd u)))

  lemma4' : P2 ≃ (T × P1)
  lemma4' = equiv to from to-from from-to  module Lemma4' where

    to : P2 → T × P1
    to = To.f  module _ where

      module To = PushoutRec {D = T × P1} (λ u → (fst u , left (snd u))) (λ u → (fst u , right (snd u))) (λ c → pair×= idp (glue (snd (fst c) , snd c)))

    from-curr : T → (P1 → P2)
    from-curr t = FromCurr.f  module _ where

      module FromCurr = PushoutRec {D = P2} (λ x → left (t , x)) (λ y → right (t , y)) (λ z → glue ((t , fst z) , snd z))

    from : T × P1 → P2
    from (t , x) = from-curr t x

    to-from : (u : T × P1) → to (from u) == u
    to-from (t , x) = to-from-curr t x  where

      to-from-curr : (t : T) (x : P1) → to (from-curr t x) == (t , x)
      to-from-curr t = Pushout-elim (λ _ → idp) (λ _ → idp) (λ c → ↓-='-in (ap-cst,id (λ _ → _) (glue c) ∙ ! (lemma5 c)))  where

        lemma5 : (c : X × Y) → ap (to ∘ from-curr t) (glue c) == pair×= idp (glue c)
        lemma5 (x , y) =
          ap (to ∘ from-curr t) (glue (x , y))
            =⟨ ap-∘ to (from-curr t) (glue (x , y)) ⟩
          ap to (ap (from-curr t) (glue (x , y)))
            =⟨ FromCurr.glue-β t (x , y) |in-ctx ap to ⟩
          ap to (glue ((t , x) , y))
            =⟨ To.glue-β ((t , x) , y) ⟩
          pair×= idp (glue (x , y)) ∎

    from-to : (x : P2) → from (to x) == x
    from-to = Pushout-elim (λ _ → idp) (λ _ → idp) (λ c → ↓-∘=idf-in from to (! (lemma42 c)))  where

      ap-pair×= : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (f : A × B → C)
        {a : A} {b b' : B} (p : b == b')
        → ap f (pair×= idp p) == ap (λ b → f (a , b)) p
      ap-pair×= f {b = b} {b' = .b} idp = idp

      lemma42 : (c : (T × X) × Y) → ap from (ap to (glue c)) == glue c
      lemma42 ((t , x) , y) =
        ap from (ap to (glue ((t , x) , y)))
          =⟨ To.glue-β ((t , x) , y) |in-ctx ap from ⟩
        ap from (pair×= idp (glue (x , y)))
          =⟨ ap-pair×= from (glue (x , y)) ⟩
        ap (from-curr t) (glue (x , y))
          =⟨ FromCurr.glue-β t (x , y) ⟩
        glue ((t , x) , y) ∎

lemma2 : M.v-h-span join-assoc-span^2 == *-span A (B * C)
lemma2 = span= (lemma3 A (A × C) fst) (ide _) (lemma4' B C A)
               (Pushout-elim (λ _ → idp) (λ _ → idp) (λ x → ↓-='-in (lemma2-1 x ∙ ! (lemma2-2 x))))
               (Pushout-elim (λ _ → idp) (λ _ → idp) (λ x → ↓-='-in (lemma2-3 x ∙ ! (M.F₃∙.glue-β join-assoc-span^2 _ ∙ ∙-unit-r (glue _))))) where

  lemma2-1 : (x : (A × B) × C) → _
  lemma2-1 ((a , b) , c) =
    ap (fst ∘ Lemma4'.to B C A) (glue ((a , b) , c))
      =⟨ ap-∘ fst (Lemma4'.to B C A) (glue ((a , b) , c)) ⟩
    ap fst (ap (Lemma4'.to B C A) (glue ((a , b) , c)))
      =⟨ Lemma4'.To.glue-β B C A ((a , b) , c) |in-ctx fst×= ⟩
    fst×= (pair×= idp (glue (b , c)))
      =⟨ fst×=-β idp (glue (b , c)) ⟩
    idp ∎

  lemma2-2 : (x : (A × B) × C) → _
  lemma2-2 ((a , b) , c) =
    ap (lemma3-fun A (A × C) fst ∘ M.f₁∙ join-assoc-span^2) (glue ((a , b) , c))
      =⟨ ap-∘ (lemma3-fun A (A × C) fst) (M.f₁∙ join-assoc-span^2) (glue ((a , b) , c)) ⟩
    ap (lemma3-fun A (A × C) fst) (ap (M.f₁∙ join-assoc-span^2) (glue ((a , b) , c)))
      =⟨ M.F₁∙.glue-β join-assoc-span^2 ((a , b) , c) |in-ctx ap (lemma3-fun A (A × C) fst) ⟩
    ap (lemma3-fun A (A × C) fst) (glue (a , c) ∙ idp)
      =⟨ ∙-unit-r (glue (a , c)) |in-ctx ap (lemma3-fun A (A × C) fst) ⟩
    ap (lemma3-fun A (A × C) fst) (glue (a , c))
      =⟨ Lemma3Fun.glue-β A (A × C) fst (a , c) ⟩
    idp ∎

  lemma2-3 : (x : (A × B) × C) → _
  lemma2-3 ((a , b) , c) =
    ap (snd ∘ Lemma4'.to B C A) (glue ((a , b) , c))
      =⟨ ap-∘ snd (Lemma4'.to B C A) (glue ((a , b) , c)) ⟩
    ap snd (ap (Lemma4'.to B C A) (glue ((a , b) , c)))
      =⟨ Lemma4'.To.glue-β B C A ((a , b) , c) |in-ctx snd×= ⟩
    snd×= (pair×= idp (glue (b , c)))
      =⟨ snd×=-β idp (glue (b , c)) ⟩
    glue (b , c) ∎

lemma2' : M.v-h-span (transpose join-assoc-span^2) == *-span (A * B) C
lemma2' = span= (ide _) (lemma3' C (A × C) snd) (lemma4 A B (A × B) C fst snd)
          (Pushout-elim (λ _ → idp) (λ _ → idp) (λ c → ↓-='-in (ap-∘ fst (Lemma4.to A B (A × B) C fst snd) (glue c) ∙ ap (ap fst) (Lemma4.To.glue-β A B (A × B) C fst snd c) ∙ fst×=-β (glue (fst c)) idp ∙ ! (∙-unit-r (glue (fst c))) ∙ ! (M.F₁∙.glue-β (transpose join-assoc-span^2) c))))
          (Pushout-elim (λ _ → idp) (λ _ → idp) (λ u → ↓-='-in (lemma2'-1 u ∙ ! (lemma2'-2 u))))  where

  lemma2'-1 : (u : (A × B) × C) → ap (snd ∘ Lemma4.to A B (A × B) C fst snd) (glue u) == idp
  lemma2'-1 u =
    ap (snd ∘ Lemma4.to A B (A × B) C fst snd) (glue u)
      =⟨ ap-∘ snd (Lemma4.to A B (A × B) C fst snd) (glue u) ⟩
    ap snd (ap (Lemma4.to A B (A × B) C fst snd) (glue u))
      =⟨ Lemma4.To.glue-β A B (A × B) C fst snd u |in-ctx snd×= ⟩
    snd×= (pair×= (glue (fst u)) idp)
      =⟨ snd×=-β (glue (fst u)) idp ⟩
    idp ∎

  lemma2'-2 : (u : (A × B) × C) → ap (lemma3'-fun C (A × C) snd ∘ M.f₃∙ (transpose join-assoc-span^2)) (glue u) == idp
  lemma2'-2 u =
    ap (lemma3'-fun C (A × C) snd ∘ M.f₃∙ (transpose join-assoc-span^2)) (glue u)
      =⟨ ap-∘ (lemma3'-fun C (A × C) snd) (M.f₃∙ (transpose join-assoc-span^2)) (glue u) ⟩
    ap (lemma3'-fun C (A × C) snd) (ap (M.f₃∙ (transpose join-assoc-span^2)) (glue u))
      =⟨ M.F₃∙.glue-β (transpose join-assoc-span^2) u |in-ctx ap (lemma3'-fun C (A × C) snd) ⟩
    ap (lemma3'-fun C (A × C) snd) (glue (fst (fst u) , snd u) ∙ idp)
      =⟨ ∙-unit-r (glue (fst (fst u) , snd u)) |in-ctx ap (lemma3'-fun C (A × C) snd) ⟩
    ap (lemma3'-fun C (A × C) snd) (glue (fst (fst u) , snd u))
      =⟨ Lemma3'Fun.glue-β C (A × C) snd (fst (fst u) , snd u) ⟩
    idp ∎

lemma1 : Pushout^2 join-assoc-span^2 == A * (B * C)
lemma1 = ap Pushout lemma2

lemma1' : Pushout^2 (transpose join-assoc-span^2) == (A * B) * C
lemma1' = ap Pushout lemma2'

*-assoc : A * (B * C) == (A * B) * C
*-assoc = ! lemma1 ∙ ua PP.theorem ∙ lemma1'

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-# OPTIONS --safe --without-K #-}
module Categories.Examples.Monad.Duration where

-- Monad induced by pairing a Monoid and a Setoid
open import Level

open import Function.Base using (_-⟪_⟫-_; _on_; _∘_) renaming (id to id→)
open import Function.Equality using (Π; _⟨$⟩_; cong)

open import Relation.Binary
open import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial

open import Data.Product using (Σ; _,_; _×_; proj₁; proj₂; dmap′; zip; map₁; map₂)
open import Algebra using (Monoid)

open import Categories.Category
open import Categories.Category.Instance.Setoids
open import Categories.Functor renaming (id to idF)
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
open import Categories.Monad using (Monad)

open import Data.Nat.Properties renaming (+-0-monoid to +-0-nat-monoid)
open import Data.Integer.Properties renaming (+-0-monoid to +-0-integer-monoid)
open import Data.Rational.Properties renaming (+-0-monoid to +-0-rational-monoid)

open Monoid public

monoid×-₀ : ∀ {l₁ l₂ e₁ e₂} → Monoid l₁ e₁ → Setoid l₂ e₂ → Setoid _ _
monoid×-₀ m s = record
  { Carrier = m.Carrier × s.Carrier
  ; _≈_ = m._≈_ on proj₁ -⟪ _×_ ⟫- s._≈_ on proj₂
  ; isEquivalence = record
      { refl = m.refl , s.refl
      ; sym = dmap′ m.sym s.sym
      ; trans = zip m.trans s.trans
      }
  }
  where
    module m = Monoid m
    module s = Setoid s

monoid×-₁ : ∀ {l₁ l₂ e₁ e₂} {A B : Setoid l₂ e₂} → (m : Monoid l₁ e₁) → (f : Setoids l₂ e₂ [ A , B ]) → Setoids _ _ [ monoid×-₀ m A , monoid×-₀ m B ]
monoid×-₁ _ f = record
  { _⟨$⟩_ = map₂ (_⟨$⟩_ f)
  ; cong = map₂ (cong f)
  }

-- levels have to be the same because everything gets put into the same stop
monoid×-endo : ∀ {l₁ e₁} → Monoid l₁ e₁ → Endofunctor (Setoids l₁ e₁)
monoid×-endo m =  record
  { F₀ = monoid×-₀ m
  ; F₁ = monoid×-₁ m
  ; identity = id→
  ; homomorphism = λ {_} {_} {_} {f} {g} p → map₂ (cong g ∘ cong f) p
  ; F-resp-≈ = λ f → map₂ f
  }

monoid×-η : ∀ {l e} → (m : Monoid l e) → NaturalTransformation idF (monoid×-endo m)
monoid×-η m = ntHelper record
  { η = λ _ → record { _⟨$⟩_ = m.ε ,_ ; cong = m.refl ,_ }
  ; commute = λ f x → m.refl , cong f x
  }
  where module m = Monoid m

monoid×-μ : ∀ {l} → (m : Monoid l l) → NaturalTransformation (monoid×-endo m ∘F monoid×-endo m) (monoid×-endo m)
monoid×-μ m = ntHelper record
  { η = λ X → record
    { _⟨$⟩_ =  λ { (d , d₁ , value) → ( d m.∙ d₁) , value }
    ; cong = λ { (d , d₁ , v) → m.∙-cong d d₁ , v }
    }
  ; commute = λ { f (d , d₁ , v) → m.∙-cong d d₁ , cong f v }
  }
  where
    module m = Monoid m

monoid×-monad : ∀ {l} → Monoid l l → Monad (Setoids l l)
monoid×-monad m = record
  { F = monoid×-endo m
  ; η = monoid×-η m
  ; μ = monoid×-μ m
  ; assoc     = λ (p₀ , p₁ , p₂ , p₃) → m.trans (m.∙-cong p₀ (m.∙-cong p₁ p₂)) (m.sym (m.assoc _ _ _)) , p₃
  ; sym-assoc = λ (p₀ , p₁ , p₂ , p₃) → m.trans (m.∙-cong (m.∙-cong p₀ p₁) p₂) (      (m.assoc _ _ _)) , p₃
  ; identityˡ  = λ p → map₁ (m.trans (m.identityʳ _)) p
  ; identityʳ  = λ p → map₁ (m.trans (m.identityˡ _)) p
  }
  where module m = Monoid m

natDuration : Monad (Setoids 0ℓ 0ℓ)
natDuration = monoid×-monad +-0-nat-monoid

integerDuration : Monad (Setoids 0ℓ 0ℓ)
integerDuration = monoid×-monad +-0-integer-monoid

rationalDuration : Monad (Setoids 0ℓ 0ℓ)
rationalDuration = monoid×-monad +-0-rational-monoid

max_stars_repo_name: agda/categories-examples

max_issues_repo_name: agda/categories-examples

max_forks_repo_name: agda/categories-examples


text:
module LongList where

infixr 6 _∷_

data List (A : Set) : Set where
  [] : List A
  _∷_ : A -> List A -> List A

postulate
  Bool : Set
  t : Bool

long : List Bool
long =
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 []


text:
{-# OPTIONS --rewriting --prop --exact-split #-}

open import common

{-
An arity is something of the form (((n_1, k_1), …, (n_l, k_l)) , k), where the n_i are natural
numbers and the k_i and k are sorts. We will use two different types of sorts, so we parametrize
arities by the type of sorts.
The type [ArityArgs Sort] represents the first components of arities (the list), and [Arity Sort]
represents arities.
-}

data ArityArgs (Sort : Set) : Set where
  [] : ArityArgs Sort
  _,_ : ArityArgs Sort → (ℕ × Sort) → ArityArgs Sort

record Arity (Sort : Set) : Set where
  constructor _,_
  field
    args : ArityArgs Sort
    sort : Sort
open Arity public

SyntaxArityArgs = ArityArgs SyntaxSort
SyntaxArity = Arity SyntaxSort

{-
A signature consists of symbols, which are indexed by their arities. To have instead a set of
symbols and an arity function is very inconvenient.
-}

record Signature : Set₁ where
  field
    Symbols : SyntaxArity → Set
open Signature public

{-
Expressions are indexed by their syntactic class and their scope. An expression is either a variable
or a symbol applied to the appropriate number of arguments.
The type [Expr Σ n] is defined simultaneously with the type [Args Σ n args] which represents the
type of the arguments of a symbol with arity (args, _).
-}

data Args (Σ : Signature) (n : ℕ) : SyntaxArityArgs → Set

data Expr (Σ : Signature) (n : ℕ) : SyntaxSort → Set where
  var : VarPos n → Expr Σ n Tm
  sym : {ar : SyntaxArity} (s : Symbols Σ ar) → Args Σ n (args ar) → Expr Σ n (sort ar)

data Args Σ n where
  [] : Args Σ n []
  _,_ : {m : ℕ} {k : SyntaxSort} {args : SyntaxArityArgs}
      → Args Σ n args
      → Expr Σ (n + m) k
      → Args Σ n (args , (m , k))

{- Abbreviations for type-/term-expressions -}

TyExpr : (Σ : Signature) → ℕ → Set
TyExpr Σ n = Expr Σ n Ty

TmExpr : (Σ : Signature) → ℕ → Set
TmExpr Σ n = Expr Σ n Tm

{-
weakenV : {n m : ℕ} {{_ : n ≤ m}} (p : WeakPos n) → VarPos n → VarPos m
weakenV ⦃ ≤r ⦄ p x = x
weakenV ⦃ ≤S r ⦄ last x = prev (weakenV {{r}} last x)
weakenV ⦃ ≤S r ⦄ (prev p) last = last
weakenV ⦃ ≤S r ⦄ (prev p) (prev x) = prev (weakenV {{≤P (≤S r)}} p x)
-}

-- weakenVL : {n m : ℕ} {{_ : n ≤ m}} → VarPos n → VarPos m
-- weakenVL {{ ≤r }} x = x
-- weakenVL {{ ≤S p }} x = prev (weakenVL {{p}} x)

-- postulate
--   weakenV : {n m : ℕ} {{_ : n ≤ m}} (p : WeakPos n) → VarPos n → VarPos m
-- weakenV {m = _} ⦃ ≤r ⦄ last last = last
-- weakenV {m = _} ⦃ ≤S r ⦄ last last = prev (weakenV {{r}} last last)
-- weakenV {m = suc m} ⦃ r ⦄ (prev p) last = last
-- weakenV {m = suc m} ⦃ ≤r ⦄ last (prev x) = prev x
-- weakenV {m = suc m} ⦃ ≤S r ⦄ last (prev x) = prev (weakenV {m = m} {{≤P (≤S r)}} last x)
-- weakenV {m = suc m} ⦃ r ⦄ (prev p) (prev x) = prev (weakenV {m = m} {{≤P r}} p x)

-- weakenV {m = suc m}       (prev wp) last = last
-- weakenV {m = suc m} {{p}} (prev wp) (prev x) = prev (weakenV {{≤P p}} wp x)
-- weakenV {m = suc m} ⦃ ≤r ⦄ last x = x
-- weakenV {m = suc m} ⦃ ≤S r ⦄ last x = prev (weakenV {{r}} last x)

-- weakenV {m = suc m} ⦃ p ⦄ (prev wp) last = last
-- weakenV {m = suc m} ⦃ p ⦄ (prev wp) (prev x) = prev (weakenV {{≤P p}} wp x)
-- weakenV {m = suc m} ⦃ ≤r ⦄ last x = x
-- weakenV {m = suc m} ⦃ ≤S p ⦄ last x = prev (weakenV {{p}} last x)

postulate
  TODO : {A : Set} → A

weaken : {Σ : Signature} {k : _} {n m : ℕ} {{_ : n ≤ m}} (p : WeakPos n) → Expr Σ n k → Expr Σ m k
weakenA : {Σ : Signature} {ar : _} {n m : ℕ} {{_ : n ≤ m}} (p : WeakPos n) → Args Σ n ar → Args Σ m ar

weaken p (var x) = var (weakenV p x)
weaken p (sym s es) = sym s (weakenA p es)

weakenA p [] = []
weakenA {{q}} p (_,_ {m = m} es e) = (weakenA p es , weaken {{≤+ m {{q}}}} (weakenPos (≤-+ {m = m}) p) e)

weaken' : {Σ : Signature} {k : _} {n m : ℕ} {{_ : n ≤ m}} (p : WeakPos n) → Expr Σ n k → Expr Σ m k
weaken' ⦃ ≤r ⦄ p e = e
weaken' ⦃ ≤S q ⦄ p e = weaken {{≤S q}} p e

weakenL : {Σ : Signature} {k : _} {m n : ℕ} → Expr Σ m k → Expr Σ (m + n) k
weakenL {n = zero} e = e
weakenL {n = suc n} e = weaken last e

weaken0 : {Σ : Signature} {k : _} {n : ℕ} → Expr Σ 0 k → Expr Σ n k
weaken0 e = weaken {{0≤}} last e

weaken0' : {Σ : Signature} {k : _} {n : ℕ} → Expr Σ 0 k → Expr Σ n k
weaken0' {n = zero} e = e
weaken0' {n = suc n} e = weaken last e

weakenAL : {Σ : Signature} {ar : _} {m n : ℕ} → Args Σ m ar → Args Σ (m + n) ar
weakenAL {n = zero} es = es
weakenAL {n = suc n} es = weakenA last es

prev^last : (n l : ℕ) → WeakPos (n + l)
prev^last n zero = last
prev^last n (suc l) = prev (prev^last n l)

-- weaken≤ : {Σ : Signature} {k : _} {n m l : ℕ} {{_ : n ≤ m}} → Expr Σ (n + l) k → Expr Σ (m + l) k
-- weaken≤ ⦃ ≤r ⦄ e = e
-- weaken≤ {n = n} {l = l} ⦃ ≤S p ⦄ e = weaken {{TODO}} (prev^last n l) e

-- weaken^V' : {l m n : ℕ} → VarPos (l + m) → VarPos (l + n + m)
-- weaken^' : {Σ : Signature} {k : _} {l m n : ℕ} → Expr Σ (l + m) k → Expr Σ (l + n + m) k
-- weaken^A' : {Σ : Signature} {ar : _} {l m n : ℕ} → Args Σ (l + m) ar → Args Σ (l + n + m) ar

-- weaken^V' {zero} {m} {zero} k = k
-- weaken^V' {zero} {m} {suc n} k = prev (weaken^V' {zero} {m} {n} k)
-- weaken^V' {suc l} {m} {n} last = last
-- weaken^V' {suc l} {m} {n} (prev k) = prev (weaken^V' {l} {m} {n} k)

-- weaken^' {l = l} {m} {n} (var k) = var (weaken^V' {l = _} {m} {n} k)
-- weaken^' {l = l} {m} {n} (sym s x) = sym s (weaken^A' {l = _} {m} {n} x)

-- weaken^A' [] = []
-- weaken^A' {l = l} {m} {n} (_,_ {m = _} a x) = (weaken^A' {l = _} {m} {n} a , weaken^' {l = _} {m} {n} x)

-- -- this should not be defined as iterated weakening, it should reduce on expressions
-- weaken^ : {Σ : Signature} {k : _} {l n m : ℕ} {{p : n ≤ m}} → Expr Σ (l + n) k → Expr Σ (l + m) k
-- weaken^ {l = l} {n} {m} {{p}} k = weaken^' {l = l} {{!n!}} {{!!}} k

-- weaken^A : {Σ : Signature} {ar : _} {l n m : ℕ} {{p : n ≤ m}} → Args Σ (l + n) ar → Args Σ (l + m) ar
-- weaken^A {{p}} = weaken^A' {{p}}

-- weakenV≤r : {n : ℕ} {p : WeakPos n} (v : VarPos n) → weakenV {{≤r}} p v ≡ v
-- weakenV≤r {p = last} last = refl
-- weakenV≤r {p = prev p} last = refl
-- weakenV≤r {p = last} (prev v) = refl
-- weakenV≤r {p = prev p} (prev v) = ap prev (weakenV≤r {p = p} v)

-- weaken≤r : {Σ : Signature} {k : _} {n : ℕ} {p : WeakPos n} (e : Expr Σ n k) → weaken p e ≡ e
-- weakenA≤r : {Σ : Signature} {k : _} {n : ℕ} {p : WeakPos n} (as : Args Σ n k) → weakenA p as ≡ as

-- weaken≤r {p = p} (var x) = ap var (weakenV≤r {p = p} x)
-- weaken≤r (sym s x) = ap (sym s) (weakenA≤r x)

-- weakenA≤r [] = refl
-- weakenA≤r (es , e) = ap2 _,_ (weakenA≤r es) (weaken≤r e)

-- -- {-# REWRITE weaken^'≤r #-}

{- Contexts, [Ctx Σ n] represents contexts in signature [Σ] and of length [n] -}

data Ctx (Σ : Signature) : ℕ → Set where
  ◇ : Ctx Σ 0
  _,_ : {n : ℕ} (Γ : Ctx Σ n) (A : TyExpr Σ n) → Ctx Σ (suc n)

{- TODO
Dependent contexts, [DepCtx Σ n m] represents contexts in signature [Σ], in scope [n], and of
length [m]. They are built in the other direction compared to [Ctx], we add types to the left
instead of adding them to the right. The reason is that the "purpose" of dependent contexts is to
move the types one by one to the context on the left.
-}

data DepCtx (Σ : Signature) (n : ℕ) : ℕ → Set where
  ◇ : DepCtx Σ n 0
  _,_ : {m : ℕ} → DepCtx Σ n m → TyExpr Σ (n + m) → DepCtx Σ n (suc m)

{-
Extraction of types from contexts.
We need this partial version instead of the total well-typed one (below, not used).
-}

get : {Σ : Signature} {n : ℕ} (k : ℕ) → Ctx Σ n → Partial (VarPos n × TyExpr Σ n)
get k ◇ = fail
get zero (Γ , A) = return (last , weaken last A)
get (suc k) (Γ , X) = do
  (k' , A) ← get k Γ
  return (prev k' , weaken last A)

getTotal : {Σ : Signature} {n : ℕ} (k : VarPos n) → Ctx Σ n → TyExpr Σ n
getTotal last (Γ , A) = weaken last A
getTotal (prev k) (Γ , X) = weaken last (getTotal k Γ)

{-
In order to deal with extensions of signatures, we need a notion of map between signatures. There
are a few possible options:
- Mapping symbols to symbols: not strong enough, as later we need to map a symbol s(-) to the
  expression s(a, -)
- Mapping expressions to expressions: too strong, makes it impossible to look inside expressions
- Mapping symbols to expression-building function: this is the approach we take. A symbol will be
  mapped to a function of the corresponding arity between expressions of the codomain signature.

We need sometimes to restrict them to expressions in a certain scope (bounded below). This happens
for instance when turning typing rules to partial functions on the syntax, we replace something by a
specific term which lives in a scope, so the map between signatures does not work for a lower scope.
We need to have it bounded below (as opposed to having a fixed scope) otherwise we cannot map
expressions to expressions (as they may bind new variables).

Therefore we define [(Σ →Sig Σ') n] which represents maps from symbols of [Σ] to expression-building
functions for signature [Σ'], and which works for any scope above (and including) [n].
-}

record _→Sig_ (Σ Σ' : Signature) (n : ℕ) : Set where
  constructor sub
  field
    _$_ : {m : ℕ} {{p : n ≤ m}} {ar : SyntaxArity} (s : Symbols Σ ar) → Args Σ' m (args ar) → Expr Σ' m (sort ar)
open _→Sig_ public

{- Identity map -}

idSig : {n : ℕ} {Σ : Signature} → (Σ →Sig Σ) n
idSig $ s = sym s

{- Lifting at a higher scope -}

liftSig : {m n : ℕ} {Σ Σ' : Signature} → (Σ →Sig Σ') m → (Σ →Sig Σ') (m + n)
(liftSig {n = n} ↑ $ s) x = _$_ ↑ {{≤tr {{≤-+ {m = n}}}}} s x

{- Lifting of a map between signatures to expressions -}

↑Expr : {Σ Σ' : Signature} {n : ℕ} {k : SyntaxSort} → (Σ →Sig Σ') n → Expr Σ n k → Expr Σ' n k
↑Args : {Σ Σ' : Signature} {n : ℕ} {args : SyntaxArityArgs} → (Σ →Sig Σ') n → Args Σ n args → Args Σ' n args

↑Expr ↑ (var x) = var x
↑Expr ↑ (sym s x) = (↑ $ s) (↑Args ↑ x)

↑Args ↑ [] = []
↑Args ↑ (_,_ {m = m} es e) = ↑Args ↑ es , ↑Expr (liftSig ↑) e

{-
[ExtSig Σ ar] extends the signature [Σ] by an arity [ar].
In order to add a symbol only at the correct arity, we use an inductive family (another possibility
would be to use decidable equality of arities but that would be very ugly).
-}

data ExtSigSymbols (S : SyntaxArity → Set) (ar : SyntaxArity) : SyntaxArity → Set where
  prev : {ar' : SyntaxArity} → S ar' → (ExtSigSymbols S ar) ar'
  new : (ExtSigSymbols S ar) ar

ExtSig : Signature → SyntaxArity → Signature
Symbols (ExtSig Σ ar) = ExtSigSymbols (Symbols Σ) ar

{- If an extended signature maps to [Σ'], then the original signature too. -}
Ext→ : {Σ Σ' : Signature} {ar : SyntaxArity} {n : ℕ} → (ExtSig Σ ar →Sig Σ') n → (Σ →Sig Σ') n
Ext→ ↑ $ s = ↑ $ (prev s)

{- Arities of metavariables -}

MArityArgs : ℕ → SyntaxArityArgs
MArityArgs zero = []
MArityArgs (suc n) = MArityArgs n , (0 , Tm)

MArity : ℕ → SyntaxSort → SyntaxArity
args (MArity n k) = MArityArgs n
sort (MArity n k) = k

{- [ExtSig^ Σ args] extends the signature [Σ] by symbols for metavariables with arities given by [args] -}

ExtSig^ : Signature → SyntaxArityArgs → Signature
ExtSig^ Σ [] = Σ
ExtSig^ Σ (args , (n , k)) = ExtSig (ExtSig^ Σ args) (MArity n k)

{- Example
ExtSig^ Σ ((0, Ty), (1, Ty)) = extend Σ with one symbol of arity (() , Ty) and
                                             one symbol of arity ((0 , Tm), Ty)
-}

{-
Given two signatures [Σ] and [Σ'], we can map from a signature extended over [Σ] to [Σ'] as long as
we can map from [Σ] to [Σ'] and that we have terms [as] in [Σ'] to replace the new symbols.
[SubstM ↑ as] represents that map.
-}

-- trExpr : {Σ : Signature} {n n' : ℕ} (p : n === n') {k : SyntaxSort} → Expr Σ n k → Expr Σ n' k
-- trExpr refl u = u

-- trExpr! : {Σ : Signature} {n n' : ℕ} (p : n === n') {k : SyntaxSort} → Expr Σ n' k → Expr Σ n k
-- trExpr! refl u = u

pred : ℕ → ℕ
pred zero = zero
pred (suc n) = n

trV  : {n m : ℕ} → n ≡ m → VarPos n → VarPos m
trV {m = suc m} p last = last
trV {m = suc m} p (prev x) = prev (trV (ap pred p) x)

tr  : {Σ : Signature} {k : SyntaxSort} {n m : ℕ} → n ≡ m → Expr Σ n k → Expr Σ m k
trA : {Σ : Signature} {ar : SyntaxArityArgs} {n m : ℕ} → n ≡ m → Args Σ n ar → Args Σ m ar

tr p (var x) = var (trV p x)
tr p (sym s es) = sym s (trA p es)

trA p [] = []
trA p (es , x) = (trA p es , tr (ap (_+ _) p) x)

tr! : {Σ : Signature} {k : SyntaxSort} {n m : ℕ} → m ≡ n → Expr Σ n k → Expr Σ m k
tr! p e = tr (! p) e

data Mor (Σ : Signature) (n : ℕ) : ℕ → Set where
 ◇ : Mor Σ n 0
 _,_ : {m : ℕ} (δ : Mor Σ n m) (u : TmExpr Σ n) → Mor Σ n (suc m)

weakenMor : {Σ : Signature} {n m : ℕ} → Mor Σ m n → Mor Σ (suc m) n
weakenMor ◇ = ◇
weakenMor (δ , u) = (weakenMor δ , weaken last u)

idMor : {Σ : Signature} {n : ℕ} → Mor Σ n n
idMor {n = zero} = ◇
idMor {n = suc n} = (weakenMor idMor , var last)

weakenMor+ : {Σ : Signature} (k : ℕ) {n m : ℕ} → Mor Σ m n → Mor Σ (m + k) (n + k)
weakenMor+ zero δ = δ
weakenMor+ (suc k) δ = (weakenMor (weakenMor+ k δ) , var last)

SubstMor  : {Σ : Signature} {n m : ℕ} {k : SyntaxSort} → Expr Σ n k → Mor Σ m n → Expr Σ m k
SubstAMor : {Σ : Signature} {n m : ℕ} {args : SyntaxArityArgs} → Args Σ n args → Mor Σ m n → Args Σ m args

SubstMor (var last) (δ , u) = u
SubstMor (var (prev x)) (δ , u) = SubstMor (var x) δ
SubstMor (sym s es) δ = sym s (SubstAMor es δ)

SubstAMor [] δ = []
SubstAMor (_,_ {m = m} es x) δ = (SubstAMor es δ , SubstMor x (weakenMor+ m δ))

-- Subst1  : {Σ : Signature} {n : ℕ} (m : ℕ) {k : SyntaxSort} → Expr Σ (suc n + m) k → TmExpr Σ n → Expr Σ (n + m) k
-- Subst1A : {Σ : Signature} {n : ℕ} (m : ℕ) {args : SyntaxArityArgs} → Args Σ (suc n + m) args → TmExpr Σ n → Args Σ (n + m) args

-- Subst1 n (sym s x) a = sym s (Subst1A n x a)
-- Subst1 zero (var last) a = a
-- Subst1 zero (var (prev x)) a = var x
-- Subst1 (suc m) (var last) a = var last
-- Subst1 (suc m) (var (prev x)) a = weaken last (Subst1 m (var x) a)

-- Subst1A m [] a = []
-- Subst1A {n = n} m (_,_ {m = k} es e) a = (Subst1A m es a , tr! (assoc {n} {m} {k}) (Subst1 (m + k) (tr (assoc {suc n} {m} {k}) e) a))

Subst  : {Σ : Signature} {l m : ℕ} {k : SyntaxSort} → Expr Σ (m + l) k → Args Σ m (MArityArgs l) → Expr Σ m k
Subst {l = zero} e [] = e
Subst {l = suc l} {m} e (as , a) = Subst (SubstMor e (idMor , weakenL a)) as

SubstM : {Σ Σ' : Signature} {m : ℕ} {args : SyntaxArityArgs}
      → (Σ →Sig Σ') m
      → Args Σ' m args
      → ((ExtSig^ Σ args) →Sig Σ') m
SubstM ↑ [] = ↑
SubstM ↑ (as , a) $ prev s = SubstM ↑ as $ s
(SubstM ↑ (_,_ {m = l} as a)) $ new = Subst (weaken' {{≤+ l}} (prev^last _ l) a)

subst : {n m : ℕ} {k : SyntaxSort} {Σ Σ' : Signature} (↑ : (Σ →Sig Σ') n) {args : SyntaxArityArgs} (as : Args Σ' (n + m) args)
      → Expr (ExtSig^ Σ args) (n + m) k
      → Expr Σ' (n + m) k
subst {m = m} ↑ as e = ↑Expr (SubstM (liftSig ↑) as) e

-- {-
-- Example:

-- args = ((0, Ty), (1, Ty), (1, Tm))
-- ExtSig^ Σ args = Σ + {A} + {B} + {u} where A has arity ((), Ty), B has arity ((0, Tm), Ty), u has arity ((0, Tm), Tm)
-- To get a map from it to Σ', we need
-- - a map from Σ to Σ'
-- - a type expression in Σ' (for A)
-- - a type expression in Σ' in scope (m + 1)  (for B)
-- - a term expression in Σ' in scope (m + 1)  (for u)
-- -}

max_stars_repo_name: guillaumebrunerie/general-type-theories

max_issues_repo_name: guillaumebrunerie/general-type-theories

max_forks_repo_name: guillaumebrunerie/general-type-theories


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

module Relation.Nullary.Decidable.Logic where

open import Prelude
open import Data.Sum
open import Relation.Nullary.Decidable

disj : (A → C) → (B → C) → (¬ A → ¬ B → ¬ C) → Dec A → Dec B → Dec C
disj l r n x y .does = x .does or y .does
disj l r n (yes x) y .why = l x
disj l r n (no  x) (yes y) .why = r y
disj l r n (no ¬x) (no ¬y) .why = n ¬x ¬y

conj : (A → B → C) → (¬ A → ¬ C) → (¬ B → ¬ C) → Dec A → Dec B → Dec C
conj c l r x y .does = x .does and y .does
conj c l r (no ¬x) y .why = l ¬x
conj c l r (yes x) (no ¬y) .why = r ¬y
conj c l r (yes x) (yes y) .why = c x y

negate : (A → ¬ B) → (¬ A → B) → Dec A → Dec B
negate t f d .does = not (d .does)
negate t f (yes d) .why = t d
negate t f (no ¬d) .why = f ¬d

! : Dec A → Dec (¬ A)
! = negate (λ x ¬x → ¬x x) id

infixl 7 _&&_
_&&_ : Dec A → Dec B → Dec (A × B)
_&&_ = conj _,_ (_∘ fst) (_∘ snd)

infixl 6 _||_
_||_ : Dec A → Dec B → Dec (A ⊎ B)
_||_ = disj inl inr either

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground