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

module Properties.TypeCheck where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Bool using (Bool; true; false)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import FFI.Data.Either using (Either)
open import Luau.TypeCheck using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; string; app; function; block; binexp; done; return; local; nothing; orUnknown; tgtBinOp)
open import Luau.Syntax using (Block; Expr; Value; BinaryOperator; yes; nil; addr; number; bool; string; val; var; binexp; _$_; function_is_end; block_is_end; _∙_; return; done; local_←_; _⟨_⟩; _⟨_⟩∈_; var_∈_; name; fun; arg; +; -; *; /; <; >; ==; ~=; <=; >=)
open import Luau.Type using (Type; nil; unknown; never; number; boolean; string; _⇒_; src; tgt)
open import Luau.RuntimeType using (RuntimeType; nil; number; function; string; valueType)
open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_) renaming (_[_] to _[_]ⱽ)
open import Luau.Addr using (Addr)
open import Luau.Var using (Var; _≡ⱽ_)
open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ)
open import Properties.Contradiction using (CONTRADICTION)
open import Properties.Dec using (yes; no)
open import Properties.Equality using (_≢_; sym; trans; cong)
open import Properties.Product using (_×_; _,_)
open import Properties.Remember using (Remember; remember; _,_)

typeOfᴼ : Object yes → Type
typeOfᴼ (function f ⟨ var x ∈ S ⟩∈ T is B end) = (S ⇒ T)

typeOfᴹᴼ : Maybe(Object yes) → Maybe Type
typeOfᴹᴼ nothing = nothing
typeOfᴹᴼ (just O) = just (typeOfᴼ O)

typeOfⱽ : Heap yes → Value → Maybe Type
typeOfⱽ H nil = just nil
typeOfⱽ H (bool b) = just boolean
typeOfⱽ H (addr a) = typeOfᴹᴼ (H [ a ]ᴴ)
typeOfⱽ H (number n) = just number
typeOfⱽ H (string x) = just string

typeOfᴱ : Heap yes → VarCtxt → (Expr yes) → Type
typeOfᴮ : Heap yes → VarCtxt → (Block yes) → Type

typeOfᴱ H Γ (var x) = orUnknown(Γ [ x ]ⱽ)
typeOfᴱ H Γ (val v) = orUnknown(typeOfⱽ H v)
typeOfᴱ H Γ (M $ N) = tgt(typeOfᴱ H Γ M)
typeOfᴱ H Γ (function f ⟨ var x ∈ S ⟩∈ T is B end) = S ⇒ T
typeOfᴱ H Γ (block var b ∈ T is B end) = T
typeOfᴱ H Γ (binexp M op N) = tgtBinOp op

typeOfᴮ H Γ (function f ⟨ var x ∈ S ⟩∈ T is C end ∙ B) = typeOfᴮ H (Γ ⊕ f ↦ (S ⇒ T)) B
typeOfᴮ H Γ (local var x ∈ T ← M ∙ B) = typeOfᴮ H (Γ ⊕ x ↦ T) B
typeOfᴮ H Γ (return M ∙ B) = typeOfᴱ H Γ M
typeOfᴮ H Γ done = nil

mustBeFunction : ∀ H Γ v → (never ≢ src (typeOfᴱ H Γ (val v))) → (function ≡ valueType(v))
mustBeFunction H Γ nil p = CONTRADICTION (p refl)
mustBeFunction H Γ (addr a) p = refl
mustBeFunction H Γ (number n) p = CONTRADICTION (p refl)
mustBeFunction H Γ (bool true) p = CONTRADICTION (p refl)
mustBeFunction H Γ (bool false) p = CONTRADICTION (p refl)
mustBeFunction H Γ (string x) p = CONTRADICTION (p refl)

mustBeNumber : ∀ H Γ v → (typeOfᴱ H Γ (val v) ≡ number) → (valueType(v) ≡ number)
mustBeNumber H Γ (addr a) p with remember (H [ a ]ᴴ)
mustBeNumber H Γ (addr a) p | (just O , q) with trans (cong orUnknown (cong typeOfᴹᴼ (sym q))) p
mustBeNumber H Γ (addr a) p | (just function f ⟨ var x ∈ T ⟩∈ U is B end , q) | ()
mustBeNumber H Γ (addr a) p | (nothing , q) with trans (cong orUnknown (cong typeOfᴹᴼ (sym q))) p
mustBeNumber H Γ (addr a) p | nothing , q | ()
mustBeNumber H Γ (number n) p = refl

mustBeString : ∀ H Γ v → (typeOfᴱ H Γ (val v) ≡ string) → (valueType(v) ≡ string)
mustBeString H Γ (addr a) p with remember (H [ a ]ᴴ)
mustBeString H Γ (addr a) p | (just O , q) with trans (cong orUnknown (cong typeOfᴹᴼ (sym q))) p
mustBeString H Γ (addr a) p | (just function f ⟨ var x ∈ T ⟩∈ U is B end , q) | ()
mustBeString H Γ (addr a) p | (nothing , q) with trans (cong orUnknown (cong typeOfᴹᴼ (sym q))) p
mustBeString H Γ (addr a) p | (nothing , q) | ()
mustBeString H Γ (string x) p = refl

typeCheckᴱ : ∀ H Γ M → (Γ ⊢ᴱ M ∈ (typeOfᴱ H Γ M))
typeCheckᴮ : ∀ H Γ B → (Γ ⊢ᴮ B ∈ (typeOfᴮ H Γ B))

typeCheckᴱ H Γ (var x) = var refl
typeCheckᴱ H Γ (val nil) = nil
typeCheckᴱ H Γ (val (addr a)) = addr (orUnknown (typeOfᴹᴼ (H [ a ]ᴴ)))
typeCheckᴱ H Γ (val (number n)) = number
typeCheckᴱ H Γ (val (bool b)) = bool
typeCheckᴱ H Γ (val (string x)) = string
typeCheckᴱ H Γ (M $ N) = app (typeCheckᴱ H Γ M) (typeCheckᴱ H Γ N)
typeCheckᴱ H Γ (function f ⟨ var x ∈ T ⟩∈ U is B end) = function (typeCheckᴮ H (Γ ⊕ x ↦ T) B)
typeCheckᴱ H Γ (block var b ∈ T is B end) = block (typeCheckᴮ H Γ B)
typeCheckᴱ H Γ (binexp M op N) = binexp (typeCheckᴱ H Γ M) (typeCheckᴱ H Γ N)

typeCheckᴮ H Γ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) = function (typeCheckᴮ H (Γ ⊕ x ↦ T) C) (typeCheckᴮ H (Γ ⊕ f ↦ (T ⇒ U)) B)
typeCheckᴮ H Γ (local var x ∈ T ← M ∙ B) = local (typeCheckᴱ H Γ M) (typeCheckᴮ H (Γ ⊕ x ↦ T) B)
typeCheckᴮ H Γ (return M ∙ B) = return (typeCheckᴱ H Γ M) (typeCheckᴮ H Γ B)
typeCheckᴮ H Γ done = done

typeCheckᴼ : ∀ H O → (⊢ᴼ O)
typeCheckᴼ H nothing = nothing
typeCheckᴼ H (just function f ⟨ var x ∈ T ⟩∈ U is B end) = function (typeCheckᴮ H (x ↦ T) B)

typeCheckᴴ : ∀ H → (⊢ᴴ H)
typeCheckᴴ H a {O} p = typeCheckᴼ H (O)

typeCheckᴴᴱ : ∀ H Γ M → (Γ ⊢ᴴᴱ H ▷ M ∈ typeOfᴱ H Γ M)
typeCheckᴴᴱ H Γ M = (typeCheckᴴ H , typeCheckᴱ H Γ M)

typeCheckᴴᴮ : ∀ H Γ M → (Γ ⊢ᴴᴮ H ▷ M ∈ typeOfᴮ H Γ M)
typeCheckᴴᴮ H Γ M = (typeCheckᴴ H , typeCheckᴮ H Γ M)

max_stars_repo_name: MeltzDev/luau

max_issues_repo_name: MeltzDev/luau

max_forks_repo_name: MeltzDev/luau


text:
open import Oscar.Prelude
open import Oscar.Data.¶
open import Oscar.Data.Descender
open import Oscar.Data.Fin
open import Oscar.Data.Term

module Oscar.Data.Substitist where

module Substitist {𝔭} (𝔓 : Ø 𝔭) where

  open Term 𝔓

  Substitist = flip Descender⟨ (λ n-o → Fin (↑ n-o) × Term n-o) ⟩

ext: agda


text:
module Type where

open import Type.Core   public
open import Type.NbE    public
open import Type.Lemmas public

max_stars_repo_name: AriFordsham/plutus

max_issues_repo_name: AriFordsham/plutus

max_forks_repo_name: AriFordsham/plutus


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

module Data.Sigma where

open import Data.Sigma.Base public

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
{-# OPTIONS --sized-types #-}
module SOList.Lower {A : Set}(_≤_ : A → A → Set)  where

open import Data.List
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Size

data SOList : {ι : Size} → Bound → Set where
  onil : {ι : Size}{b : Bound}
                   → SOList {↑ ι} b
  :< : {ι : Size}{b : Bound}{x : A}
                   → LeB b (val x)
                   → SOList {ι} (val x)
                   → SOList {↑ ι} b

forget : {b : Bound} → SOList b → List A
forget onil = []
forget (:< {x = x} _  xs) = x ∷ forget xs

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

module Cubical.Categories.Type where

open import Cubical.Foundations.Prelude
open import Cubical.Categories.Category

module _ ℓ where
  TYPE : Precategory (ℓ-suc ℓ) ℓ
  TYPE .ob = Type ℓ
  TYPE .hom A B = A → B
  TYPE .idn A  = λ x → x
  TYPE .seq f g = λ x → g (f x)
  TYPE .seq-λ f = refl
  TYPE .seq-ρ f = refl
  TYPE .seq-α f g h = refl

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


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

open import HoTT

module homotopy.WedgeExtension
  {i j} {A : Type i} {a₀ : A} {B : Type j} {b₀ : B} where

  -- easier to keep track of than a long list of arguments
  record args : Type (lmax (lsucc i) (lsucc j)) where
    field
      n m : ℕ₋₂
      {{cA}} : is-connected (S n) A
      {{cB}} : is-connected (S m) B
      P : A → B → (n +2+ m) -Type (lmax i j)
      f : (a : A) → fst (P a b₀)
      g : (b : B) → fst (P a₀ b)
      p : f a₀ == g b₀

  private
    module _ (r : args) where
      open args r

      Q : A → n -Type (lmax i j)
      Q a = ((Σ (∀ b → fst (P a b)) (λ k → (k ∘ cst b₀) == cst (f a)) ,
                conn-extend-general (pointed-conn-out B b₀)
                                    (P a) (cst (f a))))

      l : Π A (fst ∘ Q)
      l = conn-extend (pointed-conn-out A a₀)
                      Q (λ (_ : Unit) → (g , ap cst (! p)))

  module _ (r : args) where
    open args r

    ext : ∀ a → ∀ b → fst (P a b)
    ext a = fst (l r a)

  module _ {r : args} where
    open args r

    abstract
      β-l : ∀ a → ext r a b₀ == f a
      β-l a = ap (λ t → t unit) (snd (l r a))

    private
      abstract
        β-r-aux : fst (l r a₀) == g
        β-r-aux = fst= (conn-extend-β
          (pointed-conn-out A a₀)
          (Q r) (λ (_ : Unit) → (g , ap cst (! p))) unit)

    abstract
      β-r : ∀ b → ext r a₀ b == g b
      β-r = app= β-r-aux

    abstract
      coh : ! (β-l a₀) ∙ β-r b₀ == p
      coh =
        ! (β-l a₀) ∙ β-r b₀
          =⟨ ! lemma₂ |in-ctx (λ w → ! w ∙ β-r b₀) ⟩
        ! (β-r b₀ ∙ ! p) ∙ β-r b₀
          =⟨ !-∙ (β-r b₀) (! p) |in-ctx (λ w → w ∙ β-r b₀) ⟩
        (! (! p) ∙ ! (β-r b₀)) ∙ β-r b₀
          =⟨ ∙-assoc (! (! p)) (! (β-r b₀)) (β-r b₀) ⟩
        ! (! p) ∙ (! (β-r b₀) ∙ β-r b₀)
          =⟨ ap2 _∙_ (!-! p) (!-inv-l (β-r b₀)) ⟩
        p ∙ idp
          =⟨ ∙-unit-r p ⟩
        p =∎
        where
        lemma₁ : β-l a₀ == ap (λ s → s unit) (ap cst (! p))
                 [ (λ k → k b₀ == f a₀) ↓ β-r-aux ]
        lemma₁ = ap↓ (ap (λ s → s unit)) $
                      snd= (conn-extend-β (pointed-conn-out A a₀)
                           (Q r) (λ (_ : Unit) → (g , ap cst (! p))) unit)

        lemma₂ : β-r b₀ ∙ ! p == β-l a₀
        lemma₂ = ap (λ w → β-r b₀ ∙ w)
                    (! (ap-idf (! p)) ∙ ap-∘ (λ s → s unit) cst (! p))
                 ∙ (! (↓-app=cst-out lemma₁))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
{-

 This file contains a proof of the following fact:
 for a commutative ring R with elements f and g s.t.
 ⟨f,g⟩ = R, we get a get a pullback square

                 _/1
            R   ----> R[1/f]
              ⌟
       _/1  |         | χ₁
            v         v

            R[1/g] -> R[1/fg]
                   χ₂

 where the morphisms χ are induced by the universal property
 of localization.

 -}

{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.CommRing.Localisation.PullbackSquare where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Powerset renaming (_∈_ to _∈ₚ_)
open import Cubical.Foundations.Transport
open import Cubical.Functions.FunExtEquiv

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Bool
open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_
                                      ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc
                                      ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Vec
open import Cubical.Data.Sigma.Base
open import Cubical.Data.Sigma.Properties
open import Cubical.Data.FinData
open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary

open import Cubical.Algebra.Group
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Localisation.Base
open import Cubical.Algebra.CommRing.Localisation.UniversalProperty
open import Cubical.Algebra.CommRing.Localisation.InvertingElements
open import Cubical.Algebra.CommRing.Ideal
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.RadicalIdeal

open import Cubical.Algebra.RingSolver.Reflection

open import Cubical.HITs.SetQuotients as SQ
open import Cubical.HITs.PropositionalTruncation as PT

open import Cubical.Categories.Category.Base
open import Cubical.Categories.Instances.CommRings
open import Cubical.Categories.Limits.Pullback

open Iso

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ

module _ (R' : CommRing ℓ) (f g : (fst R')) where

 open IsRingHom
 open isMultClosedSubset
 open CommRingTheory R'
 open RingTheory (CommRing→Ring R')
 open CommIdeal R'
 open RadicalIdeal R'
 open Exponentiation R'
 open InvertingElementsBase R'

 open CommRingStr ⦃...⦄
 private
  R = R' .fst
  ⟨_⟩ : {n : ℕ} → FinVec R n → CommIdeal
  ⟨ V ⟩ = ⟨ V ⟩[ R' ]
  fgVec : FinVec R 2
  fgVec zero = f
  fgVec (suc zero) = g
  ⟨f,g⟩ = ⟨ fgVec ⟩
  fⁿgⁿVec : (n : ℕ) → FinVec R 2
  fⁿgⁿVec n zero = f ^ n
  fⁿgⁿVec n (suc zero) = g ^ n
  ⟨fⁿ,gⁿ⟩ : (n : ℕ) → CommIdeal
  ⟨fⁿ,gⁿ⟩ n = ⟨ (fⁿgⁿVec n) ⟩

  instance
   _ = R' .snd
   _ = R[1/ f ]AsCommRing .snd
   _ = R[1/ g ]AsCommRing .snd
   _ = R[1/ (R' .snd .CommRingStr._·_ f g) ]AsCommRing .snd

 open Loc R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f)
      renaming (_≈_ to _≈ᶠ_ ; locIsEquivRel to locIsEquivRelᶠ ; S to Sᶠ)
 open S⁻¹RUniversalProp R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f)
      renaming ( _/1 to _/1ᶠ ; /1AsCommRingHom to /1ᶠAsCommRingHom
               ; S⁻¹RHasUniversalProp to R[1/f]HasUniversalProp)
 open Loc R' [ g ⁿ|n≥0] (powersFormMultClosedSubset g)
      renaming (_≈_ to _≈ᵍ_ ; locIsEquivRel to locIsEquivRelᵍ ; S to Sᵍ)
 open S⁻¹RUniversalProp R' [ g ⁿ|n≥0] (powersFormMultClosedSubset g)
      renaming ( _/1 to _/1ᵍ ; /1AsCommRingHom to /1ᵍAsCommRingHom
               ; S⁻¹RHasUniversalProp to R[1/g]HasUniversalProp)
 open Loc R' [ (f · g) ⁿ|n≥0] (powersFormMultClosedSubset (f · g))
      renaming (_≈_ to _≈ᶠᵍ_ ; locIsEquivRel to locIsEquivRelᶠᵍ ; S to Sᶠᵍ)
 open S⁻¹RUniversalProp R' [ (f · g) ⁿ|n≥0] (powersFormMultClosedSubset (f · g))
      renaming ( _/1 to _/1ᶠᵍ ; /1AsCommRingHom to /1ᶠᵍAsCommRingHom)

 -- the pullback legs
 private
  -- using RadicalLemma doesn't compute...
  χ₁ : CommRingHom R[1/ f ]AsCommRing R[1/ (f · g) ]AsCommRing
  χ₁ = R[1/f]HasUniversalProp _ /1ᶠᵍAsCommRingHom unitHelper .fst .fst
   where
   unitHelper : ∀ s → s ∈ₚ [ f ⁿ|n≥0] → s /1ᶠᵍ ∈ₚ (R[1/ (f · g) ]AsCommRing) ˣ
   unitHelper = powersPropElim (λ s → Units.inverseUniqueness _ (s /1ᶠᵍ))
                  λ n → [ g ^ n , (f · g) ^ n , ∣ n , refl ∣ ]
                        , eq/ _ _ ((1r , powersFormMultClosedSubset (f · g) .containsOne)
                        , path n)
    where
    useSolver1 : ∀ a b → 1r · (a · b) · 1r ≡ a · b
    useSolver1 = solve R'
    useSolver2 : ∀ a → a ≡ (1r · 1r) · (1r · a)
    useSolver2 = solve R'

    path : (n : ℕ) → 1r · (f ^ n · g ^ n) · 1r ≡ (1r · 1r) · (1r · ((f · g) ^ n))
    path n = useSolver1 _ _ ∙ sym (^-ldist-· f g n) ∙ useSolver2 _

  χ₂ : CommRingHom R[1/ g ]AsCommRing R[1/ (f · g) ]AsCommRing
  χ₂ = R[1/g]HasUniversalProp _ /1ᶠᵍAsCommRingHom unitHelper .fst .fst
   where
   unitHelper : ∀ s → s ∈ₚ [ g ⁿ|n≥0] → s /1ᶠᵍ ∈ₚ (R[1/ (f · g) ]AsCommRing) ˣ
   unitHelper = powersPropElim (λ s → Units.inverseUniqueness _ (s /1ᶠᵍ))
                  λ n → [ f ^ n , (f · g) ^ n , ∣ n , refl ∣ ]
                        , eq/ _ _ ((1r , powersFormMultClosedSubset (f · g) .containsOne)
                              , path n)
    where
    useSolver1 : ∀ a b → 1r · (a · b) · 1r ≡ b · a
    useSolver1 = solve R'
    useSolver2 : ∀ a → a ≡ (1r · 1r) · (1r · a)
    useSolver2 = solve R'

    path : (n : ℕ) → 1r · (g ^ n · f ^ n) · 1r ≡ (1r · 1r) · (1r · ((f · g) ^ n))
    path n = useSolver1 _ _ ∙ sym (^-ldist-· f g n) ∙ useSolver2 _

 injectivityLemma : 1r ∈ ⟨f,g⟩ → ∀ (x : R) → x /1ᶠ ≡ 0r → x /1ᵍ ≡ 0r → x ≡ 0r
 injectivityLemma 1∈⟨f,g⟩ x x≡0overF x≡0overG =
                    PT.rec2 (is-set _ _) annihilatorHelper exAnnihilatorF exAnnihilatorG
  where
  exAnnihilatorF : ∃[ s ∈ Sᶠ ] (fst s · x · 1r ≡ fst s · 0r · 1r)
  exAnnihilatorF = isEquivRel→TruncIso locIsEquivRelᶠ _ _ .fun x≡0overF

  exAnnihilatorG : ∃[ s ∈ Sᵍ ] (fst s · x · 1r ≡ fst s · 0r · 1r)
  exAnnihilatorG = isEquivRel→TruncIso locIsEquivRelᵍ _ _ .fun x≡0overG

  annihilatorHelper : Σ[ s ∈ Sᶠ ] (fst s · x · 1r ≡ fst s · 0r · 1r)
                    → Σ[ s ∈ Sᵍ ] (fst s · x · 1r ≡ fst s · 0r · 1r)
                    → x ≡ 0r
  annihilatorHelper ((u , u∈[fⁿ]) , p) ((v , v∈[gⁿ]) , q) =
                      PT.rec2 (is-set _ _) exponentHelper u∈[fⁿ] v∈[gⁿ]
   where
   ux≡0 : u · x ≡ 0r
   ux≡0 = sym (·Rid _) ∙ p ∙ cong (_· 1r) (0RightAnnihilates _) ∙ (·Rid _)

   vx≡0 : v · x ≡ 0r
   vx≡0 = sym (·Rid _) ∙ q ∙ cong (_· 1r) (0RightAnnihilates _) ∙ (·Rid _)

   exponentHelper : Σ[ n ∈ ℕ ] u ≡ f ^ n
                  → Σ[ n ∈ ℕ ] v ≡ g ^ n
                  → x ≡ 0r
   exponentHelper (n , u≡fⁿ) (m , v≡gᵐ) =
                   PT.rec (is-set _ _) Σhelper (GeneratingPowers.thm R' l _ fgVec 1∈⟨f,g⟩)
    where
    l = max n m

    fˡx≡0 : f ^ l · x ≡ 0r
    fˡx≡0 = f ^ l · x               ≡⟨ cong (λ k → f ^ k · x) (sym (≤-∸-+-cancel left-≤-max)) ⟩
            f ^ ((l ∸ n) +ℕ n) · x  ≡⟨ cong (_· x) (sym (·-of-^-is-^-of-+ _ _ _)) ⟩
            f ^ (l ∸ n) · f ^ n · x ≡⟨ cong (λ y → f ^ (l ∸ n) · y · x) (sym u≡fⁿ) ⟩
            f ^ (l ∸ n) · u · x     ≡⟨ sym (·Assoc _ _ _) ⟩
            f ^ (l ∸ n) · (u · x)   ≡⟨ cong (f ^ (l ∸ n) ·_) ux≡0 ⟩
            f ^ (l ∸ n) · 0r        ≡⟨ 0RightAnnihilates _ ⟩
            0r ∎

    gˡx≡0 : g ^ l · x ≡ 0r
    gˡx≡0 = g ^ l · x               ≡⟨ cong (λ k → g ^ k · x) (sym (≤-∸-+-cancel right-≤-max)) ⟩
            g ^ ((l ∸ m) +ℕ m) · x  ≡⟨ cong (_· x) (sym (·-of-^-is-^-of-+ _ _ _)) ⟩
            g ^ (l ∸ m) · g ^ m · x ≡⟨ cong (λ y → g ^ (l ∸ m) · y · x) (sym v≡gᵐ) ⟩
            g ^ (l ∸ m) · v · x     ≡⟨ sym (·Assoc _ _ _) ⟩
            g ^ (l ∸ m) · (v · x)   ≡⟨ cong (g ^ (l ∸ m) ·_) vx≡0 ⟩
            g ^ (l ∸ m) · 0r        ≡⟨ 0RightAnnihilates _ ⟩
            0r ∎

    Σhelper : Σ[ α ∈ FinVec R 2 ] 1r ≡ α zero · f ^ l + (α (suc zero) · g ^ l + 0r)
            → x ≡ 0r
    Σhelper (α , 1≡α₀fˡ+α₁gˡ+0) = path
     where
     α₀ = α zero
     α₁ = α (suc zero)

     1≡α₀fˡ+α₁gˡ : 1r ≡ α₀ · f ^ l + α₁ · g ^ l
     1≡α₀fˡ+α₁gˡ = 1≡α₀fˡ+α₁gˡ+0 ∙ cong (α₀ · f ^ l +_) (+Rid _)

     path : x ≡ 0r
     path = x                                   ≡⟨ sym (·Lid _) ⟩
            1r · x                              ≡⟨ cong (_· x) 1≡α₀fˡ+α₁gˡ ⟩
            (α₀ · f ^ l + α₁ · g ^ l) · x       ≡⟨ ·Ldist+ _ _ _ ⟩
            α₀ · f ^ l · x + α₁ · g ^ l · x     ≡⟨ cong₂ _+_ (sym (·Assoc _ _ _))
                                                             (sym (·Assoc _ _ _)) ⟩
            α₀ · (f ^ l · x) + α₁ · (g ^ l · x) ≡⟨ cong₂ (λ y z → α₀ · y + α₁ · z)
                                                         fˡx≡0 gˡx≡0 ⟩
            α₀ · 0r + α₁ · 0r                   ≡⟨ cong₂ _+_ (0RightAnnihilates _)
                                                             (0RightAnnihilates _) ∙ +Rid _ ⟩
            0r ∎

 equalizerLemma : 1r ∈ ⟨f,g⟩
                → ∀ (x : R[1/ f ]) (y : R[1/ g ])
                → χ₁ .fst x ≡ χ₂ .fst y
                → ∃![ z ∈ R ] (z /1ᶠ ≡ x) × (z /1ᵍ ≡ y)
 equalizerLemma 1∈⟨f,g⟩ = invElPropElim2 (λ _ _ → isPropΠ (λ _ → isProp∃!)) baseCase
  where
  baseCase : ∀ (x y : R) (n : ℕ)
           → fst χ₁ ([ x , f ^ n , ∣ n , refl ∣ ]) ≡ fst χ₂ ([ y , g ^ n , ∣ n , refl ∣ ])
           → ∃![ z ∈ R ] ((z /1ᶠ ≡ [ x , f ^ n , ∣ n , refl ∣ ])
                        × (z /1ᵍ ≡ [ y , g ^ n , ∣ n , refl ∣ ]))
  baseCase x y n χ₁[x/fⁿ]≡χ₂[y/gⁿ] = PT.rec isProp∃! annihilatorHelper exAnnihilator
   where
   -- doesn't compute that well but at least it computes...
   exAnnihilator : ∃[ s ∈ Sᶠᵍ ] -- s.t.
     (fst s · (x · transport refl (g ^ n)) · (1r · transport refl ((f · g) ^ n))
    ≡ fst s · (y · transport refl (f ^ n)) · (1r · transport refl ((f · g) ^ n)))
   exAnnihilator = isEquivRel→TruncIso locIsEquivRelᶠᵍ _ _ .fun χ₁[x/fⁿ]≡χ₂[y/gⁿ]

   annihilatorHelper : Σ[ s ∈ Sᶠᵍ ]
     (fst s · (x · transport refl (g ^ n)) · (1r · transport refl ((f · g) ^ n))
    ≡ fst s · (y · transport refl (f ^ n)) · (1r · transport refl ((f · g) ^ n)))
    → ∃![ z ∈ R ] ((z /1ᶠ ≡ [ x , f ^ n , ∣ n , refl ∣ ])
                 × (z /1ᵍ ≡ [ y , g ^ n , ∣ n , refl ∣ ]))
   annihilatorHelper ((s , s∈[fgⁿ]) , p) = PT.rec isProp∃! exponentHelper s∈[fgⁿ]
    where
    sxgⁿ[fg]ⁿ≡syfⁿ[fg]ⁿ : s · x · g ^ n · (f · g) ^ n ≡ s · y · f ^ n · (f · g) ^ n
    sxgⁿ[fg]ⁿ≡syfⁿ[fg]ⁿ =
       s · x · g ^ n · (f · g) ^ n

      ≡⟨ transpHelper _ _ _ _ ⟩

       s · x · transport refl (g ^ n) · transport refl ((f · g) ^ n)

      ≡⟨ useSolver _ _ _ _ ⟩

       s · (x · transport refl (g ^ n)) · (1r · transport refl ((f · g) ^ n))

      ≡⟨ p ⟩

       s · (y · transport refl (f ^ n)) · (1r · transport refl ((f · g) ^ n))

      ≡⟨ sym (useSolver _ _ _ _) ⟩

       s · y · transport refl (f ^ n) · transport refl ((f · g) ^ n)

      ≡⟨ sym (transpHelper _ _ _ _) ⟩

       s · y · f ^ n · (f · g) ^ n ∎

      where
      transpHelper : ∀ a b c d → a · b · c · d
                               ≡ a · b · transport refl c · transport refl d
      transpHelper a b c d i = a · b · transportRefl c (~ i) · transportRefl d (~ i)
      useSolver : ∀ a b c d → a · b · c · d ≡ a · (b · c) · (1r · d)
      useSolver = solve R'

    exponentHelper : Σ[ m ∈ ℕ ] s ≡ (f · g) ^ m
                   → ∃![ z ∈ R ] ((z /1ᶠ ≡ [ x , f ^ n , ∣ n , refl ∣ ])
                                × (z /1ᵍ ≡ [ y , g ^ n , ∣ n , refl ∣ ]))
    exponentHelper (m , s≡[fg]ᵐ) =
       PT.rec isProp∃! Σhelper (GeneratingPowers.thm R' 2n+m _ fgVec 1∈⟨f,g⟩)
     where
     -- the path we'll actually work with
     xgⁿ[fg]ⁿ⁺ᵐ≡yfⁿ[fg]ⁿ⁺ᵐ : x · g ^ n · (f · g) ^ (n +ℕ m) ≡ y · f ^ n · (f · g) ^ (n +ℕ m)
     xgⁿ[fg]ⁿ⁺ᵐ≡yfⁿ[fg]ⁿ⁺ᵐ =
        x · g ^ n · (f · g) ^ (n +ℕ m)

       ≡⟨ cong (x · (g ^ n) ·_) (sym (·-of-^-is-^-of-+ _ _ _)) ⟩

        x · g ^ n · ((f · g) ^ n · (f · g) ^ m)

       ≡⟨ useSolver _ _ _ _ ⟩

         (f · g) ^ m · x · g ^ n · (f · g) ^ n

       ≡⟨ cong (λ a → a · x · g ^ n · (f · g) ^ n) (sym s≡[fg]ᵐ) ⟩

         s · x · g ^ n · (f · g) ^ n

       ≡⟨ sxgⁿ[fg]ⁿ≡syfⁿ[fg]ⁿ ⟩

         s · y · f ^ n · (f · g) ^ n

       ≡⟨ cong (λ a → a · y · f ^ n · (f · g) ^ n) s≡[fg]ᵐ ⟩

         (f · g) ^ m · y · f ^ n · (f · g) ^ n

       ≡⟨ sym (useSolver _ _ _ _)  ⟩

         y · f ^ n · ((f · g) ^ n · (f · g) ^ m)

       ≡⟨ cong (y · (f ^ n) ·_) (·-of-^-is-^-of-+ _ _ _) ⟩

        y · f ^ n · (f · g) ^ (n +ℕ m) ∎

       where
       useSolver : ∀ a b c d → a · b · (c · d) ≡ d · a · b · c
       useSolver = solve R'

     -- critical exponent
     2n+m = n +ℕ (n +ℕ m)
     -- extracting information from the fact that R=⟨f,g⟩
     Σhelper : Σ[ α ∈ FinVec R 2 ] 1r ≡ linearCombination R' α (fⁿgⁿVec 2n+m)
             → ∃![ z ∈ R ] ((z /1ᶠ ≡ [ x , f ^ n , ∣ n , refl ∣ ])
                          × (z /1ᵍ ≡ [ y , g ^ n , ∣ n , refl ∣ ]))
     Σhelper (α , linCombi) = uniqueExists z (z/1≡x/fⁿ , z/1≡y/gⁿ)
                                             (λ _ → isProp× (is-set _ _) (is-set _ _))
                                             uniqueness
      where
      α₀ = α zero
      α₁ = α (suc zero)

      1≡α₀f²ⁿ⁺ᵐ+α₁g²ⁿ⁺ᵐ : 1r ≡ α₀ · f ^ 2n+m + α₁ · g ^ 2n+m
      1≡α₀f²ⁿ⁺ᵐ+α₁g²ⁿ⁺ᵐ = linCombi ∙ cong (α₀ · f ^ 2n+m +_) (+Rid _)

      -- definition of the element
      z = α₀ · x · f ^ (n +ℕ m) + α₁ · y · g ^ (n +ℕ m)

      z/1≡x/fⁿ : (z /1ᶠ) ≡ [ x , f ^ n , ∣ n , refl ∣ ]
      z/1≡x/fⁿ = eq/ _ _ ((f ^ (n +ℕ m) , ∣ n +ℕ m , refl ∣) , path)
       where
       useSolver1 : ∀ x y α₀ α₁ fⁿ⁺ᵐ gⁿ⁺ᵐ fⁿ
                  → fⁿ⁺ᵐ · (α₀ · x · fⁿ⁺ᵐ + α₁ · y · gⁿ⁺ᵐ) · fⁿ
                  ≡ fⁿ⁺ᵐ · (α₀ · x · (fⁿ · fⁿ⁺ᵐ)) + α₁ · (y · fⁿ · (fⁿ⁺ᵐ · gⁿ⁺ᵐ))
       useSolver1 = solve R'

       useSolver2 : ∀ x α₀ α₁ fⁿ⁺ᵐ g²ⁿ⁺ᵐ f²ⁿ⁺ᵐ
                  → fⁿ⁺ᵐ · (α₀ · x · f²ⁿ⁺ᵐ) + α₁ · (x · fⁿ⁺ᵐ · g²ⁿ⁺ᵐ)
                  ≡ fⁿ⁺ᵐ · x · (α₀ · f²ⁿ⁺ᵐ + α₁ · g²ⁿ⁺ᵐ)
       useSolver2 = solve R'

       path : f ^ (n +ℕ m) · z · f ^ n ≡ f ^ (n +ℕ m) · x · 1r
       path =
           f ^ (n +ℕ m) · z · f ^ n

         ≡⟨ useSolver1 _ _ _ _ _ _ _ ⟩

           f ^ (n +ℕ m) · (α₀ · x · (f ^ n · f ^ (n +ℕ m))) + α₁ · (y · f ^ n · (f ^ (n +ℕ m) · g ^ (n +ℕ m)))

         ≡⟨ cong₂ (λ a b → f ^ (n +ℕ m) · (α₀ · x · a) + α₁ · ((y · f ^ n) · b))
                  (·-of-^-is-^-of-+ _ _ _) (sym (^-ldist-· _ _ _)) ⟩

           f ^ (n +ℕ m) · (α₀ · x · (f ^ 2n+m)) + α₁ · (y · f ^ n · (f · g) ^ (n +ℕ m))

         ≡⟨ cong (λ a → f ^ (n +ℕ m) · (α₀ · x · f ^ 2n+m) + α₁ · a)
                 (sym xgⁿ[fg]ⁿ⁺ᵐ≡yfⁿ[fg]ⁿ⁺ᵐ) ⟩

           f ^ (n +ℕ m) · (α₀ · x · (f ^ 2n+m)) + α₁ · (x · g ^ n · (f · g) ^ (n +ℕ m))

         ≡⟨ cong (λ a → f ^ (n +ℕ m) · (α₀ · x · (f ^ 2n+m)) + α₁ · (x · g ^ n · a)) (^-ldist-· _ _ _)  ⟩

           f ^ (n +ℕ m) · (α₀ · x · (f ^ 2n+m)) + α₁ · (x · g ^ n · (f ^ (n +ℕ m) · g ^ (n +ℕ m)))

         ≡⟨ cong (λ a → f ^ (n +ℕ m) · (α₀ · x · (f ^ 2n+m)) + α₁ · a) (·CommAssocSwap _ _ _ _) ⟩

           f ^ (n +ℕ m) · (α₀ · x · (f ^ 2n+m)) + α₁ · (x · f ^ (n +ℕ m) · (g ^ n · g ^ (n +ℕ m)))

         ≡⟨ cong (λ a → f ^ (n +ℕ m) · (α₀ · x · (f ^ 2n+m)) + α₁ · (x · f ^ (n +ℕ m) · a))
                 (·-of-^-is-^-of-+ _ _ _) ⟩

           f ^ (n +ℕ m) · (α₀ · x · (f ^ 2n+m)) + α₁ · (x · f ^ (n +ℕ m) · g ^ 2n+m)

         ≡⟨ useSolver2 _ _ _ _ _ _ ⟩

           f ^ (n +ℕ m) · x · (α₀ · f ^ 2n+m + α₁ · g ^ 2n+m)

         ≡⟨ cong (f ^ (n +ℕ m) · x ·_) (sym 1≡α₀f²ⁿ⁺ᵐ+α₁g²ⁿ⁺ᵐ) ⟩

           f ^ (n +ℕ m) · x · 1r ∎

      z/1≡y/gⁿ : (z /1ᵍ) ≡ [ y , g ^ n , ∣ n , refl ∣ ]
      z/1≡y/gⁿ = eq/ _ _ ((g ^ (n +ℕ m) , ∣ n +ℕ m , refl ∣) , path)
       where
       useSolver1 : ∀ x y α₀ α₁ fⁿ⁺ᵐ gⁿ⁺ᵐ gⁿ
                  → gⁿ⁺ᵐ · (α₀ · x · fⁿ⁺ᵐ + α₁ · y · gⁿ⁺ᵐ) · gⁿ
                  ≡ α₀ · (x · gⁿ · (fⁿ⁺ᵐ · gⁿ⁺ᵐ)) + gⁿ⁺ᵐ · (α₁ · y · (gⁿ · gⁿ⁺ᵐ))
       useSolver1 = solve R'

       useSolver2 : ∀ y α₀ α₁ gⁿ⁺ᵐ g²ⁿ⁺ᵐ f²ⁿ⁺ᵐ
                  → α₀ · (y · f²ⁿ⁺ᵐ · gⁿ⁺ᵐ) + gⁿ⁺ᵐ · (α₁ · y · g²ⁿ⁺ᵐ)
                  ≡ gⁿ⁺ᵐ · y · (α₀ · f²ⁿ⁺ᵐ + α₁ · g²ⁿ⁺ᵐ)
       useSolver2 = solve R'

       path : g ^ (n +ℕ m) · z · g ^ n ≡ g ^ (n +ℕ m) · y · 1r
       path =
           g ^ (n +ℕ m) · z · g ^ n

         ≡⟨ useSolver1 _ _ _ _ _ _ _ ⟩

           α₀ · (x · g ^ n · (f ^ (n +ℕ m) · g ^ (n +ℕ m))) + g ^ (n +ℕ m) · (α₁ · y · (g ^ n · g ^ (n +ℕ m)))

         ≡⟨ cong₂ (λ a b → α₀ · (x · g ^ n · a) + g ^ (n +ℕ m) · (α₁ · y · b))
                  (sym (^-ldist-· _ _ _)) (·-of-^-is-^-of-+ _ _ _) ⟩

           α₀ · (x · g ^ n · (f · g) ^ (n +ℕ m)) + g ^ (n +ℕ m) · (α₁ · y · g ^ 2n+m)

         ≡⟨ cong (λ a → α₀ · a + g ^ (n +ℕ m) · (α₁ · y · g ^ 2n+m))
                 xgⁿ[fg]ⁿ⁺ᵐ≡yfⁿ[fg]ⁿ⁺ᵐ ⟩

           α₀ · (y · f ^ n · (f · g) ^ (n +ℕ m)) + g ^ (n +ℕ m) · (α₁ · y · g ^ 2n+m)

         ≡⟨ cong (λ a → α₀ · (y · f ^ n · a) + g ^ (n +ℕ m) · (α₁ · y · g ^ 2n+m)) (^-ldist-· _ _ _) ⟩

           α₀ · (y · f ^ n · (f ^ (n +ℕ m) · g ^ (n +ℕ m))) + g ^ (n +ℕ m) · (α₁ · y · g ^ 2n+m)

         ≡⟨ cong (λ a → α₀ · a + g ^ (n +ℕ m) · (α₁ · y · g ^ 2n+m)) (·-assoc2 _ _ _ _) ⟩

           α₀ · (y · (f ^ n · f ^ (n +ℕ m)) · g ^ (n +ℕ m)) + g ^ (n +ℕ m) · (α₁ · y · g ^ 2n+m)

         ≡⟨ cong (λ a → α₀ · (y · a · g ^ (n +ℕ m)) + g ^ (n +ℕ m) · (α₁ · y · g ^ 2n+m))
                 (·-of-^-is-^-of-+ _ _ _) ⟩

           α₀ · (y · f ^ 2n+m · g ^ (n +ℕ m)) + g ^ (n +ℕ m) · (α₁ · y · g ^ 2n+m)

         ≡⟨ useSolver2 _ _ _ _ _ _ ⟩

           g ^ (n +ℕ m) · y · (α₀ · f ^ 2n+m + α₁ · g ^ 2n+m)

         ≡⟨ cong (g ^ (n +ℕ m) · y ·_) (sym 1≡α₀f²ⁿ⁺ᵐ+α₁g²ⁿ⁺ᵐ) ⟩

           g ^ (n +ℕ m) · y · 1r ∎

      uniqueness : ∀ a → ((a /1ᶠ) ≡ [ x , f ^ n , ∣ n , refl ∣ ])
                       × ((a /1ᵍ) ≡ [ y , g ^ n , ∣ n , refl ∣ ])
                       → z ≡ a
      uniqueness a (a/1≡x/fⁿ , a/1≡y/gⁿ) = equalByDifference _ _
                   (injectivityLemma 1∈⟨f,g⟩ (z - a) [z-a]/1≡0overF [z-a]/1≡0overG)
       where
       [z-a]/1≡0overF : (z - a) /1ᶠ ≡ 0r
       [z-a]/1≡0overF = (z - a) /1ᶠ

                      ≡⟨ /1ᶠAsCommRingHom .snd .pres+ _ _ ⟩ -- (-a)/1=-(a/1) by refl!

                        (z /1ᶠ) - (a /1ᶠ)

                      ≡⟨ cong₂ _-_ z/1≡x/fⁿ a/1≡x/fⁿ ⟩

                        [ x , f ^ n , ∣ n , refl ∣ ] - [ x , f ^ n , ∣ n , refl ∣ ]

                      ≡⟨ +Rinv ([ x , f ^ n , ∣ n , refl ∣ ]) ⟩

                        0r ∎

       [z-a]/1≡0overG : (z - a) /1ᵍ ≡ 0r
       [z-a]/1≡0overG = (z - a) /1ᵍ

                      ≡⟨ /1ᵍAsCommRingHom .snd .pres+ _ _ ⟩ -- (-a)/1=-(a/1) by refl!

                        (z /1ᵍ) - (a /1ᵍ)

                      ≡⟨ cong₂ _-_ z/1≡y/gⁿ a/1≡y/gⁿ ⟩

                        [ y , g ^ n , ∣ n , refl ∣ ] - [ y , g ^ n , ∣ n , refl ∣ ]

                      ≡⟨ +Rinv ([ y , g ^ n , ∣ n , refl ∣ ]) ⟩

                        0r ∎

 {-
 putting everything together with the pullback machinery:
 If ⟨f,g⟩ = R then we get a square

                 _/1ᶠ
            R   ----> R[1/f]
              ⌟
       _/1ᵍ |         | χ₁
            v         v

            R[1/g] -> R[1/fg]
                   χ₂
 -}

 open Category (CommRingsCategory {ℓ})
 open Cospan

 fgCospan : Cospan CommRingsCategory
 l fgCospan = R[1/ g ]AsCommRing
 m fgCospan = R[1/ (f · g) ]AsCommRing
 r fgCospan = R[1/ f ]AsCommRing
 s₁ fgCospan = χ₂
 s₂ fgCospan = χ₁

 -- the commutative square
 private
  /1χComm : ∀ (x : R) → χ₂ .fst (x /1ᵍ) ≡ χ₁ .fst (x /1ᶠ)
  /1χComm x = eq/ _ _ ((1r , powersFormMultClosedSubset (f · g) .containsOne) , refl)

  /1χHomComm : /1ᵍAsCommRingHom ⋆ χ₂ ≡ /1ᶠAsCommRingHom ⋆ χ₁
  /1χHomComm = RingHom≡ (funExt /1χComm)

 fgSquare : 1r ∈ ⟨f,g⟩
          → isPullback _ fgCospan /1ᵍAsCommRingHom /1ᶠAsCommRingHom /1χHomComm
 fgSquare 1∈⟨f,g⟩ {d = A} ψ φ ψχ₂≡φχ₁ = (χ , χCoh) , χUniqueness
  where
  instance
   _ = snd A

  applyEqualizerLemma : ∀ a → ∃![ χa ∈ R ] (χa /1ᶠ ≡ fst φ a) × (χa /1ᵍ ≡ fst ψ a)
  applyEqualizerLemma a =
    equalizerLemma 1∈⟨f,g⟩ (fst φ a) (fst ψ a) (cong (_$ a) (sym ψχ₂≡φχ₁))

  χ : CommRingHom A R'
  fst χ a = applyEqualizerLemma a .fst .fst
  snd χ = makeIsRingHom
       (cong fst (applyEqualizerLemma 1r .snd (1r , 1Coh)))
        (λ x y → cong fst (applyEqualizerLemma (x + y) .snd (_ , +Coh x y)))
         (λ x y → cong fst (applyEqualizerLemma (x · y) .snd (_ , ·Coh x y)))
   where
   open IsRingHom
   1Coh : (1r /1ᶠ ≡ fst φ 1r) × (1r /1ᵍ ≡ fst ψ 1r)
   1Coh = (sym (φ .snd .pres1)) , sym (ψ .snd .pres1)

   +Coh : ∀ x y → ((fst χ x + fst χ y) /1ᶠ ≡ fst φ (x + y))
                × ((fst χ x + fst χ y) /1ᵍ ≡ fst ψ (x + y))
   fst (+Coh x y) = /1ᶠAsCommRingHom .snd .pres+ _ _
                  ∙∙ cong₂ _+_ (applyEqualizerLemma x .fst .snd .fst)
                             (applyEqualizerLemma y .fst .snd .fst)
                  ∙∙ sym (φ .snd .pres+ x y)
   snd (+Coh x y) = /1ᵍAsCommRingHom .snd .pres+ _ _
                  ∙∙ cong₂ _+_ (applyEqualizerLemma x .fst .snd .snd)
                               (applyEqualizerLemma y .fst .snd .snd)
                  ∙∙ sym (ψ .snd .pres+ x y)

   ·Coh : ∀ x y → ((fst χ x · fst χ y) /1ᶠ ≡ fst φ (x · y))
                × ((fst χ x · fst χ y) /1ᵍ ≡ fst ψ (x · y))
   fst (·Coh x y) = /1ᶠAsCommRingHom .snd .pres· _ _
                  ∙∙ cong₂ _·_ (applyEqualizerLemma x .fst .snd .fst)
                             (applyEqualizerLemma y .fst .snd .fst)
                  ∙∙ sym (φ .snd .pres· x y)
   snd (·Coh x y) = /1ᵍAsCommRingHom .snd .pres· _ _
                  ∙∙ cong₂ _·_ (applyEqualizerLemma x .fst .snd .snd)
                               (applyEqualizerLemma y .fst .snd .snd)
                  ∙∙ sym (ψ .snd .pres· x y)

  χCoh : (ψ ≡ χ ⋆ /1ᵍAsCommRingHom) × (φ ≡ χ ⋆ /1ᶠAsCommRingHom)
  fst χCoh = RingHom≡ (funExt (λ a → sym (applyEqualizerLemma a .fst .snd .snd)))
  snd χCoh = RingHom≡ (funExt (λ a → sym (applyEqualizerLemma a .fst .snd .fst)))

  χUniqueness : (y : Σ[ θ ∈ CommRingHom A R' ]
                       (ψ ≡ θ ⋆ /1ᵍAsCommRingHom) × (φ ≡ θ ⋆ /1ᶠAsCommRingHom))
              → (χ , χCoh) ≡ y
  χUniqueness (θ , θCoh) = Σ≡Prop (λ _ → isProp× (isSetRingHom _ _ _ _)
                                                 (isSetRingHom _ _ _ _))
    (RingHom≡ (funExt (λ a → cong fst (applyEqualizerLemma a .snd (θtriple a)))))
      where
      θtriple : ∀ a → Σ[ x ∈ R ] (x /1ᶠ ≡ fst φ a) × (x /1ᵍ ≡ fst ψ a)
      θtriple a = fst θ a , sym (cong (_$ a) (θCoh .snd))
                          , sym (cong (_$ a) (θCoh .fst))

 -- packaging it all up
 open Pullback
 fgPullback : 1r ∈ ⟨f,g⟩ → Pullback _ fgCospan
 pbOb (fgPullback 1r∈⟨f,g⟩) = _
 pbPr₁ (fgPullback 1r∈⟨f,g⟩) = _
 pbPr₂ (fgPullback 1r∈⟨f,g⟩) = _
 pbCommutes (fgPullback 1r∈⟨f,g⟩) = /1χHomComm
 univProp (fgPullback 1r∈⟨f,g⟩) = fgSquare 1r∈⟨f,g⟩

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
module IndexInference where

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

data Vec (A : Set) : Nat -> Set where
  []   : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

infixr 40 _::_

-- The length of the vector can be inferred from the pattern.
foo : Vec Nat _ -> Nat
foo (a :: b :: c :: []) = c

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
module ImplArg2 where

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

data Vec (A : Set) : Nat -> Set where
  vnil  : Vec A zero
  vcons : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

cons : {A : Set} (a : A) {n : Nat} -> Vec A n -> Vec A (suc n)
cons a = vcons a

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
------------------------------------------------------------------------------
-- First-order logic with equality
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

-- This module exported all the logical constants and the
-- propositional equality. This module is re-exported by the "base"
-- modules whose theories are defined on first-order logic + equality.

module Common.FOL.FOL-Eq where

-- First-order logic (without equality).
open import Common.FOL.FOL public

-- Propositional equality.
open import Common.FOL.Relation.Binary.PropositionalEquality public

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Categories
open import Functors
open import RMonads

module RMonads.CatofRAdj.TermRAdjObj {a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}
                                     {J : Fun C D}(M : RMonad J) where

open import Library
open import Naturals
open import RAdjunctions
open import RMonads.CatofRAdj M
open import Categories.Terminal
open import RMonads.REM M
open import RMonads.REM.Adjunction M
open import RAdjunctions.RAdj2RMon

open Cat
open Fun
open NatT
open RAdj

lemX : R REMAdj ○ L REMAdj ≅ TFun M
lemX = FunctorEq _ _ refl refl

EMObj : Obj CatofAdj
EMObj  = record {
  E       = EM;
  adj     = REMAdj;
  law     = lemX;
  ηlaw    = idl D;
  bindlaw = λ{X}{Y}{f} →
    cong bind
         (stripsubst (Hom D (OMap J X))
                     f
                     (fcong Y (cong OMap (sym lemX))))} where open RMonad M

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
{-# OPTIONS --without-K #-}
open import function.extensionality.core

module hott.equivalence.alternative where

open import sum
open import equality.core
open import equality.calculus
open import function.core
open import function.extensionality.proof
open import function.isomorphism.core
open import function.isomorphism.coherent
open import function.isomorphism.utils
open import hott.level.core
open import hott.equivalence.core
open import hott.univalence

module _ {i j}{X : Set i}{Y : Set j} where
  open ≅-Reasoning

  private
    we-split-iso : (f : X → Y) → _
    we-split-iso f = begin
        weak-equiv f
      ≅⟨ ΠΣ-swap-iso ⟩
        ( Σ ((y : Y) → f ⁻¹ y) λ gβ
        → (y : Y)(u : f ⁻¹ y) → gβ y ≡ u )
      ≅⟨ Σ-ap-iso₁ ΠΣ-swap-iso ⟩
        ( Σ (Σ (Y → X) λ g → (y : Y) → f (g y) ≡ y) λ { (g , β)
        → (y : Y)(u : f ⁻¹ y) → (g y , β y) ≡ u } )
      ≅⟨ Σ-assoc-iso ⟩
        ( Σ (Y → X) λ g
        → Σ ((y : Y) → f (g y) ≡ y) λ β
        → (y : Y)(u : f ⁻¹ y) → (g y , β y) ≡ u )
      ≅⟨ ( Σ-ap-iso₂ λ g
         → Σ-ap-iso₂ λ β
         → Π-ap-iso refl≅ λ y
         → curry-iso (λ x p → (g y , β y) ≡ (x , p)) ) ⟩
        ( Σ (Y → X) λ g
        → Σ ((y : Y) → f (g y) ≡ y) λ β
        → (y : Y)(x : X)(p : f x ≡ y)
        → (g y , β y) ≡ (x , p) )
      ≅⟨ ( Σ-ap-iso₂ λ g
          → Σ-ap-iso₂ λ β
          → Π-ap-iso refl≅ λ y
          → Π-ap-iso refl≅ λ x
          → Π-ap-iso refl≅ λ p
          → sym≅ Σ-split-iso ) ⟩
        ( Σ (Y → X) λ g
        → Σ ((y : Y) → f (g y) ≡ y) λ β
        → (y : Y)(x : X)(p : f x ≡ y)
        → Σ (g y ≡ x) λ q
        → subst (λ x' → f x' ≡ y) q (β y) ≡ p )
      ≅⟨ ( Σ-ap-iso₂ λ g
          → Σ-ap-iso₂ λ β
          → Π-ap-iso refl≅ λ y
          → Π-ap-iso refl≅ λ x
          → Π-ap-iso refl≅ λ p
          → Σ-ap-iso₂ λ q
          → sym≅ ( trans≡-iso (
                 subst-naturality (λ x' → x' ≡ y) f q (β y)
               · subst-eq (ap f q) (β y)) )) ⟩
        ( Σ (Y → X) λ g
        → Σ ((y : Y) → f (g y) ≡ y) λ β
        → (y : Y)(x : X)(p : f x ≡ y)
        → Σ (g y ≡ x) λ q
        → sym (ap f q) · β y ≡ p )
      ≅⟨ ( Σ-ap-iso₂ λ g
          → Σ-ap-iso₂ λ β
          → Π-comm-iso ) ⟩
        ( Σ (Y → X) λ g
        → Σ ((y : Y) → f (g y) ≡ y) λ β
        → (x : X)(y : Y)(p : f x ≡ y)
        → Σ (g y ≡ x) λ q
        → sym (ap f q) · β y ≡ p )
      ≅⟨ ( Σ-ap-iso₂ λ g
         → Σ-ap-iso₂ λ β
         → Π-ap-iso refl≅ λ x
         → sym≅ J-iso ) ⟩
        ( Σ (Y → X) λ g
        → Σ ((y : Y) → f (g y) ≡ y) λ β
        → (x : X)
        → Σ (g (f x) ≡ x) λ q
        → sym (ap f q) · β (f x) ≡ refl )
      ≅⟨ ( Σ-ap-iso₂ λ g
         → Σ-ap-iso₂ λ β
         → ΠΣ-swap-iso ) ⟩
        ( Σ (Y → X) λ g
        → Σ ((y : Y) → f (g y) ≡ y) λ β
        → Σ ((x : X) → g (f x) ≡ x) λ α
        → (x : X) → sym (ap f (α x)) · β (f x) ≡ refl )
      ≅⟨ ( Σ-ap-iso₂ λ g
         → Σ-ap-iso₂ λ β
         → Σ-ap-iso₂ λ α
         → Π-ap-iso refl≅ λ x
         → sym≅ (trans≅ (trans≡-iso (left-unit (ap f (α x))))
                         (move-≡-iso (ap f (α x)) refl (β (f x)))) ) ⟩
        ( Σ (Y → X) λ g
        → Σ ((y : Y) → f (g y) ≡ y) λ β
        → Σ ((x : X) → g (f x) ≡ x) λ α
        → (x : X) → ap f (α x) ≡ β (f x) )
      ≅⟨ ( Σ-ap-iso₂ λ g → Σ-comm-iso ) ⟩
        ( Σ (Y → X) λ g
        → Σ ((x : X) → g (f x) ≡ x) λ α
        → Σ ((y : Y) → f (g y) ≡ y) λ β
        → ((x : X) → ap f (α x) ≡ β (f x)) )
      ∎

  ≈⇔≅' : (X ≈ Y) ≅ (X ≅' Y)
  ≈⇔≅' = begin
      (X ≈ Y)
    ≅⟨ Σ-ap-iso₂ we-split-iso ⟩
      ( Σ (X → Y) λ f
      → Σ (Y → X) λ g
      → Σ ((x : X) → g (f x) ≡ x) λ α
      → Σ ((y : Y) → f (g y) ≡ y) λ β
      → ((x : X) → ap f (α x) ≡ β (f x)) )
    ≅⟨ record
         { to = λ {(f , g , α , β , γ) → iso f g α β , γ }
         ; from = λ { (iso f g α β , γ) → f , g , α , β , γ }
         ; iso₁ = λ _ → refl
         ; iso₂ = λ _ → refl } ⟩
      (X ≅' Y)
    ∎

  open _≅_ ≈⇔≅' public using ()
    renaming ( to to ≈⇒≅'
             ; from to ≅'⇒≈ )

  ≅⇒≈ : (X ≅ Y) → (X ≈ Y)
  ≅⇒≈ = ≅'⇒≈ ∘ ≅⇒≅'

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


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

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat hiding (_<_)

data _<_ : Nat → Nat → Set where
  zero-< : ∀ {n} → zero < suc n
  suc-<  : ∀ {m n} → m < n → suc m < suc n

record Acc (a : Nat) : Prop where
  inductive
  pattern
  constructor acc
  field acc< : (∀ b → b < a → Acc b)

open Acc

AccRect : ∀ {P : Nat → Set} → (∀ a → (∀ b → b < a → Acc b) → (∀ b → b < a → P b) → P a) → ∀ a → Acc a → P a
AccRect f a (acc p) = f a p (λ b b<a → AccRect f b (p b b<a))

AccRectProp : ∀ {P : Nat → Prop} → (∀ a → (∀ b → b < a → Acc b) → (∀ b → b < a → P b) → P a) → ∀ a → Acc a → P a
AccRectProp f a (acc p) = f a p (λ b b<a → AccRectProp f b (p b b<a))

AccInv : ∀ a → Acc a → ∀ b → b < a → Acc b
AccInv = AccRectProp (λ _ p _ → p)

example : ∀ {P : Nat → Set} → (f : ∀ a → (∀ b → b < a → P b) → P a) → ∀ a → (access : Acc a) →
  AccRect {P} (λ a _ r → f a r) a access ≡ f a (λ b b<a → AccRect {P} (λ a _ r → f a r) b (AccInv a access b b<a))
example f a access = ?

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-
This second-order equational theory was created from the following second-order syntax description:

syntax GroupAction | GA

type
  * : 0-ary
  X : 0-ary

term
  unit : * | ε
  add  : *  *  ->  * | _⊕_ l20
  neg  : *  ->  * | ⊖_ r40
  act  : *  X  ->  X | _⊙_ r30

theory
  (εU⊕ᴸ) a |> add (unit, a) = a
  (εU⊕ᴿ) a |> add (a, unit) = a
  (⊕A) a b c |> add (add(a, b), c) = add (a, add(b, c))
  (⊖N⊕ᴸ) a |> add (neg (a), a) = unit
  (⊖N⊕ᴿ) a |> add (a, neg (a)) = unit
  (εU⊙)      x : X |> act (unit,      x) = x
  (⊕A⊙) g h  x : X |> act (add(g, h), x) = act (g, act(h, x))
-}

module GroupAction.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import GroupAction.Signature
open import GroupAction.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution GA:Syn
open import SOAS.Metatheory.SecondOrder.Equality GA:Syn

private
  variable
    α β γ τ : GAT
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ GA) α Γ → (𝔐 ▷ GA) α Γ → Set where
  εU⊕ᴸ : ⁅ * ⁆̣             ▹ ∅ ⊢       ε ⊕ 𝔞 ≋ₐ 𝔞
  εU⊕ᴿ : ⁅ * ⁆̣             ▹ ∅ ⊢       𝔞 ⊕ ε ≋ₐ 𝔞
  ⊕A   : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (𝔞 ⊕ 𝔟) ⊕ 𝔠 ≋ₐ 𝔞 ⊕ (𝔟 ⊕ 𝔠)
  ⊖N⊕ᴸ : ⁅ * ⁆̣             ▹ ∅ ⊢   (⊖ 𝔞) ⊕ 𝔞 ≋ₐ ε
  ⊖N⊕ᴿ : ⁅ * ⁆̣             ▹ ∅ ⊢   𝔞 ⊕ (⊖ 𝔞) ≋ₐ ε
  εU⊙  : ⁅ X ⁆̣             ▹ ∅ ⊢       ε ⊙ 𝔞 ≋ₐ 𝔞
  ⊕A⊙  : ⁅ * ⁆ ⁅ * ⁆ ⁅ X ⁆̣ ▹ ∅ ⊢ (𝔞 ⊕ 𝔟) ⊙ 𝔠 ≋ₐ 𝔞 ⊙ (𝔟 ⊙ 𝔠)

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
-- A variant of code reported by Andreas Abel, due to Andreas Abel and
-- Nicolas Pouillard.

-- npouillard, 2011-10-04

{-# OPTIONS --guardedness --sized-types #-}

open import Common.Coinduction renaming (∞ to co)
open import Common.Size

data ⊥ : Set where

data Mu-co : Size → Set where
  inn : ∀ {i} → co (Mu-co i) → Mu-co (↑ i)

iter : ∀ {i} → Mu-co i → ⊥
iter (inn t) = iter (♭ t)

bla : Mu-co ∞
bla = inn (♯ bla)

false : ⊥
false = iter bla

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- Properties of functions, such as associativity and commutativity
------------------------------------------------------------------------

-- This file contains some core definitions which are reexported by
-- Algebra.FunctionProperties. They are placed here because
-- Algebra.FunctionProperties is a parameterised module, and the
-- parameters are irrelevant for these definitions.

module Algebra.FunctionProperties.Core where

------------------------------------------------------------------------
-- Unary and binary operations

Op₁ : Set → Set
Op₁ A = A → A

Op₂ : Set → Set
Op₂ A = A → A → A

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module sn-calculus-confluence.helper where

open import Data.List.All
open import Function
  using (_∘_)
open import Data.List.Any using (Any ; here ; there)
open import Data.Nat using (_+_)
open import utility
open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Environment as Env
open import Esterel.Context
open import Data.Product
open import Data.Sum
open import Data.Bool
open import Data.List
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import sn-calculus
open import context-properties
open import Esterel.Lang.Binding
open import Data.List.Any.Properties
  renaming ( ++⁺ˡ to ++ˡ ; ++⁺ʳ to ++ʳ )

open import Data.FiniteMap
import Data.OrderedListMap as OMap
open import Data.Nat as Nat using (ℕ)
open import Esterel.Variable.Signal as Signal
  using (Signal)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar)
open import Esterel.Variable.Sequential as SeqVar

set-dist' : ∀{key value inject surject} → ∀{inject-injective : ∀{k1 : key} → ∀{k2 : key} → (inject k1) ≡ (inject k2) → k1 ≡ k2}
            → ∀{surject-inject : ∀{k} → inject (surject k) ≡ k}
            → ∀{A : Map {key} inject surject inject-injective surject-inject value} → ∀{B : Map {key} inject surject inject-injective surject-inject value}
            → distinct' (keys {key} inject surject inject-injective surject-inject {value} A) (keys {key} inject surject inject-injective surject-inject {value}  B)
            → (union {key} inject surject inject-injective surject-inject {value} A B) ≡ (union  {key} inject surject inject-injective surject-inject {value} B A)
set-dist'{key}{value}{inject}{surject}{inject-injective}{surject-inject}{A}{B} d = OMap.U-comm key inject value {A} {B} d

set-dist : ∀{θ θ'} → distinct (Dom θ) (Dom θ') → (θ ← θ') ≡ (θ' ← θ)
set-dist {Θ sig₁ shr₁ var₁} {Θ sig₂ shr₂ var₂} (a , b , c)
    rewrite  set-dist'{inject = _}{Signal.wrap}{inject-injective = Signal.unwrap-injective}{Signal.bijective}{sig₁}{sig₂} a
           | set-dist'{inject = _}{SharedVar.wrap}{inject-injective = SharedVar.unwrap-injective}{SharedVar.bijective}{shr₁}{shr₂} b
           | set-dist'{inject = _}{SeqVar.wrap}{inject-injective = SeqVar.unwrap-injective}{SeqVar.bijective}{var₁}{var₂} c = refl

done≠rho : ∀{p E θ q A} → done p → (p ≐ E ⟦ (ρ⟨ θ , A ⟩· q) ⟧e) → ⊥
done≠rho (dhalted hnothin) ()
done≠rho (dhalted (hexit n)) ()
done≠rho (dpaused p/paused) p≐E⟦ρθq⟧ with paused-⟦⟧e p/paused p≐E⟦ρθq⟧
... | ()

plug≡ : ∀{r q E w} → r ≐ E ⟦ w ⟧e → q ≐ E ⟦ w ⟧e  → r ≡ q
plug≡ r≐E⟦w⟧ q≐E⟦w⟧ = trans (sym (unplug r≐E⟦w⟧)) (unplug q≐E⟦w⟧)

RE-split : ∀{p θ p' E E' q A}
           → p ≐ E ⟦ ρ⟨ θ , A ⟩· p' ⟧e
           → p ≐ E' ⟦ q ⟧e
           → E a~ E'
           → ∃ (λ d → ∃ (λ Eout → d ≐ E ⟦ p' ⟧e × d ≐ Eout ⟦ q ⟧e × E' ~ Eout × Eout a~ E ))
RE-split {.(ρ⟨ _ , _ ⟩· _)} dehole dehole ()
RE-split {.(_ ∥ _)} (depar₁ eq1) dehole ()
RE-split {.(_ >> _)} (deseq eq1) dehole ()
RE-split {.(trap _)} (detrap eq1) dehole ()
RE-split {.(_ ∥ _)} (depar₂ eq1) dehole ()
RE-split {.(suspend _ _)} (desuspend eq1) dehole ()
RE-split {(pin ∥ qin)}{θ}{p'}{((epar₁ _) ∷ E)}{(epar₂ _) ∷ E'} (depar₁ eq1) (depar₂ eq2) par2
   = (t ∥ qin) , (epar₂ t) ∷ E' , (depar₁ (plug refl) , depar₂ eq2 , parl (~ref E') , par) where t = (E ⟦ p' ⟧e)
RE-split {(pin ∥ qin)}{θ}{p'}{((epar₂ _) ∷ E)}{(epar₁ _) ∷ E'} (depar₂ eq1) (depar₁ eq2) par
   = (pin ∥ t) , ((epar₁ t) ∷ E' , (depar₂ (plug refl) , depar₁ eq2 , parr (~ref E') , par2)) where t = (E ⟦ p' ⟧e)
RE-split {(pin ∥ qin)} (depar₁ eq1) (depar₁ eq2) (parr neg) with RE-split eq1 eq2 neg
... | (d , Eout , (eqd , eqo , ~ , a~)) = d ∥ qin , (epar₁ qin) ∷ Eout , (depar₁ eqd , depar₁ eqo , parr ~ , parr a~)
RE-split {(pin ∥ qin)} (depar₂ eq1) (depar₂ eq2) (parl neg) with RE-split eq1 eq2 neg
... | (d , Eout , (eqd , eqo , ~ , a~)) = pin ∥ d , (epar₂ pin) ∷ Eout , (depar₂ eqd , depar₂ eqo , parl ~ , parl a~)
RE-split {(loopˢ _ q)} (deloopˢ eq1) (deloopˢ eq2) (loopˢ neg) with RE-split eq1 eq2 neg
... | (d , Eout , (eqd , eqo , ~ , a~)) = (loopˢ d q) , (eloopˢ q) ∷ Eout , (deloopˢ eqd , deloopˢ eqo , loopˢ ~ , loopˢ a~)
RE-split {(._ >> q)} (deseq eq1) (deseq eq2) (seq neg) with RE-split eq1 eq2 neg
... | (d , Eout , (eqd , eqo , ~ , a~)) = (d >> q) , (eseq q) ∷ Eout , (deseq eqd , deseq eqo , seq ~ , seq a~)
RE-split {(suspend ._ S)} (desuspend eq1) (desuspend eq2) (susp neg) with RE-split eq1 eq2 neg
... | (d , Eout , (eqd , eqo , ~ , a~)) = (suspend d S) , ((esuspend S) ∷ Eout) , (desuspend eqd , desuspend eqo , susp ~ , susp a~)
RE-split {.(trap _)} (detrap eq1) (detrap eq2) (trp neg) with RE-split eq1 eq2 neg
... | (d , Eout , (eqd , eqo , ~ , a~)) = (trap d) , (etrap ∷ Eout) , (detrap eqd , detrap eqo , trp ~ , trp a~)

ready-maint : ∀{θ e} → (S : Signal) → (S∈ : (Env.isSig∈ S θ)) → (stat : Signal.Status) → all-ready e θ
                     → all-ready e (Env.set-sig{S} θ S∈ stat)
ready-maint {θ} {.(plus [])} S S∈ stat (aplus []) = aplus []
ready-maint {θ} {.(plus (num _ ∷ _))} S S∈ stat (aplus (brnum ∷ x₁)) with ready-maint S S∈ stat (aplus x₁)
... | (aplus r) = aplus (brnum ∷ r)
ready-maint {θ} {.(plus (seq-ref _ ∷ _))} S S∈ stat (aplus (brseq x₁ ∷ x₂)) with ready-maint S S∈ stat (aplus x₂)
... | (aplus r) = aplus (brseq x₁ ∷ r)
ready-maint {θ} {.(plus (shr-ref _ ∷ _))} S S∈ stat (aplus (brshr s∈ x ∷ x₁)) with ready-maint S S∈ stat (aplus x₁)
... | (aplus r) = aplus (brshr s∈ x ∷ r)

ready-irr : ∀{θ e} → (S : Signal) → (S∈ : (Env.isSig∈ S θ)) → (stat : Signal.Status)
                   → (e' : all-ready e θ)
                   → (e'' : all-ready e (Env.set-sig{S} θ S∈ stat))
                   → δ e' ≡ δ e''

ready-irr {θ} {.(plus [])} S S∈ stat (aplus []) (aplus []) = refl
ready-irr {θ} {.(plus (num _ ∷ _))} S S∈ stat (aplus (brnum ∷ x₁)) (aplus (brnum ∷ x₂))
 rewrite ready-irr S S∈ stat (aplus x₁) (aplus x₂) = refl
ready-irr {θ@(Θ Ss ss xs)} {.(plus (seq-ref _ ∷ _))} S S∈ stat (aplus (brseq{_}{x} x₁ ∷ x₂)) (aplus (brseq x₃ ∷ x₄))
 rewrite ready-irr S S∈ stat (aplus x₂) (aplus x₄) | seq∈-eq'{x}{xs} x₁ x₃ = refl
ready-irr {θ@(Θ Ss ss xs)} {.(plus (shr-ref _ ∷ _))} S S∈ stat (aplus (brshr{_}{s} s∈ x ∷ x₁)) (aplus (brshr s∈₁ x₂ ∷ x₃))
 rewrite ready-irr S S∈ stat (aplus x₁) (aplus x₃) | shr∈-eq'{s}{ss} s∈ s∈₁ = refl

ready-maint/irr : ∀{θ e} → (S : Signal) → (S∈ : (Env.isSig∈ S θ)) → (stat : Signal.Status)
                         → (e' : all-ready e θ)
                         → Σ[ e'' ∈ all-ready e (Env.set-sig{S} θ S∈ stat) ] δ e' ≡ δ e''
ready-maint/irr {θ}{e} S S∈ stat e' with ready-maint{θ}{e} S S∈ stat e'
... | e'' = e'' , (ready-irr{θ}{e} S S∈ stat e' e'')

ready-maint/x : ∀{θ e} → (x : SeqVar) → (x∈ : (Env.isVar∈ x θ)) → (n : ℕ) → all-ready e θ
                       → all-ready e (Env.set-var{x} θ x∈ n)
ready-maint/x {θ} {.(plus [])} x x∈ n (aplus []) = aplus []
ready-maint/x {θ} {.(plus (num _ ∷ _))} x₁ x∈ n (aplus (brnum ∷ x₂)) with ready-maint/x x₁ x∈ n (aplus x₂)
... | (aplus r) = aplus (brnum ∷ r)
ready-maint/x {θ} {.(plus (seq-ref _ ∷ _))} x₁ x∈ n (aplus (brseq{x = x2} x₂ ∷ x₃)) with ready-maint/x x₁ x∈ n (aplus x₃)
... | (aplus r) = aplus ((brseq (seq-set-mono'{x2}{x₁}{θ}{n}{x∈} x₂)) ∷ r)
ready-maint/x {θ} {.(plus (shr-ref _ ∷ _))} x₁ x∈ n (aplus (brshr s∈ x ∷ x₂))  with ready-maint/x x₁ x∈ n (aplus x₂)
... | (aplus r) = aplus (brshr s∈ x ∷ r)

ready-maint-s : ∀{θ e} → (s : SharedVar) → (n : ℕ) → (s∈ : Env.isShr∈ s θ) → ¬ (Env.shr-stats {s} θ s∈ ≡ SharedVar.ready) → (e' : all-ready e θ)
                       → all-ready e (Env.set-shr{s = s} θ s∈ SharedVar.new n)
ready-maint-s {e = .(plus [])} s n s∈ ¬≡ (aplus []) = aplus []
ready-maint-s {e = .(plus (num _ ∷ _))} s n₁ s∈ ¬≡ (aplus (brnum ∷ x₁)) with ready-maint-s s n₁ s∈ ¬≡ (aplus x₁)
... | aplus rec  = aplus (brnum ∷ rec)
ready-maint-s {e = .(plus (seq-ref _ ∷ _))} s n s∈ ¬≡ (aplus (brseq x₁ ∷ x₂)) with ready-maint-s s n s∈ ¬≡ (aplus x₂)
... | aplus rec = aplus (brseq x₁ ∷ rec)
ready-maint-s{θ} {e = (plus (shr-ref s ∷ ._))} s₁ n s∈ ¬≡ (aplus (brshr s∈₁ x ∷ x₁)) with ready-maint-s s₁ n s∈ ¬≡ (aplus x₁) | s SharedVar.≟ s₁
... | aplus rec | yes refl with shr-stats-∈-irr{s}{θ} s∈ s∈₁
... | eq rewrite eq = ⊥-elim (¬≡ x)
ready-maint-s{θ = θ} {e = (plus (shr-ref s ∷ ._))} s₁ n s∈ ¬≡ (aplus (brshr s∈₁ x ∷ x₁)) | aplus rec | no ¬s≡s₁
 with shr-putputget{θ = θ}{v2l = SharedVar.new}{n} ¬s≡s₁ s∈₁ s∈ (shr-set-mono'{s}{s₁}{θ}{n = n}{s∈} s∈₁) x refl
... | (eq1 , eq2) = aplus (brshr ((shr-set-mono'{s}{s₁}{θ}{n = n}{s∈} s∈₁)) eq1 ∷ rec)

ready-irr-on-irr-s-helper : ∀{θ e} → (s : SharedVar) → (n : ℕ) → (s∈ : Env.isShr∈ s θ) → ¬ (Env.shr-stats {s} θ s∈ ≡ SharedVar.ready) → (e' : all-ready e θ)
                            → (e'' : all-ready e (Env.set-shr{s = s} θ s∈ SharedVar.new n)) →  δ e' ≡ δ e''
ready-irr-on-irr-s-helper {θ} {.(plus [])} s n s∈ ¬≡ (aplus []) (aplus []) = refl
ready-irr-on-irr-s-helper {θ} {.(plus (num _ ∷ _))} s n s∈ ¬≡ (aplus (brnum ∷ x₁)) (aplus (brnum ∷ x'))
  rewrite ready-irr-on-irr-s-helper s n s∈ ¬≡ (aplus x₁) (aplus x') = refl
ready-irr-on-irr-s-helper {θ@(Θ Ss ss xs)} {(plus (seq-ref x ∷ _))} s n s∈ ¬≡ (aplus (brseq x₁ ∷ x₂)) (aplus (brseq x₃ ∷ x'))
  rewrite ready-irr-on-irr-s-helper s n s∈ ¬≡ (aplus x₂) (aplus x') | seq∈-eq'{x}{xs} x₁ x₃ = refl
ready-irr-on-irr-s-helper {θ@(Θ Ss ss xs)} {(plus (shr-ref sₑ ∷ _))} s n s∈ ¬≡ (aplus (brshr s∈₁ x ∷ x₁)) (aplus (brshr s∈₂ x₂ ∷ x'))
  with sₑ SharedVar.≟ s
... | yes sₑ≡s rewrite sₑ≡s | shr∈-eq'{s}{ss} s∈ s∈₁ = ⊥-elim (¬≡ x)
... | no ¬sₑ≡s with shr-putputget{θ = θ}{v2l = SharedVar.new}{n} ¬sₑ≡s s∈₁ s∈ s∈₂ x refl
... | (eq1 , eq2) rewrite ready-irr-on-irr-s-helper s n s∈ ¬≡ (aplus x₁) (aplus x') | eq2 = refl

ready-irr-on-irr-s : ∀{θ e} → (s : SharedVar) → (n : ℕ) → (s∈ : Env.isShr∈ s θ) → ¬ (Env.shr-stats {s} θ s∈ ≡ SharedVar.ready) → (e' : all-ready e θ)
                     → Σ[ e'' ∈ all-ready e (Env.set-shr{s = s} θ s∈ SharedVar.new n) ] δ e' ≡ δ e''
ready-irr-on-irr-s s n s∈ ¬≡ e' = e'' , (ready-irr-on-irr-s-helper s n s∈ ¬≡ e' e'')
  where e'' = ready-maint-s s n s∈ ¬≡ e'

-- copied and pasted form above
-- TODO: maybe someday abstract over SharedVar.new/SharedVar.ready to sharedvar-status
ready-maint-s/ready : ∀{θ e} → (s : SharedVar) → (n : ℕ) → (s∈ : Env.isShr∈ s θ) → ¬ (Env.shr-stats {s} θ s∈ ≡ SharedVar.ready) → (e' : all-ready e θ)
                       → all-ready e (Env.set-shr{s = s} θ s∈ SharedVar.ready n)
ready-maint-s/ready {e = .(plus [])} s n s∈ ¬≡ (aplus []) = aplus []
ready-maint-s/ready {e = .(plus (num _ ∷ _))} s n₁ s∈ ¬≡ (aplus (brnum ∷ x₁)) with ready-maint-s/ready s n₁ s∈ ¬≡ (aplus x₁)
... | aplus rec  = aplus (brnum ∷ rec)
ready-maint-s/ready {e = .(plus (seq-ref _ ∷ _))} s n s∈ ¬≡ (aplus (brseq x₁ ∷ x₂)) with ready-maint-s/ready s n s∈ ¬≡ (aplus x₂)
... | aplus rec = aplus (brseq x₁ ∷ rec)
ready-maint-s/ready{θ} {e = (plus (shr-ref s ∷ ._))} s₁ n s∈ ¬≡ (aplus (brshr s∈₁ x ∷ x₁)) with ready-maint-s/ready s₁ n s∈ ¬≡ (aplus x₁) | s SharedVar.≟ s₁
... | aplus rec | yes refl with shr-stats-∈-irr{s}{θ} s∈ s∈₁
... | eq rewrite eq = ⊥-elim (¬≡ x)
ready-maint-s/ready{θ = θ} {e = (plus (shr-ref s ∷ ._))} s₁ n s∈ ¬≡ (aplus (brshr s∈₁ x ∷ x₁)) | aplus rec | no ¬s≡s₁
 with shr-putputget{θ = θ}{v2l = SharedVar.ready}{n} ¬s≡s₁ s∈₁ s∈ (shr-set-mono'{s}{s₁}{θ}{n = n}{s∈} s∈₁) x refl
... | (eq1 , eq2) = aplus (brshr ((shr-set-mono'{s}{s₁}{θ}{n = n}{s∈} s∈₁)) eq1 ∷ rec)

ready-irr-on-irr-s-helper/ready : ∀{θ e} → (s : SharedVar) → (n : ℕ) → (s∈ : Env.isShr∈ s θ) → ¬ (Env.shr-stats {s} θ s∈ ≡ SharedVar.ready) → (e' : all-ready e θ)
                            → (e'' : all-ready e (Env.set-shr{s = s} θ s∈ SharedVar.ready n)) →  δ e' ≡ δ e''
ready-irr-on-irr-s-helper/ready {θ} {.(plus [])} s n s∈ ¬≡ (aplus []) (aplus []) = refl
ready-irr-on-irr-s-helper/ready {θ} {.(plus (num _ ∷ _))} s n s∈ ¬≡ (aplus (brnum ∷ x₁)) (aplus (brnum ∷ x'))
  rewrite ready-irr-on-irr-s-helper/ready s n s∈ ¬≡ (aplus x₁) (aplus x') = refl
ready-irr-on-irr-s-helper/ready {θ@(Θ Ss ss xs)} {(plus (seq-ref x ∷ _))} s n s∈ ¬≡ (aplus (brseq x₁ ∷ x₂)) (aplus (brseq x₃ ∷ x'))
  rewrite ready-irr-on-irr-s-helper/ready s n s∈ ¬≡ (aplus x₂) (aplus x') | seq∈-eq'{x}{xs} x₁ x₃ = refl
ready-irr-on-irr-s-helper/ready {θ@(Θ Ss ss xs)} {(plus (shr-ref sₑ ∷ _))} s n s∈ ¬≡ (aplus (brshr s∈₁ x ∷ x₁)) (aplus (brshr s∈₂ x₂ ∷ x'))
  with sₑ SharedVar.≟ s
... | yes sₑ≡s rewrite sₑ≡s | shr∈-eq'{s}{ss} s∈ s∈₁ = ⊥-elim (¬≡ x)
... | no ¬sₑ≡s with shr-putputget{θ = θ}{v2l = SharedVar.ready}{n} ¬sₑ≡s s∈₁ s∈ s∈₂ x refl
... | (eq1 , eq2) rewrite ready-irr-on-irr-s-helper/ready s n s∈ ¬≡ (aplus x₁) (aplus x') | eq2 = refl

ready-irr-on-irr-s/ready : ∀{θ e} → (s : SharedVar) → (n : ℕ) → (s∈ : Env.isShr∈ s θ) → ¬ (Env.shr-stats {s} θ s∈ ≡ SharedVar.ready) → (e' : all-ready e θ)
                     → Σ[ e'' ∈ all-ready e (Env.set-shr{s = s} θ s∈ SharedVar.ready n) ] δ e' ≡ δ e''
ready-irr-on-irr-s/ready s n s∈ ¬≡ e' = e'' , (ready-irr-on-irr-s-helper/ready s n s∈ ¬≡ e' e'')
  where e'' = ready-maint-s/ready s n s∈ ¬≡ e'

ready-irr-on-irr-x-help : ∀{θ e} x n → (x∈ : Env.isVar∈ x θ) → (e' : all-ready e θ) → (SeqVar.unwrap x) ∉ (Xs (FVₑ e))
                          → (e'' : all-ready e (Env.set-var{x = x} θ x∈ n))
                          →  δ e' ≡ δ e''
ready-irr-on-irr-x-help x n x∈ (aplus []) x∉FV (aplus []) = refl
ready-irr-on-irr-x-help x₁ n x∈ (aplus (brnum ∷ a)) x∉FV (aplus (brnum ∷ b)) rewrite ready-irr-on-irr-x-help x₁ n x∈ (aplus a) x∉FV (aplus b) = refl
ready-irr-on-irr-x-help{θ}{e} x₁ n x∈ (aplus (brseq{x = x} x₂ ∷ a)) x∉FV (aplus (brseq x₃ ∷ b))
    with x SeqVar.≟ x₁
... | yes refl = ⊥-elim (x∉FV (here refl))
... | no  ¬x≡x₁ rewrite seq-putputget{θ = θ} ¬x≡x₁ x₂ x∈ x₃ refl
                      | ready-irr-on-irr-x-help x₁ n x∈ (aplus a) (λ x → x∉FV (there x)) (aplus b) = refl
ready-irr-on-irr-x-help{θ} x₁ n x∈ (aplus (brshr{s = s} s∈ x ∷ a)) x∉FV (aplus (brshr s∈₁ x₂ ∷ b))
  rewrite ready-irr-on-irr-x-help x₁ n x∈ (aplus a) x∉FV (aplus b)
        | shr∈-eq'{s = s}{θ = (shr θ)} s∈ s∈₁
  = refl

ready-maint-x : ∀{θ e} x n → (x∈ : Env.isVar∈ x θ) → (e' : all-ready e θ) → (SeqVar.unwrap x) ∉ (Xs (FVₑ e))
                → all-ready e (Env.set-var{x = x} θ x∈ n)
ready-maint-x x n x∈ (aplus []) x∉FV = aplus []
ready-maint-x x₁ n₁ x∈ (aplus (brnum ∷ a)) x∉FV with ready-maint-x x₁ n₁ x∈ (aplus a) x∉FV
... | (aplus r) = aplus (brnum ∷ r)
ready-maint-x{θ} x₁ n x∈ (aplus (brseq{x = x} x₂ ∷ a)) x∉FV with ready-maint-x x₁ n x∈ (aplus a) (λ x₃ → x∉FV (there x₃))
... | (aplus r) = aplus ((brseq ((seq-set-mono'{x}{x₁}{θ}{n}{x∈} x₂))) ∷ r)
ready-maint-x x₁ n x∈ (aplus (brshr s∈ x ∷ a)) x∉FV  with ready-maint-x x₁ n x∈ (aplus a) x∉FV
... | (aplus r) = aplus ((brshr s∈ x) ∷ r)

ready-irr-on-irr-x : ∀{θ e} x n → (x∈ : Env.isVar∈ x θ) → (e' : all-ready e θ) → (SeqVar.unwrap x) ∉ (Xs (FVₑ e))
                     → Σ[ e'' ∈ all-ready e (Env.set-var{x = x} θ x∈ n) ] δ e' ≡ δ e''
ready-irr-on-irr-x x n x∈ e' x∉FV = _ , ready-irr-on-irr-x-help x n x∈ e' x∉FV (ready-maint-x x n x∈ e' x∉FV)

ready-maint-θˡ : ∀{θ e} θ' → (e' : all-ready e θ) → (distinct (Dom θ') (FVₑ e)) → (all-ready e (θ ← θ'))
ready-maint-θˡ θ' (aplus []) Domθ'≠FVe = aplus []
ready-maint-θˡ θ' (aplus (brnum ∷ x₁)) Domθ'≠FVe with ready-maint-θˡ θ' (aplus x₁) Domθ'≠FVe
... | (aplus f) = (aplus (brnum ∷ f))
ready-maint-θˡ{θ} θ' (aplus (brseq{x = x} x₁ ∷ x₂)) Domθ'≠FVe  with ready-maint-θˡ θ' (aplus x₂) ((proj₁ Domθ'≠FVe) , (proj₁ (proj₂ Domθ'≠FVe)) , dist':: (proj₂ (proj₂ Domθ'≠FVe)))
... | (aplus f) = aplus (brseq (Env.seq-←-monoˡ x θ θ' x₁) ∷ f)
ready-maint-θˡ{θ} θ' (aplus (brshr{s = s} s∈ s≡ ∷ x₁)) Domθ'≠FVe  with ready-maint-θˡ θ' (aplus x₁) (((proj₁ Domθ'≠FVe) ,  dist':: (proj₁ (proj₂ Domθ'≠FVe)) , (proj₂ (proj₂ Domθ'≠FVe))))
    | shr-←-irr-get{θ}{θ'}{s} s∈ (λ x → (proj₁ (proj₂ Domθ'≠FVe)) _ x (here refl))
... | (aplus f) | (s∈2 , eq) rewrite eq = aplus ((brshr s∈2 s≡) ∷ f)
ready-irr-on-irr-θˡ-help : ∀{θ e} θ' → (e' : all-ready e θ) → (distinct (Dom θ') (FVₑ e))
                     → (e'' : (all-ready e (θ ← θ'))) → δ e' ≡ δ e''
ready-irr-on-irr-θˡ-help θ' (aplus []) Domθ'≠FVe (aplus []) = refl
ready-irr-on-irr-θˡ-help θ' (aplus (brnum ∷ x₁)) Domθ'≠FVe (aplus (brnum ∷ x₂))
   rewrite ready-irr-on-irr-θˡ-help θ' (aplus x₁) Domθ'≠FVe (aplus x₂)
   = refl
ready-irr-on-irr-θˡ-help{θ} θ' (aplus (brseq{x = x} x₁ ∷ x₂)) Domθ'≠FVe (aplus (brseq x₃ ∷ x₄))
   rewrite ready-irr-on-irr-θˡ-help θ' (aplus x₂) ((proj₁ Domθ'≠FVe) , (proj₁ (proj₂ Domθ'≠FVe)) , dist':: (proj₂ (proj₂ Domθ'≠FVe))) (aplus x₄)
         | seq-←-irr-get'{θ}{θ'}{x} x₁ (λ x → (proj₂ (proj₂ Domθ'≠FVe)) _ x (here refl)) x₃
   = refl
ready-irr-on-irr-θˡ-help{θ} θ' (aplus (brshr{s = s} s∈ x ∷ x₁)) Domθ'≠FVe (aplus (brshr s∈₁ x₂ ∷ x₃))
    rewrite ready-irr-on-irr-θˡ-help θ' (aplus x₁) ((proj₁ Domθ'≠FVe) , dist':: (proj₁ (proj₂ Domθ'≠FVe)) , (proj₂ (proj₂ Domθ'≠FVe))) (aplus x₃)
          | shr-←-irr-get/vals'{θ}{θ'}{s} s∈ (λ x → (proj₁ (proj₂ Domθ'≠FVe)) _ x (here refl)) s∈₁
    = refl

ready-irr-on-irr-θˡ : ∀{θ e} θ' → (e' : all-ready e θ) → (distinct (Dom θ') (FVₑ e))
                     → Σ[ e'' ∈ (all-ready e (θ ← θ')) ] δ e' ≡ δ e''
ready-irr-on-irr-θˡ θ' e' Domθ'≠FVe = _ , ready-irr-on-irr-θˡ-help θ' e' Domθ'≠FVe (ready-maint-θˡ θ' e' Domθ'≠FVe)

ready-maint-θʳ : ∀ {θ' e} θ → (e' : all-ready e θ') → all-ready e (θ ← θ')
ready-maint-θʳ θ (aplus []) = aplus []
ready-maint-θʳ θ (aplus (brnum ∷ bound-readys))
  with ready-maint-θʳ θ (aplus bound-readys)
... | aplus bound-readys' = aplus (brnum ∷ bound-readys')
ready-maint-θʳ {θ'} θ (aplus (brseq {x = x} x∈Domθ' ∷ bound-readys))
  with ready-maint-θʳ θ (aplus bound-readys)
... | aplus bound-readys' = aplus (brseq (seq-←-monoʳ x θ' θ x∈Domθ') ∷ bound-readys')
ready-maint-θʳ {θ'} θ (aplus (brshr {s = s} s∈Domθ' θ's≡ready ∷ bound-readys))
  with ready-maint-θʳ θ (aplus bound-readys)
... | aplus bound-readys' =
  aplus (brshr (shr-←-monoʳ s θ' θ s∈Domθ')
               (trans
                 (shr-stats-←-right-irr' s θ θ' s∈Domθ'
                   (shr-←-monoʳ s θ' θ s∈Domθ'))
                 θ's≡ready) ∷
         bound-readys')

ready-irr-on-irr-θʳ-help : ∀ {θ' e} θ →
  (e' : all-ready e θ') →
  (e'' : all-ready e (θ ← θ')) →
  δ e' ≡ δ e''
ready-irr-on-irr-θʳ-help {θ'} θ (aplus []) (aplus []) = refl
ready-irr-on-irr-θʳ-help {θ'} θ (aplus (brnum ∷ bound-readys')) (aplus (brnum ∷ bound-readys''))
  with ready-irr-on-irr-θʳ-help θ (aplus bound-readys') (aplus bound-readys'')
... | δe'≡δe'' rewrite δe'≡δe'' = refl
ready-irr-on-irr-θʳ-help {θ'} θ
  (aplus (brseq {x = x}  x∈Domθ' ∷ bound-readys'))
  (aplus (brseq {x = .x} x∈Domθ←θ' ∷ bound-readys''))
  with ready-irr-on-irr-θʳ-help θ (aplus bound-readys') (aplus bound-readys'')
... | δe'≡δe'' rewrite δe'≡δe'' | var-vals-←-right-irr' x θ θ' x∈Domθ' x∈Domθ←θ' = refl
ready-irr-on-irr-θʳ-help {θ'} θ
  (aplus (brshr {s = s}  s∈Domθ'   θ's≡ready     ∷ bound-readys'))
  (aplus (brshr {s = .s} s∈Domθ←θ' ⟨θ←θ'⟩s≡ready ∷ bound-readys''))
  with ready-irr-on-irr-θʳ-help θ (aplus bound-readys') (aplus bound-readys'')
... | δe'≡δe'' rewrite δe'≡δe'' | shr-vals-←-right-irr' s θ θ' s∈Domθ' s∈Domθ←θ' = refl

ready-irr-on-irr-θʳ : ∀ {θ' e} θ →
  (e' : all-ready e θ') →
  Σ[ e'' ∈ all-ready e (θ ← θ') ] δ e' ≡ δ e''
ready-irr-on-irr-θʳ θ e' = _ , ready-irr-on-irr-θʳ-help θ e' (ready-maint-θʳ θ e')

CBE⟦p⟧=>CBp : ∀{BV FV E p} → CorrectBinding (E ⟦ p ⟧e) BV FV → ∃ (λ BV → ∃ (λ FV → (CorrectBinding p BV FV)))
CBE⟦p⟧=>CBp{BV}{FV} {E = []} CB = BV , FV , CB
CBE⟦p⟧=>CBp {E = epar₁ q ∷ E} (CBpar CB CB₁ x x₁ x₂ x₃) = CBE⟦p⟧=>CBp{E = E} CB
CBE⟦p⟧=>CBp {E = epar₂ p ∷ E} (CBpar CB CB₁ x x₁ x₂ x₃) = CBE⟦p⟧=>CBp{E = E} CB₁
CBE⟦p⟧=>CBp {E = eloopˢ q ∷ E} (CBloopˢ CB CB₁ x _) = CBE⟦p⟧=>CBp{E = E} CB
CBE⟦p⟧=>CBp {E = eseq q ∷ E} (CBseq CB CB₁ x) = CBE⟦p⟧=>CBp{E = E} CB
CBE⟦p⟧=>CBp {E = esuspend S ∷ E} (CBsusp CB x) = CBE⟦p⟧=>CBp{E = E} CB
CBE⟦p⟧=>CBp {E = etrap ∷ E} (CBtrap CB) = CBE⟦p⟧=>CBp{E = E} CB

CBE⟦p⟧=>CBp' : ∀{BV FV E p p'} → p ≐ E ⟦ p' ⟧e →  CorrectBinding (p) BV FV → ∃ (λ BV → ∃ (λ FV → (CorrectBinding p' BV FV)))
CBE⟦p⟧=>CBp'{E = E}{p' = p'} peq cb = CBE⟦p⟧=>CBp{E = E}{p = p'} (subst (λ x → CorrectBinding x _ _) (sym (unplug peq)) cb)
-- , (BV⊆S , BV⊆s , BV⊆x)

CBp⊆CBE⟦p⟧ : ∀{BVp FVp BVE FVE} → (E : EvaluationContext ) → (p : Term) → CorrectBinding p BVp FVp → CorrectBinding (E ⟦ p ⟧e) BVE FVE → (FVp ⊆ FVE × BVp ⊆ BVE)

CBp⊆CBE⟦p⟧ [] p CBp CBE with binding-is-function CBp CBE
... | (e1 , e2) rewrite e1 | e2 = (((λ x z → z) , (λ x z → z) , (λ x z → z))) , (((λ x z → z) , (λ x z → z) , (λ x z → z)))
CBp⊆CBE⟦p⟧ (epar₁ q ∷ E) p CBp (CBpar CBE CBE₁ x x₁ x₂ x₃) with CBp⊆CBE⟦p⟧ E p CBp CBE
... | (FV⊆S , FV⊆s , FV⊆x) , (BV⊆S , BV⊆s , BV⊆x) = ((λ x y → ++ˡ (FV⊆S x y)) , ((λ x y → ++ˡ (FV⊆s x y))) , ((λ x y → ++ˡ (FV⊆x x y)))) , (((λ x y → ++ˡ (BV⊆S x y))) , ((λ x y → ++ˡ (BV⊆s x y))) , ((λ x y → ++ˡ (BV⊆x x y))))

CBp⊆CBE⟦p⟧ (epar₂ p ∷ E) p₁ CBp (CBpar{BVp = BVp}{FVp = FVp} CBE CBE₁ x x₁ x₂ x₃) with CBp⊆CBE⟦p⟧ E p₁ CBp CBE₁
... | (FV⊆S , FV⊆s , FV⊆x) , (BV⊆S , BV⊆s , BV⊆x)
   = ((λ x z → ++ʳ (proj₁ FVp) (FV⊆S x z)) , (λ x → (++ʳ (proj₁ (proj₂ FVp))) ∘ (FV⊆s x)) , ((λ x → (++ʳ (proj₂ (proj₂ FVp))) ∘ (FV⊆x x))))
   , ((λ x z → ++ʳ (proj₁ BVp) (BV⊆S x z)) , (λ x → (++ʳ (proj₁ (proj₂ BVp))) ∘ (BV⊆s x)) , ((λ x → (++ʳ (proj₂ (proj₂ BVp))) ∘ (BV⊆x x))))
CBp⊆CBE⟦p⟧ (eloopˢ q ∷ E) p CBp (CBloopˢ CBE CBE₁ x _) with CBp⊆CBE⟦p⟧ E p CBp CBE
... | (FV⊆S , FV⊆s , FV⊆x) , (BV⊆S , BV⊆s , BV⊆x) = ((λ x y → ++ˡ (FV⊆S x y)) , ((λ x → ++ˡ ∘ (FV⊆s x)) ) , get FV⊆x) , (get BV⊆S , get BV⊆s , get BV⊆x)
   where
   get : ∀{a b c} → a ⊆¹ b → a ⊆¹ (b ++ c)
   get f = λ x y → ++ˡ (f x y)
CBp⊆CBE⟦p⟧ (eseq q ∷ E) p CBp (CBseq CBE CBE₁ x) with CBp⊆CBE⟦p⟧ E p CBp CBE
... | (FV⊆S , FV⊆s , FV⊆x) , (BV⊆S , BV⊆s , BV⊆x) = ((λ x y → ++ˡ (FV⊆S x y)) , ((λ x → ++ˡ ∘ (FV⊆s x)) ) , get FV⊆x) , (get BV⊆S , get BV⊆s , get BV⊆x)
   where
   get : ∀{a b c} → a ⊆¹ b → a ⊆¹ (b ++ c)
   get f = λ x y → ++ˡ (f x y)
   --(λ x₁ x₂ → {!there x₂!})
CBp⊆CBE⟦p⟧ (esuspend S ∷ E) p CBp (CBsusp CBE x) with CBp⊆CBE⟦p⟧ E p CBp CBE
... | (FV⊆S , FV⊆s , FV⊆x) , BV⊆ = (((λ x y → there (FV⊆S x y)) , FV⊆s , FV⊆x)) , BV⊆
CBp⊆CBE⟦p⟧ (etrap ∷ E) p CBp (CBtrap CBE) = CBp⊆CBE⟦p⟧ E p CBp CBE

CBp⊆CBE⟦p⟧' : ∀{BVp FVp BVE FVE} E p p' → p ≐ E ⟦ p' ⟧e → CorrectBinding p' BVp FVp → CorrectBinding p BVE FVE → (FVp ⊆ FVE × BVp ⊆ BVE)
CBp⊆CBE⟦p⟧' E p p' peq cbp' cbp = CBp⊆CBE⟦p⟧ E p' cbp' (subst (λ x → CorrectBinding x _ _) (sym (unplug peq)) cbp)

inspecting-cb-distinct-double-unplug : ∀{p q Ep Eq p' q' BV FV} → CorrectBinding (p ∥ q) BV FV
                            → p ≐ Ep ⟦ p' ⟧e → q ≐ Eq ⟦ q' ⟧e
                            →
                            Σ (Term × VarList × VarList)
                              λ {(o , BVo , FVo)
                                → CorrectBinding o BVo FVo
                                × o ≡ (p' ∥ q')}
inspecting-cb-distinct-double-unplug{p' = p'}{q'} (CBpar CBp CBq BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) p=Ep⟦p'⟧ q=Eq⟦q'⟧
     with CBE⟦p⟧=>CBp' p=Ep⟦p'⟧ CBp | CBE⟦p⟧=>CBp' q=Eq⟦q'⟧ CBq
... | (BVp' , FVp' , CBp') | (BVq' , FVq' , CBq')
   with CBp⊆CBE⟦p⟧' _ _ _ p=Ep⟦p'⟧ CBp' CBp | CBp⊆CBE⟦p⟧' _ _ _ q=Eq⟦q'⟧ CBq' CBq
... | (FVp'⊆FVp , BVp'⊆BVp) | (FVq'⊆FVq , BVq'⊆BVq)
  = (_ , _ , _) , CBpar CBp' CBq' (⊆-rep-dist-both BVp'⊆BVp BVq'⊆BVq BVp≠BVq) (⊆-rep-dist-both FVp'⊆FVp BVq'⊆BVq FVp≠BVq) (⊆-rep-dist-both BVp'⊆BVp FVq'⊆FVq BVp≠FVq) (⊆¹-rep-dist-both (proj₂ (proj₂ FVp'⊆FVp)) (proj₂ (proj₂ FVq'⊆FVq)) Xp≠Xq) , refl
  where
    ⊆¹-rep-dist-both : ∀{a b c d} → a ⊆¹ b →  c ⊆¹ d → distinct' b d → distinct' a c
    ⊆¹-rep-dist-both sub1 sub2 dist = λ z z₁ z₂ → dist z (sub1 z z₁) (sub2 z z₂)
    ⊆-rep-dist-both : ∀{a b c d} → a ⊆ b →  c ⊆ d → distinct b d → distinct a c
    ⊆-rep-dist-both a b c = (⊆¹-rep-dist-both , ⊆¹-rep-dist-both , ⊆¹-rep-dist-both) # a # b # c

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
module Fail.TupleType where

open import Haskell.Prelude

idT : ∀ {as} → Tuple as → Tuple as
idT x = x

{-# COMPILE AGDA2HS idT #-}


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Adjoint.Equivalents where

-- Theorems about equivalent formulations to Adjoint
-- (though some have caveats)

open import Level

open import Data.Product using (_,_; _×_)
open import Function using (_$_) renaming (_∘_ to _∙_)
open import Function.Equality using (Π; _⟶_)
import Function.Inverse as FI
open import Relation.Binary using (Rel; IsEquivalence; Setoid)

-- be explicit in imports to 'see' where the information comes from
open import Categories.Adjoint using (Adjoint; _⊣_)
open import Categories.Category.Core using (Category)
open import Categories.Category.Product using (Product; _⁂_)
open import Categories.Category.Instance.Setoids
open import Categories.Morphism
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Functor.Bifunctor using (Bifunctor)
open import Categories.Functor.Hom using (Hom[_][-,-])
open import Categories.Functor.Construction.LiftSetoids
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper; _∘ₕ_; _∘ᵥ_; _∘ˡ_; _∘ʳ_)
  renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism; unitorˡ; unitorʳ; associator; _≃_)
import Categories.Morphism.Reasoning as MR

private
  variable
    o o′ o″ ℓ ℓ′ ℓ″ e e′ e″ : Level
    C D E : Category o ℓ e

-- a special case of the natural isomorphism in which homsets in C and D have the same
-- universe level. therefore there is no need to lift Setoids to the same level.
-- this is helpful when combining with Yoneda lemma.
module _ {C : Category o ℓ e} {D : Category o′ ℓ e} {L : Functor C D} {R : Functor D C} where
  private
    module C = Category C
    module D = Category D
    module L = Functor L
    module R = Functor R

  module _ (adjoint : L ⊣ R) where
    open Adjoint adjoint

    -- in this case, the hom functors are naturally isomorphism directly
    Hom-NI′ : NaturalIsomorphism Hom[L-,-] Hom[-,R-]
    Hom-NI′ = record
      { F⇒G = ntHelper record
        { η       = λ _ → Hom-inverse.to
        ; commute = λ _ eq → Ladjunct-comm eq
        }
      ; F⇐G = ntHelper record
        { η       = λ _ → Hom-inverse.from
        ; commute = λ _ eq → Radjunct-comm eq
        }
      ; iso = λ _ → record
        { isoˡ = λ eq → let open D.HomReasoning in RLadjunct≈id ○ eq
        ; isoʳ = λ eq → let open C.HomReasoning in LRadjunct≈id ○ eq
        }
      }

  -- now goes from natural isomorphism back to adjoint.
  -- for simplicity, just construct the case in which homsetoids of C and D
  -- are compatible.

  private
    Hom[L-,-] : Bifunctor C.op D (Setoids _ _)
    Hom[L-,-] = Hom[ D ][-,-] ∘F (L.op ⁂ idF)

    Hom[-,R-] : Bifunctor C.op D (Setoids _ _)
    Hom[-,R-] = Hom[ C ][-,-] ∘F (idF ⁂ R)

  module _ (Hni : NaturalIsomorphism Hom[L-,-] Hom[-,R-]) where
    open NaturalIsomorphism Hni
    open NaturalTransformation
    open Functor
    open Π

    private
      unitη : ∀ X → F₀ Hom[L-,-] (X , L.F₀ X) ⟶ F₀ Hom[-,R-] (X , L.F₀ X)
      unitη X = ⇒.η (X , L.F₀ X)

      unit : NaturalTransformation idF (R ∘F L)
      unit = ntHelper record
        { η       = λ X → unitη X ⟨$⟩ D.id
        ; commute = λ {X} {Y} f → begin
          (unitη Y ⟨$⟩ D.id) ∘ f                             ≈⟨ introˡ R.identity ⟩
          R.F₁ D.id ∘ (unitη Y  ⟨$⟩ D.id) ∘ f                ≈˘⟨ ⇒.commute (f , D.id) D.Equiv.refl ⟩
          ⇒.η (X , L.F₀ Y) ⟨$⟩ (D.id D.∘ D.id D.∘ L.F₁ f)    ≈⟨ cong (⇒.η (X , L.F₀ Y)) (D.Equiv.trans D.identityˡ D.identityˡ) ⟩
          ⇒.η (X , L.F₀ Y) ⟨$⟩ L.F₁ f                        ≈⟨ cong (⇒.η (X , L.F₀ Y)) (MR.introʳ D (MR.elimʳ D L.identity)) ⟩
          ⇒.η (X , L.F₀ Y) ⟨$⟩ (L.F₁ f D.∘ D.id D.∘ L.F₁ id) ≈⟨ ⇒.commute (C.id , L.F₁ f) D.Equiv.refl ⟩
          R.F₁ (L.F₁ f) ∘ (unitη X ⟨$⟩ D.id) ∘ id            ≈⟨ refl⟩∘⟨ identityʳ ⟩
          R.F₁ (L.F₁ f) ∘ (unitη X ⟨$⟩ D.id)                 ∎
        }
        where open C
              open HomReasoning
              open MR C

      counitη : ∀ X → F₀ Hom[-,R-] (R.F₀ X , X) ⟶ F₀ Hom[L-,-] (R.F₀ X , X)
      counitη X = ⇐.η (R.F₀ X , X)

      counit : NaturalTransformation (L ∘F R) idF
      counit = ntHelper record
        { η       = λ X → counitη X ⟨$⟩ C.id
        ; commute = λ {X} {Y} f → begin
          (counitη Y ⟨$⟩ C.id) ∘ L.F₁ (R.F₁ f)               ≈˘⟨ identityˡ ⟩
          id ∘ (counitη Y ⟨$⟩ C.id) ∘ L.F₁ (R.F₁ f)          ≈˘⟨ ⇐.commute (R.F₁ f , D.id) C.Equiv.refl ⟩
          ⇐.η (R.F₀ X , Y) ⟨$⟩ (R.F₁ id C.∘ C.id C.∘ R.F₁ f) ≈⟨ cong (⇐.η (R.F₀ X , Y)) (C.Equiv.trans (MR.elimˡ C R.identity) C.identityˡ) ⟩
          ⇐.η (R.F₀ X , Y) ⟨$⟩ R.F₁ f                        ≈⟨ cong (⇐.η (R.F₀ X , Y)) (MR.introʳ C C.identityˡ) ⟩
          ⇐.η (R.F₀ X , Y) ⟨$⟩ (R.F₁ f C.∘ C.id C.∘ C.id)    ≈⟨ ⇐.commute (C.id , f) C.Equiv.refl ⟩
          f ∘ (counitη X ⟨$⟩ C.id) ∘ L.F₁ C.id               ≈⟨ refl⟩∘⟨ elimʳ L.identity ⟩
          f ∘ (counitη X ⟨$⟩ C.id)                           ∎
        }
        where open D
              open HomReasoning
              open MR D

    Hom-NI⇒Adjoint : L ⊣ R
    Hom-NI⇒Adjoint = record
      { unit   = unit
      ; counit = counit
      ; zig    = λ {A} →
        let open D
            open HomReasoning
            open Equiv
            open MR D
        in begin
          η counit (L.F₀ A) ∘ L.F₁ (η unit A)      ≈˘⟨ identityˡ ⟩
          id ∘ η counit (L.F₀ A) ∘ L.F₁ (η unit A) ≈˘⟨ ⇐.commute (η unit A , id) C.Equiv.refl ⟩
          ⇐.η (A , L.F₀ A) ⟨$⟩ (R.F₁ id C.∘ C.id C.∘ η unit A)
                                                   ≈⟨ cong (⇐.η (A , L.F₀ A)) (C.Equiv.trans (MR.elimˡ C R.identity) C.identityˡ) ⟩
          ⇐.η (A , L.F₀ A) ⟨$⟩ η unit A            ≈⟨ isoˡ refl ⟩
          id
                                                   ∎
      ; zag    = λ {B} →
        let open C
            open HomReasoning
            open Equiv
            open MR C
        in begin
          R.F₁ (η counit B) ∘ η unit (R.F₀ B)      ≈˘⟨ refl⟩∘⟨ identityʳ ⟩
          R.F₁ (η counit B) ∘ η unit (R.F₀ B) ∘ id ≈˘⟨ ⇒.commute (id , η counit B) D.Equiv.refl ⟩
          ⇒.η (R.F₀ B , B) ⟨$⟩ (η counit B D.∘ D.id D.∘ L.F₁ id)
                                                   ≈⟨ cong (⇒.η (R.F₀ B , B)) (MR.elimʳ D (MR.elimʳ D L.identity)) ⟩
          ⇒.η (R.F₀ B , B) ⟨$⟩ η counit B          ≈⟨ isoʳ refl ⟩
          id                                       ∎
      }
      where module i {X} = Iso (iso X)
            open i

-- the general case from isomorphic Hom setoids to adjoint functors
module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {L : Functor C D} {R : Functor D C} where
  private
    module C = Category C
    module D = Category D
    module L = Functor L
    module R = Functor R
    open Functor
    open Π

    Hom[L-,-] : Bifunctor C.op D (Setoids _ _)
    Hom[L-,-] = LiftSetoids ℓ e ∘F Hom[ D ][-,-] ∘F (L.op ⁂ idF)

    Hom[-,R-] : Bifunctor C.op D (Setoids _ _)
    Hom[-,R-] = LiftSetoids ℓ′ e′ ∘F Hom[ C ][-,-] ∘F (idF ⁂ R)

  module _ (Hni : Hom[L-,-] ≃ Hom[-,R-]) where
    open NaturalIsomorphism Hni using (module ⇒; module ⇐; iso)
    private
      unitη : ∀ X → F₀ Hom[L-,-] (X , L.F₀ X) ⟶ F₀ Hom[-,R-] (X , L.F₀ X)
      unitη X = ⇒.η (X , L.F₀ X)

      unit : NaturalTransformation idF (R ∘F L)
      unit = ntHelper record
        { η       = λ X → lower (unitη X ⟨$⟩ lift D.id)
        ; commute = λ {X Y} f → begin
          lower (unitη Y ⟨$⟩ lift D.id) ∘ f
            ≈⟨ introˡ R.identity ⟩
          R.F₁ D.id ∘ lower (unitη Y ⟨$⟩ lift D.id) ∘ f
            ≈˘⟨ lower (⇒.commute (f , D.id) (lift D.Equiv.refl)) ⟩
          lower (⇒.η (X , L.F₀ Y) ⟨$⟩ lift (D.id D.∘ D.id D.∘ L.F₁ f))
            ≈⟨ lower (cong (⇒.η (X , L.F₀ Y)) (lift (D.Equiv.trans D.identityˡ D.identityˡ))) ⟩
          lower (⇒.η (X , L.F₀ Y) ⟨$⟩ lift (L.F₁ f))
            ≈⟨ lower (cong (⇒.η (X , L.F₀ Y)) (lift (MR.introʳ D (MR.elimʳ D L.identity)))) ⟩
          lower (⇒.η (X , L.F₀ Y) ⟨$⟩ lift (L.F₁ f D.∘ D.id D.∘ L.F₁ id))
            ≈⟨ lower (⇒.commute (C.id , L.F₁ f) (lift D.Equiv.refl)) ⟩
          R.F₁ (L.F₁ f) ∘ lower (⇒.η (X , L.F₀ X) ⟨$⟩ lift D.id) ∘ id
            ≈⟨ refl⟩∘⟨ identityʳ ⟩
          F₁ (R ∘F L) f ∘ lower (unitη X ⟨$⟩ lift D.id)                ∎
        }
        where open C
              open HomReasoning
              open MR C

      counitη : ∀ X → F₀ Hom[-,R-] (R.F₀ X , X) ⟶ F₀ Hom[L-,-] (R.F₀ X , X)
      counitη X = ⇐.η (R.F₀ X , X)

      counit : NaturalTransformation (L ∘F R) idF
      counit = ntHelper record
        { η       = λ X → lower (counitη X ⟨$⟩ lift C.id)
        ; commute = λ {X} {Y} f → begin
          lower (⇐.η (R.F₀ Y , Y) ⟨$⟩ lift C.id) ∘ L.F₁ (R.F₁ f)
            ≈˘⟨ identityˡ ⟩
          id ∘ lower (⇐.η (R.F₀ Y , Y) ⟨$⟩ lift C.id) ∘ L.F₁ (R.F₁ f)
            ≈˘⟨ lower (⇐.commute (R.F₁ f , D.id) (lift C.Equiv.refl)) ⟩
          lower (⇐.η (R.F₀ X , Y) ⟨$⟩ lift (R.F₁ id C.∘ C.id C.∘ R.F₁ f))
            ≈⟨ lower (cong (⇐.η (R.F₀ X , Y)) (lift (C.Equiv.trans (MR.elimˡ C R.identity) C.identityˡ))) ⟩
          lower (⇐.η (R.F₀ X , Y) ⟨$⟩ lift (R.F₁ f))
            ≈⟨ lower (cong (⇐.η (R.F₀ X , Y)) (lift (MR.introʳ C C.identityˡ))) ⟩
          lower (⇐.η (R.F₀ X , Y) ⟨$⟩ lift (R.F₁ f C.∘ C.id C.∘ C.id))
            ≈⟨ lower (⇐.commute (C.id , f) (lift C.Equiv.refl)) ⟩
          f ∘ lower (⇐.η (R.F₀ X , X) ⟨$⟩ lift C.id) ∘ L.F₁ C.id
            ≈⟨ refl⟩∘⟨ elimʳ L.identity ⟩
          f ∘ lower (⇐.η (R.F₀ X , X) ⟨$⟩ lift C.id)
            ∎
        }
        where open D
              open HomReasoning
              open MR D

    Hom-NI′⇒Adjoint : L ⊣ R
    Hom-NI′⇒Adjoint = record
      { unit   = unit
      ; counit = counit
      ; zig    = λ {A} →
        let open D
            open HomReasoning
            open Equiv
            open MR D
        in begin
          lower (counitη (L.F₀ A) ⟨$⟩ lift C.id) ∘ L.F₁ (η unit A)
            ≈˘⟨ identityˡ ⟩
          id ∘ lower (counitη (L.F₀ A) ⟨$⟩ lift C.id) ∘ L.F₁ (η unit A)
            ≈˘⟨ lower (⇐.commute (η unit A , id) (lift C.Equiv.refl)) ⟩
          lower (⇐.η (A , L.F₀ A) ⟨$⟩ lift (R.F₁ id C.∘ C.id C.∘ lower (⇒.η (A , L.F₀ A) ⟨$⟩ lift id)))
            ≈⟨ lower (cong (⇐.η (A , L.F₀ A)) (lift (C.Equiv.trans (MR.elimˡ C R.identity) C.identityˡ))) ⟩
          lower (⇐.η (A , L.F₀ A) ⟨$⟩ (⇒.η (A , L.F₀ A) ⟨$⟩ lift id))
            ≈⟨ lower (isoˡ (lift refl)) ⟩
          id ∎
      ; zag    = λ {B} →
        let open C
            open HomReasoning
            open Equiv
            open MR C
        in begin
          R.F₁ (lower (⇐.η (R.F₀ B , B) ⟨$⟩ lift id)) ∘ lower (⇒.η (R.F₀ B , L.F₀ (R.F₀ B)) ⟨$⟩ lift D.id)
            ≈˘⟨ refl⟩∘⟨ identityʳ ⟩
          R.F₁ (lower (⇐.η (R.F₀ B , B) ⟨$⟩ lift id)) ∘ lower (⇒.η (R.F₀ B , L.F₀ (R.F₀ B)) ⟨$⟩ lift D.id) ∘ id
            ≈˘⟨ lower (⇒.commute (id , η counit B) (lift D.Equiv.refl)) ⟩
          lower (⇒.η (R.F₀ B , B) ⟨$⟩ lift (lower (⇐.η (R.F₀ B , B) ⟨$⟩ lift id) D.∘ D.id D.∘ L.F₁ id))
            ≈⟨ lower (cong (⇒.η (R.F₀ B , B)) (lift (MR.elimʳ D (MR.elimʳ D L.identity)))) ⟩
          lower (⇒.η (R.F₀ B , B) ⟨$⟩ lift (lower (⇐.η (R.F₀ B , B) ⟨$⟩ lift id)))
            ≈⟨ lower (isoʳ (lift refl)) ⟩
          id ∎
      }
      where open NaturalTransformation
            module _ {X} where
              open Iso (iso X) public

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

open import LogicalFormulae
open import Groups.DirectSum.Definition
open import Setoids.Setoids
open import Rings.Definition

module Rings.DirectSum {a b c d : _} {A : Set a} {S : Setoid {a} {b} A} {_+1_ : A → A → A} {_*1_ : A → A → A} {C : Set c} {T : Setoid {c} {d} C} {_+2_ : C → C → C} {_*2_ : C → C → C} (R1 : Ring S _+1_ _*1_) (R2 : Ring T _+2_ _*2_) where

open import Setoids.Product S T

pairPlus : A && C → A && C → A && C
pairPlus (a ,, b) (c ,, d) = (a +1 c) ,, (b +2 d)

pairTimes : A && C → A && C → A && C
pairTimes (a ,, b) (c ,, d) = (a *1 c) ,, (b *2 d)

directSumRing : Ring productSetoid pairPlus pairTimes
Ring.additiveGroup directSumRing = directSumGroup (Ring.additiveGroup R1) (Ring.additiveGroup R2)
Ring.*WellDefined directSumRing r=t s=u = productLift (Ring.*WellDefined R1 (_&&_.fst r=t) (_&&_.fst s=u)) (Ring.*WellDefined R2 (_&&_.snd r=t) (_&&_.snd s=u))
Ring.1R directSumRing = Ring.1R R1 ,, Ring.1R R2
Ring.groupIsAbelian directSumRing = productLift (Ring.groupIsAbelian R1) (Ring.groupIsAbelian R2)
Ring.*Associative directSumRing = productLift (Ring.*Associative R1) (Ring.*Associative R2)
Ring.*Commutative directSumRing = productLift (Ring.*Commutative R1) (Ring.*Commutative R2)
Ring.*DistributesOver+ directSumRing = productLift (Ring.*DistributesOver+ R1) (Ring.*DistributesOver+ R2)
Ring.identIsIdent directSumRing = productLift (Ring.identIsIdent R1) (Ring.identIsIdent R2)


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

open import Prelude
import GSeTT.Typed-Syntax
import Globular-TT.Syntax
import Globular-TT.Rules

module Globular-TT.Globular-TT {l} (index : Set l) (rule : index → GSeTT.Typed-Syntax.Ctx × (Globular-TT.Syntax.Pre-Ty index))
                                                   (assumption : Globular-TT.Rules.well-founded index rule)
                                                   (eqdec-index : eqdec index)
                                                   where

  open import Globular-TT.Syntax index
  open import Globular-TT.Eqdec-syntax index eqdec-index
  open import Globular-TT.Rules index rule
  open import Globular-TT.CwF-Structure index rule
  open import Globular-TT.Uniqueness-Derivations index rule eqdec-index
  open import Globular-TT.Disks index rule eqdec-index
  open import Globular-TT.Typed-Syntax index rule eqdec-index
  open import Globular-TT.Dec-Type-Checking index rule assumption eqdec-index

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: ThiBen/catt-formalization

max_forks_repo_name: ThiBen/catt-formalization


text:
-- {-# OPTIONS -v interaction:50 #-}

x : Set → Set
x = {!λ x → x!}

-- "refine" (C-c C-r) should behave the same as "give" here
-- Old, bad result:
-- x = λ x₁ → x₁
-- New, expected result:
-- x = λ x → x

-- Expected interaction test case behavior:
--
--   (agda2-give-action 0 'no-paren)


text:
module Luau.Type where

data Type : Set where
  nil : Type
  _⇒_ : Type → Type → Type
  none : Type
  any : Type
  _∪_ : Type → Type → Type
  _∩_ : Type → Type → Type

max_stars_repo_name: FreakingBarbarians/luau

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau


text:
------------------------------------------------------------------------------
-- FOCT list terms properties
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Base.List.PropertiesATP where

open import FOTC.Base
open import FOTC.Base.List

------------------------------------------------------------------------------
-- Congruence properties

postulate ∷-leftCong : ∀ {x y xs} → x ≡ y → x ∷ xs ≡ y ∷ xs
{-# ATP prove ∷-leftCong #-}

postulate ∷-rightCong : ∀ {x xs ys} → xs ≡ ys → x ∷ xs ≡ x ∷ ys
{-# ATP prove ∷-rightCong #-}

postulate ∷-Cong : ∀ {x y xs ys} → x ≡ y → xs ≡ ys → x ∷ xs ≡ y ∷ ys
{-# ATP prove ∷-Cong #-}

postulate headCong : ∀ {xs ys} → xs ≡ ys → head₁ xs ≡ head₁ ys
{-# ATP prove headCong #-}

postulate tailCong : ∀ {xs ys} → xs ≡ ys → tail₁ xs ≡ tail₁ ys
{-# ATP prove tailCong #-}

------------------------------------------------------------------------------
-- Injective properties

postulate ∷-injective : ∀ {x y xs ys} → x ∷ xs ≡ y ∷ ys → x ≡ y ∧ xs ≡ ys
{-# ATP prove ∷-injective #-}


text:
module 030-semigroup where

-- We need equivalence.

open import 020-equivalence

-- Semigroups are basically a set with equality and some binary
-- operator which is associative and respects equality.

record SemiGroup
  {M : Set}
  (_==_ : M -> M -> Set)
  (_*_ : M -> M -> M)
  : Set1 where

  field
    equiv : Equivalence _==_
    assoc : ∀ {r s t} -> ((r * s) * t) == (r * (s * t))
    cong : ∀ {r s u v} -> (r == s) -> (u == v) -> (r * u) == (s * v)

  -- The next line brings all fields and declarations of Equivalence
  -- into this record's namespace so we can refer to them in an
  -- unqualified way in proofs (for example, we can write "refl" for
  -- "Equivalence.symm equiv" and so on).

  open Equivalence equiv public

  -- No theorems here yet.

max_stars_repo_name: mcmtroffaes/agda-proofs

max_issues_repo_name: mcmtroffaes/agda-proofs

max_forks_repo_name: mcmtroffaes/agda-proofs


text:
{-# OPTIONS --sized-types #-}
open import Relation.Binary.Core

module SOList.Total.Properties {A : Set}
               (_≤_ : A → A → Set)
               (trans≤ : Transitive _≤_)  where

open import Bound.Total A
open import Bound.Total.Order _≤_
open import Bound.Total.Order.Properties _≤_ trans≤
open import List.Order.Bounded _≤_
open import List.Order.Bounded.Properties _≤_ trans≤
open import List.Sorted _≤_
open import Size
open import SOList.Total _≤_

lemma-solist≤ : {ι : Size}{b t : Bound} → SOList {ι} b t → LeB b t
lemma-solist≤ (onil b≤t) = b≤t
lemma-solist≤ (ocons x xs ys) = transLeB (lemma-solist≤ xs) (lemma-solist≤ ys)

lemma-solist≤* : {ι : Size}{b : Bound}{x : A} → (xs : SOList {ι} b (val x)) → forget xs ≤* (val x)
lemma-solist≤* (onil _) = lenx
lemma-solist≤* (ocons x xs ys) = lemma-++≤* (lemma-solist≤ ys) (lemma-solist≤* xs) (lemma-solist≤* ys)

lemma-solist*≤ : {ι : Size}{b t : Bound} → (xs : SOList {ι} b t) → b *≤ forget xs
lemma-solist*≤ (onil _) = genx
lemma-solist*≤ (ocons x xs ys) = lemma-++*≤ (lemma-solist≤ xs) (lemma-solist*≤ xs) (lemma-solist*≤ ys)

lemma-solist-sorted : {ι : Size}{b t : Bound}(xs : SOList {ι} b t) → Sorted (forget xs)
lemma-solist-sorted (onil _) = nils
lemma-solist-sorted (ocons x xs ys) = lemma-sorted++ (lemma-solist≤* xs) (lemma-solist*≤ ys) (lemma-solist-sorted xs) (lemma-solist-sorted ys)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module test.AddInteger where

open import Type
open import Declarative
open import Builtin
open import Builtin.Constant.Type
open import Builtin.Constant.Term Ctx⋆ Kind * # _⊢⋆_ con size⋆
open import Agda.Builtin.Sigma

-- zerepoch/zerepoch-core/test/data/addInteger.plc

addI : ∀{Γ} →
  Γ ⊢ con integer (size⋆ 8) ⇒ con integer (size⋆ 8) ⇒ con integer (size⋆ 8)
addI =
  ƛ (ƛ (builtin addInteger (λ { Z → size⋆ 8 ; (S ())}) (` (S Z) Σ., ` Z Σ., _)))

max_stars_repo_name: Quantum-One-DLT/zerepoch

max_issues_repo_name: Quantum-One-DLT/zerepoch

max_forks_repo_name: Quantum-One-DLT/zerepoch


text:
-- {-# OPTIONS -v tc.proj.like:10 #-} {-# OPTIONS -v tc.conv:10 #-}
import Common.Level

module ProjectionLikeAndModules1 (A : Set) (a : A) where

record ⊤ : Set where
  constructor tt

data Wrap (W : Set) : Set where
  wrap : W → Wrap W

data Bool : Set where
  true false : Bool

-- `or' should be projection like in the module parameters
if : Bool → {B : Set} → B → B → B
if true  a b = a
if false a b = b

postulate
  u v : ⊤
  P : Wrap ⊤ -> Set

test : (y : Bool)
  -> P (if y (wrap u) (wrap tt))
  -> P (if y (wrap tt) (wrap v))
test y h = h

-- Error:
-- u != tt of type Set
-- when checking that the expression h has type
-- P (if y (wrap tt) (wrap v))

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Everything

module Test.SurjidentityP where

module _
    {𝔬₁} {𝔒₁ : Ø 𝔬₁}
    {𝔯₁} (_∼₁_ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁)
    {𝔬₂} {𝔒₂ : Ø 𝔬₂}
    {𝔯₂} (_∼₂_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂)
         (_∼₂2_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂)
    {𝔯₂'} (_∼₂'_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂')
    {ℓ₂} (_∼̇₂_ : ∀ {x y} → x ∼₂ y → x ∼₂ y → Ø ℓ₂)
         (_∼̇₂'_ : ∀ {x y} → x ∼₂' y → x ∼₂' y → Ø ℓ₂)
         (_∼̇₂2_ : ∀ {x y} → x ∼₂2 y → x ∼₂2 y → Ø ℓ₂)
    ⦃ _ : Surjection.class 𝔒₁ 𝔒₂ ⦄
    ⦃ _ : Smap!.class _∼₁_ _∼₂_                         ⦄
    ⦃ _ : Smap!.class _∼₁_ _∼₂'_                        ⦄
    ⦃ _ : Smap!.class _∼₁_ _∼₂2_                        ⦄
    ⦃ _ : Reflexivity.class _∼₁_                               ⦄
    ⦃ _ : Reflexivity.class _∼₂_                               ⦄
    ⦃ _ : Reflexivity.class _∼₂'_                                ⦄
    ⦃ _ : Reflexivity.class _∼₂2_                                ⦄
    ⦃ _ : Surjidentity!.class _∼₁_ _∼₂_ _∼̇₂_                        ⦄
    ⦃ _ : Surjidentity!.class _∼₁_ _∼₂'_ _∼̇₂'_                     ⦄
    ⦃ _ : Surjidentity!.class _∼₁_ _∼₂2_ _∼̇₂2_                     ⦄
    where

  test-surj : Surjidentity!.type _∼₁_ _∼₂_ _∼̇₂_
  test-surj = surjidentity

  test-surj[] : Surjidentity!.type _∼₁_ _∼₂_ _∼̇₂_
  test-surj[] = surjidentity[ _∼₁_ , _∼̇₂_ ]


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

open import Cubical.Core.Everything
open import Cubical.Relation.Binary
open import Cubical.Data.Sigma using (_×_)
open import Cubical.Data.Sum using (_⊎_)
open import Cubical.HITs.PropositionalTruncation using (∥_∥)

open import Cubical.Algebra.Base

private
  variable
    a b c ℓ : Level
    A : Type a
    B : Type b
    C : Type c

------------------------------------------------------------------------
-- Properties of operations

Congruent₁ : Rel A ℓ → Op₁ A → Type _
Congruent₁ R f = f Preserves R ⟶ R

Congruent₂ : Rel A ℓ → Op₂ A → Type _
Congruent₂ R • = • Preserves₂ R ⟶ R ⟶ R

LeftCongruent : Rel A ℓ → Op₂ A → Type _
LeftCongruent R _•_ = ∀ {x} → (x •_) Preserves R ⟶ R

RightCongruent : Rel A ℓ → Op₂ A → Type _
RightCongruent R _•_ = ∀ {x} → (_• x) Preserves R ⟶ R

Homomorphic₀ : (A → B) → A → B → Type _
Homomorphic₀ ⟦_⟧ x y = ⟦ x ⟧ ≡ y

Homomorphic₁ : (A → B) → Op₁ A → Op₁ B → Type _
Homomorphic₁ ⟦_⟧ f g = ∀ x → ⟦ f x ⟧ ≡ g ⟦ x ⟧

Homomorphic₂ : (A → B) → Op₂ A → Op₂ B → Type _
Homomorphic₂ ⟦_⟧ _•_ _◦_ = ∀ x y → ⟦ x • y ⟧ ≡ ⟦ x ⟧ ◦ ⟦ y ⟧

Contramorphic₂ : (A → B) → Op₂ A → Op₂ B → Type _
Contramorphic₂ ⟦_⟧ _•_ _◦_ = ∀ x y → ⟦ x • y ⟧ ≡ ⟦ y ⟧ ◦ ⟦ x ⟧

Associative : Op₂ A → Type _
Associative _•_ = ∀ x y z → (x • y) • z ≡ x • (y • z)

Commutative : Op₂ A → Type _
Commutative _•_ = ∀ x y → x • y ≡ y • x

LeftIdentity : A → Opₗ A B → Type _
LeftIdentity e _•_ = ∀ x → e • x ≡ x

RightIdentity : A → Opᵣ A B → Type _
RightIdentity e _•_ = ∀ x → x • e ≡ x

Identity : A → Op₂ A → Type _
Identity e • = (LeftIdentity e •) × (RightIdentity e •)

LeftZero : A → Opᵣ B A → Type _
LeftZero z _•_ = ∀ x → z • x ≡ z

RightZero : A → Opₗ B A → Type _
RightZero z _•_ = ∀ x → x • z ≡ z

Zero : A → Op₂ A → Type _
Zero z • = (LeftZero z •) × (RightZero z •)

LeftInverse : C → (A → B) → (B → A → C) → Type _
LeftInverse e _⁻¹ _•_ = ∀ x → (x ⁻¹) • x ≡ e

RightInverse : C → (A → B) → (A → B → C) → Type _
RightInverse e _⁻¹ _•_ = ∀ x → x • (x ⁻¹) ≡ e

Inverse : A → Op₁ A → Op₂ A → Type _
Inverse e ⁻¹ • = (LeftInverse e ⁻¹ •) × (RightInverse e ⁻¹ •)

LeftConical : B → Opᵣ A B → Type _
LeftConical e _•_ = ∀ x y → x • y ≡ e → x ≡ e

RightConical : B → Opₗ A B → Type _
RightConical e _•_ = ∀ x y → x • y ≡ e → y ≡ e

Conical : A → Op₂ A → Type _
Conical e • = (LeftConical e •) × (RightConical e •)

_DistributesOverˡ_ : Opₗ A B → Op₂ B → Type _
_*_ DistributesOverˡ _+_ =
  ∀ x y z → (x * (y + z)) ≡ ((x * y) + (x * z))

_DistributesOverʳ_ : Opᵣ A B → Op₂ B → Type _
_*_ DistributesOverʳ _+_ =
  ∀ x y z → ((y + z) * x) ≡ ((y * x) + (z * x))

_DistributesOver_ : Op₂ A → Op₂ A → Type _
* DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +)

_IdempotentOn_ : Op₂ A → A → Type _
_•_ IdempotentOn x = (x • x) ≡ x

Idempotent : Op₂ A → Type _
Idempotent • = ∀ x → • IdempotentOn x

IdempotentFun : Op₁ A → Type _
IdempotentFun f = ∀ x → f (f x) ≡ f x

Selective : Op₂ A → Type _
Selective _•_ = ∀ x y → ∥ (x • y ≡ x) ⊎ (x • y ≡ y) ∥

_Absorbs_ : Op₂ A → Op₂ A → Type _
_∧_ Absorbs _∨_ = ∀ x y → (x ∧ (x ∨ y)) ≡ x

Absorptive : Op₂ A → Op₂ A → Type _
Absorptive ∧ ∨ = (∧ Absorbs ∨) × (∨ Absorbs ∧)

Involutive : Op₁ A → Type _
Involutive f = ∀ x → f (f x) ≡ x

LeftCancellative : (A → B → C) → Type _
LeftCancellative _•_ = ∀ x {y z} → (x • y) ≡ (x • z) → y ≡ z

RightCancellative : (A → B → C) → Type _
RightCancellative _•_ = ∀ {x y} z → (x • z) ≡ (y • z) → x ≡ y

Cancellative : (A → A → B) → Type _
Cancellative • = (LeftCancellative •) × (RightCancellative •)

Interchangeable : Op₂ A → Op₂ A → Type _
Interchangeable _•_ _◦_ = ∀ w x y z → ((w • x) ◦ (y • z)) ≡ ((w ◦ y) • (x ◦ z))


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

module Luau.Heap where

open import Agda.Builtin.Equality using (_≡_; refl)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import FFI.Data.Vector using (Vector; length; snoc; empty; lookup-snoc-not)
open import Luau.Addr using (Addr; _≡ᴬ_)
open import Luau.Var using (Var)
open import Luau.Syntax using (Block; Expr; Annotated; FunDec; nil; function_is_end)
open import Properties.Equality using (_≢_; trans)
open import Properties.Remember using (remember; _,_)
open import Properties.Dec using (yes; no)

-- Heap-allocated objects
data Object (a : Annotated) : Set where

  function_is_end : FunDec a → Block a → Object a

Heap : Annotated → Set
Heap a = Vector (Object a)

data _≡_⊕_↦_ {a} : Heap a → Heap a → Addr → Object a → Set where

  defn : ∀ {H val} →

    -----------------------------------
    (snoc H val) ≡ H ⊕ (length H) ↦ val

_[_] : ∀ {a} → Heap a → Addr → Maybe (Object a)
_[_] = FFI.Data.Vector.lookup

∅ : ∀ {a} → Heap a
∅ = empty

data AllocResult a (H : Heap a) (V : Object a) : Set where
  ok : ∀ b H′ → (H′ ≡ H ⊕ b ↦ V) → AllocResult a H V

alloc : ∀ {a} H V → AllocResult a H V
alloc H V = ok (length H) (snoc H V) defn

next : ∀ {a} → Heap a → Addr
next = length

allocated : ∀ {a} → Heap a → Object a → Heap a
allocated = snoc

lookup-not-allocated : ∀ {a} {H H′ : Heap a} {b c O} → (H′ ≡ H ⊕ b ↦ O) → (c ≢ b) → (H [ c ] ≡ H′ [ c ])
lookup-not-allocated {H = H} {O = O} defn p = lookup-snoc-not O H p

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau