text:
------------------------------------------------------------------------------
-- Data and postulates
------------------------------------------------------------------------------

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

-- Are the FOTC natural numbers defined by data and postulates the
-- same?

module DataPostulate where

------------------------------------------------------------------------------
postulate
  D    : Set
  zero : D
  succ : D → D

-- The FOTC natural numbers using data.
data N : D → Set where
  zN :               N zero
  sN : ∀ {n} → N n → N (succ n)

N-ind : (P : D → Set) →
        P zero →
        (∀ {n} → N n → P n → P (succ n)) →
        ∀ {n} → N n → P n
N-ind P P0 h zN      = P0
N-ind P P0 h (sN Nn) = h Nn (N-ind P P0 h Nn)

-- The FOTC natural numbers using postulates (we chose 'M' by 'Model').
postulate
  M    : D → Set
  zM   : M zero
  sM   : ∀ {n} → M n → M (succ n)
  M-ind : (P : D → Set) →
          P zero →
          (∀ {n} → M n → P n → P (succ n)) →
          ∀ {n} → M n → P n

------------------------------------------------------------------------------
-- The predicates

-- From the data predicate to the postulated one: Using the induction
-- principle.
nat-D2P : ∀ {n} → N n → M n
nat-D2P = N-ind M zM (λ _ Mn → sM Mn)

-- From the data predicate to the postulated one: Using pattern
-- matching.
nat-D2P' : ∀ {n} → N n → M n
nat-D2P' zN      = zM
nat-D2P' (sN Nn) = sM (nat-D2P' Nn)

-- From the postulated predicate to the data one.
nat-P2D : ∀ {n} → M n → N n
nat-P2D = M-ind N zN (λ _ Nn → sN Nn)

------------------------------------------------------------------------------
-- The induction principles

-- The postulated inductive principle from the data one.
D2P-ind : (P : D → Set) → P zero →
          (∀ {n} → M n → P n → P (succ n)) →
          ∀ {n} → M n → P n
D2P-ind P P0 ih Mn = N-ind P P0 (λ {_} Nn → ih (nat-D2P Nn)) (nat-P2D Mn)

-- The data inductive principle from the postulated one.
P2D-ind : (P : D → Set) → P zero →
          (∀ {n} → N n → P n → P (succ n)) →
          ∀ {n} → N n → P n
P2D-ind P P0 ih Nn = M-ind P P0 (λ {_} Mn → ih (nat-P2D Mn)) (nat-D2P Nn)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
import Common.Reflect

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

data Bool : Set where
  true false : Bool

data True : Set where
  true : True

-- Should print names as "quote Bool.true" (making sure to disambiguate)
-- and "quote false" rather than "Issue619.Bool.true/false" in error message.
not-true : quote Bool.true ≡ quote Bool.false
not-true = refl

ext: agda

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
-- It seems as if our fix for singleton records was not good enough;
-- the following code was accepted by Agda 2.2.6.
-- Fixed now.
module Issue245 where

record ⊤ : Set where

postulate
  A : Set
  x : A

record R₁ (P : A → Set) : Set where
  field
    f : P x

record R₂ : Set₁ where
  field
    F : A → Set
    f : R₁ F

record R₃ (R : R₂) : Set where
  field
    f : A

R : R₂
R = record
  { F = λ (x : A) → ⊤
  ; f = record {}
  }

foo : R₃ R → A
foo = R₃.f {_}

-- No unsolved metas at the following locations:
--   /home/nad/research/dtp/lib/Bug.agda:32,13-14

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
open import Agda.Builtin.IO
open import Agda.Builtin.Reflection
open import Agda.Builtin.Strict
open import Agda.Builtin.String
open import Agda.Builtin.Unit

postulate
  putStr : String → IO ⊤

{-# FOREIGN GHC import qualified Data.Text.IO #-}
{-# COMPILE GHC putStr = Data.Text.IO.putStr #-}
{-# COMPILE JS putStr =
    function (x) {
      return function(cb) {
        process.stdout.write(x); cb(0); }; } #-}

main : IO ⊤
main = primForce commitTC λ _ → putStr "Success\n"

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module SizedTypesFunctionFromSuccSize where

open import Common.Size

data Nat : {size : Size} → Set where
  zero : {size : Size} → Nat {↑ size}
  suc  : {size : Size} → Nat {size} → Nat {↑ size}

bad : {i : Size} → Nat {↑ i} → Set
bad zero    = bad zero
bad (suc x) = Nat

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of operations on strings
------------------------------------------------------------------------

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

module Data.String.Properties where

open import Data.Bool.Base using (Bool)
import Data.Char.Properties as Charₚ
import Data.List.Properties as Listₚ
import Data.List.Relation.Binary.Pointwise as Pointwise
import Data.List.Relation.Binary.Lex.Strict as StrictLex
open import Data.String.Base
open import Function
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (map′; isYes)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality.Core
import Relation.Binary.Construct.On as On
import Relation.Binary.PropositionalEquality as PropEq

------------------------------------------------------------------------
-- Primitive properties

open import Agda.Builtin.String.Properties public
  renaming ( primStringToListInjective to toList-injective)

------------------------------------------------------------------------
-- Properties of _≈_

≈⇒≡ : _≈_ ⇒ _≡_
≈⇒≡ = toList-injective _ _
    ∘ Pointwise.Pointwise-≡⇒≡
    ∘ Pointwise.map Charₚ.≈⇒≡

≈-reflexive : _≡_ ⇒ _≈_
≈-reflexive = Pointwise.map Charₚ.≈-reflexive
            ∘ Pointwise.≡⇒Pointwise-≡
            ∘ cong toList

≈-refl : Reflexive _≈_
≈-refl {x} = ≈-reflexive {x} {x} refl

≈-sym : Symmetric _≈_
≈-sym = Pointwise.symmetric (λ {i j} → Charₚ.≈-sym {i} {j})

≈-trans : Transitive _≈_
≈-trans = Pointwise.transitive (λ {i j k} → Charₚ.≈-trans {i} {j} {k})

≈-subst : ∀ {ℓ} → Substitutive _≈_ ℓ
≈-subst P x≈y p = subst P (≈⇒≡ x≈y) p

infix 4 _≈?_
_≈?_ : Decidable _≈_
x ≈? y = Pointwise.decidable Charₚ._≈?_ (toList x) (toList y)

≈-isEquivalence : IsEquivalence _≈_
≈-isEquivalence = record
  { refl  = λ {i} → ≈-refl {i}
  ; sym   = λ {i j} → ≈-sym {i} {j}
  ; trans = λ {i j k} → ≈-trans {i} {j} {k}
  }

≈-setoid : Setoid _ _
≈-setoid = record
  { isEquivalence = ≈-isEquivalence
  }

≈-isDecEquivalence : IsDecEquivalence _≈_
≈-isDecEquivalence = record
  { isEquivalence = ≈-isEquivalence
  ; _≟_           = _≈?_
  }

≈-decSetoid : DecSetoid _ _
≈-decSetoid = record
  { isDecEquivalence = ≈-isDecEquivalence
  }

-----------------------------------------------------------------------
-- Properties of _≡_

infix 4 _≟_

_≟_ : Decidable _≡_
x ≟ y = map′ ≈⇒≡ ≈-reflexive $ x ≈? y

≡-setoid : Setoid _ _
≡-setoid = PropEq.setoid String

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

------------------------------------------------------------------------
-- Properties of _<_

infix 4 _<?_
_<?_ : Decidable _<_
x <? y = StrictLex.<-decidable Charₚ._≈?_ Charₚ._<?_ (toList x) (toList y)

<-isStrictPartialOrder-≈ : IsStrictPartialOrder _≈_ _<_
<-isStrictPartialOrder-≈ =
  On.isStrictPartialOrder
    toList
    (StrictLex.<-isStrictPartialOrder Charₚ.<-isStrictPartialOrder-≈)

<-isStrictTotalOrder-≈ : IsStrictTotalOrder _≈_ _<_
<-isStrictTotalOrder-≈ =
  On.isStrictTotalOrder
    toList
    (StrictLex.<-isStrictTotalOrder Charₚ.<-isStrictTotalOrder-≈)

<-strictPartialOrder-≈ : StrictPartialOrder _ _ _
<-strictPartialOrder-≈ =
  On.strictPartialOrder
    (StrictLex.<-strictPartialOrder Charₚ.<-strictPartialOrder-≈)
    toList

<-strictTotalOrder-≈ : StrictTotalOrder _ _ _
<-strictTotalOrder-≈ =
  On.strictTotalOrder
    (StrictLex.<-strictTotalOrder Charₚ.<-strictTotalOrder-≈)
    toList

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

infix 4 _==_
_==_ : String → String → Bool
s₁ == s₂ = isYes (s₁ ≟ s₂)

private

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

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

  unit-test : P (_==_ "")
  unit-test = p _

-- Version 1.1

setoid = ≡-setoid
{-# WARNING_ON_USAGE setoid
"Warning: setoid was deprecated in v1.1.
Please use ≡-setoid instead."
#-}

decSetoid = ≡-decSetoid
{-# WARNING_ON_USAGE decSetoid
"Warning: decSetoid was deprecated in v1.1.
Please use ≡-decSetoid instead."
#-}

strictTotalOrder = <-strictTotalOrder-≈
{-# WARNING_ON_USAGE strictTotalOrder
"Warning: strictTotalOrder was deprecated in v1.1.
Please use <-strictTotalOrder-≈ instead."
#-}


text:
-- {-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.with.top:25 #-}
-- {-# OPTIONS -v tc.with:40 -v tc.interaction:20 -v interaction.give:20 -v tc:10 #-}

open import Common.Equality

data Unit : Set where
  unit : Unit

id : (A : Set) → A → A
id A a = a

module Works where

  dx : (x : Unit) → Unit → Unit
  dx x unit = x

  g : (x : Unit) → ∀ u → x ≡ dx x u
  g x with x
  g x | unit = id ((u : Unit) → unit ≡ dx unit u) ?

-- Now if we make (x : Unit) a module parameter
-- then we turn all applications (dx _) into just dx,
-- which actually means (dx x), i.e., dx applied to
-- the module free variables.

-- This leads to an incomprehendable rejection
-- of the following code (culprit is the first argument to id).

module M (x : Unit) where

  dx : Unit → Unit
  dx unit = x

  g : ∀ u → x ≡ dx u
  g with x
  g | unit  = id ((u : Unit) → unit ≡ dx u) ?

-- Now, `with x` is a plain error.

-- Also in harmless cases like the one below:

module CollateralDamage (x : Unit) where

  x′ = x

  bla : x ≡ x′
  bla with x
  bla | unit  = id (unit ≡ unit) refl


text:
{-# OPTIONS --cubical --no-import-sorts #-}

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

module Number.Bundles where

private
  variable
    ℓ ℓ' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Binary.Base -- Rel
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)

open import MoreAlgebra
open import Number.Structures

-- ℕ ℤ ℚ ℝ ℂ and ℚ₀⁺ ℝ₀⁺ ...
-- ring without additive inverse
record RCommSemiring : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    Carrier     : Type ℓ
    _#_ : Rel Carrier Carrier ℓ'
    -- RCommSemiring
    0f 1f       : Carrier
    _+_ _·_     : Carrier → Carrier → Carrier
    isRCommSemiring : IsRCommSemiring _#_ 0f 1f _+_ _·_

  open IsRCommSemiring isRCommSemiring public

-- ℤ ℚ ℝ ℂ
record RCommRing : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    Carrier     : Type ℓ
    _#_ : Rel Carrier Carrier ℓ'
    -- RCommSemiring
    0f 1f       : Carrier
    _+_ _·_     : Carrier → Carrier → Carrier
    -- RCommRing
    -_          : Carrier → Carrier
    isRCommRing : IsRCommRing _#_ 0f 1f _+_ _·_ -_

  open IsRCommRing isRCommRing public

-- ℚ ℝ ℂ
record RField : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    Carrier     : Type ℓ
    _#_ : Rel Carrier Carrier ℓ'
    -- RCommSemiring
    0f 1f       : Carrier
    _+_ _·_     : Carrier → Carrier → Carrier
    -- RCommRing
    -_          : Carrier → Carrier
    -- RField
    _⁻¹         : (x : Carrier) → {{ x # 0f }} → Carrier
    isRField : IsRField _#_ 0f 1f _+_ _·_ -_ _⁻¹

-- Finₖ ℕ ℤ ℚ ℚ₀⁺ ℚ⁺ ℝ ℝ₀⁺ ℝ⁺
record RLattice : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  constructor rlattice
  field
    Carrier     : Type ℓ
    _<_ _≤_ _#_ : Rel Carrier Carrier ℓ'
    min max     : Carrier → Carrier → Carrier
    isRLattice  : IsRLattice _<_ _≤_ _#_ min max

  open IsRLattice isRLattice public

  infixl 4 _<_
  infixl 4 _≤_
  infixl 4 _#_

-- ℕ ℤ ℚ ℚ₀⁺ ℚ⁺ ℝ ℝ₀⁺ ℝ⁺
-- ring without additive inverse
record ROrderedCommSemiring : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    -- RLattice
    Carrier     : Type ℓ
    _<_ _≤_ _#_ : Rel Carrier Carrier ℓ'
    min max     : Carrier → Carrier → Carrier
    -- ROrderedCommSemiring
    0f 1f       : Carrier
    _+_ _·_     : Carrier → Carrier → Carrier
    -- _-_         : (x y : Carrier) → (y ≤ x) → Carrier -- is that a good idea?
    isROrderedCommSemiring : IsROrderedCommSemiring _<_ _≤_ _#_ min max 0f 1f _+_ _·_

  open IsROrderedCommSemiring isROrderedCommSemiring public

-- ℤ ℚ ℝ
record ROrderedCommRing : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    -- RLattice
    Carrier     : Type ℓ
    _<_ _≤_ _#_ : Rel Carrier Carrier ℓ'
    min max     : Carrier → Carrier → Carrier
    -- ROrderedCommSemiring
    0f 1f       : Carrier
    _+_ _·_     : Carrier → Carrier → Carrier
    -- ROrderedCommRing
    -_          : Carrier → Carrier
    isROrderedCommRing : IsROrderedCommRing _<_ _≤_ _#_ min max 0f 1f _+_ _·_ -_

  open IsROrderedCommRing isROrderedCommRing public

  abs : Carrier → Carrier
  abs x = max x (- x)

  field
    isAbsOrderedCommRing : IsAbsOrderedCommRing _<_ _≤_ _#_ min max 0f 1f _+_ _·_ -_ abs

  open IsAbsOrderedCommRing isAbsOrderedCommRing public

-- ℚ ℝ
record ROrderedField : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    -- RLattice
    Carrier     : Type ℓ
    _<_ _≤_ _#_ : Rel Carrier Carrier ℓ'
    min max     : Carrier → Carrier → Carrier
    -- ROrderedCommSemiring
    0f 1f       : Carrier
    _+_ _·_     : Carrier → Carrier → Carrier
    -- ROrderedCommRing
    -_          : Carrier → Carrier
    -- ROrderedField
    _⁻¹         : (x : Carrier) → {{ x # 0f }} → Carrier
    isROrderedField : IsROrderedField _<_ _≤_ _#_ min max 0f 1f _+_ _·_ -_ _⁻¹

  open IsROrderedField isROrderedField public

  abs : Carrier → Carrier
  abs x = max x (- x)

  field
    isAbsOrderedCommRing : IsAbsOrderedCommRing _<_ _≤_ _#_ min max 0f 1f _+_ _·_ -_ abs

  open IsAbsOrderedCommRing isAbsOrderedCommRing public

{-

-- ℚ₀⁺ ℝ₀⁺
record ROrderedSemifield : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    -- RLattice
    Carrier     : Type ℓ
    _<_ _≤_ _#_ : Rel Carrier Carrier ℓ'
    min max     : Carrier → Carrier → Carrier
    -- ROrderedCommSemiring
    0f 1f       : Carrier
    _+_ _·_     : Carrier → Carrier → Carrier
    -- ROrderedSemifield
    _-_         : (x y : Carrier) → (y ≤ x) → Carrier -- is that a good idea?
    _⁻¹         : (x : Carrier) → {{ 0f < x }} → Carrier

-- ℚ⁺ ℝ⁺
record ROrderedSemifieldWithoutZero : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    -- RLattice
    Carrier     : Type ℓ
    _<_ _≤_ _#_ : Rel Carrier Carrier ℓ'
    min max     : Carrier → Carrier → Carrier
    -- ROrderedSemifieldWithoutZero
    1f          : Carrier
    _+_ _·_     : Carrier → Carrier → Carrier
    _-_         : (x y : Carrier) → (y < x) → Carrier -- is that a good idea?
    _⁻¹         : Carrier → Carrier

-}

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
module Lvl where

open import Type

open import Agda.Primitive public
  using (Level; _⊔_)
  renaming (lzero to 𝟎; lsuc to 𝐒)

-- Wraps a lower level set in a higher level wrapper set.
record Up {ℓ₁ ℓ₂} (T : Type{ℓ₂}) : Type{ℓ₁ ⊔ ℓ₂} where
  constructor up
  field obj : T

of : ∀{ℓ} → Type{ℓ} → Level
of {ℓ} _ = ℓ
{-# INLINE of #-}

ofType : ∀{ℓ} → Type{𝐒(ℓ)} → Level
ofType {ℓ} _ = ℓ
{-# INLINE ofType #-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.UnivariateFun.Polyn-nPoly where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv

open import Cubical.Data.Nat renaming (_+_ to _+n_; _·_ to _·n_)
open import Cubical.Data.Sigma

open import Cubical.Algebra.Ring
open import Cubical.Algebra.GradedRing.DirectSumFun
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Instances.Polynomials.UnivariatePolyHIT
open import Cubical.Algebra.CommRing.Instances.Polynomials.UnivariatePolyFun
open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly

open import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.Poly0-A
open import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.An[Am[X]]-Anm[X]
open import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.AB-An[X]Bn[X]
open import Cubical.Algebra.Polynomials.UnivariateHIT.Polyn-nPoly

open CommRingEquivs renaming (compCommRingEquiv to _∘-ecr_ ; invCommRingEquiv to inv-ecr)

private variable
  ℓ : Level

-----------------------------------------------------------------------------
-- Definition

Equiv1 : (A' : CommRing ℓ) → CommRingEquiv (nUnivariatePolyHIT A' 1) (nUnivariatePolyFun A' 1)
Equiv1 A' = CommRingEquiv-DirectSumGradedRing _ _ _  _ _ _ _ _ _ _ _ _ _ _ _

Equiv-Polyn-nPolyFun : (A' : CommRing ℓ) → (n : ℕ) → CommRingEquiv (PolyCommRing A' n) (nUnivariatePolyFun A' n)
Equiv-Polyn-nPolyFun A' zero = CRE-Poly0-A A'
Equiv-Polyn-nPolyFun A' (suc n) =       inv-ecr _ _ (CRE-PolyN∘M-PolyN+M A' 1 n)
                               ∘-ecr (lift-equiv-poly _ _ 1 (Equiv-Polyn-nPolyFun A' n)
                               ∘-ecr (Equiv-Polyn-nPolyHIT (nUnivariatePolyFun A' n) 1
                                     ∘-ecr Equiv1 (nUnivariatePolyFun A' n)))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Make the type checker loop. How can we ensure that the record is not
-- recursive?
module RecursiveRecord where

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

F : Set -> Set
F _ = R
  where
    record R : Set where
      field x : F Nat

r : F Nat
r = _

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module examplesPaperJFP.WxGraphicsLib where

open import SizedIO.Base
open import StateSizedIO.GUI.BaseStateDependent

open import Size

open import Data.Bool.Base
open import Data.List.Base

open import Function

open import NativeIO

open import StateSizedIO.GUI.WxBindingsFFI
open import StateSizedIO.GUI.VariableList

data GuiLev1Command : Set where
  makeFrame   :  GuiLev1Command
  makeButton  :  Frame  →  GuiLev1Command
  addButton   :  Frame  →  Button  →  GuiLev1Command
  drawBitmap  :  DC     →  Bitmap  →  Point → Bool → GuiLev1Command
  repaint     :  Frame  →  GuiLev1Command

GuiLev1Response : GuiLev1Command → Set
GuiLev1Response  makeFrame       = Frame
GuiLev1Response (makeButton _)   = Button
GuiLev1Response  _               = Unit

GuiLev1Interface : IOInterface
Command   GuiLev1Interface  =  GuiLev1Command
Response  GuiLev1Interface  =  GuiLev1Response

GuiLev2State : Set₁
GuiLev2State = VarList

data GuiLev2Command (s :  GuiLev2State) : Set₁ where
  level1C           :  GuiLev1Command → GuiLev2Command s
  createVar         :  {A : Set} → A → GuiLev2Command s
  setButtonHandler  :  Button
                       → List (prod s → IO GuiLev1Interface ∞ (prod s))
                       → GuiLev2Command s
  setOnPaint        :  Frame
                       → List (prod s → DC → Rect → IO GuiLev1Interface ∞ (prod s))
                       → GuiLev2Command s

GuiLev2Response : (s : GuiLev2State) → GuiLev2Command s → Set
GuiLev2Response  _ (level1C c)        =  GuiLev1Response c
GuiLev2Response  _ (createVar {A} a)  =  Var A
GuiLev2Response  _  _                 =  Unit

GuiLev2Next : (s : GuiLev2State) → (c : GuiLev2Command s)
              → GuiLev2Response s c
              → GuiLev2State
GuiLev2Next s (createVar {A} a)  var  =  addVar A var s
GuiLev2Next s _                   _   =  s

GuiLev2Interface : IOInterfaceˢ
Stateˢ     GuiLev2Interface  =  GuiLev2State
Commandˢ   GuiLev2Interface  =  GuiLev2Command
Responseˢ  GuiLev2Interface  =  GuiLev2Response
nextˢ      GuiLev2Interface  =  GuiLev2Next

translateLev1Local : (c : GuiLev1Command) → NativeIO (GuiLev1Response c)
translateLev1Local  makeFrame              =  nativeNewFrame "dummy title"
translateLev1Local (makeButton fra)        =  nativeMakeButton fra "dummy button label"
translateLev1Local (addButton fra bt)      =  nativeAddButton fra bt
translateLev1Local (drawBitmap dc bm p b)  =  nativeDrawBitmap dc bm p b
translateLev1Local (repaint fra)           =  nativeRepaint fra

translateLev1 : {A : Set} → IO GuiLev1Interface ∞ A → NativeIO A
translateLev1 = translateIO translateLev1Local

translateLev1List : {A : Set} → List (IO GuiLev1Interface ∞ A) → List (NativeIO A)
translateLev1List l = map translateLev1 l

translateLev2Local  :   (s : GuiLev2State)
                        → (c : GuiLev2Command s)
                        → NativeIO (GuiLev2Response s c)
translateLev2Local s (level1C c)        =  translateLev1Local c
translateLev2Local s (createVar {A} a)  =  nativeNewVar {A} a
translateLev2Local s (setButtonHandler bt proglist) =
  nativeSetButtonHandler bt
         (dispatchList s (map (λ prog → translateLev1 ∘ prog)  proglist))
translateLev2Local s (setOnPaint fra proglist) =
  nativeSetOnPaint fra (λ dc rect → dispatchList s
         (map (λ prog aa → translateLev1 (prog aa dc rect)) proglist))

translateLev2 : ∀ {A s} → IOˢ GuiLev2Interface ∞ (λ _ → A) s → NativeIO A
translateLev2 = translateIOˢ  translateLev2Local

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


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

open import Container

module Container.Membership {s p} (𝒞 : Container s p) where

open import Prelude
open import HLevels

infixr 5 _∈_ _∈!_
_∈_ : A → ⟦ 𝒞 ⟧ A → Type _
x ∈ xs = fiber (snd xs) x

_∈!_ : A → ⟦ 𝒞 ⟧ A → Type _
x ∈! xs = isContr (x ∈ xs)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-# OPTIONS --copatterns #-}
-- {-# OPTIONS -v tc.lhs.split:50 -v tc.cover:20 -v tc.cc:15 -v tc.lhs.top:10 #-}
-- {-# OPTIONS -v term:20 #-}
-- {-# OPTIONS --no-positivity-check #-}
-- {-# OPTIONS -v tc.def.fun:50  #-}
-- {-# OPTIONS -v 100  #-}
module CoPatStream where

import Common.Level
open import Common.Prelude hiding (map)
open import Common.Equality

record Stream (A : Set) : Set where
  coinductive
  constructor cons
  field
    head : A
    tail : Stream A
module S = Stream

record _≈_ {A : Set}(s t : Stream A) : Set where
  coinductive
  field
    head : S.head s ≡ S.head t
    tail : S.tail s ≈ S.tail t
module B = _≈_

repeat : {A : Set}(a : A) → Stream A
-- repeat a = cons a (repeat a)
S.head (repeat a) = a
S.tail (repeat a) = repeat a

module Cycle where

  cycle : Nat -> Stream Nat
  cycle n = cycle' n where
    cycle' : Nat -> Stream Nat
    S.head (cycle' n) = n
    S.tail (cycle' zero    ) = cycle n
    S.tail (cycle' (suc n')) = cycle' n'

module CoPat where

  map : {A B : Set} → (A → B) → Stream A → Stream B
  S.head (map f s) = f (S.head s)
  S.tail (map f s) = map f (S.tail s)

  map_id : {A : Set}(s : Stream A) → map (λ x → x) s ≈ s
  B.head (map_id s) = refl
  B.tail (map_id s) = map_id (S.tail s)

module HandTranslated where

  {-# NON_TERMINATING #-}
  map : {A B : Set} → (A → B) → Stream A → Stream B
  map f s = record
    { head = f (S.head s)
    ; tail = map f (S.tail s)
    }

  {- rejected because map is not unfolded
  {-# NON_TERMINATING #-}
  map_id : {A : Set}(s : Stream A) → map (λ x → x) s ≈ s
  map_id s = record
    { head = refl
    ; tail = map_id (S.tail s)
    }
  -}

module DeepCoPat where

  repeat₂ : {A : Set}(a₁ a₂ : A) → Stream A
  (       (S.head (repeat₂ a₁ a₂))) = a₁
  (S.head (S.tail (repeat₂ a₁ a₂))) = a₂
  (S.tail (S.tail (repeat₂ a₁ a₂))) = repeat₂ a₁ a₂

  repeat≈repeat₂ : {A : Set}(a : A) → repeat a ≈ repeat₂ a a
  (       (B.head (repeat≈repeat₂ a))) = refl
  (B.head (B.tail (repeat≈repeat₂ a))) = refl
  (B.tail (B.tail (repeat≈repeat₂ a))) = repeat≈repeat₂ a

module ProjectionRHS where

  repeat′ : {A : Set}(a : A) → Stream A
  (       (S.head (repeat′ a))) = a
  (S.head (S.tail (repeat′ a))) = a
  (S.tail (S.tail (repeat′ a))) = S.tail (repeat′ a)

-- -- Type error:
--   repeat≈repeat′ : {A : Set}(a : A) → repeat a ≈ repeat′ a
--   (       (B.head (repeat≈repeat′ a))) = refl
--   (B.head (B.tail (repeat≈repeat′ a))) = refl
--   (B.tail (B.tail (repeat≈repeat′ a))) = repeat≈repeat′ a


text:
{-

Definition of and facts about Smith normal form

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.IntegerMatrix.Smith.NormalForm where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Nat
  hiding   (_·_)
  renaming (_+_ to _+ℕ_ ; +-assoc to +Assocℕ)
open import Cubical.Data.Int
  hiding   (_+_ ; _·_ ; _-_ ; -_ ; addEq)
open import Cubical.Data.Int.Divisibility
open import Cubical.Data.FinData

open import Cubical.Data.Empty as Empty
open import Cubical.Data.Unit  as Unit
open import Cubical.Data.Sigma
open import Cubical.Data.List

open import Cubical.Relation.Nullary

open import Cubical.Algebra.Matrix.CommRingCoefficient
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Instances.Int
  renaming (ℤ to ℤRing)

private
  variable
    m n k : ℕ

open Coefficient  ℤRing

-- Sequence of consecutively divisible integers

_∣all_ : ℤ → List ℤ → Type
n ∣all [] = ¬ n ≡ 0
n ∣all (x ∷ ys) = n ∣ x × n ∣all ys

isProp∣all : {n : ℤ}{xs : List ℤ} → isProp (n ∣all xs)
isProp∣all {xs = []}= isPropΠ (λ _ → isProp⊥)
isProp∣all {xs = x ∷ xs} = isProp× isProp∣ isProp∣all

isConsDivs : List ℤ → Type
isConsDivs [] = Unit
isConsDivs (x ∷ xs) = x ∣all xs × isConsDivs xs

isPropIsConsDivs : (xs : List ℤ) → isProp (isConsDivs xs)
isPropIsConsDivs [] = isPropUnit
isPropIsConsDivs (x ∷ xs) = isProp× isProp∣all (isPropIsConsDivs xs)

ConsDivs : Type
ConsDivs = Σ[ xs ∈ List ℤ ] isConsDivs xs

cons : (n : ℤ)(xs : ConsDivs) → n ∣all xs .fst → ConsDivs
cons n (xs , _) _ .fst = n ∷ xs
cons n ([] , _) p .snd = p , tt
cons n (x ∷ xs , q) p .snd = p , q

-- Smith normal matrix

_+length_ : ConsDivs → ℕ → ℕ
xs +length n = length (xs .fst) +ℕ n

smithMat : (xs : List ℤ)(m n : ℕ) → Mat (length xs +ℕ m) (length xs +ℕ n)
smithMat [] _ _ = 𝟘
smithMat (x ∷ xs) _ _ = x ⊕ smithMat xs _ _

smithMat∣ :
    (a : ℤ)(xs : ConsDivs){m n : ℕ}
  → ¬ a ≡ 0
  → ((i : Fin (xs +length m))(j : Fin (xs +length n)) → a ∣ smithMat (xs .fst) m n i j)
  → a ∣all xs .fst
smithMat∣ _ ([] , _) q _ = q
smithMat∣ a (x ∷ xs , p) q h = h zero zero , smithMat∣ a (xs , p .snd) q (λ i j → h (suc i) (suc j))

smithMat⊕ :
    (a : ℤ)(xs : ConsDivs){m n : ℕ}
  → (div : a ∣all xs .fst)
  → a ⊕ smithMat (xs .fst) m n ≡ smithMat (cons a xs div .fst) m n
smithMat⊕ _ _ _ = refl

-- Matrix with smith normality

record isSmithNormal (M : Mat m n) : Type where
  field
    divs : ConsDivs
    rowNull : ℕ
    colNull : ℕ

    rowEq : divs +length rowNull ≡ m
    colEq : divs +length colNull ≡ n
    matEq : PathP (λ t → Mat (rowEq t) (colEq t)) (smithMat (divs .fst) rowNull colNull) M

open isSmithNormal

row col : {M : Mat m n} → isSmithNormal M → ℕ
row isNorm = isNorm .divs +length isNorm .rowNull
col isNorm = isNorm .divs +length isNorm .colNull

smith∣ :
    (a : ℤ){M : Mat m n}(isNorm : isSmithNormal M)
  → ¬ a ≡ 0
  → ((i : Fin m)(j : Fin n) → a ∣ M i j)
  → a ∣all isNorm . divs .fst
smith∣ a isNorm p h =
  let a∣smith = λ
        { i j →
          subst (a ∣_) (λ t → isNorm .matEq (~ t)
            (subst-filler Fin (isNorm .rowEq) i (~ t))
            (subst-filler Fin (isNorm .colEq) j (~ t))) (h _ _) }
  in  smithMat∣ _ (isNorm .divs) p a∣smith

-- Similarity to a normal form

open Sim

record Smith (M : Mat m n) : Type where
  field
    sim : Sim M
    isnormal : isSmithNormal (sim .result)

open Smith

simSmith : {M : Mat m n}(sim : Sim M) → Smith (sim .result) → Smith M
simSmith simM smith .sim      = compSim simM (smith .sim)
simSmith _    smith .isnormal = smith .isnormal

-- Simple special cases of normal matrices

isSmithNormal𝟘 : isSmithNormal (𝟘 {m = m} {n = n})
isSmithNormal𝟘 .divs = [] , tt
isSmithNormal𝟘 {m = m} .rowNull = m
isSmithNormal𝟘 {n = n} .colNull = n
isSmithNormal𝟘 .rowEq = refl
isSmithNormal𝟘 .colEq = refl
isSmithNormal𝟘 .matEq = refl

isSmithNormalEmpty : (M : Mat 0 n) → isSmithNormal M
isSmithNormalEmpty _ .divs = [] , tt
isSmithNormalEmpty _ .rowNull = 0
isSmithNormalEmpty {n = n} _ .colNull = n
isSmithNormalEmpty _ .rowEq = refl
isSmithNormalEmpty _ .colEq = refl
isSmithNormalEmpty _ .matEq = isContr→isProp isContrEmpty _ _

isSmithNormalEmptyᵗ : (M : Mat m 0) → isSmithNormal M
isSmithNormalEmptyᵗ _ .divs = [] , tt
isSmithNormalEmptyᵗ {m = m} _ .rowNull = m
isSmithNormalEmptyᵗ _ .colNull = 0
isSmithNormalEmptyᵗ _ .rowEq = refl
isSmithNormalEmptyᵗ _ .colEq = refl
isSmithNormalEmptyᵗ _ .matEq = isContr→isProp isContrEmptyᵗ _ _

smith𝟘 : Smith (𝟘 {m = m} {n = n})
smith𝟘 .sim      = idSim _
smith𝟘 .isnormal = isSmithNormal𝟘

smithEmpty : (M : Mat 0 n) → Smith M
smithEmpty _ .sim      = idSim _
smithEmpty M .isnormal = isSmithNormalEmpty M

smithEmptyᵗ : (M : Mat m 0) → Smith M
smithEmptyᵗ _ .sim      = idSim _
smithEmptyᵗ M .isnormal = isSmithNormalEmptyᵗ M

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Solver for equations in commutative monoids
--
-- Adapted from Algebra.Solver.Monoid
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Solver.CommutativeMonoid {m₁ m₂} (M : CommutativeMonoid m₁ m₂) where

open import Data.Fin using (Fin; zero; suc)
open import Data.Maybe as Maybe
  using (Maybe; decToMaybe; From-just; from-just)
open import Data.Nat as ℕ using (ℕ; zero; suc; _+_)
open import Data.Nat.GeneralisedArithmetic using (fold)
open import Data.Product using (_×_; uncurry)
open import Data.Vec using (Vec; []; _∷_; lookup; replicate)

open import Function using (_∘_)

import Relation.Binary.Reasoning.Setoid as EqReasoning
import Relation.Binary.Reflection as Reflection
import Relation.Nullary.Decidable as Dec
import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise

open import Relation.Binary.PropositionalEquality as P using (_≡_; decSetoid)
open import Relation.Nullary using (Dec)

open CommutativeMonoid M
open EqReasoning setoid

------------------------------------------------------------------------
-- Monoid expressions

-- There is one constructor for every operation, plus one for
-- variables; there may be at most n variables.

infixr 5 _⊕_
infixr 10 _•_

data Expr (n : ℕ) : Set where
  var : Fin n → Expr n
  id  : Expr n
  _⊕_ : Expr n → Expr n → Expr n

-- An environment contains one value for every variable.

Env : ℕ → Set _
Env n = Vec Carrier n

-- The semantics of an expression is a function from an environment to
-- a value.

⟦_⟧ : ∀ {n} → Expr n → Env n → Carrier
⟦ var x   ⟧ ρ = lookup ρ x
⟦ id      ⟧ ρ = ε
⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ

------------------------------------------------------------------------
-- Normal forms

-- A normal form is a vector of multiplicities (a bag).

Normal : ℕ → Set
Normal n = Vec ℕ n

-- The semantics of a normal form.

⟦_⟧⇓ : ∀ {n} → Normal n → Env n → Carrier
⟦ []    ⟧⇓ _ = ε
⟦ n ∷ v ⟧⇓ (a ∷ ρ) = fold (⟦ v ⟧⇓ ρ) (λ b → a ∙ b) n

------------------------------------------------------------------------
-- Constructions on normal forms

-- The empty bag.

empty : ∀{n} → Normal n
empty = replicate 0

-- A singleton bag.

sg : ∀{n} (i : Fin n) → Normal n
sg zero    = 1 ∷ empty
sg (suc i) = 0 ∷ sg i

-- The composition of normal forms.

_•_  : ∀{n} (v w : Normal n) → Normal n
[]      • []      = []
(l ∷ v) • (m ∷ w) = l + m ∷ v • w

------------------------------------------------------------------------
-- Correctness of the constructions on normal forms

-- The empty bag stands for the unit ε.

empty-correct : ∀{n} (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε
empty-correct [] = refl
empty-correct (a ∷ ρ) = empty-correct ρ

-- The singleton bag stands for a single variable.

sg-correct : ∀{n} (x : Fin n) (ρ : Env n) →  ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x
sg-correct zero (x ∷ ρ) = begin
    x ∙ ⟦ empty ⟧⇓ ρ   ≈⟨ ∙-congˡ (empty-correct ρ) ⟩
    x ∙ ε              ≈⟨ identityʳ _ ⟩
    x                  ∎
sg-correct (suc x) (m ∷ ρ) = sg-correct x ρ

-- Normal form composition corresponds to the composition of the monoid.

comp-correct : ∀ {n} (v w : Normal n) (ρ : Env n) →
              ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ)
comp-correct [] [] ρ =  sym (identityˡ _)
comp-correct (l ∷ v) (m ∷ w) (a ∷ ρ) = lemma l m (comp-correct v w ρ)
  where
    flip12 : ∀ a b c → a ∙ (b ∙ c) ≈ b ∙ (a ∙ c)
    flip12 a b c = begin
        a ∙ (b ∙ c)  ≈⟨ sym (assoc _ _ _) ⟩
        (a ∙ b) ∙ c  ≈⟨ ∙-congʳ (comm _ _) ⟩
        (b ∙ a) ∙ c  ≈⟨ assoc _ _ _ ⟩
        b ∙ (a ∙ c)  ∎
    lemma : ∀ l m {d b c} (p : d ≈ b ∙ c) →
      fold d (a ∙_) (l + m) ≈ fold b (a ∙_) l ∙ fold c (a ∙_) m
    lemma zero zero p = p
    lemma zero (suc m) p = trans (∙-congˡ (lemma zero m p)) (flip12 _ _ _)
    lemma (suc l) m p = trans (∙-congˡ (lemma l m p)) (sym (assoc a _ _))

------------------------------------------------------------------------
-- Normalization

-- A normaliser.

normalise : ∀ {n} → Expr n → Normal n
normalise (var x)   = sg x
normalise id        = empty
normalise (e₁ ⊕ e₂) = normalise e₁ • normalise e₂

-- The normaliser preserves the semantics of the expression.

normalise-correct : ∀ {n} (e : Expr n) (ρ : Env n) →
    ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ
normalise-correct (var x)   ρ = sg-correct x ρ
normalise-correct id        ρ = empty-correct ρ
normalise-correct (e₁ ⊕ e₂) ρ =  begin

    ⟦ normalise e₁ • normalise e₂ ⟧⇓ ρ

  ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩

    ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ

  ≈⟨ ∙-cong (normalise-correct e₁ ρ) (normalise-correct e₂ ρ) ⟩

    ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
  ∎

------------------------------------------------------------------------
-- "Tactics"

open module R = Reflection
                  setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) normalise-correct
  public using (solve; _⊜_)

-- We can decide if two normal forms are /syntactically/ equal.

infix 5 _≟_

_≟_ : ∀ {n} (nf₁ nf₂ : Normal n) → Dec (nf₁ ≡ nf₂)
nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≟_ nf₁ nf₂)
  where open Pointwise

-- We can also give a sound, but not necessarily complete, procedure
-- for determining if two expressions have the same semantics.

prove′ : ∀ {n} (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
prove′ e₁ e₂ =
  Maybe.map lemma (decToMaybe (normalise e₁ ≟ normalise e₂))
  where
  lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
  lemma eq ρ =
    R.prove ρ e₁ e₂ (begin
      ⟦ normalise e₁ ⟧⇓ ρ  ≡⟨ P.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
      ⟦ normalise e₂ ⟧⇓ ρ  ∎)

-- This procedure can be combined with from-just.

prove : ∀ n (e₁ e₂ : Expr n) → From-just (prove′ e₁ e₂)
prove _ e₁ e₂ = from-just (prove′ e₁ e₂)

-- prove : ∀ n (es : Expr n × Expr n) →
--         From-just (uncurry prove′ es)
-- prove _ = from-just ∘ uncurry prove′


text:
open import Data.List hiding ([_]) renaming (_∷_ to _∷ₗ_)
open import Data.Maybe
open import Data.Product

open import AEff
open import EffectAnnotations
open import Renamings
open import Substitutions renaming (⟨_,_⟩ to ⟨_,,_⟩)
open import Types

open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary

module Preservation where

-- BINDING CONTEXTS

BCtx = List VType

-- WELL-TYPED EVALUATION CONTEXTS

data _⊢E[_]⦂_ (Γ : Ctx) : (Δ : BCtx) → CType → Set where

  [-]              : {C : CType} →
                     -------------
                     Γ ⊢E[ [] ]⦂ C

  let=_`in_        : {Δ : BCtx}
                     {X Y : VType}
                     {o : O}
                     {i : I} →
                     Γ ⊢E[ Δ ]⦂ X ! (o , i) →
                     Γ ∷ X ⊢C⦂ Y ! (o , i) →
                     ------------------------
                     Γ ⊢E[ Δ ]⦂ Y ! (o , i)

  ↑                : {Δ : BCtx}
                     {X : VType}
                     {o : O}
                     {i : I} →
                     (op : Σₛ) →
                     op ∈ₒ o →
                     Γ ⊢V⦂ proj₁ (payload op) →
                     Γ ⊢E[ Δ ]⦂ X ! (o , i) →
                     --------------------------
                     Γ ⊢E[ Δ ]⦂ X ! (o , i)

  ↓                : {Δ : BCtx}
                     {X : VType}
                     {o : O}
                     {i : I}
                     (op : Σₛ) →
                     Γ ⊢V⦂ proj₁ (payload op) →
                     Γ ⊢E[ Δ ]⦂ X ! (o , i) →
                     ---------------------------
                     Γ ⊢E[ Δ ]⦂ X ! op ↓ₑ (o , i)

  promise_∣_↦_`in_ : {Δ : BCtx}
                     {X Y : VType}
                     {o o' : O}
                     {i i' : I} →
                     (op : Σₛ) →
                     (o' , i') ⊑ lkpᵢ op i →
                     Γ ∷ proj₁ (payload op) ∷ (𝟙 ⇒ (⟨ X ⟩ ! (∅ₒ , ∅ᵢ [ op ↦ just (o' , i') ]ᵢ))) ⊢C⦂ ⟨ X ⟩ ! (o' , i') →
                     Γ ∷ ⟨ X ⟩ ⊢E[ Δ ]⦂ Y ! (o , i) →
                     ----------------------------------------------
                     Γ ⊢E[ X ∷ₗ Δ ]⦂ Y ! (o , i)

  spawn            : {Δ : BCtx}
                     {C D : CType} →
                     Γ ■ ⊢C⦂ C →
                     Γ ⊢E[ Δ ]⦂ D →
                     ---------------
                     Γ ⊢E[ Δ ]⦂ D

  coerce           : {Δ : BCtx}
                     {X : VType}
                     {o o' : O}
                     {i i' : I} →
                     o ⊑ₒ o' →
                     i ⊑ᵢ i' →
                     Γ ⊢E[ Δ ]⦂ X ! (o , i) →
                     ------------------------
                     Γ ⊢E[ Δ ]⦂ X ! (o' , i')

-- MERGING AN ORDINARY CONTEXT AND A BINDING CONTEXT

infix 30 _⋈_

_⋈_ : Ctx → BCtx → Ctx
Γ ⋈ [] = Γ
Γ ⋈ (X ∷ₗ Δ) = (Γ ∷ ⟨ X ⟩) ⋈ Δ

-- FINDING THE TYPE OF THE HOLE OF A WELL-TYPED EVALUATION CONTEXT

hole-ty-e : {Γ : Ctx} {Δ : BCtx} {C : CType} → Γ ⊢E[ Δ ]⦂ C → CType
hole-ty-e {_} {_} {C} [-] =
  C
hole-ty-e (let= E `in M) =
  hole-ty-e E
hole-ty-e (↑ op p V E) =
  hole-ty-e E
hole-ty-e (↓ op V E) =
  hole-ty-e E
hole-ty-e (promise op ∣ p ↦ M `in E) =
  hole-ty-e E
hole-ty-e (spawn M E) =
  hole-ty-e E
hole-ty-e (coerce p q E) =
  hole-ty-e E

-- FILLING A WELL-TYPED EVALUATION CONTEXT

infix 30 _[_]

_[_] : {Γ : Ctx} {Δ : BCtx} {C : CType} → (E : Γ ⊢E[ Δ ]⦂ C) → Γ ⋈ Δ ⊢C⦂ (hole-ty-e E) → Γ ⊢C⦂ C
[-] [ M ] =
  M
(let= E `in N) [ M ] =
  let= (E [ M ]) `in N
(↑ op p V E) [ M ] =
  ↑ op p V (E [ M ])
(↓ op V E) [ M ] =
  ↓ op V (E [ M ])
(promise op ∣ p ↦ N `in E) [ M ] =
  promise op ∣ p ↦ N `in (E [ M ])
(spawn N E) [ M ] =
  spawn N (E [ M ])
(coerce p q E) [ M ] =
  coerce p q (E [ M ])

-- STRENGTHENING OF GROUND VALUES WRT BOUND PROMISES

strengthen-var : {Γ : Ctx} → (Δ : BCtx) → {X : VType} →
                 mobile X →
                 X ∈ Γ ⋈ Δ →
                 --------------------------------------
                 X ∈ Γ

strengthen-var [] p x = x
strengthen-var (y ∷ₗ Δ) p x with strengthen-var Δ p x
... | Tl-v z = z

strengthen-■-var : {Γ : Ctx} → (Γ' : Ctx) →
                   (Δ : BCtx) → {X : VType} →
                   X ∈ (Γ ⋈ Δ) ■ ++ₖ Γ' →
                   --------------------------
                   X ∈ Γ ■ ++ₖ Γ'

strengthen-■-var Γ' [] x = x
strengthen-■-var [] (y ∷ₗ Δ) x with strengthen-■-var [] Δ x
... | Tl-■ p (Tl-v z) = Tl-■ p z
strengthen-■-var (Γ' ∷ Z) (y ∷ₗ Δ) Hd = Hd
strengthen-■-var (Γ' ∷ Z) (y ∷ₗ Δ) (Tl-v x) with strengthen-■-var Γ' (y ∷ₗ Δ) x
... | q = Tl-v q
strengthen-■-var (Γ' ■) (y ∷ₗ Δ) (Tl-■ p x) with strengthen-■-var Γ' (y ∷ₗ Δ) x
... | q = Tl-■ p q

mutual
  strengthen-■-v : {Γ Γ' : Ctx} {Δ : BCtx} {X : VType} →
                   (Γ ⋈ Δ) ■ ++ₖ Γ' ⊢V⦂ X →
                   -------------------------------------
                   Γ ■ ++ₖ Γ' ⊢V⦂ X

  strengthen-■-v {_} {Γ'} {Δ} (` x) =
    ` strengthen-■-var Γ' Δ x
  strengthen-■-v (´ c) =
    ´ c
  strengthen-■-v ⋆ =
    ⋆
  strengthen-■-v {Γ} {Γ'} {Δ} (ƛ M) =
    ƛ (strengthen-■-c {Γ} {Γ' ∷ _} {Δ} M)
  strengthen-■-v {Γ} {Γ'} {Δ} ⟨ V ⟩ =
    ⟨ strengthen-■-v {Γ} {Γ'} {Δ} V ⟩
  strengthen-■-v {Γ} {Γ'} {Δ} (□ V) =
    □ (strengthen-■-v {Γ' = _ ■} {Δ = Δ} V)

  strengthen-■-c : {Γ Γ' : Ctx} {Δ : BCtx} {C : CType} →
                   (Γ ⋈ Δ) ■ ++ₖ Γ' ⊢C⦂ C →
                   -------------------------------------
                   Γ ■ ++ₖ Γ' ⊢C⦂ C

  strengthen-■-c {Γ} {Γ'} {Δ} (return V) =
    return (strengthen-■-v {Γ} {Γ'} {Δ} V)
  strengthen-■-c {Γ} {Γ'} {Δ} (let= M `in N) =
    let= (strengthen-■-c {Γ} {Γ'} {Δ} M) `in (strengthen-■-c {Γ} {Γ' ∷ _} {Δ} N)
  strengthen-■-c {Γ} {Γ'} {Δ} (V · W) =
    (strengthen-■-v {Γ} {Γ'} {Δ} V) · (strengthen-■-v {Γ} {Γ'} {Δ} W)
  strengthen-■-c {Γ} {Γ'} {Δ} (↑ op p V M) =
    ↑ op p (strengthen-■-v {Γ} {Γ'} {Δ} V) (strengthen-■-c {Γ} {Γ'} {Δ} M)
  strengthen-■-c {Γ} {Γ'} {Δ} (↓ op V M) =
    ↓ op (strengthen-■-v {Γ} {Γ'} {Δ} V) (strengthen-■-c {Γ} {Γ'} {Δ} M)
  strengthen-■-c {Γ} {Γ'} {Δ} (promise op ∣ p ↦ M `in N) =
    promise op ∣ p ↦ (strengthen-■-c {Γ} {Γ' ∷ proj₁ (payload op) ∷ _} {Δ} M) `in (strengthen-■-c {Γ} {Γ' ∷ ⟨ _ ⟩} {Δ} N)
  strengthen-■-c {Γ} {Γ'} {Δ} (await V until N) =
    await (strengthen-■-v {Γ} {Γ'} {Δ} V) until (strengthen-■-c {Γ} {Γ' ∷ _} {Δ} N)
  strengthen-■-c {Γ} {Γ'} {Δ} (unbox V `in N) =
    unbox (strengthen-■-v {Γ} {Γ'} {Δ} V) `in (strengthen-■-c {Γ} {Γ' ∷ _} {Δ} N)
  strengthen-■-c {Γ} {Γ'} {Δ} (spawn M N) =
    spawn (strengthen-■-c {Γ' = _ ■} {Δ = Δ} M) (strengthen-■-c {Δ = Δ} N)
  strengthen-■-c {Γ} {Γ'} {Δ} (coerce p q M) =
    coerce p q (strengthen-■-c {Γ} {Γ'} {Δ} M)

strengthen-val : {Γ : Ctx} {Δ : BCtx} {X : VType} →
                 mobile X →
                 Γ ⋈ Δ ⊢V⦂ X →
                 ----------------------------------
                 Γ ⊢V⦂ X

strengthen-val {_} {Δ} p (` x) =
  ` strengthen-var Δ p x
strengthen-val p (´ c) =
  ´ c
strengthen-val p ⋆ =
  ⋆
strengthen-val {Γ} {Δ} p (□ V) =
  □ (strengthen-■-v {Γ} {[]} {Δ} V)

-- SMALL-STEP OPERATIONAL SEMANTICS FOR WELL-TYPED COMPUTATIONS
-- (ADDITIONALLY SERVES AS THE PRESERVATION THEOREM)

infix 10 _↝_

data _↝_ {Γ : Ctx} : {C : CType} → Γ ⊢C⦂ C → Γ ⊢C⦂ C → Set where

  -- COMPUTATIONAL RULES

  apply           : {X : VType}
                    {C : CType} →
                    (M : Γ ∷ X ⊢C⦂ C) →
                    (V : Γ ⊢V⦂ X) →
                    ----------------------
                    (ƛ M) · V
                    ↝
                    M [ sub-id [ V ]s ]c

  let-return      : {X Y : VType}
                    {o : O}
                    {i : I} →
                    (V : Γ ⊢V⦂ X) →
                    (N : Γ ∷ X ⊢C⦂ Y ! (o , i)) →
                    -----------------------------
                    let= (return V) `in N
                    ↝
                    N [ sub-id [ V ]s ]c

  let-↑           : {X Y : VType}
                    {o : O}
                    {i : I}
                    {op : Σₛ} →
                    (p : op ∈ₒ o) →
                    (V : Γ ⊢V⦂ proj₁ (payload op)) →
                    (M : Γ ⊢C⦂ X ! (o , i)) →
                    (N : Γ ∷ X ⊢C⦂ Y ! (o , i)) →
                    -----------------------------
                    let= (↑ op p V M) `in N
                    ↝
                    ↑ op p V (let= M `in N)

  let-promise     : {X Y Z : VType}
                    {o o' : O}
                    {i i' : I}
                    {op : Σₛ} →
                    (p : (o' , i') ⊑ lkpᵢ op i) →
                    (M₁ : Γ ∷ proj₁ (payload op) ∷ (𝟙 ⇒ (⟨ X ⟩ ! (∅ₒ , ∅ᵢ [ op ↦ just (o' , i') ]ᵢ))) ⊢C⦂ ⟨ X ⟩ ! (o' , i')) →
                    (M₂ : Γ ∷ ⟨ X ⟩ ⊢C⦂ Y ! (o , i)) →
                    (N : Γ ∷ Y ⊢C⦂ Z ! (o , i)) →
                    ----------------------------------------------------------------------------------------------------------
                    let= (promise op ∣ p ↦ M₁ `in M₂) `in N
                    ↝
                    (promise op ∣ p ↦ M₁ `in (let= M₂ `in (C-rename (ren-cong ren-wk) N)))

  let-await       : {X Y Z : VType}
                    {o : O}
                    {i : I} →
                    (V : Γ ⊢V⦂ ⟨ X ⟩) →
                    (M : Γ ∷ X ⊢C⦂ Y ! (o , i)) →
                    (N : Γ ∷ Y ⊢C⦂ Z ! (o , i)) →
                    -------------------------------------------------------
                    let= (await V until M) `in N
                    ↝
                    await V until (let= M `in C-rename (ren-cong ren-wk) N)

  let-spawn       : {X Y : VType}
                    {C : CType}
                    {o : O}
                    {i : I} →
                    (M : Γ ■ ⊢C⦂ C) →
                    (N : Γ ⊢C⦂ X ! (o , i)) →
                    (K : Γ ∷ X ⊢C⦂ Y ! (o , i)) →
                    ---------------------------------------
                    let= (spawn M N) `in K
                    ↝
                    spawn M (let= N `in K)

  promise-↑       : {X Y : VType}
                    {o o' : O}
                    {i i' : I}
                    {op op' : Σₛ} →
                    (p : (o' , i') ⊑ lkpᵢ op i) →
                    (q : op' ∈ₒ o) →
                    (V : Γ ∷ ⟨ X ⟩ ⊢V⦂ proj₁ (payload op')) →
                    (M : Γ ∷ proj₁ (payload op) ∷ (𝟙 ⇒ (⟨ X ⟩ ! (∅ₒ , ∅ᵢ [ op ↦ just (o' , i') ]ᵢ))) ⊢C⦂ ⟨ X ⟩ ! (o' , i')) →
                    (N : Γ ∷ ⟨ X ⟩ ⊢C⦂ Y ! (o , i)) →
                    -----------------------------------------------------------------------------------------
                    (promise op ∣ p ↦ M `in (↑ op' q V N))
                    ↝
                    ↑ op' q (strengthen-val {Δ = X ∷ₗ []} (proj₂ (payload op')) V) (promise op ∣ p ↦ M `in N)

  promise-spawn   : {X Y : VType}
                    {C : CType}
                    {o o' : O}
                    {i i' : I}
                    {op : Σₛ} →
                    (p : (o' , i') ⊑ lkpᵢ op i) →
                    (M : Γ ∷ proj₁ (payload op) ∷ (𝟙 ⇒ (⟨ X ⟩ ! (∅ₒ , ∅ᵢ [ op ↦ just (o' , i') ]ᵢ))) ⊢C⦂ ⟨ X ⟩ ! (o' , i')) →
                    (N : Γ ∷ ⟨ X ⟩ ■ ⊢C⦂ C) →
                    (K : Γ ∷ ⟨ X ⟩ ⊢C⦂ Y ! (o , i)) →
                    ---------------------------------------------------------------------------
                    (promise op ∣ p  ↦ M `in (spawn N K))
                    ↝
                    spawn (strengthen-■-c {Γ' = []} {Δ = X ∷ₗ []} N) (promise op ∣ p ↦ M `in K)

  ↓-return        : {X : VType}
                    {o : O}
                    {i : I}
                    {op : Σₛ} →
                    (V : Γ ⊢V⦂ proj₁ (payload op)) →
                    (W : Γ ⊢V⦂ X) →
                    ----------------------------------------------------------------
                    ↓ {o = o} {i = i} op V (return W)
                    ↝
                    return {o = proj₁ (op ↓ₑ (o , i))} {i = proj₂ (op ↓ₑ (o , i))} W

  ↓-↑             : {X : VType}
                    {o : O}
                    {i : I}
                    {op : Σₛ}
                    {op' : Σₛ} →
                    (p : op' ∈ₒ o) →
                    (V : Γ ⊢V⦂ proj₁ (payload op)) →
                    (W : Γ ⊢V⦂ proj₁ (payload op')) →
                    (M : Γ ⊢C⦂ X ! (o , i)) →
                    --------------------------------
                    ↓ op V (↑ op' p W M)
                    ↝
                    ↑ op' (↓ₑ-⊑ₒ op' p) W (↓ op V M)

  ↓-promise-op    : {X Y : VType}
                    {o o' : O}
                    {i i' : I}
                    {op : Σₛ} →
                    (p : (o' , i') ⊑ lkpᵢ op i) →
                    (V : Γ ⊢V⦂ proj₁ (payload op)) →
                    (M : Γ ∷ proj₁ (payload op) ∷ (𝟙 ⇒ (⟨ X ⟩ ! (∅ₒ , ∅ᵢ [ op ↦ just (o' , i') ]ᵢ))) ⊢C⦂ ⟨ X ⟩ ! (o' , i')) →
                    (N : Γ ∷ ⟨ X ⟩ ⊢C⦂ Y ! (o , i)) →
                    --------------------------------------------------------------------------------------------------------------------------------------------------------
                    ↓ op V (promise op ∣ p ↦ M `in N )
                    ↝
                    (let= (coerce (⊑ₒ-trans (proj₁ (⊑-proj p (proj₂ (proj₂ (⊑-just p))))) (↓ₑ-⊑ₒ-o' {o = o} (proj₂ (proj₂ (⊑-just p)))))
                                  (⊑ᵢ-trans (proj₂ (⊑-proj p (proj₂ (proj₂ (⊑-just p))))) (↓ₑ-⊑ₒ-i' {o = o} (proj₂ (proj₂ (⊑-just p)))))
                                  (M [ (sub-id [ V ]s)
                                     [ ƛ (promise op ∣ subst (λ oi → (o' , i') ⊑ oi) (sym ite-≡) ⊑-refl ↦ C-rename (ren-cong (ren-cong ren-wk)) M `in return (` Hd)) ]s ]c))
                     `in (↓ op (V-rename ren-wk V) N))

  ↓-promise-op'   : {X Y : VType}
                    {o o' : O}
                    {i i' : I}
                    {op op' : Σₛ} →
                    (p : ¬ op ≡ op') →
                    (q : (o' , i') ⊑ lkpᵢ op' i) →
                    (V : Γ ⊢V⦂ proj₁ (payload op)) →
                    (M : Γ ∷ proj₁ (payload op') ∷ (𝟙 ⇒ (⟨ X ⟩ ! (∅ₒ , ∅ᵢ [ op' ↦ just (o' , i') ]ᵢ))) ⊢C⦂ ⟨ X ⟩ ! (o' , i')) →
                    (N : Γ ∷ ⟨ X ⟩ ⊢C⦂ Y ! (o , i)) →
                    ----------------------------------------------------------------------------------------------------------
                    ↓ op V (promise op' ∣ q ↦ M `in N )
                    ↝
                    promise op' ∣ (lkpᵢ-↓ₑ-neq-⊑ {o = o} {i = i} p q) ↦ M `in ↓ op (V-rename ren-wk V) N

  ↓-await         : {X Y : VType}
                    {o : O}
                    {i : I}
                    {op : Σₛ} →
                    (V : Γ ⊢V⦂ proj₁ (payload op)) →
                    (W : Γ ⊢V⦂ ⟨ X ⟩) →
                    (M : Γ ∷ X ⊢C⦂ Y ! (o , i)) →
                    ------------------------------------------
                    ↓ op V (await W until M)
                    ↝
                    await W until (↓ op (V-rename ren-wk V) M)

  ↓-spawn         : {X : VType}
                    {C : CType}
                    {o : O}
                    {i : I}
                    {op : Σₛ} →
                    (V : Γ ⊢V⦂ proj₁ (payload op)) →
                    (M : Γ ■ ⊢C⦂ C) →
                    (N : Γ ⊢C⦂ X ! (o , i)) →
                    --------------------------------
                    ↓ op V (spawn M N)
                    ↝
                    spawn M (↓ op V N)

  await-promise   : {X : VType}
                    {C : CType} →
                    (V : Γ ⊢V⦂ X) →
                    (M : Γ ∷ X ⊢C⦂ C) →
                    --------------------
                    await ⟨ V ⟩ until M
                    ↝
                    M [ sub-id [ V ]s ]c

  box-unbox       : {X : VType}
                    {C : CType} →
                    (V : Γ ■ ⊢V⦂ X) →
                    (M : Γ ∷ X ⊢C⦂ C) →
                    -------------------
                    unbox (□ V) `in M
                    ↝
                    M [ ⟨ sub-id ,, ■-str-v {Γ' = []} V ⟩ ]c

  -- EVALUATION CONTEXT RULE

  context         : {Δ : BCtx}
                    {C : CType} →
                    (E : Γ ⊢E[ Δ ]⦂ C) →
                    {M N : Γ ⋈ Δ ⊢C⦂ (hole-ty-e E)} →
                    M ↝ N →
                    -------------------------------
                    E [ M ] ↝ E [ N ]

  -- COERCION RULES
  -- (THE RESULT OF WORKING WITH WELL-TYPED SYNTAX AND MAKING SUBSUMPTION INTO AN EXPLICIT COERCION)

  coerce-return   : {X : VType}
                    {o o' : O}
                    {i i' : I}
                    {p : o ⊑ₒ o'}
                    {q : i ⊑ᵢ i'} →
                    (V : Γ ⊢V⦂ X) →
                    --------------------------------
                    coerce p q (return V) ↝ return V

  coerce-↑        : {X : VType}
                    {o o' : O}
                    {i i' : I}
                    {p : o ⊑ₒ o'}
                    {q : i ⊑ᵢ i'}
                    {op : Σₛ} →
                    (r : op ∈ₒ o) →
                    (V : Γ ⊢V⦂ proj₁ (payload op)) →
                    (M : Γ ⊢C⦂ X ! (o , i)) →
                    --------------------------------
                    coerce p q (↑ op r V M)
                    ↝
                    ↑ op (p op r) V (coerce p q M)

  coerce-promise  : {X Y : VType}
                    {o o' o'' : O}
                    {i i' i'' : I}
                    {p : o ⊑ₒ o'}
                    {q : i ⊑ᵢ i'}
                    {op : Σₛ} →
                    (r : (o'' , i'') ⊑ lkpᵢ op i)
                    (M : Γ ∷ proj₁ (payload op) ∷ (𝟙 ⇒ (⟨ X ⟩ ! (∅ₒ , ∅ᵢ [ op ↦ just (o'' , i'') ]ᵢ))) ⊢C⦂ ⟨ X ⟩ ! (o'' , i'')) →
                    (N : Γ ∷ ⟨ X ⟩ ⊢C⦂ Y ! (o , i)) →
                    -------------------------------------------------------------------------------------------------------------
                    coerce p q (promise op ∣ r ↦ M `in N)
                    ↝
                    promise_∣_↦_`in_ op (subst (λ oi → (o'' , i'') ⊑ oi) (sym (lkpᵢ-next-eq q (proj₂ (proj₂ (⊑-just r)))))
                                          (⊑-trans r (proj₂ (proj₂ (⊑-just r))) (
                                            (lkpᵢ-next-⊑ₒ q (proj₂ (proj₂ (⊑-just r)))) ,
                                            (lkpᵢ-next-⊑ᵢ q (proj₂ (proj₂ (⊑-just r)))))))
                                        M
                                        (coerce p q N)

  coerce-await   : {X Y : VType}
                   {o o' : O}
                   {i i' : I}
                   {p : o ⊑ₒ o'}
                   {q : i ⊑ᵢ i'} →
                   (V : Γ ⊢V⦂ ⟨ X ⟩) →
                   (M : Γ ∷ X ⊢C⦂ Y ! (o , i)) →
                   -----------------------------
                   coerce p q (await V until M)
                   ↝
                   await V until (coerce p q M)

  coerce-spawn   : {X : VType}
                   {C : CType}
                   {o o' : O}
                   {i i' : I}
                   {p : o ⊑ₒ o'}
                   {q : i ⊑ᵢ i'} →
                   (M : Γ ■ ⊢C⦂ C) →
                   (N : Γ ⊢C⦂ X ! (o , i)) →
                   -------------------------
                   coerce p q (spawn M N)
                   ↝
                   spawn M (coerce p q N)

max_stars_repo_name: danelahman/higher-order-aeff-agda

max_issues_repo_name: danelahman/modal-aeff-agda

max_forks_repo_name: danelahman/modal-aeff-agda


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

module FormalLanguage.Proofs {ℓ} where

import      Lvl
open import Data
open import Data.Boolean
open import Data.Boolean.Proofs
open import Data.Boolean.Operators
open        Data.Boolean.Operators.Programming
open import Data.Boolean.Stmt
open import Data.Boolean.Stmt.Proofs
import      Data.Tuple as Tuple
open import FormalLanguage
open import FormalLanguage.Equals
open import Functional using (id)
open import Sized.Data.List renaming (∅ to [])
open import Lang.Size
open import Logic.Predicate
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Relator.Equals using ([≡]-intro) renaming (_≡_ to _≡ₑ_)
open import Relator.Equals.Proofs
import      Function.Names as Names
open import Structure.Setoid
open import Structure.Operator.Monoid
import      Structure.Operator.Names as Names
open import Structure.Operator.Proofs
open import Structure.Operator.Properties
-- open import Structure.Operator.SetAlgebra
open import Structure.Operator
open import Structure.Function.Domain
open import Structure.Relator
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Type

-- TODO: Prove all these
-- TODO: http://www.cse.chalmers.se/~abela/jlamp17.pdf

private variable s s₁ s₂ s₃ : Size

{-
module _ {Σ : Alphabet{ℓ}} where
  open Oper{ℓ}{Σ}
  open Language renaming (accepts-ε to accepts ; suffix-lang to suffix)

  instance
    [∪]-associativity : Associativity ⦃ [≅]-equiv {s = s} ⦄ (_∪_)
    Associativity.proof([∪]-associativity {s = s}) = [∪]-associativity-raw {s = s} where
      [∪]-associativity-raw : ∀{s} → Names.Associativity ⦃ [≅]-equiv {s = s} ⦄ (_∪_)
      _≅[_]≅_.accepts-ε   ([∪]-associativity-raw {x = A})     = associativity(_||_) {Language.accepts-ε A}
      _≅[_]≅_.suffix-lang ([∪]-associativity-raw {x = A}) {c} = [∪]-associativity-raw {x = Language.suffix-lang A c}

  instance
    [∪]-commutativity : Commutativity ⦃ [≅]-equiv {s = s} ⦄ (_∪_)
    Commutativity.proof([∪]-commutativity {s = s}) = [∪]-commutativity-raw {s = s} where
      [∪]-commutativity-raw : ∀{s} → Names.Commutativity ⦃ [≅]-equiv {s = s} ⦄ (_∪_)
      _≅[_]≅_.accepts-ε   ([∪]-commutativity-raw {x = A})     = commutativity(_||_) {Language.accepts-ε A}
      _≅[_]≅_.suffix-lang ([∪]-commutativity-raw {x = A}) {c} = [∪]-commutativity-raw {x = Language.suffix-lang A c}

  instance
    [∪]-identityₗ : Identityₗ ⦃ [≅]-equiv {s = s} ⦄ (_∪_)(∅)
    Identityₗ.proof([∪]-identityₗ {s = s}) = [∪]-identityₗ-raw {s = s} where
      [∪]-identityₗ-raw : ∀{s} → Names.Identityₗ ⦃ [≅]-equiv {s = s} ⦄ (_∪_)(∅)
      _≅[_]≅_.accepts-ε   ([∪]-identityₗ-raw {x = A})     = [≡]-intro
      _≅[_]≅_.suffix-lang ([∪]-identityₗ-raw {x = A}) {c} = [∪]-identityₗ-raw {x = Language.suffix-lang A c}

  instance
    [∪]-identityᵣ : Identityᵣ ⦃ [≅]-equiv {s = s} ⦄ (_∪_)(∅)
    Identityᵣ.proof([∪]-identityᵣ {s = s}) = [∪]-identityᵣ-raw {s = s} where
      [∪]-identityᵣ-raw : ∀{s} → Names.Identityᵣ ⦃ [≅]-equiv {s = s} ⦄ (_∪_)(∅)
      _≅[_]≅_.accepts-ε   ([∪]-identityᵣ-raw {x = A})     = [≡]-intro
      _≅[_]≅_.suffix-lang ([∪]-identityᵣ-raw {x = A}) {c} = [∪]-identityᵣ-raw {x = Language.suffix-lang A c}

  instance
    [∪]-identity : Identity ⦃ [≅]-equiv {s = s} ⦄ (_∪_)(∅)
    [∪]-identity = intro

  instance
    [∪]-absorberₗ : Absorberₗ ⦃ [≅]-equiv {s = s} ⦄ (_∪_)(𝐔)
    Absorberₗ.proof([∪]-absorberₗ {s = s}) = [∪]-absorberₗ-raw {s = s} where
      [∪]-absorberₗ-raw : ∀{s} → Names.Absorberₗ ⦃ [≅]-equiv {s = s} ⦄ (_∪_)(𝐔)
      _≅[_]≅_.accepts-ε   ([∪]-absorberₗ-raw {x = A})     = [≡]-intro
      _≅[_]≅_.suffix-lang ([∪]-absorberₗ-raw {x = A}) {c} = [∪]-absorberₗ-raw {x = Language.suffix-lang A c}

  instance
    [∪]-absorberᵣ : Absorberᵣ ⦃ [≅]-equiv {s = s} ⦄ (_∪_)(𝐔)
    Absorberᵣ.proof([∪]-absorberᵣ {s = s}) = [∪]-absorberᵣ-raw {s = s} where
      [∪]-absorberᵣ-raw : ∀{s} → Names.Absorberᵣ ⦃ [≅]-equiv {s = s} ⦄ (_∪_)(𝐔)
      _≅[_]≅_.accepts-ε   ([∪]-absorberᵣ-raw {x = A})     = [≡]-intro
      _≅[_]≅_.suffix-lang ([∪]-absorberᵣ-raw {x = A}) {c} = [∪]-absorberᵣ-raw {x = Language.suffix-lang A c}

  instance
    [∪]-absorber : Absorber ⦃ [≅]-equiv {s = s} ⦄ (_∪_)(𝐔)
    [∪]-absorber = intro

  instance
    [∪]-binary-operator : BinaryOperator ⦃ [≅]-equiv {s = s} ⦄ ⦃ [≅]-equiv {s = s} ⦄ ⦃ [≅]-equiv {s = s} ⦄ (_∪_)
    BinaryOperator.congruence([∪]-binary-operator {s = s}) = [∪]-binary-operator-raw {s = s} where
      [∪]-binary-operator-raw : ∀{s} → Names.Congruence₂ ⦃ [≅]-equiv {s = s} ⦄ ⦃ [≅]-equiv {s = s} ⦄ ⦃ [≅]-equiv {s = s} ⦄ (_∪_)
      _≅[_]≅_.accepts-ε   ([∪]-binary-operator-raw aeq beq) = [≡]-with-op(_||_) (_≅[_]≅_.accepts-ε aeq) (_≅[_]≅_.accepts-ε beq)
      _≅[_]≅_.suffix-lang ([∪]-binary-operator-raw aeq beq) = [∪]-binary-operator-raw (_≅[_]≅_.suffix-lang aeq) (_≅[_]≅_.suffix-lang beq)

  instance
    [∪]-monoid : Monoid ⦃ [≅]-equiv {s = s} ⦄ (_∪_)
    Monoid.identity-existence [∪]-monoid = [∃]-intro(∅)

  instance
    [∩]-associativity : Associativity ⦃ [≅]-equiv {s = s} ⦄ (_∩_)
    Associativity.proof([∩]-associativity {s = s}) = [∩]-associativity-raw {s = s} where
      [∩]-associativity-raw : ∀{s} → Names.Associativity ⦃ [≅]-equiv {s = s} ⦄ (_∩_)
      _≅[_]≅_.accepts-ε   ([∩]-associativity-raw {x = A})     = associativity(_&&_) {Language.accepts-ε A}
      _≅[_]≅_.suffix-lang ([∩]-associativity-raw {x = A}) {c} = [∩]-associativity-raw {x = Language.suffix-lang A c}

  instance
    [∩]-commutativity : Commutativity ⦃ [≅]-equiv {s = s} ⦄ (_∩_)
    Commutativity.proof([∩]-commutativity {s = s}) = [∩]-commutativity-raw {s = s} where
      [∩]-commutativity-raw : ∀{s} → Names.Commutativity ⦃ [≅]-equiv {s = s} ⦄ (_∩_)
      _≅[_]≅_.accepts-ε   ([∩]-commutativity-raw {x = A})     = commutativity(_&&_) {Language.accepts-ε A}
      _≅[_]≅_.suffix-lang ([∩]-commutativity-raw {x = A}) {c} = [∩]-commutativity-raw {x = Language.suffix-lang A c}

  instance
    [∩]-identityₗ : Identityₗ ⦃ [≅]-equiv {s = s} ⦄ (_∩_)(𝐔)
    Identityₗ.proof([∩]-identityₗ {s = s}) = [∩]-identityₗ-raw {s = s} where
      [∩]-identityₗ-raw : ∀{s} → Names.Identityₗ ⦃ [≅]-equiv {s = s} ⦄ (_∩_)(𝐔)
      _≅[_]≅_.accepts-ε   ([∩]-identityₗ-raw {x = A})     = [≡]-intro
      _≅[_]≅_.suffix-lang ([∩]-identityₗ-raw {x = A}) {c} = [∩]-identityₗ-raw {x = Language.suffix-lang A c}

  instance
    [∩]-identityᵣ : Identityᵣ ⦃ [≅]-equiv {s = s} ⦄ (_∩_)(𝐔)
    Identityᵣ.proof([∩]-identityᵣ {s = s}) = [∩]-identityᵣ-raw {s = s} where
      [∩]-identityᵣ-raw : ∀{s} → Names.Identityᵣ ⦃ [≅]-equiv {s = s} ⦄ (_∩_)(𝐔)
      _≅[_]≅_.accepts-ε   ([∩]-identityᵣ-raw {x = A})     = [≡]-intro
      _≅[_]≅_.suffix-lang ([∩]-identityᵣ-raw {x = A}) {c} = [∩]-identityᵣ-raw {x = Language.suffix-lang A c}

  instance
    [∩]-identity : Identity ⦃ [≅]-equiv {s = s} ⦄ (_∩_)(𝐔)
    [∩]-identity = intro

  instance
    [∩]-absorberₗ : Absorberₗ ⦃ [≅]-equiv {s = s} ⦄ (_∩_)(∅)
    Absorberₗ.proof([∩]-absorberₗ {s = s}) = [∩]-absorberₗ-raw {s = s} where
      [∩]-absorberₗ-raw : ∀{s} → Names.Absorberₗ ⦃ [≅]-equiv {s = s} ⦄ (_∩_)(∅)
      _≅[_]≅_.accepts-ε   ([∩]-absorberₗ-raw {x = A})     = [≡]-intro
      _≅[_]≅_.suffix-lang ([∩]-absorberₗ-raw {x = A}) {c} = [∩]-absorberₗ-raw {x = Language.suffix-lang A c}

  instance
    [∩]-absorberᵣ : Absorberᵣ ⦃ [≅]-equiv {s = s} ⦄ (_∩_)(∅)
    Absorberᵣ.proof([∩]-absorberᵣ {s = s}) = [∩]-absorberᵣ-raw {s = s} where
      [∩]-absorberᵣ-raw : ∀{s} → Names.Absorberᵣ ⦃ [≅]-equiv {s = s} ⦄ (_∩_)(∅)
      _≅[_]≅_.accepts-ε   ([∩]-absorberᵣ-raw {x = A})     = [≡]-intro
      _≅[_]≅_.suffix-lang ([∩]-absorberᵣ-raw {x = A}) {c} = [∩]-absorberᵣ-raw {x = Language.suffix-lang A c}

  instance
    [∩]-absorber : Absorber ⦃ [≅]-equiv {s = s} ⦄ (_∩_)(∅)
    [∩]-absorber = intro

  instance
    [∩]-binary-operator : BinaryOperator ⦃ [≅]-equiv {s = s} ⦄ ⦃ [≅]-equiv {s = s} ⦄ ⦃ [≅]-equiv {s = s} ⦄ (_∩_)
    BinaryOperator.congruence([∩]-binary-operator {s = s}) = [∩]-binary-operator-raw {s = s} where
      [∩]-binary-operator-raw : ∀{s} → Names.Congruence₂ ⦃ [≅]-equiv {s = s} ⦄ ⦃ [≅]-equiv {s = s} ⦄ ⦃ [≅]-equiv {s = s} ⦄(_∩_)
      _≅[_]≅_.accepts-ε   ([∩]-binary-operator-raw aeq beq) = [≡]-with-op(_&&_) (_≅[_]≅_.accepts-ε aeq) (_≅[_]≅_.accepts-ε beq)
      _≅[_]≅_.suffix-lang ([∩]-binary-operator-raw aeq beq) = [∩]-binary-operator-raw (_≅[_]≅_.suffix-lang aeq) (_≅[_]≅_.suffix-lang beq)

  instance
    [∩]-monoid : Monoid ⦃ [≅]-equiv {s = s} ⦄ (_∩_)
    Monoid.identity-existence [∩]-monoid = [∃]-intro(𝐔)

  instance
    [∪][∩]-distributivityₗ : Distributivityₗ ⦃ [≅]-equiv {s = s} ⦄ (_∪_)(_∩_)
    Distributivityₗ.proof([∪][∩]-distributivityₗ {s = s}) = [∪][∩]-distributivityₗ-raw {s = s} where
      [∪][∩]-distributivityₗ-raw : ∀{s} → Names.Distributivityₗ ⦃ [≅]-equiv {s = s} ⦄ (_∪_)(_∩_)
      _≅[_]≅_.accepts-ε   ([∪][∩]-distributivityₗ-raw {x = A})     = distributivityₗ(_||_)(_&&_) {x = Language.accepts-ε A}
      _≅[_]≅_.suffix-lang ([∪][∩]-distributivityₗ-raw {x = A}) {c} = [∪][∩]-distributivityₗ-raw {x = Language.suffix-lang A c}

  instance
    [∩][∪]-distributivityₗ : Distributivityₗ ⦃ [≅]-equiv {s = s} ⦄ (_∩_)(_∪_)
    Distributivityₗ.proof([∩][∪]-distributivityₗ {s = s}) = [∩][∪]-distributivityₗ-raw {s = s} where
      [∩][∪]-distributivityₗ-raw : ∀{s} → Names.Distributivityₗ ⦃ [≅]-equiv {s = s} ⦄ (_∩_)(_∪_)
      _≅[_]≅_.accepts-ε   ([∩][∪]-distributivityₗ-raw {x = A})     = distributivityₗ(_&&_)(_||_) {x = Language.accepts-ε A}
      _≅[_]≅_.suffix-lang ([∩][∪]-distributivityₗ-raw {x = A}) {c} = [∩][∪]-distributivityₗ-raw {x = Language.suffix-lang A c}

  instance
    [𝁼][∪]-distributivityₗ : Distributivityₗ ⦃ [≅]-equiv {s = s} ⦄ (_𝁼_)(_∪_)
    Distributivityₗ.proof ([𝁼][∪]-distributivityₗ {s = s}) = [𝁼][∪]-distributivityₗ-raw {s = s} where
      [𝁼][∪]-distributivityₗ-raw : ∀{s} → Names.Distributivityₗ ⦃ [≅]-equiv {s = s} ⦄ (_𝁼_)(_∪_)
      _≅[_]≅_.accepts-ε ([𝁼][∪]-distributivityₗ-raw {x = x}) with accepts x
      ... | 𝑇 = [≡]-intro
      ... | 𝐹 = [≡]-intro
      _≅[_]≅_.suffix-lang ([𝁼][∪]-distributivityₗ-raw {x = x}{y}{z}) {c} with accepts x
      ... | 𝑇 =
        ((suffix x c) 𝁼 (y ∪ z)) ∪ ((suffix y c) ∪ (suffix z c))                  🝖[ _≅_ ]-[ congruence₂ₗ(_∪_) _ [𝁼][∪]-distributivityₗ-raw ]
        (((suffix x c) 𝁼 y) ∪ ((suffix x c) 𝁼 z)) ∪ ((suffix y c) ∪ (suffix z c)) 🝖[ _≅_ ]-[ One.associate-commute4 (commutativity(_∪_)) ]
        (((suffix x c) 𝁼 y) ∪ (suffix y c)) ∪ (((suffix x c) 𝁼 z) ∪ (suffix z c)) 🝖[ _≅_ ]-end
      ... | 𝐹 = [𝁼][∪]-distributivityₗ-raw

{-TODO
idempotence-by-dist-id-abs-idemp
x ∪ x
(x ∩ x) ∪ (x ∩ x)
(x ∪ x) ∩ x
(x ∪ x) ∩ (x ∪ ∅)
x ∪ (x ∩ ∅)
x ∪ ∅
x

idempotence-by-dist-inv-id
x ∪ x
(x ∪ x) ∩ 𝐔
(x ∪ x) ∩ (x ∪ (∁ x))
x ∪ (x ∩ (∁ x))
x ∪ ∅
x
-}

  instance
    [𝁼][∪]-distributivityᵣ : Distributivityᵣ ⦃ [≅]-equiv {s = s} ⦄ (_𝁼_)(_∪_)
    Distributivityᵣ.proof ([𝁼][∪]-distributivityᵣ {s}) = [𝁼][∪]-distributivityᵣ-raw where
      [𝁼][∪]-distributivityᵣ-raw : ∀{s} → Names.Distributivityᵣ ⦃ [≅]-equiv {s = s} ⦄ (_𝁼_)(_∪_)
      _≅[_]≅_.accepts-ε ([𝁼][∪]-distributivityᵣ-raw {x = x}{y}{z}) with accepts z
      ... | 𝑇 = [≡]-intro
      ... | 𝐹 = [≡]-intro
      _≅[_]≅_.suffix-lang ([𝁼][∪]-distributivityᵣ-raw {x = x}{y}{z}) {c} with accepts x | accepts y
      ... | 𝑇 | 𝑇 =
        (((suffix x c) ∪ (suffix y c)) 𝁼 z) ∪ (suffix z c)                        🝖[ _≅_ ]-[ congruence₂ₗ(_∪_) _ [𝁼][∪]-distributivityᵣ-raw ]
        (((suffix x c) 𝁼 z) ∪ ((suffix y c) 𝁼 z)) ∪ (suffix z c)                  🝖[ _≅_ ]-[ congruence₂ᵣ(_∪_) _ {!!} ]-sym
        (((suffix x c) 𝁼 z) ∪ ((suffix y c) 𝁼 z)) ∪ ((suffix z c) ∪ (suffix z c)) 🝖[ _≅_ ]-[ One.associate-commute4 (commutativity(_∪_)) ]
        (((suffix x c) 𝁼 z) ∪ (suffix z c)) ∪ (((suffix y c) 𝁼 z) ∪ (suffix z c)) 🝖[ _≅_ ]-end
      ... | 𝑇 | 𝐹 = {!!}
      ... | 𝐹 | 𝑇 = {!!}
      ... | 𝐹 | 𝐹 = {!!}

  instance
    [𝁼]-associativity : Associativity ⦃ [≅]-equiv {s = s} ⦄ (_𝁼_)
    Associativity.proof ([𝁼]-associativity {s = s}) = [𝁼]-associativity-raw {s = s} where
      [𝁼]-associativity-raw : ∀{s} → Names.Associativity ⦃ [≅]-equiv {s = s} ⦄ (_𝁼_)
      _≅[_]≅_.accepts-ε   ([𝁼]-associativity-raw {s = s} {x} {y} {z} ) with Language.accepts-ε(x)
      ... | 𝑇 = [≡]-intro
      ... | 𝐹 = [≡]-intro
      _≅[_]≅_.suffix-lang ([𝁼]-associativity-raw {s = s} {x} {y} {z}) {c} {sₛ} with [𝁼]-associativity-raw {s = sₛ} {suffix x c}{y}{z} | accepts(x) | accepts(y)
      ... | p | 𝑇 | 𝑇 =
        ((((suffix x c) 𝁼 y) ∪ (suffix y c)) 𝁼 z) ∪ (suffix z c)       🝖[ _≅_ ]-[ congruence₂ₗ(_∪_) _ (distributivityᵣ(_𝁼_)(_∪_)) ]
        ((((suffix x c) 𝁼 y) 𝁼 z) ∪ ((suffix y c) 𝁼 z)) ∪ (suffix z c) 🝖[ _≅_ ]-[ congruence₂ₗ(_∪_) _ (congruence₂ₗ(_∪_) _ p) ]
        (((suffix x c) 𝁼 (y 𝁼 z)) ∪ ((suffix y c) 𝁼 z)) ∪ (suffix z c) 🝖[ _≅_ ]-[ associativity(_∪_) ]
        ((suffix x c) 𝁼 (y 𝁼 z)) ∪ (((suffix y c) 𝁼 z) ∪ (suffix z c)) 🝖[ _≅_ ]-end
      ... | p | 𝑇 | 𝐹 =
        (((suffix x c) 𝁼 y) ∪ (suffix y c)) 𝁼 z       🝖[ _≅_ ]-[ distributivityᵣ(_𝁼_)(_∪_) ]
        (((suffix x c) 𝁼 y) 𝁼 z) ∪ ((suffix y c) 𝁼 z) 🝖[ _≅_ ]-[ congruence₂ₗ(_∪_) _ p ]
        ((suffix x c) 𝁼 (y 𝁼 z)) ∪ ((suffix y c) 𝁼 z) 🝖[ _≅_ ]-end
      ... | p | 𝐹 | _ = p

  {- TODO: Is it possible to describe concatenation using an algebraic property? Maybe something about that it behaves like (_⨯_) (combining every element with each other in some way)? Probably a "Kleene algebra".

  postulate [𝁼]-identityₗ : Identityₗ(_𝁼_)(ε)
  -- Identityₗ.proof([𝁼]-identityₗ) {x} =

  postulate [𝁼]-identityᵣ : Identityᵣ(_𝁼_)(ε)
  postulate [𝁼]-absorberₗ : Absorberₗ(_𝁼_)(∅)
  postulate [𝁼]-absorberᵣ : Absorberᵣ(_𝁼_)(∅)
--  postulate [*]-fixpoint-[ε] : FixPoint(_*)(ε)
  postulate [*]-on-[∅] : (∅ * ≡ ε)
  postulate [*]-on-[*] : ∀{L} → ((L *)* ≡ L *)
  postulate [𝁼]-commutativity-with-[*] : ∀{L} → ((L *) 𝁼 L ≡ L 𝁼 (L *))
  -- postulate [𝁼]-set-algebra : SetAlgebra -- TODO: Complement is missing
  -}

-}

module _ {Σ : Alphabet{ℓ}} where
  open Oper{ℓ}{Σ}
  open Language renaming (accepts-ε to accepts ; suffix-lang to suffix)

  open import Logic.IntroInstances
  open import Structure.Sets.Operator hiding (_∪_ ; _∩_ ; ∁ ; ∅ ; 𝐔)
  open import Structure.Sets.Relator hiding (_≡_ ; _⊆_)

  instance
    [≅]-set-equality : SetEqualityRelation([ s ]_∈_)([ s ]_∈_)(_≅[ s ]≅_)
    SetEqualityRelation.membership [≅]-set-equality {A}{B} = [↔]-intro (l{A = A}{B = B}) (r{A = A}{B = B}) where
      l : ∀{A B : Language(Σ)} → (A ≅[ s ]≅ B) ← (∀{w} → ([ s ] w ∈ A) ↔ ([ s ] w ∈ B))
      _≅[_]≅_.accepts-ε (l {A = A} {B = B} p) with accepts A | accepts B | p{[]}
      ... | 𝑇 | 𝑇 | _ = [≡]-intro
      ... | 𝑇 | 𝐹 | q with () ← [↔]-to-[→] q <>
      ... | 𝐹 | 𝑇 | q with () ← [↔]-to-[←] q <>
      ... | 𝐹 | 𝐹 | _ = [≡]-intro
      _≅[_]≅_.suffix-lang (l {A = A} {B = B} p) {c} = l {A = suffix A c}{B = suffix B c} (\{w} → p{c ⊰ w})

      r : ∀{A B : Language(Σ)} → (A ≅[ s ]≅ B) → (∀{w} → ([ s ] w ∈ A) ↔ ([ s ] w ∈ B))
      Tuple.left (r ab {[]}) wB = substitute₁ₗ(IsTrue) (_≅[_]≅_.accepts-ε ab) wB
      Tuple.right (r ab {[]}) wA = substitute₁ᵣ(IsTrue) (_≅[_]≅_.accepts-ε ab) wA
      Tuple.left (r {s = s} {A} {B} ab {_⊰_ {sₛ} x w}) wB = [↔]-to-[←] (r {s = sₛ} (_≅[_]≅_.suffix-lang {s = s} ab {sₛ = sₛ}) {w}) wB
      Tuple.right (r {s = s} {A} {B} ab {_⊰_ {sₛ} x w}) wA = [↔]-to-[→] (r {s = sₛ} (_≅[_]≅_.suffix-lang {s = s} ab {sₛ = sₛ}) {w}) wA

  instance
    [∪]-operator : UnionOperator([ s ]_∈_)([ s ]_∈_)([ s ]_∈_)(_∪_)
    UnionOperator.membership [∪]-operator {A}{B}{w} = [↔]-intro (l{w = w}{A}{B}) (r{w = w}{A}{B}) where
      l : ∀{w}{A B} → ([ s ] w ∈ (A ∪ B)) ← (([ s ] w ∈ A) ∨ ([ s ] w ∈ B))
      l {w = []}    = [↔]-to-[←] IsTrue.preserves-[||][∨]
      l {w = c ⊰ w} = l {w = w}

      r : ∀{w}{A B} → ([ s ] w ∈ (A ∪ B)) → (([ s ] w ∈ A) ∨ ([ s ] w ∈ B))
      r {w = []}    = [↔]-to-[→] IsTrue.preserves-[||][∨]
      r {w = c ⊰ w} = r {w = w}

  instance
    [∩]-operator : IntersectionOperator([ s ]_∈_)([ s ]_∈_)([ s ]_∈_)(_∩_)
    IntersectionOperator.membership [∩]-operator {A}{B}{w} = [↔]-intro (l{w = w}{A}{B}) (r{w = w}{A}{B}) where
      l : ∀{w}{A B} → ([ s ] w ∈ (A ∩ B)) ← (([ s ] w ∈ A) ∧ ([ s ] w ∈ B))
      l {w = []}    = [↔]-to-[←] IsTrue.preserves-[&&][∧]
      l {w = c ⊰ w} = l {w = w}

      r : ∀{w}{A B} → ([ s ] w ∈ (A ∩ B)) → (([ s ] w ∈ A) ∧ ([ s ] w ∈ B))
      r {w = []}    = [↔]-to-[→] IsTrue.preserves-[&&][∧]
      r {w = c ⊰ w} = r {w = w}

  instance
    [∁]-operator : ComplementOperator([ s ]_∈_)([ s ]_∈_)(∁_)
    ComplementOperator.membership [∁]-operator {A}{w} = [↔]-intro (l{w = w}{A}) (r{w = w}{A}) where
      l : ∀{w}{A} → ([ s ] w ∈ (∁ A)) ← ¬([ s ] w ∈ A)
      l {w = []}    = [↔]-to-[←] IsTrue.preserves-[!][¬]
      l {w = c ⊰ w} = l {w = w}

      r : ∀{w}{A} → ([ s ] w ∈ (∁ A)) → ¬([ s ] w ∈ A)
      r {w = []} = [↔]-to-[→] IsTrue.preserves-[!][¬]
      r {w = c ⊰ w} = r {w = w}

  instance
    [∅]-set : EmptySet([ s ]_∈_)(∅)
    EmptySet.membership [∅]-set {x = w} = p{w = w} where
      p : ∀{w} → ¬([ s ] w ∈ ∅)
      p {w = []} ()
      p {w = x ⊰ w} = p {w = w}

  instance
    [𝐔]-set : UniversalSet([ s ]_∈_)(𝐔)
    UniversalSet.membership [𝐔]-set {x = w} = p{w = w} where
      p : ∀{w} → ([ s ] w ∈ 𝐔)
      p {w = []}    = [⊤]-intro
      p {w = c ⊰ w} = p {w = w}

  [ε]-set : ∀{x} → (x ∈ ε) ↔ (x ≡ [])
  [ε]-set {x} = [↔]-intro (l{x}) (r{x}) where
    l : ∀{x} → (x ∈ ε) ← (x ≡ [])
    l {[]} [≡]-intro = [⊤]-intro

    r : ∀{x} → (x ∈ ε) → (x ≡ [])
    r {[]}    _     = [≡]-intro
    r {a ⊰ l} proof with () ← [∅]-membership {x = l} proof

  {-open import Structure.Container.SetLike hiding (_∪_ ; _∩_ ; ∁ ; ∅ ; 𝐔)
  -- TODO: Copy-pasted from the previous code that only used coinduction
  instance
    [𝁼][∪]-distributivityₗ : Distributivityₗ ⦃ [≅]-equiv {s = s} ⦄ (_𝁼_)(_∪_)
    Distributivityₗ.proof ([𝁼][∪]-distributivityₗ {s = s}) = [𝁼][∪]-distributivityₗ-raw {s = s} where
      [𝁼][∪]-distributivityₗ-raw : ∀{s} → Names.Distributivityₗ ⦃ [≅]-equiv {s = s} ⦄ (_𝁼_)(_∪_)
      _≅[_]≅_.accepts-ε ([𝁼][∪]-distributivityₗ-raw {x = x}) with accepts x
      ... | 𝑇 = [≡]-intro
      ... | 𝐹 = [≡]-intro
      _≅[_]≅_.suffix-lang ([𝁼][∪]-distributivityₗ-raw {s = s} {x = x}{y}{z}) {c} with accepts x
      ... | 𝑇 =
        ((suffix x c) 𝁼 (y ∪ z)) ∪ ((suffix y c) ∪ (suffix z c))                  🝖[ _≅[ s ]≅_ ]-[ congruence₂ₗ(_∪_) _ [𝁼][∪]-distributivityₗ-raw ]
        (((suffix x c) 𝁼 y) ∪ ((suffix x c) 𝁼 z)) ∪ ((suffix y c) ∪ (suffix z c)) 🝖[ _≅[ s ]≅_ ]-[ One.associate-commute4 (commutativity(_∪_)) ]
        (((suffix x c) 𝁼 y) ∪ (suffix y c)) ∪ (((suffix x c) 𝁼 z) ∪ (suffix z c)) 🝖[ _≅[ s ]≅_ ]-end
      ... | 𝐹 = [𝁼][∪]-distributivityₗ-raw
  -}

{- -- TODO: Sizes and (_++_)
  [𝁼]-membershipₗ : ∀{x y}{A B : Language(Σ)} → ([ s ] x ∈ A) → ([ s ] y ∈ B) → ([ s ] (x ++ y) ∈ (A 𝁼 B))
  [𝁼]-membershipₗ {x = []}   {[]}   {A}{B} xA yB with accepts A | accepts B
  ... | 𝑇 | 𝑇 = <>
  [𝁼]-membershipₗ {x = []}   {c ⊰ y}{A}{B} xA yB with accepts A
  ... | 𝑇 = [↔]-to-[←] (Union.membership {a = suffix A c 𝁼 B} {b = suffix B c} {x = y}) ([∨]-introᵣ yB)
  [𝁼]-membershipₗ {x = c ⊰ x}{y}{A}{B} xA yB with accepts A
  ... | 𝑇 = {!!}
  ... | 𝐹 = [𝁼]-membershipₗ {x = x}{y}{suffix A c}{B} {!xA!} {!!}
-}

-- [𝁼]-membershipₗ {[]}{y}{suffix }
-- [↔]-to-[←] (Union.membership {a = {!!}}{b = {!!}}{x = {!!}}) ([∨]-introᵣ yB)
{-

  single-containment : ⦃ _ : ComputablyDecidable(_≡_) ⦄ → ∀{x}{a} → (x ∈ single(a)) ↔ (x ≡ singleton(a))
  single-containment ⦃ dec ⦄ = [↔]-intro l r where
    postulate l : ∀{x}{a} → (x ∈ single(a)) ← (x ≡ singleton(a))
    {-l {c ⊰ w} [≡]-intro with ComputablyDecidable.decide(_≡_) ⦃ dec ⦄ c c
    ... | 𝑇 = {!!}
    ... | 𝐹 = {!!}-}

    postulate r : ∀{x}{a} → (x ∈ single(a)) → (x ≡ singleton(a))
    --r {c ⊰ w} p = {![↔]-to-[←] (ComputablyDecidable.proof-istrue(_≡_) {x = ?}) ?!}

  Language-list-suffix : Language(Σ) → List(Σ) → Language(Σ)
  Language-list-suffix A []      = A
  Language-list-suffix A (x ⊰ l) = Language.suffix-lang(A)(x)

  postulate suffix-concat-step : ∀{A : Language(Σ)}{l₁ l₂} → ((l₁ ++ l₂) ∈ A) → (l₂ ∈ Language-list-suffix(A)(l₁))
  -- suffix-concat-step {A}{[]}         p = p
  -- suffix-concat-step {A}{x ⊰ l₁}{l₂} p = {!!}

  postulate [𝁼]-containmentₗ : ∀{x y}{A B : Language(Σ)} → (x ∈ A) → (y ∈ B) → ((x ++ y) ∈ (A 𝁼 B))
  -- [𝁼]-containmentₗ {x} {y} {A} {B} xa xb with Language.accepts-ε(A) | y Oper.∈? B
  {-[𝁼]-containmentₗ {LongOper.empty} {LongOper.empty} {A} {B} xa xb with Language.accepts-ε(A) | Language.accepts-ε(B)
  [𝁼]-containmentₗ {LongOper.empty} {LongOper.empty} {A} {B} xa xb | 𝑇 | 𝑇 = [⊤]-intro
  [𝁼]-containmentₗ {LongOper.empty} {LongOper.prepend x y} {A} {B} xa xb = {![⊤]-intro!} where
    test : ∀{A B : Language(Σ)}{a} → ([] ∈ A) → (a ∈ B) → (a ∈ (A 𝁼 B))
    test {A}{B}{LongOper.empty} p q with Language.accepts-ε(A) | Language.accepts-ε(B)
    test {A}{B}{LongOper.empty} p q | 𝑇 | 𝑇 = [⊤]-intro
    test {A}{B}{LongOper.prepend x a} p q = {!test {A}{B}{a} p !}
    -- test {LongOper.prepend x a} p q with test {a} p (Language.suffix-lang q)
    -- ... | test = ?

  [𝁼]-containmentₗ {LongOper.prepend x x₁} {LongOper.empty} {A} {B} xa xb = {!!}
  [𝁼]-containmentₗ {LongOper.prepend x x₁} {LongOper.prepend x₂ y} {A} {B} xa xb = {!!}
-}

  -- [𝁼]-containment : ∀{x}{A B : Language(Σ)} → (x ∈ (A 𝁼 B)) ↔ ∃(a ↦ ∃ b ↦ (a ++ b ≡ x)∧(a ∈ A)∧(b ∈ B))
  -- [𝁼]-containment {x} = [↔]-intro (l{x}) (r{x}) where

-- TODO: Set properties
-- TODO: Connection with logic (from sets) in relations
-}


text:
module comb where

infixr 50 _⟶_

data Ty : Set where
  ι : Ty
  _⟶_ : Ty -> Ty -> Ty

data Tm : Ty -> Set where
  K : {σ τ : Ty} -> Tm (σ ⟶ τ ⟶ σ)
  S : {σ τ ρ : Ty} -> Tm ((σ ⟶ τ ⟶ ρ) ⟶ (σ ⟶ τ) ⟶ σ ⟶ ρ)
  _$_ : {σ τ : Ty} -> Tm (σ ⟶ τ) -> Tm σ -> Tm τ

data Nf : Ty -> Set where
  Kⁿ : {σ τ : Ty} -> Nf (σ ⟶ τ ⟶ σ)
  Kⁿ¹ : {σ τ : Ty} -> Nf σ -> Nf (τ ⟶ σ)
  Sⁿ : {σ τ ρ : Ty} -> Nf ((σ ⟶ τ ⟶ ρ) ⟶ (σ ⟶ τ) ⟶ σ ⟶ ρ)
  Sⁿ¹ : {σ τ ρ : Ty} -> Nf (σ ⟶ τ ⟶ ρ) -> Nf ((σ ⟶ τ) ⟶ σ ⟶ ρ)
  Sⁿ² : {σ τ ρ : Ty} -> Nf (σ ⟶ τ ⟶ ρ) -> Nf (σ ⟶ τ) -> Nf (σ ⟶ ρ)

_$$_ : {σ τ : Ty} -> Nf (σ ⟶ τ) -> Nf σ -> Nf τ
Kⁿ      $$ x = Kⁿ¹ x
Kⁿ¹ x   $$ y = x
Sⁿ      $$ x = Sⁿ¹ x
Sⁿ¹ x   $$ y = Sⁿ² x y
Sⁿ² x y $$ z = (x $$ z) $$ (y $$ z)

nf : {σ : Ty} -> Tm σ -> Nf σ
nf K = Kⁿ
nf S = Sⁿ
nf (t $ u) = nf t $$ nf u

data _$ⁿ_⇓_ : {σ τ : Ty} -> Nf (σ ⟶ τ) -> Nf σ -> Nf τ -> Set where
  rKⁿ  : {σ τ : Ty} -> {x : Nf σ} -> Kⁿ {σ} {τ} $ⁿ x ⇓ Kⁿ¹ x
  rKⁿ¹ : {σ τ : Ty} -> {x : Nf σ} -> {y : Nf τ} -> Kⁿ¹ x $ⁿ y ⇓ x
  rSⁿ  : {σ τ ρ : Ty} -> {x : Nf (σ ⟶ τ ⟶ ρ)} -> Sⁿ $ⁿ x ⇓ Sⁿ¹ x
  rSⁿ¹ : {σ τ ρ : Ty} -> {x : Nf (σ ⟶ τ ⟶ ρ)} -> {y : Nf (σ ⟶ τ)} ->
    Sⁿ¹ x $ⁿ y ⇓ Sⁿ² x y
  rSⁿ² : {σ τ ρ : Ty} -> {x : Nf (σ ⟶ τ ⟶ ρ)} -> {y : Nf (σ ⟶ τ)} ->
    {z : Nf σ} -> {u : Nf (τ ⟶ ρ)} -> x $ⁿ z ⇓ u -> {v : Nf τ} ->
    y $ⁿ z ⇓ v -> {w : Nf ρ} -> u $ⁿ v ⇓ w -> Sⁿ² x y $ⁿ z ⇓ w

data _⇓_ : {σ : Ty} -> Tm σ -> Nf σ -> Set where
  rK : {σ τ : Ty} -> K {σ} {τ} ⇓ Kⁿ
  rS : {σ τ ρ : Ty} -> S {σ} {τ} {ρ} ⇓ Sⁿ
  r$ : {σ τ : Ty} -> {t : Tm (σ ⟶ τ)} -> {f : Nf (σ ⟶ τ)} -> t ⇓ f ->
    {u : Tm σ} -> {a : Nf σ} -> u ⇓ a -> {v : Nf τ} -> f $ⁿ a ⇓ v  ->
    t $ u ⇓ v

data _==_ {A : Set}(a : A) : {B : Set} -> (b : B) -> Set where
  refl : a == a

data Σ {A : Set}(B : A -> Set) : Set where
  sig : (a : A) -> (b : B a) -> Σ B

σ₀ : {A : Set} -> {B : A -> Set} -> Σ B -> A
σ₀ (sig x _) = x

σ₁ : {A : Set} -> {B : A -> Set} -> (s : Σ B) -> B (σ₀ s)
σ₁ (sig _ y) = y

_$$⁼_&_ : {σ τ : Ty} -> (f : Nf (σ ⟶ τ)) -> (a : Nf σ) -> {n : Nf τ} ->
  f $ⁿ a ⇓ n ->     Σ \(n' : Nf τ) -> n' == n
Kⁿ      $$⁼ x & rKⁿ  = sig (Kⁿ¹ x) refl
Kⁿ¹ x   $$⁼ y & rKⁿ¹ = sig x refl
Sⁿ      $$⁼ x & rSⁿ  = sig (Sⁿ¹ x) refl
Sⁿ¹ x   $$⁼ y & rSⁿ¹ = sig (Sⁿ² x y) refl
Sⁿ² x y $$⁼ z & (rSⁿ² p q r) with x $$⁼ z & p | y $$⁼ z & q
Sⁿ² x y $$⁼ z & (rSⁿ² p q r)  |   sig u refl  | sig v refl with u $$⁼ v & r
Sⁿ² x y $$⁼ z & (rSⁿ² p q r)  |   sig u refl  | sig v refl  |   sig w refl =
  sig w refl

nf⁼ : {σ : Ty} -> (t : Tm σ) -> {n : Nf σ} -> t ⇓ n ->
  Σ \(n' : Nf σ) -> n' == n
nf⁼ K rK = sig Kⁿ refl
nf⁼ S rS = sig Sⁿ refl
nf⁼ (t $ u) (r$ p q r) with nf⁼ t p    | nf⁼ u q
nf⁼ (t $ u) (r$ p q r)  |   sig f refl | sig a refl with f $$⁼ a & r
nf⁼ (t $ u) (r$ p q r)  |   sig f refl | sig a refl  |   sig v refl =
  sig v refl

proof : {σ : Ty} -> (t : Tm σ) -> Σ \(n : Nf σ) -> t ⇓ n
proof = {! !}

nf⇓ :  {σ : Ty} -> Tm σ -> Nf σ
nf⇓ t = σ₀ (nf⁼ t (σ₁ (proof t)))


text:
{-

Constant structure: _ ↦ A

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Relational.Constant where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.RelationalStructure

open import Cubical.Structures.Constant

private
  variable
    ℓ ℓ' : Level

-- Structured relations

module _ (A : hSet ℓ') where

  preservesSetsConstant : preservesSets {ℓ = ℓ} (ConstantStructure (A .fst))
  preservesSetsConstant _ = A .snd

  ConstantRelStr : StrRel {ℓ = ℓ} (ConstantStructure (A .fst)) ℓ'
  ConstantRelStr _ a₀ a₁ = a₀ ≡ a₁

  open SuitableStrRel

  constantSuitableRel : SuitableStrRel {ℓ = ℓ} (ConstantStructure (A .fst)) ConstantRelStr
  constantSuitableRel .quo _ _ _ = isContrSingl _
  constantSuitableRel .symmetric _ = sym
  constantSuitableRel .transitive _ _ = _∙_
  constantSuitableRel .prop _ = A .snd

  constantRelMatchesEquiv : StrRelMatchesEquiv {ℓ = ℓ} ConstantRelStr (ConstantEquivStr (A .fst))
  constantRelMatchesEquiv _ _ _ = idEquiv _

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
module SystemF.BigStep.Extrinsic.Terms where

open import Prelude
open import SystemF.BigStep.Types
open import Data.List
open import Data.Fin.Substitution

-- erased (type-free) System F syntax
data Term : Set where
  unit : Term
  ƛ : Term → Term
  Λ : Term → Term
  _·_ : Term → Term → Term
  _[-] : Term → Term
  var : ℕ → Term


text:
-- There was a bug with module applications in let.
module Issue34 where

module A (X : Set) where
  postulate A : Set

T : (X : Set) -> let open A X in A -> Set
T X _ = X

record B (X : Set) : Set where
  open A X
  field f : A

postulate
  foo : (X : Set)(b : B X) ->
        let open A X
            open B b in
        A -> Set


text:
-- Andreas, 2019-11-11, issue #4189, reported by nad.

-- Record constructors living in the record module are problematic
-- as the record module is parameterized over the record value,
-- but the constructor not.

-- Thus, a record constructor does not live in the record module
-- any more.

-- {-# OPTIONS -v tc.mod.apply:100 #-}

record ⊤ : Set where
  constructor tt

module Unit = ⊤ renaming (tt to unit)
  -- WAS: internal error
  -- NOW: warning about tt not being in scope

tt′ : ⊤
tt′ = ⊤.tt
  -- WAS: success
  -- NOW: Not in scope: ⊤.tt


text:
{-# OPTIONS --instance-search-depth=10 #-}

open import Agda.Primitive

it : ∀ {a} {A : Set a} {{x : A}} -> A
it {{x}} = x

infixr 5 _,_
postulate
  Pair : ∀ {a} (A : Set a) {b} (B : Set b) -> Set (a ⊔ b)
  _,_  : ∀ {a} {A : Set a} {b} {B : Set b} -> A -> B -> Pair A B

data Constraint {a} {A : Set a} (x : A) : Set where
  mkConstraint : Constraint x

record Inner {l a} {A : Set a} (x : A) (_ : Constraint x) (C : Set l) : Set l where
  field
    value : C

Class : ∀ {l a} {A : Set a} (x : A) (C : Set l) -> Set l
Class x C = Inner x mkConstraint C

FunctionClass = λ
  {a} (A : Set a)
  -> Class A (A -> A)

DiagonalClass = λ
  {i} {I : Set i}
  {r} (R : I -> I -> Set r)
  x
  -> Class (R , x) (R x x)

DiagonalFunctionClass = λ
  {i} {I : Set i}
  {r} (R : I -> I -> Set r)
  x
  -> Class (R , x) (R x x -> R x x)

postulate
  toDiagonalFunctionClass : ∀
    {i} {I : Set i}
    {r} {R : I -> I -> Set r}
    {{iD : ∀ {x} -> DiagonalClass R x}}
    -> ∀ {x} -> DiagonalFunctionClass R x

DiagonalPropertyType = λ
  {i r p} {I : Set i}
  (R : I -> I -> Set r)
  (P : ∀ x -> R x x -> Set p)
  -> ∀ x (d : R x x) -> P _ d

DiagonalPropertyClass = λ
  {i r p} {I : Set i}
  (R : I -> I -> Set r)
  (P : ∀ x -> R x x -> Set p)
  (C : FunctionClass I)
  -> Class (R , P , C) (DiagonalPropertyType R P)

diagonalProperty : ∀
  {i r p} {I : Set i}
  {R : I -> I -> Set r}
  {P : ∀ x -> R x x -> Set p}
  {{C : FunctionClass I}}
  {{iDP : DiagonalPropertyClass R P C}}
  -> DiagonalPropertyType R P
diagonalProperty {{iDP = iDP}} = Inner.value iDP

-- works-1 works-2
fails : ∀
  {r p} {I : Set}
  {R : I -> I -> Set r}
  {P : ∀ x -> R x x -> Set p}
  (C : FunctionClass I)
  {{iDP : DiagonalPropertyClass R P C}}
  -> DiagonalPropertyType R P

-- works-1 C x d =
--   let instance iC = C
--   in diagonalProperty _ d

-- works-2 C x d =
--   let instance iC = C
--                iDF = toDiagonalFunctionClass
--   in diagonalProperty {{it}} _ d

fails C x d =
  let instance iC = C
               iDF = toDiagonalFunctionClass
  in diagonalProperty _ d -- Instance search depth exhausted


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.CommRing.RadicalIdeal where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Powerset using (⊆-isProp)
open import Cubical.Foundations.HLevels

open import Cubical.Data.Sigma
open import Cubical.Data.Sum hiding (map)
open import Cubical.Data.FinData hiding (elim)
open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_
                                      ; +-comm to +ℕ-comm
                                      ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm
                                      ; _choose_ to _ℕchoose_ ; snotz to ℕsnotz)
open import Cubical.Data.Nat.Order

open import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Ideal
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.BinomialThm
open import Cubical.Algebra.Ring.Properties
open import Cubical.Algebra.Ring.BigOps
open import Cubical.Algebra.RingSolver.ReflectionSolving

private
  variable
    ℓ : Level

module RadicalIdeal (R' : CommRing ℓ) where
 private R = fst R'
 open CommRingStr (snd R')
 open RingTheory (CommRing→Ring R')
 open Sum (CommRing→Ring R')
 open CommRingTheory R'
 open Exponentiation R'
 open BinomialThm R'
 open CommIdeal R'
 open isCommIdeal

 √ : CommIdeal → CommIdeal
 fst (√ I) x = (∃[ n ∈ ℕ ] x ^ n ∈ I) , isPropPropTrunc
 +Closed (snd (√ I)) {x = x} {y = y} = map2 +ClosedΣ
  where
  +ClosedΣ : Σ[ n ∈ ℕ ] x ^ n ∈ I → Σ[ n ∈ ℕ ] y ^ n ∈ I → Σ[ n ∈ ℕ ] (x + y) ^ n ∈ I
  +ClosedΣ (n , xⁿ∈I) (m , yᵐ∈I) = (n +ℕ m)
                                  , subst-∈ I (sym (BinomialThm (n +ℕ m) _ _)) ∑Binomial∈I
   where
   binomialCoeff∈I : ∀ i → ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ (n +ℕ m ∸ toℕ i) ∈ I
   binomialCoeff∈I i with ≤-+-split n m (toℕ i) (pred-≤-pred (toℕ<n i))
   ... | inl n≤i = subst-∈ I (sym path) (·Closed (I .snd) _ xⁿ∈I)
    where
    useSolver : ∀ a b c d → a · (b · c) · d ≡ a · b · d · c
    useSolver = solve R'
    path : ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ (n +ℕ m ∸ toℕ i)
         ≡ ((n +ℕ m) choose toℕ i) · x ^ (toℕ i ∸ n) · y ^ (n +ℕ m ∸ toℕ i) · x ^ n
    path = ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ (n +ℕ m ∸ toℕ i)
         ≡⟨ cong (λ k → ((n +ℕ m) choose toℕ i) · x ^ k · y ^ (n +ℕ m ∸ toℕ i))
                 (sym (≤-∸-+-cancel n≤i)) ⟩
           ((n +ℕ m) choose toℕ i) · x ^ ((toℕ i ∸ n) +ℕ n) · y ^ (n +ℕ m ∸ toℕ i)
         ≡⟨ cong (λ z → ((n +ℕ m) choose toℕ i) · z · y ^ (n +ℕ m ∸ toℕ i))
                 (sym (·-of-^-is-^-of-+ x (toℕ i ∸ n) n)) ⟩
           ((n +ℕ m) choose toℕ i) · (x ^ (toℕ i ∸ n) · x ^ n) · y ^ (n +ℕ m ∸ toℕ i)
         ≡⟨ useSolver _ _ _ _ ⟩
           ((n +ℕ m) choose toℕ i) · x ^ (toℕ i ∸ n) · y ^ (n +ℕ m ∸ toℕ i) · x ^ n ∎

   ... | inr m≤n+m-i = subst-∈ I (sym path) (·Closed (I .snd) _ yᵐ∈I)
    where
    path : ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ (n +ℕ m ∸ toℕ i)
         ≡ ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ ((n +ℕ m ∸ toℕ i) ∸ m) · y ^ m
    path = ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ (n +ℕ m ∸ toℕ i)
         ≡⟨ cong (λ k → ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ k)
                 (sym (≤-∸-+-cancel m≤n+m-i)) ⟩
           ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ (((n +ℕ m ∸ toℕ i) ∸ m) +ℕ m)
         ≡⟨ cong (((n +ℕ m) choose toℕ i) · x ^ toℕ i ·_)
                 (sym (·-of-^-is-^-of-+ y ((n +ℕ m ∸ toℕ i) ∸ m) m)) ⟩
           ((n +ℕ m) choose toℕ i) · x ^ toℕ i · (y ^ ((n +ℕ m ∸ toℕ i) ∸ m) · y ^ m)
         ≡⟨ ·Assoc _ _ _ ⟩
           ((n +ℕ m) choose toℕ i) · x ^ toℕ i · y ^ ((n +ℕ m ∸ toℕ i) ∸ m) · y ^ m ∎

   ∑Binomial∈I : ∑ (BinomialVec (n +ℕ m) x y) ∈ I
   ∑Binomial∈I = ∑Closed I (BinomialVec (n +ℕ m) _ _) binomialCoeff∈I
 contains0 (snd (√ I)) =
   ∣ 1 , subst-∈ I (sym (0LeftAnnihilates 1r)) ((I .snd) .contains0) ∣
 ·Closed (snd (√ I)) r =
   map λ { (n , xⁿ∈I) → n , subst-∈ I (sym (^-ldist-· r _ n)) ((I .snd) .·Closed (r ^ n) xⁿ∈I) }

 ^∈√→∈√ : ∀ (I : CommIdeal) (x : R) (n : ℕ) → x ^ n ∈ √ I → x ∈ √ I
 ^∈√→∈√ I x n =
         map (λ { (m , [xⁿ]ᵐ∈I) → (n ·ℕ m) , subst-∈ I (sym (^-rdist-·ℕ x n m)) [xⁿ]ᵐ∈I })

 ∈→∈√ : ∀ (I : CommIdeal) (x : R) → x ∈ I → x ∈ √ I
 ∈→∈√ I _ x∈I = ∣ 1 , subst-∈ I (sym (·Rid _)) x∈I ∣

 -- important lemma for characterization of the Zariski lattice
 open KroneckerDelta (CommRing→Ring R')
 √FGIdealCharLImpl : {n : ℕ} (V : FinVec R n) (I : CommIdeal)
         → √ ⟨ V ⟩[ R' ] ⊆ √ I → (∀ i → V i ∈ √ I)
 √FGIdealCharLImpl V I √⟨V⟩⊆√I i = √⟨V⟩⊆√I _ (∈→∈√ ⟨ V ⟩[ R' ] (V i)
                                       ∣ (λ j → δ i j) , sym (∑Mul1r _ _ i) ∣)

 √FGIdealCharRImpl : {n : ℕ} (V : FinVec R n) (I : CommIdeal)
         → (∀ i → V i ∈ √ I) → √ ⟨ V ⟩[ R' ] ⊆ √ I
 √FGIdealCharRImpl V I ∀i→Vi∈√I x = PT.elim (λ _ → √ I .fst x .snd)
                               λ { (n , xⁿ∈⟨V⟩) → ^∈√→∈√ I x n (elimHelper _ xⁿ∈⟨V⟩) }
  where
  elimHelper : ∀ (y : R) → y ∈ ⟨ V ⟩[ R' ] → y ∈ √ I
  elimHelper y = PT.elim (λ _ → √ I .fst y .snd)
                  λ { (α , y≡∑αV) → subst-∈ (√ I) (sym y≡∑αV)
                                          (∑Closed (√ I)
                                          (λ i → α i · V i)
                                          (λ i → √ I .snd .·Closed (α i) (∀i→Vi∈√I i))) }

 √FGIdealChar : {n : ℕ} (V : FinVec R n) (I : CommIdeal)
                → √ ⟨ V ⟩[ R' ] ⊆ √ I ≃ (∀ i → V i ∈ √ I)
 √FGIdealChar V I = propBiimpl→Equiv (⊆-isProp (√ ⟨ V ⟩[ R' ] .fst) (√ I .fst))
                                     (isPropΠ (λ _ → √ I .fst _ .snd))
                                     (√FGIdealCharLImpl V I)
                                     (√FGIdealCharRImpl V I)

 √+RContrLIncl : (I J : CommIdeal) → √ (I +i √ J) ⊆ √ (I +i J)
 √+RContrLIncl I J x = PT.elim (λ _ → isPropPropTrunc)
             (uncurry (λ n → PT.elim (λ _ → isPropPropTrunc)
               (uncurry3 (curriedIncl1 n))))
  where
  curriedIncl1 : (n : ℕ) (y : R × R)
               → (y .fst ∈ I)
               → (y . snd ∈ √ J)
               → (x ^ n ≡ y .fst + y .snd)
               → x ∈ √ (I +i J)
  curriedIncl1 n (y , z) y∈I = PT.elim (λ _ → isPropΠ λ _ → isPropPropTrunc) Σhelper
   where
   yVec : (m : ℕ) → FinVec R m
   yVec m = (BinomialVec m y z) ∘ suc

   ∑yVec∈I : ∀ m → ∑ (yVec m) ∈ I
   ∑yVec∈I zero = I .snd .contains0
   ∑yVec∈I (suc m) = ∑Closed I (yVec (suc m))
                        λ _ → subst-∈ I (useSolver _ _ _ _) (I .snd .·Closed _ y∈I)
    where
    useSolver : (bc y y^i z^m-i : R) → (bc · y^i · z^m-i) · y ≡ bc · (y · y^i) · z^m-i
    useSolver = solve R'

   path : (m : ℕ) → x ^ n ≡ y + z → x ^ (n ·ℕ m) ≡ ∑ (yVec m) + z ^ m
   path m p = x ^ (n ·ℕ m) ≡⟨ ^-rdist-·ℕ x n m ⟩
              (x ^ n) ^ m ≡⟨ cong (_^ m) p ⟩
              (y + z) ^ m ≡⟨ BinomialThm m y z ⟩
              ∑ (BinomialVec m y z) ≡⟨ useSolver _ _ ⟩
              ∑ (yVec m) + z ^ m ∎
    where
    useSolver : (zm ∑yVec : R) → 1r · 1r · zm + ∑yVec ≡ ∑yVec + zm
    useSolver = solve R'

   Σhelper : Σ[ m ∈ ℕ ] (z ^ m ∈ J) → x ^ n ≡ y + z → x ∈ √ (I +i J)
   Σhelper (m , z^m∈J) x^n≡y+z =
     ∣ n ·ℕ m , ∣ (∑ (yVec m) , z ^ m) , ∑yVec∈I m  , z^m∈J , path m x^n≡y+z ∣ ∣

 √+RContrRIncl : (I J : CommIdeal) → √ (I +i J) ⊆ √ (I +i √ J)
 √+RContrRIncl I J x = PT.elim (λ _ → isPropPropTrunc) (uncurry curriedIncl2)
  where
  curriedIncl2 : (n : ℕ) → (x ^ n ∈ (I +i J)) → x ∈ √ ((I +i √ J))
  curriedIncl2 n = map λ ((y , z) , y∈I , z∈J , x≡y+z)
                          → n , ∣ (y , z) , y∈I , ∈→∈√ J z z∈J , x≡y+z ∣

 √+RContr : (I J : CommIdeal) → √ (I +i √ J) ≡ √ (I +i J)
 √+RContr I J = CommIdeal≡Char (√+RContrLIncl I J) (√+RContrRIncl I J)

 √+LContr : (I J : CommIdeal) → √ (√ I +i J) ≡ √ (I +i J)
 √+LContr I J = cong √ (+iComm (√ I) J) ∙∙ √+RContr J I ∙∙ cong √ (+iComm J I)

 √·RContrLIncl : (I J : CommIdeal) → √ (I ·i √ J) ⊆ √ (I ·i J)
 √·RContrLIncl I J x = PT.elim (λ _ → isPropPropTrunc)
             (uncurry (λ n → PT.elim (λ _ → isPropPropTrunc)
               (uncurry4 (curriedIncl1 n))))
  where
  curriedIncl1 : (n m : ℕ) (α : FinVec R m × FinVec R m)
               → (∀ i → α .fst i ∈ I)
               → (∀ i → α .snd i ∈ √ J)
               → (x ^ n ≡ linearCombination R' (α .fst) (α .snd))
               → x ∈ √ (I ·i J)
  curriedIncl1 n m (α , β) α∈I β∈√J xⁿ≡∑αβ = ^∈√→∈√ (I ·i J) x n
   (subst-∈ (√ (I ·i J)) (sym xⁿ≡∑αβ)
   (∑Closed (√ (I ·i J)) (λ i → α i · β i) λ i → prodHelper i (β∈√J i)))
   where
   curriedHelper : ∀ x y → x ∈ I → ∀ l → y ^ l ∈ J → (x · y) ∈ √ (I ·i J)
   curriedHelper x y x∈I zero 1∈J = subst (λ K → (x · y) ∈ √ K)
                                      (sym (·iRContains1id I J 1∈J)) --1∈J → √J ≡ √ ⊃ I
                                      (∈→∈√ I _ (·RClosed (I .snd) y x∈I))
   curriedHelper x y x∈I (suc l) y^l+1∈J = -- (xy)^l+1 ≡ x^l · x (∈I) · y^l+1 (∈J)
     ∣ suc l , subst-∈ (I ·i J) (sym (^-ldist-· _ _ (suc l)))
     (prodInProd I J _ _ (subst-∈ I (·-comm _ _) (I .snd .·Closed (x ^ l) x∈I)) y^l+1∈J) ∣

   prodHelper : ∀ i → β i ∈ √ J → α i · β i ∈ √ (I ·i J)
   prodHelper i = PT.elim (λ _ → isPropPropTrunc) (uncurry (curriedHelper (α i) (β i) (α∈I i)))

 √·RContrRIncl : (I J : CommIdeal) → √ (I ·i J) ⊆ √ (I ·i √ J)
 √·RContrRIncl I J x =  PT.elim (λ _ → isPropPropTrunc) (uncurry curriedIncl2)
  where
  curriedIncl2 : (n : ℕ) → x ^ n ∈ (I ·i J) → x ∈ √ (I ·i √ J)
  curriedIncl2 n = map λ (m , (α , β) , α∈I , β∈J , xⁿ≡∑αβ)
                   → n , ∣ m , (α , β) , α∈I , (λ i → ∈→∈√ J (β i) (β∈J i)) , xⁿ≡∑αβ ∣

 √·RContr : (I J : CommIdeal) → √ (I ·i √ J) ≡ √ (I ·i J)
 √·RContr I J = CommIdeal≡Char (√·RContrLIncl I J) (√·RContrRIncl I J)

 √·LContr : (I J : CommIdeal) → √ (√ I ·i J) ≡ √ (I ·i J)
 √·LContr I J = cong √ (·iComm (√ I) J) ∙∙ √·RContr J I ∙∙ cong √ (·iComm J I)

 √·IdemLIncl : ∀ (I : CommIdeal) → √ (I ·i I) ⊆ √ I
 √·IdemLIncl I x = map λ (n , x^n∈II) → (n , ·iLincl I I _ x^n∈II)

 √·IdemRIncl : ∀ (I : CommIdeal) → √ I ⊆ √ (I ·i I)
 √·IdemRIncl I x = map λ (n , x^n∈I) → (n +ℕ n , subst-∈ (I ·i I)
                                (·-of-^-is-^-of-+ x n n) -- x²ⁿ≡xⁿ (∈I) · xⁿ (∈I)
                                (prodInProd I I _ _ x^n∈I x^n∈I))

 √·Idem : ∀ (I : CommIdeal) → √ (I ·i I) ≡ √ I
 √·Idem I = CommIdeal≡Char (√·IdemLIncl I) (√·IdemRIncl I)

 √·Absorb+LIncl : ∀ (I J : CommIdeal) → √ (I ·i (I +i J)) ⊆ √ I
 √·Absorb+LIncl I J x = map λ (n , x^n∈I[I+J]) → (n , ·iLincl I (I +i J) _ x^n∈I[I+J])

 √·Absorb+RIncl : ∀ (I J : CommIdeal) → √ I ⊆ √ (I ·i (I +i J))
 √·Absorb+RIncl I J x = map λ (n , x^n∈I) → (n +ℕ n , subst-∈ (I ·i (I +i J))
                                (·-of-^-is-^-of-+ x n n) -- x²ⁿ≡xⁿ (∈I) · xⁿ (∈I⊆I+J)
                                (prodInProd I (I +i J) _ _ x^n∈I (+iLincl I J _ x^n∈I)))

 √·Absorb+ : ∀ (I J : CommIdeal) → √ (I ·i (I +i J)) ≡ √ I
 √·Absorb+ I J = CommIdeal≡Char (√·Absorb+LIncl I J) (√·Absorb+RIncl I J)

max_stars_repo_name: dolio/cubical

max_issues_repo_name: dolio/cubical

max_forks_repo_name: dolio/cubical


text:
module sum-thms where

open import eq
open import sum
open import list
open import product
open import negation

inj₁-inj : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'}{x : A}{x'} → inj₁{ℓ}{ℓ'}{A}{B} x ≡ inj₁ x' → x ≡ x'
inj₁-inj refl = refl

¬∨ : ∀ {A B : Set} → ¬ A ∧ ¬ B → ¬ (A ∨ B)
¬∨ (u , u') (inj₁ x) = u x
¬∨ (u , u') (inj₂ y) = u' y

¬Σ : ∀{A : Set}{B : A → Set} → (∀(x : A) → ¬ B x) → ¬ Σ A B
¬Σ p (a , b) = p a b

¬∧1 : ∀ {A B : Set} → ¬ A → ¬ (A ∧ B)
¬∧1 f (a , b) = f a

¬∧2 : ∀ {A B : Set} → ¬ B → ¬ (A ∧ B)
¬∧2 f (a , b) = f b

¬∀ : ∀{A : Set}{B : A → Set} → Σ A (λ x → ¬ B x) → ¬ ∀(x : A) → B x
¬∀ (a , b) f = b (f a)

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial