text:
module BBHeap.Properties {A : Set}(_≤_ : A → A → Set) where

open import BBHeap _≤_
open import BBHeap.Perfect _≤_
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Data.Empty

sym≃ : {b b' : Bound}{h : BBHeap b}{h' : BBHeap b'} → h ≃ h' → h' ≃ h
sym≃ ≃lf = ≃lf
sym≃ (≃nd b≤x b'≤x' l⋘r l'⋘r' l≃r l'≃r' l≃l') = ≃nd b'≤x' b≤x l'⋘r' l⋘r l'≃r' l≃r (sym≃ l≃l')

trans≃ : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}{h'' : BBHeap b''} → h ≃ h' → h' ≃ h'' → h ≃ h''
trans≃ ≃lf ≃lf = ≃lf
trans≃ (≃nd b≤x b'≤x' l⋘r l'⋘r' l≃r _ l≃l') (≃nd .b'≤x' b''≤x'' .l'⋘r' l''⋘r'' _ l''≃r'' l'≃l'') = ≃nd b≤x b''≤x'' l⋘r l''⋘r'' l≃r l''≃r'' (trans≃ l≃l' l'≃l'')

lemma≃ : {b b' : Bound}{h : BBHeap b}{h' : BBHeap b'} → h ≃ h' → h ⋘ h'
lemma≃ ≃lf = lf⋘
lemma≃ (≃nd b≤x b'≤x' l⋘r l'⋘r' l≃r l'≃r' l≃l') = ll⋘ b≤x b'≤x' l⋘r l'⋘r' l'≃r' (trans≃ (sym≃ l≃r) l≃l')

lemma⋗≃ : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}{h'' : BBHeap b''} → h ⋗ h' → h' ≃ h'' → h ⋗ h''
lemma⋗≃ (⋗lf b≤x) ≃lf = ⋗lf b≤x
lemma⋗≃ (⋗nd b≤x b'≤x' l⋘r l'⋘r' l≃r _ l⋗l') (≃nd .b'≤x' b''≤x'' .l'⋘r' l''⋘r'' _ l''≃r'' l'≃l'') = ⋗nd b≤x b''≤x'' l⋘r l''⋘r'' l≃r l''≃r'' (lemma⋗≃ l⋗l' l'≃l'')

lemma⋗ : {b b' : Bound}{h : BBHeap b}{h' : BBHeap b'} → h ⋗ h'  → h ⋙ h'
lemma⋗ (⋗lf b≤x) = ⋙lf b≤x
lemma⋗ (⋗nd b≤x b'≤x' l⋘r l'⋘r' l≃r l'≃r' l⋗l') = ⋙rl b≤x b'≤x' l⋘r l≃r l'⋘r' (lemma⋗≃ l⋗l' l'≃r')

lemma⋗⋗ : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}{h'' : BBHeap b''} → h ⋗ h' → h'' ⋗ h'  → h ≃ h''
lemma⋗⋗ (⋗lf b≤x) (⋗lf b''≤x'') = ≃nd b≤x b''≤x'' lf⋘ lf⋘ ≃lf ≃lf ≃lf
lemma⋗⋗ (⋗nd b≤x b'≤x' l⋘r l'⋘r' l≃r _ l⋗l') (⋗nd b''≤x'' .b'≤x' l''⋘r'' .l'⋘r' l''≃r'' _ l''⋗l') = ≃nd b≤x b''≤x'' l⋘r l''⋘r'' l≃r l''≃r'' (lemma⋗⋗ l⋗l' l''⋗l')

lemma⋗⋗' : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}{h'' : BBHeap b''} → h ⋗ h' → h ⋗ h''  → h' ≃ h''
lemma⋗⋗' (⋗lf b≤x) (⋗nd .b≤x _ .lf⋘ _ _ _ ())
lemma⋗⋗' (⋗nd .b≤x _ .lf⋘ _ _ _ ()) (⋗lf b≤x)
lemma⋗⋗' (⋗lf b≤x) (⋗lf .b≤x) = ≃lf
lemma⋗⋗' (⋗nd b≤x b'≤x' l⋘r l'⋘r' _ l'≃r' l⋗l') (⋗nd .b≤x b''≤x'' .l⋘r l''⋘r'' _ l''≃r'' l⋗l'') = ≃nd b'≤x' b''≤x'' l'⋘r' l''⋘r'' l'≃r' l''≃r'' (lemma⋗⋗' l⋗l' l⋗l'')

lemma≃⋗ : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}{h'' : BBHeap b''} → h ≃ h' → h' ⋗ h'' → h ⋗ h''
lemma≃⋗ (≃nd b≤x b'≤x' l⋘r l'⋘r' l≃r _ l≃l') (⋗nd .b'≤x' b''≤x'' .l'⋘r' l''⋘r'' _ l''≃r'' l'⋗l'') = ⋗nd b≤x b''≤x'' l⋘r l''⋘r'' l≃r l''≃r'' (lemma≃⋗ l≃l' l'⋗l'')
lemma≃⋗ (≃nd b≤x b'≤x' lf⋘ lf⋘ ≃lf ≃lf ≃lf) (⋗lf .b'≤x') = ⋗lf b≤x

lemma-⋘-≃ : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}{h'' : BBHeap b''} → h ⋘ h' → h' ≃ h'' → h ⋘ h''
lemma-⋘-≃ lf⋘ ≃lf = lf⋘
lemma-⋘-≃ (ll⋘ b≤x b'≤x' l⋘r l'⋘r' _ r≃l') (≃nd .b'≤x' b''≤x'' .l'⋘r' l''⋘r'' _ l''≃r'' l'≃l'') = ll⋘ b≤x b''≤x'' l⋘r l''⋘r'' l''≃r'' (trans≃ r≃l' l'≃l'')
lemma-⋘-≃ (lr⋘ b≤x b'≤x' l⋙r l'⋘r' _ l⋗l') (≃nd .b'≤x' b''≤x'' .l'⋘r' l''⋘r'' _ l''≃r'' l'≃l'') = lr⋘ b≤x b''≤x'' l⋙r l''⋘r'' l''≃r'' (lemma⋗≃ l⋗l' l'≃l'')

lemma-≃-⋙ : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}{h'' : BBHeap b''} → h ≃ h' → h' ⋙ h'' → h ⋙ h''
lemma-≃-⋙ (≃nd b≤x b'≤x' lf⋘ lf⋘ ≃lf ≃lf ≃lf) (⋙lf .b'≤x') = ⋙lf b≤x
lemma-≃-⋙ (≃nd b≤x b'≤x' l⋘r l'⋘r' l≃r _ l≃l') (⋙rl .b'≤x' b''≤x'' .l'⋘r' _ l''⋘r'' l'⋗r'') = ⋙rl b≤x b''≤x'' l⋘r l≃r l''⋘r'' (lemma≃⋗ l≃l' l'⋗r'')
lemma-≃-⋙ (≃nd b≤x b'≤x' l⋘r l'⋘r' l≃r _ l≃l') (⋙rr .b'≤x' b''≤x'' .l'⋘r' _ l''⋙r'' l'≃l'') = ⋙rr b≤x b''≤x'' l⋘r l≃r l''⋙r'' (trans≃ l≃l' l'≃l'')

lemma-⋘-⋗ : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}{h'' : BBHeap b''} → h ⋘ h' → h'' ⋗ h' → h'' ⋙ h
lemma-⋘-⋗ lf⋘ (⋗lf b≤x) = ⋙lf b≤x
lemma-⋘-⋗ (ll⋘ b≤x b'≤x' l⋘r l'⋘r' _ r≃l') (⋗nd b''≤x'' .b'≤x' l''⋘r'' .l'⋘r' l''≃r'' _ l''⋗l') = ⋙rl b''≤x'' b≤x l''⋘r'' l''≃r'' l⋘r (lemma⋗≃ l''⋗l' (sym≃ r≃l'))
lemma-⋘-⋗ (lr⋘ b≤x b'≤x' l⋙r l'⋘r' _ l⋗l') (⋗nd b''≤x'' .b'≤x' l''⋘r'' .l'⋘r' l''≃r'' _ l''⋗l') = ⋙rr b''≤x'' b≤x l''⋘r'' l''≃r'' l⋙r (lemma⋗⋗ l''⋗l' l⋗l')

lemma-≃-⊥ : {b b' : Bound}{h : BBHeap b}{h' : BBHeap b'} → h ≃ h' → h ⋗ h' → ⊥
lemma-≃-⊥ () (⋗lf _)
lemma-≃-⊥ (≃nd .b≤x .b'≤x' .l⋘r .l'⋘r' _ _ l≃l') (⋗nd b≤x b'≤x' l⋘r l'⋘r' l≃r l'≃r' l⋗l')
    with lemma-≃-⊥ l≃l' l⋗l'
... | ()

lemma-⋘-⊥ : {b b' : Bound}{x x' : A}{l r : BBHeap (val x)}{l' r' : BBHeap (val x')}(b≤x : LeB b (val x))(b'≤x' : LeB b' (val x'))(l⋙r : l ⋙ r)(l'⋘r' : l' ⋘ r') → l ≃ l' → right b≤x l⋙r ⋘ left b'≤x' l'⋘r' → ⊥
lemma-⋘-⊥ b≤x b'≤x' l⋙r l'⋘r' l≃l' (lr⋘ .b≤x .b'≤x' .l⋙r .l'⋘r' _ l⋗l')
    with lemma-≃-⊥ l≃l' l⋗l'
... | ()

lemma-perfect : {b b' : Bound}{h : BBHeap b}{h' : BBHeap b'} → h ⋘ h' → Perfect h'
lemma-perfect lf⋘ = plf
lemma-perfect (ll⋘ b≤x b'≤x' l⋘l l'⋘l' l'≃r' r≃l') = pnd b'≤x' l'⋘l' l'≃r'
lemma-perfect (lr⋘ b≤x b'≤x' l⋙r l'⋘l' l'≃r' l⋗l') = pnd b'≤x' l'⋘l' l'≃r'

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module IncompletePatternMatching where

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

data True : Set where
  tt : True

data False : Set where

_==_ : Nat -> Nat -> Set
zero  == zero  = True
suc n == suc m = n == m

thm : zero == suc zero
thm = tt

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Idiom bracket notation.
module Syntax.Idiom where

import      Lvl
open import Type

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable A B : Type{ℓ}
private variable F : Type{ℓ₁} → Type{ℓ₂}

-- The notation `⦇ f x₁ x₂ x₃ ⦈` will automatically be translated to `((pure f <*> x₁) <*> x₂) <*> x₃`.
record IdiomBrackets (F : Type{ℓ₁} → Type{ℓ₂}) : Type{Lvl.𝐒(ℓ₁) Lvl.⊔ ℓ₂} where
  constructor intro
  field
    pure : (A → F(A))
    _<*>_ : F(A → B) → (F(A) → F(B))
open IdiomBrackets ⦃ … ⦄ using (pure ; _<*>_) public

-- The notation `⦇⦈` will automatically be translated to `empty`.
record IdiomBrackets₀ (F : Type{ℓ₁} → Type{ℓ₂}) : Type{Lvl.𝐒(ℓ₁) Lvl.⊔ ℓ₂} where
  constructor intro
  field
    empty : F(A)
open IdiomBrackets₀ ⦃ … ⦄ using (empty) public

-- The notation `⦇ f₁ x₁ x₂ x₃ | f₂ y₁ y₂ | f₃ z₁ ⦈` will automatically be translated to `(((pure f <*> x₁) <*> x₂) <*> x₃) <|> (((pure f₂ <*> y₁) <*> y₂) <|> (pure f₃ <*> z₁))`.
record IdiomBrackets₊ (F : Type{ℓ₁} → Type{ℓ₂}) ⦃ _ : IdiomBrackets(F) ⦄ : Type{Lvl.𝐒(ℓ₁) Lvl.⊔ ℓ₂} where
  constructor intro
  field
    _<|>_ : F(A) → F(A) → F(A)
open IdiomBrackets₊ ⦃ … ⦄ using (_<|>_) public

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module exchange where
  -- exchanging just two disequal elements produces the same context
  swap-little : {A : Set} {x y : Nat} {τ1 τ2 : A} → (x ≠ y) →
    ((■ (x , τ1)) ,, (y , τ2)) == ((■ (y , τ2)) ,, (x , τ1))
  swap-little {A} {x} {y} {τ1} {τ2} neq = ∪comm (■ (y , τ2))
                                                (■ (x , τ1))
                                                (disjoint-singles (flip neq))

  -- really the dynamics-core of all the exchange arguments: contexts with two
  -- disequal elements exchanged are the same. we reassociate the unions,
  -- swap as above, and then associate them back.
  --
  -- note that this is generic in the contents of the context. the proofs
  -- below show the exchange properties that we actually need in the
  -- various other proofs; the remaning exchange properties for both Δ and
  -- Γ positions for all the other hypothetical judgements are exactly in
  -- this pattern.
  swap : {A : Set} {x y : Nat} {τ1 τ2 : A} (Γ : A ctx) (x≠y : x == y → ⊥) →
         ((Γ ,, (x , τ1)) ,, (y , τ2)) == ((Γ ,, (y , τ2)) ,, (x , τ1))
  swap {A} {x} {y} {τ1} {τ2} Γ neq = funext eq
    where
      eq : (z : Nat) →  ((Γ ,, (x , τ1)) ,, (y , τ2)) z == ((Γ ,, (y , τ2)) ,, (x , τ1)) z
      eq z with natEQ y z
      ... | Inr y≠z with natEQ x z
      ... | Inl refl = refl
      ... | Inr x≠z with natEQ y z
      ... | Inl refl = abort (y≠z refl)
      ... | Inr y≠z' = refl
      eq z | Inl refl with natEQ x z
      ... | Inl refl = abort (neq refl)
      ... | Inr x≠z with natEQ z z
      ... | Inl refl = refl
      ... | Inr z≠z = abort (z≠z refl)

  -- (∪assoc Γ (■ (x , τ1)) (■ (y , τ2)) (disjoint-singles neq)) ·
  --                       (ap1 (λ qq → Γ ∪ qq) (swap-little neq) ·
  -- the above exchange principle used via transport in the judgements we needed
  exchange-subst-Γ : ∀{Δ Γ x y τ1 τ2 σ Γ'} →
                   x ≠ y →
                   Δ , (Γ ,, (x , τ1) ,, (y , τ2)) ⊢ σ :s: Γ' →
                   Δ , (Γ ,, (y , τ2) ,, (x , τ1)) ⊢ σ :s: Γ'
  exchange-subst-Γ {Δ} {Γ} {x} {y} {τ1} {τ2} {σ} {Γ'} x≠y =
    tr (λ qq → Δ , qq ⊢ σ :s: Γ') (swap Γ x≠y)

  exchange-synth : ∀{Γ x y τ τ1 τ2 e}
                       → x ≠ y
                       → (Γ ,, (x , τ1) ,, (y , τ2)) ⊢ e => τ
                       → (Γ ,, (y , τ2) ,, (x , τ1)) ⊢ e => τ
  exchange-synth {Γ} {x} {y} {τ} {τ1} {τ2} {e} neq  =
    tr (λ qq → qq ⊢ e => τ) (swap Γ neq)

  exchange-ana : ∀{Γ x y τ τ1 τ2 e}
                       → x ≠ y
                       → (Γ ,, (x , τ1) ,, (y , τ2)) ⊢ e <= τ
                       → (Γ ,, (y , τ2) ,, (x , τ1)) ⊢ e <= τ
  exchange-ana {Γ} {x} {y} {τ} {τ1} {τ2} {e} neq  =
    tr (λ qq → qq ⊢ e <= τ) (swap Γ neq)

  exchange-elab-synth : ∀{Γ x y τ1 τ2 e τ d Δ} →
                        x ≠ y →
                        (Γ ,, (x , τ1) ,, (y , τ2)) ⊢ e ⇒ τ ~> d ⊣ Δ →
                        (Γ ,, (y , τ2) ,, (x , τ1)) ⊢ e ⇒ τ ~> d ⊣ Δ
  exchange-elab-synth {Γ = Γ} {e = e} {τ = τ} {d = d } {Δ = Δ} neq =
    tr (λ qq → qq ⊢ e ⇒ τ ~> d ⊣ Δ) (swap Γ neq)

  exchange-elab-ana : ∀ {Γ x y τ1 τ2 τ τ' d e Δ} →
                      x ≠ y →
                      (Γ ,, (x , τ1) ,, (y , τ2)) ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
                      (Γ ,, (y , τ2) ,, (x , τ1)) ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ
  exchange-elab-ana {Γ = Γ} {τ = τ} {τ' = τ'} {d = d} {e = e} {Δ = Δ} neq =
    tr (λ qq → qq ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ) (swap Γ neq)

  exchange-ta-Γ : ∀{Γ x y τ1 τ2 d τ Δ } →
                  x ≠ y →
                  Δ , (Γ ,, (x , τ1) ,, (y , τ2)) ⊢ d :: τ →
                  Δ , (Γ ,, (y , τ2) ,, (x , τ1)) ⊢ d :: τ
  exchange-ta-Γ {Γ = Γ} {d = d} {τ = τ} {Δ = Δ} neq =
    tr (λ qq → Δ , qq ⊢ d :: τ) (swap Γ neq)

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
{-# OPTIONS --safe #-}
module Cubical.Relation.Nullary where

open import Cubical.Relation.Nullary.Base public
open import Cubical.Relation.Nullary.Properties public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
-- Andreas, 2018-10-16, erased lambda-arguments

open import Agda.Builtin.List
open import Common.Prelude

sum : List Nat → Nat
sum (x ∷ xs) = x + sum xs
sum [] = 0

zipWith : {A B C : Set} (f : A → B → C) → List A → List B → List C
zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys
zipWith _ _ _ = []

-- Shorten the first list to the length of the second.

restrict : {A : Set} (xs ys : List A) → List A
restrict = zipWith (λ x (@0 _) → x)

-- It does not matter that we annotated the second argument as erased,
-- since the compiler does not actually erase function arguments, only
-- their content to the empty tuple.  Thus, this is no type error.

main : IO Unit
main = printNat (sum (restrict (13 ∷ 14 ∷ 15 ∷ 16 ∷ []) (1 ∷ 2 ∷ 3 ∷ [])))

-- Expected output: 42

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2014-09-23

syntax bla (λ x → e) = blub e

-- Should trigger error:
-- malformed syntax declaration: syntax must use binding holes exactly once


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some unit types
------------------------------------------------------------------------

-- The definitions in this file are reexported by Data.Unit.

module Data.Unit.Core where

open import Level

------------------------------------------------------------------------
-- A unit type defined as a data-type

-- The ⊤ type (see Data.Unit) comes with η-equality, which is often
-- nice to have, but sometimes it is convenient to be able to stop
-- unfolding (see "Hidden types" below).

data Unit : Set where
  unit : Unit

------------------------------------------------------------------------
-- Hidden types

-- "Hidden" values.

Hidden : ∀ {a} → Set a → Set a
Hidden A = Unit → A

-- The hide function can be used to hide function applications. Note
-- that the type-checker doesn't see that "hide f x" contains the
-- application "f x".

hide : ∀ {a b} {A : Set a} {B : A → Set b} →
       ((x : A) → B x) → ((x : A) → Hidden (B x))
hide f x unit = f x

-- Reveals a hidden value.

reveal : ∀ {a} {A : Set a} → Hidden A → A
reveal f = f unit


text:
{-# OPTIONS --warning=error #-}

module UselessAbstractPrimitive where

postulate Int : Set

{-# BUILTIN INTEGER Int #-}

abstract
  primitive
    primIntegerPlus : Int -> Int -> Int


text:
------------------------------------------------------------------------------
-- Distributive laws properties
------------------------------------------------------------------------------

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

module DistributiveLaws.PropertiesI where

open import DistributiveLaws.Base

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

-- The propositional equality is compatible with the binary operation.

·-leftCong : ∀ {a b c} → a ≡ b → a · c ≡ b · c
·-leftCong refl = refl

·-rightCong : ∀ {a b c} → b ≡ c → a · b ≡ a · c
·-rightCong refl = refl

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Data.Vec.All.Properties.Extra {a p}{A : Set a}{P : A → Set p} where

open import Data.List using (List)
import Data.List.Relation.Unary.All as All
open import Data.Vec hiding (_[_]≔_)
open import Data.Vec.Relation.Unary.All hiding (lookup)
open import Data.Fin

all-fromList : ∀ {xs : List A} → All.All P xs → All P (fromList xs)
all-fromList All.[] = []
all-fromList (px All.∷ p) = px ∷ all-fromList p

_[_]≔_ : ∀ {n}{l : Vec A n} → All P l → (i : Fin n) → P (lookup l i)→ All P l
[] [ () ]≔ px
(px ∷ l) [ zero ]≔ px₁ = px₁ ∷ l
(px ∷ l) [ suc i ]≔ px₁ = px ∷ (l [ i ]≔ px₁)


text:
open import Relation.Unary using ( ∅ ; _∪_ )
open import Web.Semantic.DL.Concept using ( Concept )
open import Web.Semantic.DL.Role using ( Role )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.Util using ( Subset ; ⁅_⁆ )

module Web.Semantic.DL.TBox where

infixl 5 _⊑₁_ _⊑₂_
infixr 4 _,_

{- a Terminology Box on a Signature (Concept and Role Names)
  is constructed by specifying
   - ε the empty TBox
   - Combination of TBoxes (_,_) - ie. a Union
   - subsumption relations ⊑ between roles and between concepts
   - properties of Roles (Reflexivity, Irreflexivity, Transitivity)
   - disjointness relation between Roles -}
data TBox (Σ : Signature) : Set where
  ε : TBox Σ
  _,_ : (T U : TBox Σ) → TBox Σ
  _⊑₁_ : (C D : Concept Σ) → TBox Σ
  _⊑₂_ : (Q R : Role Σ) → TBox Σ
  Ref : (R : Role Σ) → TBox Σ
  Irr : (R : Role Σ) → TBox Σ
  Tra : (R : Role Σ) → TBox Σ
  Dis : (Q R : Role Σ) → TBox Σ

Axioms : ∀ {Σ} → TBox Σ → Subset (TBox Σ)
Axioms ε         = ∅
Axioms (T , U)   = (Axioms T) ∪ (Axioms U)
Axioms (C ⊑₁ D)  = ⁅ C ⊑₁ D ⁆
Axioms (Q ⊑₂ R)  = ⁅ Q ⊑₂ R ⁆
Axioms (Ref R)   = ⁅ Ref R ⁆
Axioms (Irr R)   = ⁅ Irr R ⁆
Axioms (Tra R)   = ⁅ Tra R ⁆
Axioms (Dis Q R) = ⁅ Dis Q R ⁆

max_stars_repo_name: bblfish/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
----------------------------------------------------------------------------------
-- Types for parse trees
----------------------------------------------------------------------------------

module cws-types where

open import lib
open import parse-tree

posinfo = string

{-# FOREIGN GHC import qualified CedilleCommentsLexer #-}

data entity : Set where
    EntityComment : posinfo → posinfo → entity
    EntityNonws : entity
    EntityWs : posinfo → posinfo → entity
{-# COMPILE GHC entity = data CedilleCommentsLexer.Entity (CedilleCommentsLexer.EntityComment | CedilleCommentsLexer.EntityNonws | CedilleCommentsLexer.EntityWs) #-}

data entities : Set where
    EndEntity : entities
    Entity : entity → entities → entities
{-# COMPILE GHC entities = data CedilleCommentsLexer.Entities (CedilleCommentsLexer.EndEntity | CedilleCommentsLexer.Entity) #-}

data start : Set where
    File : entities → start
{-# COMPILE GHC start = data CedilleCommentsLexer.Start (CedilleCommentsLexer.File) #-}

postulate
  scanComments  : string → start

{-# COMPILE GHC scanComments = CedilleCommentsLexer.scanComments #-}

-- embedded types:

data ParseTreeT : Set where
  parsed-entities : entities → ParseTreeT
  parsed-entity : entity → ParseTreeT
  parsed-start : start → ParseTreeT
  parsed-posinfo : posinfo → ParseTreeT
  parsed-alpha : ParseTreeT
  parsed-alpha-bar-3 : ParseTreeT
  parsed-alpha-range-1 : ParseTreeT
  parsed-alpha-range-2 : ParseTreeT
  parsed-anychar : ParseTreeT
  parsed-anychar-bar-59 : ParseTreeT
  parsed-anychar-bar-60 : ParseTreeT
  parsed-anychar-bar-61 : ParseTreeT
  parsed-anychar-bar-62 : ParseTreeT
  parsed-anychar-bar-63 : ParseTreeT
  parsed-anynonwschar : ParseTreeT
  parsed-anynonwschar-bar-68 : ParseTreeT
  parsed-anynonwschar-bar-69 : ParseTreeT
  parsed-aws : ParseTreeT
  parsed-aws-bar-65 : ParseTreeT
  parsed-aws-bar-66 : ParseTreeT
  parsed-comment : ParseTreeT
  parsed-comment-star-64 : ParseTreeT
  parsed-nonws : ParseTreeT
  parsed-nonws-plus-70 : ParseTreeT
  parsed-num : ParseTreeT
  parsed-num-plus-5 : ParseTreeT
  parsed-numone : ParseTreeT
  parsed-numone-range-4 : ParseTreeT
  parsed-numpunct : ParseTreeT
  parsed-numpunct-bar-10 : ParseTreeT
  parsed-numpunct-bar-11 : ParseTreeT
  parsed-numpunct-bar-6 : ParseTreeT
  parsed-numpunct-bar-7 : ParseTreeT
  parsed-numpunct-bar-8 : ParseTreeT
  parsed-numpunct-bar-9 : ParseTreeT
  parsed-otherpunct : ParseTreeT
  parsed-otherpunct-bar-12 : ParseTreeT
  parsed-otherpunct-bar-13 : ParseTreeT
  parsed-otherpunct-bar-14 : ParseTreeT
  parsed-otherpunct-bar-15 : ParseTreeT
  parsed-otherpunct-bar-16 : ParseTreeT
  parsed-otherpunct-bar-17 : ParseTreeT
  parsed-otherpunct-bar-18 : ParseTreeT
  parsed-otherpunct-bar-19 : ParseTreeT
  parsed-otherpunct-bar-20 : ParseTreeT
  parsed-otherpunct-bar-21 : ParseTreeT
  parsed-otherpunct-bar-22 : ParseTreeT
  parsed-otherpunct-bar-23 : ParseTreeT
  parsed-otherpunct-bar-24 : ParseTreeT
  parsed-otherpunct-bar-25 : ParseTreeT
  parsed-otherpunct-bar-26 : ParseTreeT
  parsed-otherpunct-bar-27 : ParseTreeT
  parsed-otherpunct-bar-28 : ParseTreeT
  parsed-otherpunct-bar-29 : ParseTreeT
  parsed-otherpunct-bar-30 : ParseTreeT
  parsed-otherpunct-bar-31 : ParseTreeT
  parsed-otherpunct-bar-32 : ParseTreeT
  parsed-otherpunct-bar-33 : ParseTreeT
  parsed-otherpunct-bar-34 : ParseTreeT
  parsed-otherpunct-bar-35 : ParseTreeT
  parsed-otherpunct-bar-36 : ParseTreeT
  parsed-otherpunct-bar-37 : ParseTreeT
  parsed-otherpunct-bar-38 : ParseTreeT
  parsed-otherpunct-bar-39 : ParseTreeT
  parsed-otherpunct-bar-40 : ParseTreeT
  parsed-otherpunct-bar-41 : ParseTreeT
  parsed-otherpunct-bar-42 : ParseTreeT
  parsed-otherpunct-bar-43 : ParseTreeT
  parsed-otherpunct-bar-44 : ParseTreeT
  parsed-otherpunct-bar-45 : ParseTreeT
  parsed-otherpunct-bar-46 : ParseTreeT
  parsed-otherpunct-bar-47 : ParseTreeT
  parsed-otherpunct-bar-48 : ParseTreeT
  parsed-otherpunct-bar-49 : ParseTreeT
  parsed-otherpunct-bar-50 : ParseTreeT
  parsed-otherpunct-bar-51 : ParseTreeT
  parsed-otherpunct-bar-52 : ParseTreeT
  parsed-otherpunct-bar-53 : ParseTreeT
  parsed-otherpunct-bar-54 : ParseTreeT
  parsed-otherpunct-bar-55 : ParseTreeT
  parsed-otherpunct-bar-56 : ParseTreeT
  parsed-otherpunct-bar-57 : ParseTreeT
  parsed-otherpunct-bar-58 : ParseTreeT
  parsed-ws : ParseTreeT
  parsed-ws-plus-67 : ParseTreeT

------------------------------------------
-- Parse tree printing functions
------------------------------------------

posinfoToString : posinfo → string
posinfoToString x = "(posinfo " ^ x ^ ")"

mutual
  entitiesToString : entities → string
  entitiesToString (EndEntity) = "EndEntity" ^ ""
  entitiesToString (Entity x0 x1) = "(Entity" ^ " " ^ (entityToString x0) ^ " " ^ (entitiesToString x1) ^ ")"

  entityToString : entity → string
  entityToString (EntityComment x0 x1) = "(EntityComment" ^ " " ^ (posinfoToString x0) ^ " " ^ (posinfoToString x1) ^ ")"
  entityToString (EntityNonws) = "EntityNonws" ^ ""
  entityToString (EntityWs x0 x1) = "(EntityWs" ^ " " ^ (posinfoToString x0) ^ " " ^ (posinfoToString x1) ^ ")"

  startToString : start → string
  startToString (File x0) = "(File" ^ " " ^ (entitiesToString x0) ^ ")"

ParseTreeToString : ParseTreeT → string
ParseTreeToString (parsed-entities t) = entitiesToString t
ParseTreeToString (parsed-entity t) = entityToString t
ParseTreeToString (parsed-start t) = startToString t
ParseTreeToString (parsed-posinfo t) = posinfoToString t
ParseTreeToString parsed-alpha = "[alpha]"
ParseTreeToString parsed-alpha-bar-3 = "[alpha-bar-3]"
ParseTreeToString parsed-alpha-range-1 = "[alpha-range-1]"
ParseTreeToString parsed-alpha-range-2 = "[alpha-range-2]"
ParseTreeToString parsed-anychar = "[anychar]"
ParseTreeToString parsed-anychar-bar-59 = "[anychar-bar-59]"
ParseTreeToString parsed-anychar-bar-60 = "[anychar-bar-60]"
ParseTreeToString parsed-anychar-bar-61 = "[anychar-bar-61]"
ParseTreeToString parsed-anychar-bar-62 = "[anychar-bar-62]"
ParseTreeToString parsed-anychar-bar-63 = "[anychar-bar-63]"
ParseTreeToString parsed-anynonwschar = "[anynonwschar]"
ParseTreeToString parsed-anynonwschar-bar-68 = "[anynonwschar-bar-68]"
ParseTreeToString parsed-anynonwschar-bar-69 = "[anynonwschar-bar-69]"
ParseTreeToString parsed-aws = "[aws]"
ParseTreeToString parsed-aws-bar-65 = "[aws-bar-65]"
ParseTreeToString parsed-aws-bar-66 = "[aws-bar-66]"
ParseTreeToString parsed-comment = "[comment]"
ParseTreeToString parsed-comment-star-64 = "[comment-star-64]"
ParseTreeToString parsed-nonws = "[nonws]"
ParseTreeToString parsed-nonws-plus-70 = "[nonws-plus-70]"
ParseTreeToString parsed-num = "[num]"
ParseTreeToString parsed-num-plus-5 = "[num-plus-5]"
ParseTreeToString parsed-numone = "[numone]"
ParseTreeToString parsed-numone-range-4 = "[numone-range-4]"
ParseTreeToString parsed-numpunct = "[numpunct]"
ParseTreeToString parsed-numpunct-bar-10 = "[numpunct-bar-10]"
ParseTreeToString parsed-numpunct-bar-11 = "[numpunct-bar-11]"
ParseTreeToString parsed-numpunct-bar-6 = "[numpunct-bar-6]"
ParseTreeToString parsed-numpunct-bar-7 = "[numpunct-bar-7]"
ParseTreeToString parsed-numpunct-bar-8 = "[numpunct-bar-8]"
ParseTreeToString parsed-numpunct-bar-9 = "[numpunct-bar-9]"
ParseTreeToString parsed-otherpunct = "[otherpunct]"
ParseTreeToString parsed-otherpunct-bar-12 = "[otherpunct-bar-12]"
ParseTreeToString parsed-otherpunct-bar-13 = "[otherpunct-bar-13]"
ParseTreeToString parsed-otherpunct-bar-14 = "[otherpunct-bar-14]"
ParseTreeToString parsed-otherpunct-bar-15 = "[otherpunct-bar-15]"
ParseTreeToString parsed-otherpunct-bar-16 = "[otherpunct-bar-16]"
ParseTreeToString parsed-otherpunct-bar-17 = "[otherpunct-bar-17]"
ParseTreeToString parsed-otherpunct-bar-18 = "[otherpunct-bar-18]"
ParseTreeToString parsed-otherpunct-bar-19 = "[otherpunct-bar-19]"
ParseTreeToString parsed-otherpunct-bar-20 = "[otherpunct-bar-20]"
ParseTreeToString parsed-otherpunct-bar-21 = "[otherpunct-bar-21]"
ParseTreeToString parsed-otherpunct-bar-22 = "[otherpunct-bar-22]"
ParseTreeToString parsed-otherpunct-bar-23 = "[otherpunct-bar-23]"
ParseTreeToString parsed-otherpunct-bar-24 = "[otherpunct-bar-24]"
ParseTreeToString parsed-otherpunct-bar-25 = "[otherpunct-bar-25]"
ParseTreeToString parsed-otherpunct-bar-26 = "[otherpunct-bar-26]"
ParseTreeToString parsed-otherpunct-bar-27 = "[otherpunct-bar-27]"
ParseTreeToString parsed-otherpunct-bar-28 = "[otherpunct-bar-28]"
ParseTreeToString parsed-otherpunct-bar-29 = "[otherpunct-bar-29]"
ParseTreeToString parsed-otherpunct-bar-30 = "[otherpunct-bar-30]"
ParseTreeToString parsed-otherpunct-bar-31 = "[otherpunct-bar-31]"
ParseTreeToString parsed-otherpunct-bar-32 = "[otherpunct-bar-32]"
ParseTreeToString parsed-otherpunct-bar-33 = "[otherpunct-bar-33]"
ParseTreeToString parsed-otherpunct-bar-34 = "[otherpunct-bar-34]"
ParseTreeToString parsed-otherpunct-bar-35 = "[otherpunct-bar-35]"
ParseTreeToString parsed-otherpunct-bar-36 = "[otherpunct-bar-36]"
ParseTreeToString parsed-otherpunct-bar-37 = "[otherpunct-bar-37]"
ParseTreeToString parsed-otherpunct-bar-38 = "[otherpunct-bar-38]"
ParseTreeToString parsed-otherpunct-bar-39 = "[otherpunct-bar-39]"
ParseTreeToString parsed-otherpunct-bar-40 = "[otherpunct-bar-40]"
ParseTreeToString parsed-otherpunct-bar-41 = "[otherpunct-bar-41]"
ParseTreeToString parsed-otherpunct-bar-42 = "[otherpunct-bar-42]"
ParseTreeToString parsed-otherpunct-bar-43 = "[otherpunct-bar-43]"
ParseTreeToString parsed-otherpunct-bar-44 = "[otherpunct-bar-44]"
ParseTreeToString parsed-otherpunct-bar-45 = "[otherpunct-bar-45]"
ParseTreeToString parsed-otherpunct-bar-46 = "[otherpunct-bar-46]"
ParseTreeToString parsed-otherpunct-bar-47 = "[otherpunct-bar-47]"
ParseTreeToString parsed-otherpunct-bar-48 = "[otherpunct-bar-48]"
ParseTreeToString parsed-otherpunct-bar-49 = "[otherpunct-bar-49]"
ParseTreeToString parsed-otherpunct-bar-50 = "[otherpunct-bar-50]"
ParseTreeToString parsed-otherpunct-bar-51 = "[otherpunct-bar-51]"
ParseTreeToString parsed-otherpunct-bar-52 = "[otherpunct-bar-52]"
ParseTreeToString parsed-otherpunct-bar-53 = "[otherpunct-bar-53]"
ParseTreeToString parsed-otherpunct-bar-54 = "[otherpunct-bar-54]"
ParseTreeToString parsed-otherpunct-bar-55 = "[otherpunct-bar-55]"
ParseTreeToString parsed-otherpunct-bar-56 = "[otherpunct-bar-56]"
ParseTreeToString parsed-otherpunct-bar-57 = "[otherpunct-bar-57]"
ParseTreeToString parsed-otherpunct-bar-58 = "[otherpunct-bar-58]"
ParseTreeToString parsed-ws = "[ws]"
ParseTreeToString parsed-ws-plus-67 = "[ws-plus-67]"

------------------------------------------
-- Reorganizing rules
------------------------------------------

mutual

  {-# TERMINATING #-}
  norm-start : (x : start) → start
  norm-start x = x

  {-# TERMINATING #-}
  norm-posinfo : (x : posinfo) → posinfo
  norm-posinfo x = x

  {-# TERMINATING #-}
  norm-entity : (x : entity) → entity
  norm-entity x = x

  {-# TERMINATING #-}
  norm-entities : (x : entities) → entities
  norm-entities x = x

isParseTree : ParseTreeT → 𝕃 char → string → Set
isParseTree p l s = ⊤ {- this will be ignored since we are using simply typed runs -}

ptr : ParseTreeRec
ptr = record { ParseTreeT = ParseTreeT ; isParseTree = isParseTree ; ParseTreeToString = ParseTreeToString }

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
module Cats.Profunctor where

open import Data.Product using (_,_)
open import Level using (suc ; _⊔_)

open import Cats.Category
open import Cats.Category.Op using (_ᵒᵖ)
open import Cats.Category.Product.Binary using (_×_)
open import Cats.Category.Setoids using (Setoids)
open import Cats.Functor

import Cats.Category.Cat as Cat
import Cats.Category.Cat.Facts.Product as Cat

-- The usual definition inverts C and D, so
--
--   Profunctor C D E = Functor (Dᵒᵖ × C) E
--
-- but that's just confusing.
Profunctor : ∀ {lo la l≈ lo′ la′ l≈′ lo″ la″ l≈″}
  → Category lo la l≈
  → Category lo′ la′ l≈′
  → Category lo″ la″ l≈″
  → Set (lo ⊔ la ⊔ l≈ ⊔ lo′ ⊔ la′ ⊔ l≈′ ⊔ lo″ ⊔ la″ ⊔ l≈″)
Profunctor C D E = Functor ((C ᵒᵖ) × D) E

module Profunctor {lo la l≈ lo′ la′ l≈′ lo″ la″ l≈″}
  {C : Category lo la l≈}
  {D : Category lo′ la′ l≈′}
  {E : Category lo″ la″ l≈″}
  (F : Profunctor C D E)
  where

  private
    module C = Category C
    module D = Category D
    module E = Category E

  pobj : C.Obj → D.Obj → E.Obj
  pobj c d = fobj F (c , d)

  pmap : ∀ {c c′} (f : c′ C.⇒ c) {d d′} (g : d D.⇒ d′)
    → pobj c d E.⇒ pobj c′ d′
  pmap f g = fmap F (f , g)

  pmap₁ : ∀ {c c′ d} (f : c′ C.⇒ c)
    → pobj c d E.⇒ pobj c′ d
  pmap₁ f = pmap f D.id

  pmap₂ : ∀ {c d d′} (g : d D.⇒ d′)
    → pobj c d E.⇒ pobj c d′
  pmap₂ g = pmap C.id g

open Profunctor public

Functor→Profunctor₁ : ∀ {lo la l≈ lo′ la′ l≈′ lo″ la″ l≈″}
  → {C : Category lo la l≈} {D : Category lo′ la′ l≈′} {X : Category lo″ la″ l≈″}
  → Functor (C ᵒᵖ) D
  → Profunctor C X D
Functor→Profunctor₁ F = F Cat.∘ Cat.proj₁

Functor→Profunctor₂ : ∀ {lo la l≈ lo′ la′ l≈′ lo″ la″ l≈″}
  → {C : Category lo la l≈} {D : Category lo′ la′ l≈′} {X : Category lo″ la″ l≈″}
  → Functor C D
  → Profunctor X C D
Functor→Profunctor₂ F = F Cat.∘ Cat.proj₂

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
-- There was a rare bug in display form generation for with functions
-- in local blocks.

module WithInWhere where

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

data Z? : Nat -> Set where
  yes : Z? zero
  no  : forall {n} -> Z? (suc n)

z? : (n : Nat) -> Z? n
z? zero    = yes
z? (suc n) = no

bug : Nat -> Nat
bug n = ans
  where
    ans : Nat
    ans with z? (suc n)
    ... | no with zero
    ...   |  _ = zero


text:
module Cats.Category.Preorder.Facts.PreorderAsCategory where

open import Data.Bool using (true ; false)
open import Relation.Binary using (Preorder)

import Level

open import Cats.Category
open import Cats.Category.Preorder using (preorderAsCategory)
open import Cats.Util.Logic.Constructive

module _ {lc l≈ l≤} (P : Preorder lc l≈ l≤) where

  C : Category _ _ _
  C = preorderAsCategory P

  open module P = Preorder P using (_∼_) renaming (_≈_ to _≋_)
  open Category C

  _≈_⊔_ : Obj → Obj → Obj → Set l≤
  lub ≈ x ⊔ y = x ∼ lub ∧ y ∼ lub ∧ (lub ∼ x ∨ lub ∼ y)

  _≈_⊓_ : Obj → Obj → Obj → Set l≤
  glb ≈ x ⊓ y = glb ∼ x ∧ glb ∼ y ∧ (x ∼ glb ∨ y ∼ glb)

  IsMinimum : Obj → Set (lc Level.⊔ l≤)
  IsMinimum m = ∀ x → m ∼ x

  IsMaximum : Obj → Set (lc Level.⊔ l≤)
  IsMaximum m = ∀ x → x ∼ m

  initial : ∀ {x} → IsMinimum x → IsInitial x
  initial min y = ∃!-intro (min y) _ _

  terminal : ∀ {x} → IsMaximum x → IsTerminal x
  terminal max y = ∃!-intro (max y) _ _

  ⊓-isBinaryProduct : ∀ {glb x y}
    → (pl : glb ∼ x)
    → (pr : glb ∼ y)
    → (x ∼ glb ∨ y ∼ glb)
    → IsBinaryProduct glb pl pr
  ⊓-isBinaryProduct pl pr (∨-introl x∼glb) xl xr = ∃!-intro (x∼glb ∘ xl) _ _
  ⊓-isBinaryProduct pl pr (∨-intror y∼glb) xl xr = ∃!-intro (y∼glb ∘ xr) _ _

  ⊓-to-BinaryProduct : ∀ {glb x y} → glb ≈ x ⊓ y → BinaryProduct x y
  ⊓-to-BinaryProduct {glb} (pl , pr , maximal)
      = mkBinaryProduct pl pr (⊓-isBinaryProduct pl pr maximal)

  mono : ∀ {x y} (f : x ⇒ y) → IsMono f
  mono = _

  epi : ∀ {x y} (f : x ⇒ y) → IsEpi f
  epi = _

  unique : ∀ {x y} (f : x ⇒ y) → IsUnique f
  unique = _


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

module Cubical.Data.FinType where

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

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

open import Prelude
open import Relation.Binary

module Data.List.Mapping {kℓ} {K : Type kℓ} {r₁ r₂} (totalOrder : TotalOrder K r₁ r₂) where

open import Relation.Binary.Construct.Decision totalOrder
open import Relation.Binary.Construct.LowerBound dec-ord
open import Data.Nat using (_+_)
open TotalOrder lb-ord using (<-trans) renaming (refl to <-refl)
import Data.Unit.UniversePolymorphic as Poly
open import Data.Maybe.Properties using (IsJust)
open TotalOrder dec-ord using (_<?_; _<_; total⇒isSet; irrefl; compare)

instance
  top-inst : Poly.⊤ {ℓzero}
  top-inst = Poly.tt

private
  variable
    n m : ℕ
    v : Level
    Val : K → Type v

infixr 5 _︓_,_
data MapFrom (lb : ⌊∙⌋) {v} (Val : K → Type v) : Type (kℓ ℓ⊔ r₁ ℓ⊔ v) where
  ∅ : MapFrom lb Val
  _︓_,_ : (k : K) → ⦃ inBounds : lb <⌊ k ⌋ ⦄ → (v : Val k) → MapFrom ⌊ k ⌋ Val → MapFrom lb Val

private
  variable
    lb : ⌊∙⌋

weaken : ∀ {x} → ⦃ _ : lb <⌊ x ⌋ ⦄ → MapFrom ⌊ x ⌋ Val → MapFrom lb Val
weaken ∅ = ∅
weaken {lb = lb} {x = x} (k ︓ val , xs) = k ︓ val , xs
  where
    instance
      _ : lb <⌊ k ⌋
      _ = <-trans {x = lb} {y = ⌊ x ⌋} {z = ⌊ k ⌋} it it

-- module _ {v} {Val : K → Type v} where
--   _[_]? : MapFrom lb Val → (k : K) ⦃ inBounds : lb <⌊ k ⌋ ⦄ → Maybe (Val k)
--   ∅ [ k ]? = nothing
--   k₂ ︓ v , xs [ k₁ ]? = case compare k₁ k₂ of
--     λ { (lt _) → nothing ;
--         (eq _) → just (subst Val (sym it) v) ;
--         (gt _) → xs [ k₁ ]? }
--   infixl 4 _[_]?

-- --   _[_]︓_ : MapFrom lb Val → (k : K) ⦃ inBounds : lb <⌊ k ⌋ ⦄ → (val : Val k) → MapFrom lb Val
-- --   ∅ [ k₁ ]︓ v₁ = k₁ ︓ v₁ , ∅
-- --   (k₂ ︓ v₂ , xs) [ k₁ ]︓ v₁ =
-- --     comparing k₁ ∙ k₂
-- --       |< k₁ ︓ v₁ , k₂ ︓ v₂ , xs
-- --       |≡ k₂ ︓ subst Val it v₁ , xs
-- --       |> k₂ ︓ v₂ , (xs [ k₁ ]︓ v₁)
-- --   infixl 4 _[_]︓_

-- --   _[_]︓∅ : MapFrom lb Val → (k : K) ⦃ inBounds : lb <⌊ k ⌋ ⦄ → MapFrom lb Val
-- --   ∅ [ k₁ ]︓∅ = ∅
-- --   (k₂ ︓ v₂ , xs) [ k₁ ]︓∅ = comparing k₁ ∙ k₂
-- --       |< k₂ ︓ v₂ , xs
-- --       |≡ weaken xs
-- --       |> k₂ ︓ v₂ , (xs [ k₁ ]︓∅)
-- --   infixl 4 _[_]︓∅

-- -- infixr 0 Map
-- -- Map : ∀ {v} (Val : K → Type v) → Type _
-- -- Map = MapFrom ⌊⊥⌋

-- -- syntax Map (λ s → e) = s ↦ e

-- -- Map′ : ∀ {v} (Val : Type v) → Type _
-- -- Map′ V = Map (const V)

-- -- infixr 5 _≔_,_
-- -- data RecordFrom (lb : ⌊∙⌋) : MapFrom lb (const Type) → Type (kℓ ℓ⊔ r₁ ℓ⊔ ℓsuc ℓzero) where
-- --   ∅ : RecordFrom lb ∅
-- --   _≔_,_ : (k : K) → ⦃ inBounds : lb <⌊ k ⌋ ⦄ → {xs : MapFrom ⌊ k ⌋ (const Type)} {t : Type} → (v : t) → RecordFrom ⌊ k ⌋ xs → RecordFrom lb (k ︓ t , xs)

-- -- Record : Map′ Type → Type _
-- -- Record = RecordFrom ⌊⊥⌋

-- -- infixr 5 _∈_
-- -- _∈_ : (k : K) → ⦃ inBounds : lb <⌊ k ⌋ ⦄ → MapFrom lb Val → Type
-- -- k ∈ xs = IsJust (xs [ k ]?)

-- -- _[_]! : (xs : MapFrom lb Val) → (k : K) → ⦃ inBounds : lb <⌊ k ⌋ ⦄ → ⦃ k∈xs : k ∈ xs ⦄ → Val k
-- -- xs [ k ]! with xs [ k ]? | inspect (_[_]? xs) k
-- -- xs [ k ]! | just x  | _ = x
-- -- xs [ k ]! | nothing | _ = ⊥-elim it

-- -- infixl 4 _[_]
-- -- _[_] : {xs : MapFrom lb (const Type)} → RecordFrom lb xs → (k : K) ⦃ inBounds : lb <⌊ k ⌋ ⦄ ⦃ k∈xs : k ∈ xs ⦄ → xs [ k ]!
-- -- _[_] {xs = xs} (k₂ ≔ v , r) k₁ with xs [ k₁ ]? | compare′ k₁ k₂
-- -- (k₂ ≔ v , r) [ k₁ ] | _ | lt′ = ⊥-elim it
-- -- (k₂ ≔ v , r) [ k₁ ] | _ | eq′ = v
-- -- (k₂ ≔ v , r) [ k₁ ] | _ | gt′ = r [ k₁ ]

-- -- infixl 4 _[_]≔_
-- -- _[_]≔_ : {xs : MapFrom lb (const Type)} → RecordFrom lb xs → (k : K) ⦃ inBounds : lb <⌊ k ⌋ ⦄ → A → RecordFrom lb (xs [ k ]︓ A)
-- -- ∅ [ k ]≔ x = k ≔ x , ∅
-- -- (k₂ ≔ v₁ , rs) [ k₁ ]≔ x with compare′ k₁ k₂
-- -- (k₂ ≔ v₁ , rs) [ k₁ ]≔ x | lt′ = k₁ ≔ x , k₂ ≔ v₁ , rs
-- -- (k₂ ≔ v₁ , rs) [ k₁ ]≔ x | eq′ = k₂ ≔ x , rs
-- -- (k₂ ≔ v₁ , rs) [ k₁ ]≔ x | gt′ = k₂ ≔ v₁ , (rs [ k₁ ]≔ x)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

module Interpreter where

open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Int using (pos)
open import Agda.Builtin.Unit using (⊤)

open import FFI.IO using (getContents; putStrLn; _>>=_; _>>_)
open import FFI.Data.Aeson using (Value; eitherDecode)
open import FFI.Data.Either using (Left; Right)
open import FFI.Data.Maybe using (just; nothing)
open import FFI.Data.String using (String; _++_)
open import FFI.Data.Text.Encoding using (encodeUtf8)
open import FFI.System.Exit using (exitWith; ExitFailure)

open import Luau.StrictMode.ToString using (warningToStringᴮ)
open import Luau.Syntax using (Block; yes; maybe; isAnnotatedᴮ)
open import Luau.Syntax.FromJSON using (blockFromJSON)
open import Luau.Syntax.ToString using (blockToString; valueToString)
open import Luau.Run using (run; return; done; error)
open import Luau.RuntimeError.ToString using (errToStringᴮ)

open import Properties.StrictMode using (wellTypedProgramsDontGoWrong)

runBlock′ : ∀ a → Block a → IO ⊤
runBlock′ a block with run block
runBlock′ a block | return V D = putStrLn ("\nRAN WITH RESULT: " ++ valueToString V)
runBlock′ a block | done D = putStrLn ("\nRAN")
runBlock′ maybe block | error E D = putStrLn ("\nRUNTIME ERROR:\n" ++ errToStringᴮ _ E)
runBlock′ yes block | error E D with wellTypedProgramsDontGoWrong _ block _ D E
runBlock′ yes block | error E D | W = putStrLn ("\nRUNTIME ERROR:\n" ++ errToStringᴮ _ E ++ "\n\nTYPE ERROR:\n" ++ warningToStringᴮ _ W)

runBlock : Block maybe → IO ⊤
runBlock B with isAnnotatedᴮ B
runBlock B | nothing = putStrLn ("UNANNOTATED PROGRAM:\n" ++ blockToString B) >> runBlock′ maybe B
runBlock B | just B′ = putStrLn ("ANNOTATED PROGRAM:\n" ++ blockToString B) >> runBlock′ yes B′

runJSON : Value → IO ⊤
runJSON value with blockFromJSON(value)
runJSON value | (Left err) = putStrLn ("LUAU ERROR: " ++ err) >> exitWith (ExitFailure (pos 1))
runJSON value | (Right block) = runBlock block

runString : String → IO ⊤
runString txt with eitherDecode (encodeUtf8 txt)
runString txt | (Left err) = putStrLn ("JSON ERROR: " ++ err) >> exitWith (ExitFailure (pos 1))
runString txt | (Right value) = runJSON value

main : IO ⊤
main = getContents >>= runString

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


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

open import HoTT
open import homotopy.PtdMapSequence

module homotopy.CofiberSequence {i} where

{- Useful abbreviations -}
module _ {X Y : Ptd i} (f : X ⊙→ Y) where

  ⊙Cofiber² = ⊙Cofiber (⊙cfcod' f)
  ⊙cfcod²' = ⊙cfcod' (⊙cfcod' f)

  ⊙Cofiber³ = ⊙Cofiber ⊙cfcod²'
  ⊙cfcod³' = ⊙cfcod' ⊙cfcod²'

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

  Cofiber² = Cofiber (cfcod' f)
  cfcod²' = cfcod' (cfcod' f)

  Cofiber³ = Cofiber cfcod²'
  cfcod³' = cfcod' cfcod²'

{- For [f : X → Y], the cofiber space [Cofiber(cfcod f)] is equivalent to
 - [Susp X]. This is essentially an application of the two pushouts
 - lemma:
 -
 -       f
 -   X ––––> Y ––––––––––––––> ∙
 -   |       |                 |
 -   |       |cfcod f          |
 -   v       v                 v
 -   ∙ ––> Cofiber f ––––––––––> Cofiber² f
 -                cfcod² f
 -
 - The map [cfcod² f : Cofiber f → Cofiber² f] becomes [extract-glue : Cofiber f → ΣX],
 - and the map [cfcod³ f : Cofiber² f → Cofiber³ f] becomes [Susp-fmap f : ΣX → ΣY].
 -}
private
  {- the equivalences between [Cofiber² f] and [ΣX] (and so [Cofiber³ f] and [ΣY]) -}
  module Equiv {X Y : Ptd i} (f : X ⊙→ Y) where

    module Into = CofiberRec {f = cfcod' (fst f)} {C = Susp (de⊙ X)}
      south extract-glue (λ _ → idp)

    into : Cofiber² (fst f) → Susp (de⊙ X)
    into = Into.f

    ⊙into : ⊙Cofiber² f ⊙→ ⊙Susp X
    ⊙into = into , ! (merid (pt X))

    module Out = SuspRec {C = de⊙ (⊙Cofiber² f)}
      (cfcod cfbase) cfbase
      (λ x → ap cfcod (cfglue x) ∙ ! (cfglue (fst f x)))

    out : Susp (de⊙ X) → Cofiber² (fst f)
    out = Out.f

    abstract
      into-out : ∀ σ → into (out σ) == σ
      into-out = Susp-elim idp idp
        (λ x → ↓-∘=idf-in' into out $
          ap (ap into) (Out.merid-β x)
          ∙ ap-∙ into (ap cfcod (cfglue x)) (! (cfglue (fst f x)))
          ∙ ap (λ w → ap into (ap cfcod (cfglue x)) ∙ w)
               (ap-! into (cfglue (fst f x)) ∙ ap ! (Into.glue-β (fst f x)))
          ∙ ∙-unit-r _
          ∙ ∘-ap into cfcod (cfglue x) ∙ ExtractGlue.glue-β x)

      out-into : ∀ κ → out (into κ) == κ
      out-into = Cofiber-elim {f = cfcod' (fst f)}
        idp
        (Cofiber-elim {f = fst f} idp cfglue
          (λ x → ↓-='-from-square $
            (ap-∘ out extract-glue (cfglue x)
             ∙ ap (ap out) (ExtractGlue.glue-β x) ∙ Out.merid-β x)
            ∙v⊡ (vid-square {p = ap cfcod (cfglue x)}
                 ⊡h rt-square (cfglue (fst f x)))
            ⊡v∙ ∙-unit-r _))
        (λ y → ↓-∘=idf-from-square out into $
           ap (ap out) (Into.glue-β y) ∙v⊡ connection)

    eqv : Cofiber² (fst f) ≃ Susp (de⊙ X)
    eqv = equiv into out into-out out-into

    ⊙eqv : ⊙Cofiber² f ⊙≃ ⊙Susp X
    ⊙eqv = ≃-to-⊙≃ eqv (! (merid (pt X)))

module _ {X Y : Ptd i} (f : X ⊙→ Y) where

  ⊙Cof²-to-⊙Susp : ⊙Cofiber² f ⊙→ ⊙Susp X
  ⊙Cof²-to-⊙Susp = Equiv.⊙into f

  Cof²-to-Susp = fst ⊙Cof²-to-⊙Susp

  ⊙Susp-to-⊙Cof² : ⊙Susp X ⊙→ ⊙Cofiber² f
  ⊙Susp-to-⊙Cof² = ⊙<– (Equiv.⊙eqv f)

  Susp-to-Cof² = fst ⊙Susp-to-⊙Cof²

  Cof²-equiv-Susp : Cofiber² (fst f) ≃ Susp (de⊙ X)
  Cof²-equiv-Susp = Equiv.eqv f

  cod²-extract-glue-comm-sqr : CommSquare (cfcod²' (fst f)) extract-glue (idf _) Cof²-to-Susp
  cod²-extract-glue-comm-sqr  = comm-sqr λ _ → idp

  extract-glue-cod²-comm-sqr : CommSquare extract-glue (cfcod²' (fst f)) (idf _) Susp-to-Cof²
  extract-glue-cod²-comm-sqr = CommSquare-inverse-v cod²-extract-glue-comm-sqr
                                 (idf-is-equiv _) (snd Cof²-equiv-Susp)

  abstract
    cod³-Susp-fmap-comm-sqr : CommSquare (cfcod³' (fst f)) (Susp-fmap (fst f))
      Cof²-to-Susp (Susp-flip ∘ Equiv.into (⊙cfcod' f))
    cod³-Susp-fmap-comm-sqr = comm-sqr $ Cofiber-elim {f = cfcod' (fst f)}
      idp
      (Cofiber-elim {f = fst f}
        idp (λ y → merid y)
        (λ x → ↓-cst=app-in $
            ap (idp ∙'_)
              ( ap-∘ (Susp-fmap (fst f)) extract-glue (cfglue x)
              ∙ ap (ap (Susp-fmap (fst f))) (ExtractGlue.glue-β x)
              ∙ SuspFmap.merid-β (fst f) x)
          ∙ ∙'-unit-l (merid (fst f x))))
      (λ y → ↓-='-in' $
          ap (Susp-fmap (fst f) ∘ Cof²-to-Susp) (cfglue y)
            =⟨ ap-∘ (Susp-fmap (fst f)) Cof²-to-Susp (cfglue y) ⟩
          ap (Susp-fmap (fst f)) (ap Cof²-to-Susp (cfglue y))
            =⟨ Equiv.Into.glue-β f y |in-ctx ap (Susp-fmap (fst f)) ⟩
          idp
            =⟨ ! $ !-inv'-l (merid y) ⟩
          ! (merid y) ∙' merid y
            =⟨ ! $ SuspFlip.merid-β y |in-ctx _∙' merid y ⟩
          ap Susp-flip (merid y) ∙' merid y
            =⟨ ! $ ExtractGlue.glue-β y |in-ctx (λ p → ap Susp-flip p ∙' merid y) ⟩
          ap Susp-flip (ap extract-glue (cfglue y)) ∙' merid y
            =⟨ ! $ ap-∘ Susp-flip extract-glue (cfglue y) |in-ctx _∙' merid y ⟩
          ap (Susp-flip ∘ extract-glue) (cfglue y) ∙' merid y
            =∎)

  iterated-cofiber-seq : PtdMapSequence X (⊙Cofiber³ f)
  iterated-cofiber-seq =
    X ⊙→⟨ f ⟩ Y ⊙→⟨ ⊙cfcod' f ⟩ ⊙Cofiber f ⊙→⟨ ⊙cfcod²' f ⟩ ⊙Cofiber² f ⊙→⟨ ⊙cfcod³' f ⟩ ⊙Cofiber³ f ⊙⊣|

  cyclic-cofiber-seq : PtdMapSequence X (⊙Susp Y)
  cyclic-cofiber-seq =
    X ⊙→⟨ f ⟩ Y ⊙→⟨ ⊙cfcod' f ⟩ ⊙Cofiber f ⊙→⟨ ⊙extract-glue ⟩ ⊙Susp X ⊙→⟨ ⊙Susp-fmap f ⟩ ⊙Susp Y ⊙⊣|

  iterated-to-cyclic : PtdMapSeqMap iterated-cofiber-seq cyclic-cofiber-seq
    (⊙idf X) (⊙Susp-flip Y ⊙∘ Equiv.⊙into (⊙cfcod' f))
  iterated-to-cyclic =
    ⊙idf X                                  ⊙↓⟨ comm-sqr (λ _ → idp) ⟩
    ⊙idf Y                                  ⊙↓⟨ comm-sqr (λ _ → idp) ⟩
    ⊙idf (⊙Cofiber f)                       ⊙↓⟨ cod²-extract-glue-comm-sqr ⟩
    ⊙Cof²-to-⊙Susp                          ⊙↓⟨ cod³-Susp-fmap-comm-sqr ⟩
    ⊙Susp-flip Y ⊙∘ Equiv.⊙into (⊙cfcod' f) ⊙↓|

  iterated-to-cyclic-is-equiv : is-⊙seq-equiv iterated-to-cyclic
  iterated-to-cyclic-is-equiv =
      idf-is-equiv _
    , idf-is-equiv _
    , idf-is-equiv _
    , snd (Equiv.eqv f)
    , snd (Susp-flip-equiv ∘e (Equiv.eqv (⊙cfcod' f)))

  iterated-equiv-cyclic : PtdMapSeqEquiv iterated-cofiber-seq cyclic-cofiber-seq
    (⊙idf X) (⊙Susp-flip Y ⊙∘ Equiv.⊙into (⊙cfcod' f))
  iterated-equiv-cyclic = iterated-to-cyclic , iterated-to-cyclic-is-equiv

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
open import FRP.JS.Behaviour using ( Beh ; [_] ; hold )
open import FRP.JS.Event using ( tag )
open import FRP.JS.DOM using ( DOM ; text ; element ; listen ; click ; _++_ )
open import FRP.JS.RSet using ( ⟦_⟧ )

module FRP.JS.Demo.Button where

main : ∀ {w} → ⟦ Beh (DOM w) ⟧
main = text lab ++ but where
  but = element "button" (text ["OK"])
  lab = hold "Press me: " (tag "Pressed: " (listen click but))

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
module _ where

module A where

  infixr 5 _∷_

  data D : Set₂ where
    []  : D
    _∷_ : Set₁ → D → D

module B where

  infix 5 _∷_

  data D : Set₂ where
    _∷_ : Set₁ → Set₁ → D

open A
open B

foo : A.D
foo = Set ∷ []

bar : B.D
bar = Set ∷ Set


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

module Basic_Types where

-- Already in the builtin's of agda, there are Π types, which is ∀, and lambda
-- abstraction, which is λ{ } and function types, which is →.

-- ------------------------------------
-- Some operations for function types
-- The curly brackts ∀{} should be viewed as contexts.

-- identity function
id : ∀ {A : Set} → A → A
id = λ{ x → x }

-- function composition
comp : ∀ {A B C : Set} → (B → C) → (A → B) → A → C
comp {A} {B} {C} = λ (f : B → C) (g : A → B) (x : A) → f (g x)
-- The judgemental equality of association of functions is builtin in agda,
-- i.e., all the rules of derivation in the basic language of type theory,
-- e.g., the β-, η- reduction is automatic in agda.

-- swapping the argument
swap : ∀ {A B : Set} {C : A → B → Set} →
      (∀ (a : A) (b : B) → C a b) → (∀ (b : B) (a : A) → C a b)
swap {A} {B} {C} = λ { p → λ (b : B) (a : A) → p a b }

-- ------------------------------------
-- the unit type
data 𝟙 : Set where
  ⋆ : 𝟙

𝟙-ind : ∀ {A : 𝟙 → Set} → ∀ (a : A ⋆) → ∀ (x : 𝟙) → A x
𝟙-ind {A} a = 𝟙-indhelper
  where 𝟙-indhelper : ∀ (x : 𝟙) → A x
        𝟙-indhelper ⋆ = a

-- ------------------------------------
-- the empty type
data 𝟘 : Set where

𝟘-ind : ∀ {A : 𝟘 → Set} → ∀ (x : 𝟘) → A x
𝟘-ind {A} ()

-- define negation
¬_ : ∀ (A : Set) → Set
¬ A = A → 𝟘

-- ------------------------------------
-- the boolean type
data 𝟚 : Set where
  tt ff : 𝟚

𝟚-ind : ∀ {A : 𝟚 → Set} → A ff → A tt → ∀ (x : 𝟚) → A x
𝟚-ind Aff _ ff = Aff
𝟚-ind _ Att tt = Att

-- ------------------------------------
-- natural numbers
data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

-- ℕ induction
ℕ-ind : ∀ {A : ℕ → Set} →
        ∀ (a : A 0) → (∀ (n : ℕ) → A n → A (succ n)) → ∀ (m : ℕ) → A m
ℕ-ind {A} a p = ℕ-indhelper
  where ℕ-indhelper : ∀ (m : ℕ) → A m
        ℕ-indhelper 0        = a
        ℕ-indhelper (succ n) = p n (ℕ-indhelper n)
-- From this exercise, we can actually see that the idea of induction is
-- builtin in agda, since we essentially use the induction builtin in agda
-- to prove ℕ-ind.

-- ℕ recursion, which is a special case for ℕ induction, where the type is not
-- dependent on ℕ
ℕ-rec : ∀ {A : Set} →
        ∀ (a : A) → (∀ (n : ℕ) → A → A) → ∀ (m : ℕ) → A
ℕ-rec {A} = ℕ-ind {λ { n → A }}

-- for example, we can use ℕ-rec to define addition
add : ℕ → ℕ → ℕ
add = ℕ-rec {ℕ → ℕ} (id {ℕ}) (λ (n : ℕ) (p : ℕ → ℕ) → comp succ p)

-- ------------------------------------
-- the sum type
record Σ (A : Set) (B : A → Set) : Set where
  constructor
    _,_
  field
    a : A
    b : B a

-- the two projections
π₁ : ∀ {A : Set} {B : A → Set} → Σ A B → A
π₁ (x , y) = x

π₂ : ∀ {A : Set} {B : A → Set} → ∀ (z : Σ A B) → B (π₁ z)
π₂ (x , y) = y

syntax Σ A (λ a → b) = Σ a ∶ A , b

-- Σ induction
Σ-ind : ∀ {A : Set} {B : A → Set} {P : Σ A B → Set} →
       (∀ (a : A) (b : B a) → P (a , b)) → ∀ (z : Σ A B) → P z
Σ-ind {A} {B} {P} = λ (f : ∀ (a : A) (b : B a) → P (a , b)) →
                    λ (z : Σ A B) → f (π₁ z) (π₂ z)

-- cartesion product type
_×_ : Set → Set → Set
A × B = Σ a ∶ A , B

×-ind : ∀ {A : Set} {B : Set} {P : A × B → Set} →
       (∀ (a : A) (b : B) → P (a , b)) → ∀ (z : A × B) → P z
×-ind {A} {B} {P} = Σ-ind {A} {λ (a : A) → B} {P}

-- ------------------------------------
-- the coproduct type

data _⊎_ (A : Set) (B : Set) : Set where
  inl : A → A ⊎ B
  inr : B → A ⊎ B

⊎-ind : ∀ {A : Set} {B : Set} {P : A ⊎ B → Set} →
       (∀ (a : A) → P (inl a)) → (∀ (b : B) → P (inr b)) →
        ∀ (u : A ⊎ B) → P u
⊎-ind f _ (inl x) = f x
⊎-ind _ g (inr y) = g y


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of products
------------------------------------------------------------------------

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

module Data.Product.Properties where

open import Data.Product
open import Function using (_∘_)
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Product
import Relation.Nullary.Decidable as Dec

------------------------------------------------------------------------
-- Equality (dependent)

module _ {a b} {A : Set a} {B : A → Set b} where

  ,-injectiveˡ : ∀ {a c} {b : B a} {d : B c} → (a , b) ≡ (c , d) → a ≡ c
  ,-injectiveˡ refl = refl

  -- See also Data.Product.Properties.WithK.,-injectiveʳ.

------------------------------------------------------------------------
-- Equality (non-dependent)

module _ {a b} {A : Set a} {B : Set b} where

  ,-injectiveʳ : ∀ {a c : A} {b d : B} → (a , b) ≡ (c , d) → b ≡ d
  ,-injectiveʳ refl = refl

  ,-injective : ∀ {a c : A} {b d : B} → (a , b) ≡ (c , d) → a ≡ c × b ≡ d
  ,-injective refl = refl , refl

  ≡-dec : Decidable {A = A} _≡_ → Decidable {A = B} _≡_ →
          Decidable {A = A × B} _≡_
  ≡-dec dec₁ dec₂ (a , b) (c , d) =
    Dec.map′ (uncurry (cong₂ _,_)) ,-injective (dec₁ a c ×-dec dec₂ b d)


text:
module Options-in-right-order where

data Unit : Set where
  unit : Unit

postulate
  IO : Set → Set

{-# COMPILE GHC IO = type IO #-}
{-# BUILTIN IO IO #-}

postulate
  return : {A : Set} → A → IO A

{-# COMPILE GHC return = \_ -> return #-}

main = return unit


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

open import Categories.Category

module Categories.Object.Subobject {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level
open import Data.Product
open import Data.Unit

open import Relation.Binary using (Poset)

open import Categories.Functor
open import Categories.Category.Slice
open import Categories.Category.SubCategory
open import Categories.Category.Construction.Thin
import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR
open import Categories.Morphism.Notation

private
  module 𝒞 = Category 𝒞

-- The Full Subcategory of the over category 𝒞/c on monomorphisms
slice-mono : 𝒞.Obj → Category _ _ _
slice-mono c = FullSubCategory (Slice 𝒞 c) {I = Σ[ α ∈ 𝒞.Obj ](α ↣ c)} λ (_ , i) → sliceobj (mor i)
  where open Mor 𝒞
        open _↣_

-- Poset of subobjects for some c ∈ 𝒞
Subobjects : 𝒞.Obj → Poset _ _ _
Subobjects c = record
  { Carrier = 𝒞ᶜ.Obj
  ; _≈_ = 𝒞ᶜ [_≅_]
  ; _≤_ = 𝒞ᶜ [_,_]
  ; isPartialOrder = record
    { isPreorder = record
      { isEquivalence = Mor.≅-isEquivalence 𝒞ᶜ
      ; reflexive = λ iso → Mor._≅_.from iso
      ; trans = λ {(α , f) (β , g) (γ , h)} i j → slicearr (chase f g h i j)
      }
    ; antisym = λ {(α , f) (β , g)} h i → record
      { from = h
      ; to = i
      ; iso = record
        { isoˡ = mono f _ _ (chase f g f h i ○ ⟺ 𝒞.identityʳ)
        ; isoʳ = mono g _ _ (chase g f g i h ○ ⟺ 𝒞.identityʳ)
        }
      }
    }
  }
  where
    𝒞ᶜ : Category _ _ _
    𝒞ᶜ = slice-mono c

    module 𝒞ᶜ = Category 𝒞ᶜ

    open Mor 𝒞 using (_↣_)
    open MR 𝒞
    open 𝒞.HomReasoning
    open _↣_

    chase : ∀ {α β γ : 𝒞.Obj} (f : 𝒞 [ α ↣ c ]) (g : 𝒞 [ β ↣ c ]) (h : 𝒞 [ γ ↣ c ])
            → (i : 𝒞ᶜ [ (α , f) , (β , g) ]) → (j : 𝒞ᶜ [ (β , g) , (γ , h) ])
            → 𝒞 [ 𝒞 [ mor h ∘ 𝒞 [ Slice⇒.h j ∘ Slice⇒.h i ] ] ≈ mor f ]
    chase f g h i j = begin
      𝒞 [ mor h ∘ 𝒞 [ Slice⇒.h j ∘ Slice⇒.h i ] ] ≈⟨ pullˡ (Slice⇒.△ j)  ⟩
      𝒞 [ mor g ∘ Slice⇒.h i ]                    ≈⟨ Slice⇒.△ i ⟩
      mor f ∎

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

-- The code in this module should not be compiled. However, the
-- following re-exported code should be compiled.

open import Agda.Builtin.Bool public

postulate
  easy : {A : Set} → A

data Not-compiled : Set where

max_stars_repo_name: sseefried/agda


text:
module Bee2.Crypto.Defs where

open import Data.ByteString
open import Data.ByteVec
open import Agda.Builtin.Nat renaming (Nat to ℕ)

{-# FOREIGN GHC import qualified Bee2.Defs    #-}
postulate
  SizeT : Set
  SizeFromℕ : ℕ → SizeT
{-# COMPILE GHC SizeT = type (Bee2.Defs.Size) #-}
{-# COMPILE GHC SizeFromℕ =
    ( Prelude.fromIntegral ) #-}

Hash = ByteVec {Strict} 32

data SecurityLevel : Set where
  l128 l192 l256 : SecurityLevel


text:
module std-reduction.Properties where

open import std-reduction
open import sn-calculus

open import Relation.Binary.PropositionalEquality using (_≡_)
open _≡_

{-
std-redution-deterministic : ∀{p q r} →
                             p ⇁ q →
                             p ⇁ r →
                             q ≡ r
std-redution-deterministic = ?

std=>calc : ∀{p q} → p ⇁ q → p sn⟶₁ q
std=>calc = ?
-}

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
open import Agda.Builtin.Size

record R (A : Size → Set) (i : Size) : Set where
  field
    force : (j : Size< i) → A j

data D (A : Size → Set) (i : Size) : Set where
  c : R A i → D A i

postulate
  P : (A : Size → Set) → D A ∞ → D A ∞ → Set

F : (Size → Set) → Set
F A = (x : A ∞) (y : D A ∞) →
      P _ (c (record { force = λ j → x })) y

-- WAS:
-- x != ∞ of type Size
-- when checking that the expression y has type D (λ _ → A ∞) ∞

-- SHOULD BE:
-- x₁ != ∞ of type Size
-- when checking that the expression y has type D (λ _ → A ∞) ∞


text:
module Screen where

import Data.Nat
import Data.Bool
import Data.List
import Logic.Base

open Data.Bool
open Data.List
open Data.Nat
open Logic.Base

-- Ranges -----------------------------------------------------------------

data Range : Set where
  range : Nat -> Nat -> Range

inRange : Range -> Nat -> Bool
inRange (range lo hi) x = lo ≤ x && x ≤ hi

low : Range -> Nat
low (range lo _) = lo

high : Range -> Nat
high (range _ hi) = hi

size : Range -> Nat
size (range lo hi) = suc hi - lo

enumerate : Range -> List Nat
enumerate (range lo hi) = enum lo hi
  where
    list : Nat -> Nat -> List Nat
    list _ 0       = []
    list k (suc n) = k :: list (suc k) n

    enum : Nat -> Nat -> List Nat
    enum lo hi = map (_+_ lo) (list 0 (suc hi - lo))

-- The screen example -----------------------------------------------------

xRange : Range
xRange = range 0 79

yRange : Range
yRange = range 0 24

screenRange : Range
screenRange = range 0xb8000 0xb87ff

-- Converting (x,y) to addr

plot : Nat -> Nat -> Nat
plot x y = low screenRange + x + size xRange * y

-- The property

forAll : Range -> (Nat -> Bool) -> Bool
forAll r p = foldr (\n b -> p n && b) true (enumerate r)

prop : Bool
prop = forAll xRange \x ->
       forAll yRange \y ->
       inRange screenRange (plot x y)

proof : IsTrue prop
proof = tt


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

-- Approx. 15-20 min are required to typecheck this file (for Agda 2.6.1) on
-- my MacBook 13-inch 2017 with 3.5 GHz Core i7 CPU and 16 GB memory.
--
-- Since most of the time was spent for termination analysis, please
-- uncomment {-# TERMINATING #-} before evalR and eval to remove the
-- termination checks.

module Definitional where

open import Syntax

open import Data.Nat
open import Data.Fin using (Fin ; suc; zero)

open import Data.List using (length ; [] ; _∷_ )
open import Data.List.Properties using (length-++)
open import Data.Vec  using ([] ; _∷_)
open import Data.Vec.Relation.Unary.All using (All ; [] ; _∷_)
open import Data.Product

open import Relation.Binary.PropositionalEquality

open import Level renaming (zero to lzero ; suc to lsuc)
open ≡-Reasoning

open import Function using () renaming (case_of_ to CASE_OF_)

open import Value

open import Size
open import Codata.Thunk

module Interpreter where
  open import Codata.Delay renaming (length to dlength ; map to dmap )

  open import PInj
  open _⊢_⇔_

  -- A variant of the Delay monad in which the bind operator is
  -- frozen. While we cannot restrict levels in general, using Set is
  -- enough for enough for our purpose.

  data DELAY : (A : Set) -> (i : Size) -> Set₁ where
    Now   : ∀ {A i} -> A -> DELAY A i
    Later : ∀ {A i} -> Thunk (DELAY A) i -> DELAY A i
    Bind  : ∀ {A B i}
            -> (m : DELAY A i) -> (f : A -> DELAY B i) -> DELAY B i

  Never : ∀ {A i} -> DELAY A i
  Never = Later λ where .force -> Never

  Dmap : ∀ {A B i} -> (A -> B) -> DELAY A i -> DELAY B i
  Dmap f d = Bind d (λ x -> Now (f x))

  -- The function runD thaws the frozen operations.
  runD : ∀ {A : Set} {i : Size} -> DELAY A i -> Delay A i
  runD (Now x) = now x
  runD (Later x) = later λ where .force -> runD (force x)
  runD (Bind d f) = bind (runD d) (λ x -> runD (f x))

  -- The frozen version of _⊢_⇔_
  record _⊢F_⇔_ (i : Size) (A B : Set) : Set₁ where
    field
      Forward  : A -> DELAY B i
      Backward : B -> DELAY A i

  open _⊢F_⇔_

  forwardF  : ∀ {A B i} -> i ⊢F A ⇔ B -> A -> Delay B i
  forwardF h a = runD (Forward h a)

  backwardF : ∀ {A B i} -> i ⊢F A ⇔ B -> B -> Delay A i
  backwardF h b = runD (Backward h b)

  -- Similarly to runD, runD⇔ thawas the frozen operations in
  -- _⊢F_⇔_.
  runD⇔ : ∀ {A B i} -> i ⊢F A ⇔ B -> i ⊢ A ⇔ B
  forward  (runD⇔ f) = forwardF f
  backward (runD⇔ f) = backwardF f

  -- Environments handled by the forward and backward evaluations,
  -- which correponds to μ in the paper.
  data RValEnv : (Θ : TyEnv) (Ξ : MultEnv (length Θ)) -> Set where
    []   : RValEnv [] []
    skip : ∀ {Θ Ξ A} -> RValEnv Θ Ξ -> RValEnv (A ∷ Θ) (zero ∷ Ξ)
    _∷_  : ∀ {Θ Ξ A} -> Value [] ∅ A -> RValEnv Θ Ξ -> RValEnv (A ∷ Θ) (one ∷ Ξ)

  emptyRValEnv : ∀ {Θ} -> RValEnv Θ ∅
  emptyRValEnv {[]} = []
  emptyRValEnv {_ ∷ _} = skip emptyRValEnv

  splitRValEnv : ∀ {Θ Ξ₁ Ξ₂} -> RValEnv Θ (Ξ₁ +ₘ Ξ₂) -> RValEnv Θ Ξ₁ × RValEnv Θ Ξ₂
  splitRValEnv {[]} {[]} {[]} [] = [] , []
  splitRValEnv {_ ∷ Θ} {zero ∷ Ξ₁} {zero ∷ Ξ₂} (skip ρ)
    with splitRValEnv ρ
  ... | ρ₁ , ρ₂ = skip ρ₁ , skip ρ₂
  splitRValEnv {_ ∷ Θ} {zero ∷ Ξ₁} {one ∷ Ξ₂} (x ∷ ρ)
    with splitRValEnv ρ
  ... | ρ₁ , ρ₂ =  skip ρ₁ , x ∷ ρ₂
  splitRValEnv {_ ∷ Θ} {one ∷ Ξ₁} {zero ∷ Ξ₂} (x ∷ ρ)
    with splitRValEnv ρ
  ... | ρ₁ , ρ₂ = x ∷ ρ₁ , skip ρ₂

  -- An inverse of splitRValEnv.
  mergeRValEnv : ∀ {Θ Ξ₁ Ξ₂} -> all-no-omega (Ξ₁ +ₘ Ξ₂) -> RValEnv Θ Ξ₁ -> RValEnv Θ Ξ₂ -> RValEnv Θ (Ξ₁ +ₘ Ξ₂)
  mergeRValEnv {.[]} {.[]} {.[]} _ [] [] = []
  mergeRValEnv {.(_ ∷ _)} {.(zero ∷ _)} {.(zero ∷ _)} (_ ∷ ano) (skip ρ₁) (skip ρ₂) = skip (mergeRValEnv ano ρ₁ ρ₂)
  mergeRValEnv {.(_ ∷ _)} {.(zero ∷ _)} {.(one ∷ _)} (_ ∷ ano) (skip ρ₁) (x ∷ ρ₂) = x ∷ (mergeRValEnv ano ρ₁ ρ₂)
  mergeRValEnv {.(_ ∷ _)} {.(one ∷ _)} {.(zero ∷ _)} (_ ∷ ano) (x ∷ ρ₁) (skip ρ₂) = x ∷ mergeRValEnv ano ρ₁ ρ₂
  mergeRValEnv {.(_ ∷ _)} {.(one ∷ _)} {.(one ∷ _)} (() ∷ ano) (x ∷ ρ₁) (x₁ ∷ ρ₂)

  -- Construction of the empty value environment.
  from-all-zero : ∀ {Θ Ξ} -> all-zero Ξ -> RValEnv Θ Ξ
  from-all-zero {[]} {[]} [] = []
  from-all-zero {_ ∷ Θ} {.(zero ∷ _)} (refl ∷ az) = skip (from-all-zero az)

  -- Value environments conforms to an empty invertible environment must be empty.
  all-zero-canon : ∀ {Θ Ξ} -> (az : all-zero Ξ) -> (θ : RValEnv Θ Ξ) -> θ ≡ (from-all-zero az)
  all-zero-canon {[]} {[]} [] [] = refl
  all-zero-canon {_ ∷ Θ} {_ ∷ Ξ} (refl ∷ az) (skip θ) = cong skip (all-zero-canon az θ)

  -- Looking-up function for RValEnv
  lkup : ∀ {Θ A} {x : Θ ∋ A} {Ξ} -> varOk● Θ x Ξ -> RValEnv Θ Ξ -> Value [] ∅ A
  lkup (there ok) (skip ρ) = lkup ok ρ
  lkup (here ad) (x ∷ ρ) = x -- ad asserts ρ consists only of skip and []

  -- An inverse of lkup; the linearity matters here.
  unlkup : ∀ {Θ A} {x : Θ ∋ A} {Ξ} -> varOk● Θ x Ξ -> Value [] ∅ A -> RValEnv Θ Ξ
  unlkup (there ok) v = skip (unlkup ok v)
  unlkup (here ad) v = v ∷ from-all-zero ad

  -- Some utility functions.
  var●₀ : ∀ {A Θ} -> Residual (A ∷ Θ) (one ∷ ∅) (A ●)
  var●₀ = var● vz (here all-zero-∅)

  BindR : ∀ {i Θ Ξ A} {r : Set} -> DELAY (Value Θ Ξ (A ●)) i -> (Residual Θ Ξ (A ●) -> DELAY r i) -> DELAY r i
  BindR x f = Bind x λ { (red r) -> f r }

  -- For the do trick for the pattern matching
  -- See https://github.com/agda/agda/issues/2298
  _>>=_ : ∀ {a b : Level} {A : Set a} {B : A -> Set b} -> ∀ (x : A) -> (∀ x -> B x) -> B x
  x >>= f = f x

  -- Function application.
  apply :
    ∀ {Θ Ξ₁ Ξ₂ A m B} i ->
    all-no-omega (Ξ₁ +ₘ m ×ₘ Ξ₂) ->
    Value Θ Ξ₁ (A # m ~> B) -> Value Θ Ξ₂ A -> DELAY (Value Θ (Ξ₁ +ₘ m ×ₘ Ξ₂) B) i

  -- Forward, backward and unidirectional evalautions are given as
  -- mutually recursive functions. Notice that, the existence of these
  -- functions essentially proves the type safety (i.e., the
  -- preservation and progree prperty). Thus, in a sense, they are
  -- generalizations of Lemma 3.1 and Lemma 3.2 in the paper.

  -- Forward and backward evaluation.
  -- {-# TERMINATING #-}
  evalR :
    ∀ {Θ Ξ A} i ->
    all-no-omega Ξ -> Residual Θ Ξ (A ●) -> i ⊢F (RValEnv Θ Ξ) ⇔ Value [] ∅ A

  -- Unidirectional evaluation. Also, an important thing is that this function keeps
  -- the invariant all-no-omega (Ξₑ +ₘ Ξ) for recursive calls, which essentially supports
  -- the claim in Section 3.4: "This assumption is actually an invariant in our system ...".

  -- {-# TERMINATING #-}
  eval :
    ∀ {Θ Ξₑ Γ Δ Ξ A} i ->
    all-no-omega (Ξₑ +ₘ Ξ) -> ValEnv Γ Δ Θ Ξₑ -> Term Γ Δ Θ Ξ A -> DELAY (Value Θ (Ξₑ +ₘ Ξ) A) i

  apply {Θ} {Ξ₁} {Ξ₂} i ano (clo {Ξ' = Ξ'} {Ξₜ = Ξₜ} m refl θ t) v with all-no-omega-dist _ _ ano
  ... | ano-'t , ano-m2 = Later λ { .force {j} ->
        let T = eval j (subst all-no-omega lemma ano) (tup _ _ refl (value-to-multM ano-m2 v) θ) t
        in subst (λ x -> DELAY (Value Θ x _) j) (sym lemma) T
      }
    where
      lemma : Ξ' +ₘ Ξₜ +ₘ m ×ₘ Ξ₂ ≡ m ×ₘ Ξ₂ +ₘ Ξ' +ₘ Ξₜ
      lemma = trans (+ₘ-comm _ _)
                    (sym (+ₘ-assoc (m ×ₘ Ξ₂) Ξ' _))

  -- evalR is defined so that evalR ∞ ano r actually defines a
  -- bijection. See Invertiblity.agda for its proof.

  Forward  (evalR i ano unit●) _ = Now (unit refl)
  Backward (evalR i ano unit●) _ = Now emptyRValEnv

  Forward  (evalR i ano (letunit● r₁ r₂)) ρ = do
    ano₁ , ano₂ <- all-no-omega-dist _ _ ano
    ρ₁ , ρ₂ <- splitRValEnv ρ
    Bind (Forward (evalR i ano₁ r₁) ρ₁) λ { (unit eq) -> Forward (evalR i ano₂ r₂) ρ₂ }
  Backward (evalR i ano (letunit● r₁ r₂)) v = do
    ano₁ , ano₂ <- all-no-omega-dist _ _ ano
    Bind (Backward (evalR i ano₂ r₂) v) λ ρ₂ ->
     Bind (Backward (evalR i ano₁ r₁) (unit refl)) λ ρ₁ ->
      Now (mergeRValEnv ano ρ₁ ρ₂)

  Forward  (evalR i ano (pair● r₁ r₂)) ρ = do
    ano₁ , ano₂ <- all-no-omega-dist _ _ ano
    ρ₁  , ρ₂  <- splitRValEnv ρ
    Bind (Forward (evalR i ano₁ r₁) ρ₁) λ v₁ ->
     Bind (Forward (evalR i ano₂ r₂) ρ₂) λ v₂ ->
      Now (pair refl v₁ v₂)

  Backward (evalR i ano (pair● {A = A} {B} r₁ r₂)) (pair {Ξ₁ = []} {[]} spΞ v₁ v₂) = do
    ano₁ , ano₂ <- all-no-omega-dist _ _ ano
    Bind (Backward (evalR i ano₁ r₁) v₁) λ ρ₁ ->
     Bind (Backward (evalR i ano₂ r₂) v₂) λ ρ₂ ->
      Now (mergeRValEnv ano ρ₁ ρ₂)

  Forward (evalR i ano (letpair● r₁ r₂)) ρ = do
    ano₁ , ano₂ <- all-no-omega-dist _ _ ano
    ρ₁  , ρ₂  <- splitRValEnv ρ
    Bind (Forward (evalR i ano₁ r₁) ρ₁) λ {
      (pair {Ξ₁ = []} {[]} spΞ v₁ v₂ ) ->
        Forward (evalR i (one ∷ one ∷ ano₂) r₂) (v₁ ∷ v₂ ∷ ρ₂)
     }

  Backward (evalR i ano (letpair● r₁ r₂)) v = do
    ano₁ , ano₂ <-  all-no-omega-dist _ _ ano
    Bind (Backward (evalR i (one ∷ one ∷ ano₂) r₂) v) λ { (v₁ ∷ v₂ ∷ ρ₂) ->
      Bind (Backward (evalR i ano₁ r₁) (pair refl v₁ v₂)) λ ρ₁ ->
       Now (mergeRValEnv ano ρ₁ ρ₂)
     }

  Forward (evalR i ano (inl● r)) ρ = Bind (Forward (evalR i ano r) ρ) λ x -> Now (inl x)
  Backward (evalR i ano (inl● r)) v =
    CASE v OF λ {
      (inl v₁) -> Backward (evalR i ano r) v₁ ;
      (inr v₂) -> Never
    }

  Forward  (evalR i ano (inr● r)) ρ = Bind (Forward (evalR i ano r) ρ) λ x -> Now (inr x)
  Backward (evalR i ano (inr● r)) v =
    CASE v OF λ {
      (inl v₁) -> Never ;
      (inr v₂) -> Backward (evalR i ano r) v₂
    }

  Forward  (evalR i ano (case● {Γ₁ = Γ₁} {Γ₂} r refl θ₁ t₁ θ₂ t₂ f)) ρ = do
    ano₀ , ano- <- all-no-omega-dist _ _ ano
    ρ₀  , ρ-  <- splitRValEnv ρ
    Bind (Forward (evalR i ano₀ r) ρ₀) λ {
          (inl v₁) ->
            Bind (eval i (one ∷ ano-) (weakenΘ-valEnv Γ₁ (compat-ext-here ext-id) θ₁) t₁) λ { (red r₁) ->
              Later λ { .force {j} ->
                Bind (Forward (evalR j (one ∷ ano-) r₁) (v₁ ∷ ρ-)) λ v ->
                 Bind (apply j [] f v) λ {
                   (inl _) -> Now v ;
                   (inr _) -> Never
                  }
              }
            }
           ;
          (inr v₂) ->
            Bind (eval i (one ∷ ano-) (weakenΘ-valEnv Γ₂ (compat-ext-here ext-id) θ₂) t₂) λ { (red r₂) ->
              Later λ { .force {j} ->
                Bind (Forward (evalR j (one ∷ ano-) r₂) (v₂ ∷ ρ-)) λ v ->
                  Bind (apply j [] f v) λ {
                    (inl _) -> Never ;
                    (inr _) -> Now v
                  }
               }
            }
        }

  Backward (evalR i ano (case● {Γ₁ = Γ₁} {Γ₂} r refl θ₁ t₁ θ₂ t₂ f)) v = do
    ano₀ , ano- <- all-no-omega-dist _ _ ano
    Bind (apply i [] f v) λ {
      (inl _) ->
         Bind (eval i (one ∷ ano-) (weakenΘ-valEnv Γ₁ (compat-ext-here ext-id) θ₁) t₁) λ { (red r₁) ->
           Later λ { .force {j} ->
               Bind (Backward (evalR j (one ∷ ano-) r₁) v) λ { (v₁ ∷ ρ-) ->
                 Bind (Backward (evalR j ano₀ r) (inl v₁)) λ ρ₀ ->
                     Now (mergeRValEnv ano ρ₀ ρ-)
               }
            }
         }
      ;
      (inr _) ->
          Bind (eval i (one ∷ ano-) (weakenΘ-valEnv Γ₂ (compat-ext-here ext-id) θ₂) t₂) λ { (red r₂) ->
            Later λ where .force {j} ->
                             Bind (Backward (evalR j (one ∷ ano-) r₂) v) λ { (v₂ ∷ ρ-) ->
                               Bind (Backward (evalR j ano₀ r) (inr v₂)) λ ρ₀ ->
                                 Now (mergeRValEnv ano ρ₀ ρ-)
                             }
          }
     }

  Forward  (evalR i ano (var● x ok)) ρ = Now (lkup ok ρ)
  Backward (evalR i ano (var● x ok)) v  = Now (unlkup ok v)

  Forward (evalR i ano (pin r f))  ρ = do
    ano₁ , ano₂ <- all-no-omega-dist _ _ ano
    ρ₁  , ρ₂  <- splitRValEnv ρ
    Bind (Forward (evalR i ano₁ r) ρ₁) λ v₁ ->
      CASE f OF λ { (clo .omega refl θ t) →
        Later λ { .force {j} ->
           Bind (eval j ano₂ (tup ∅ _ (∅-lid _) (mult-omega (weakenΘ-value extendΘ v₁) refl) θ) t) λ {
            (red r₂) ->
              -- maybe another delaying would be needed here
              Bind (Forward (evalR j ano₂ r₂) ρ₂) λ v₂ ->
              Now (pair refl v₁ v₂)
           }
        }
      }

  Backward (evalR i ano (pin r (clo .omega refl θ t))) (pair {Ξ₁ = []} {[]} refl v₁ v₂) = do
    ano₁ , ano₂ <- all-no-omega-dist _ _ ano
    Later λ { .force {j} ->
      BindR (eval j ano₂ (tup ∅ _ (∅-lid _) (mult-omega (weakenΘ-value extendΘ v₁) refl) θ) t) λ r₂ ->
        Bind (Backward (evalR j ano₂ r₂) v₂) λ ρ₂ ->
        Bind (Backward (evalR j ano₁ r) v₁) λ ρ₁ ->
        Now (mergeRValEnv ano ρ₁ ρ₂)
     }

  -- The unidirectional evaluation, of which definition would be
  -- routine except for rather tedious manipulation of value
  -- environments.

  eval {Θ} _ ano θ (var x ok) = Now (subst (λ x -> Value Θ x _) (sym (∅-rid _)) (lookupVar θ ok))
  eval _ ano θ (abs m t) = Now (clo m refl θ t)

  eval {Θ} {Γ = Γ} i ano θ (app {Δ₁ = Δ₁} {Δ₂} {Ξ₁ = Ξ₁} {Ξ₂} {m = m} t₁ t₂)
      with separateEnv {Γ} Δ₁ (m ×ₘ Δ₂) θ
  ... | tup Ξₑ₁ Ξₑ₂ refl θ₁ θ₂ with eval i (proj₁ lemma) θ₁ t₁ | proj₂ lemma | un×ₘ-valEnv Γ θ₂
    where
      lemma' : Ξₑ₁ +ₘ Ξₑ₂ +ₘ (Ξ₁ +ₘ m ×ₘ Ξ₂) ≡ (Ξₑ₁ +ₘ Ξ₁) +ₘ (Ξₑ₂ +ₘ m ×ₘ Ξ₂)
      lemma' = +ₘ-transpose Ξₑ₁ Ξₑ₂ Ξ₁ (m ×ₘ Ξ₂)

      lemma : all-no-omega (Ξₑ₁ +ₘ Ξ₁) × all-no-omega (Ξₑ₂ +ₘ m ×ₘ Ξ₂)
      lemma = all-no-omega-dist (Ξₑ₁ +ₘ Ξ₁) _ (subst all-no-omega lemma' ano)
  ... | T₁ | ano-e2m2 | Ξₑ₂' , θ₂' , refl with (subst all-no-omega (sym (×ₘ-dist m Ξₑ₂' _)) ano-e2m2)
  ... | ano-m[e2'2] with eval i (all-no-omega-dist-×ₘ m (Ξₑ₂' +ₘ Ξ₂) ano-m[e2'2]) θ₂' t₂
  ... | T₂ =
    Bind T₁ (λ { (clo {Ξ' = Ξ'} {Ξₜ = Ξₜ} m spΞ θf t) → Bind T₂ λ v₂ ->
      Later λ { .force ->
        let lemma : m ×ₘ (Ξₑ₂' +ₘ Ξ₂) +ₘ Ξ' +ₘ Ξₜ ≡ Ξₑ₁ +ₘ m ×ₘ Ξₑ₂' +ₘ (Ξ₁ +ₘ m ×ₘ Ξ₂)
            lemma =
              begin
                m ×ₘ (Ξₑ₂' +ₘ Ξ₂) +ₘ Ξ' +ₘ Ξₜ
              ≡⟨ +ₘ-assoc (m ×ₘ (Ξₑ₂' +ₘ Ξ₂)) Ξ' _ ⟩
                m ×ₘ (Ξₑ₂' +ₘ Ξ₂) +ₘ (Ξ' +ₘ Ξₜ)
              ≡⟨ cong (_ +ₘ_) spΞ ⟩
                m ×ₘ (Ξₑ₂' +ₘ Ξ₂) +ₘ (Ξₑ₁ +ₘ Ξ₁)
              ≡⟨ cong (_+ₘ _) (×ₘ-dist m Ξₑ₂' Ξ₂) ⟩
                m ×ₘ Ξₑ₂' +ₘ m ×ₘ Ξ₂ +ₘ (Ξₑ₁ +ₘ Ξ₁)
              ≡⟨ +ₘ-transpose (m ×ₘ Ξₑ₂') (m ×ₘ Ξ₂) Ξₑ₁ _ ⟩
                m ×ₘ Ξₑ₂' +ₘ Ξₑ₁ +ₘ (m ×ₘ Ξ₂ +ₘ Ξ₁)
              ≡⟨ cong₂ (_+ₘ_) (+ₘ-comm _ _) (+ₘ-comm _ _) ⟩
                Ξₑ₁ +ₘ m ×ₘ Ξₑ₂' +ₘ (Ξ₁ +ₘ m ×ₘ Ξ₂)
              ∎

            lemma-ano : all-no-omega (m ×ₘ (Ξₑ₂' +ₘ Ξ₂) +ₘ Ξ' +ₘ Ξₜ)
            lemma-ano = subst all-no-omega (sym lemma) ano

        in (Bind (eval _ lemma-ano (tup (m ×ₘ (Ξₑ₂' +ₘ Ξ₂)) Ξ' refl (value-to-multM ano-m[e2'2] v₂) θf) t) λ v ->  Now (subst (λ Ξ -> Value Θ Ξ _) lemma v)
       )}
    })

  eval {Γ = Γ} _ ano θ (unit ad) with discardable-has-no-resources {Γ} θ ad
  ... | refl = Now (substV (sym (∅-lid _)) (unit refl))

  eval {Θ} {Ξₑ} {Γ} i ano θ (letunit {Δ₀ = Δ₀} {Δ} {Ξ₀ = Ξ₀} {Ξ} m t₀ t)
    with separateEnv {Γ} (m ×ₘ Δ₀) Δ θ
  ... | tup Ξₑ₁ Ξₑ₂ refl θ₁ θ₂
    with un×ₘ-valEnv Γ θ₁
  ... | Ξₑ₁' , θ₁' , refl
    with subst all-no-omega (+ₘ-transpose (m ×ₘ Ξₑ₁') Ξₑ₂ (m ×ₘ Ξ₀) _) ano
  ... | ano'
    with all-no-omega-dist (m ×ₘ Ξₑ₁' +ₘ m ×ₘ Ξ₀) _ ano'
  ... | ano-me1'm0 , ano-e2
    with eval i (all-no-omega-dist-×ₘ m (Ξₑ₁' +ₘ Ξ₀) (subst all-no-omega (sym (×ₘ-dist m Ξₑ₁' Ξ₀)) ano-me1'm0)) θ₁' t₀
  ... | T₀ = Bind T₀ λ { (unit emp-e1'0) →
      let lemma : Ξₑ₂ +ₘ Ξ ≡ (m ×ₘ Ξₑ₁' +ₘ Ξₑ₂) +ₘ ((m ×ₘ Ξ₀) +ₘ Ξ)
          lemma =
            begin
              Ξₑ₂ +ₘ Ξ
            ≡⟨ sym (∅-lid _) ⟩
              ∅ +ₘ (Ξₑ₂ +ₘ Ξ)
            ≡⟨ cong (_+ₘ (Ξₑ₂ +ₘ Ξ)) (sym (×ₘ∅ m)) ⟩
              m ×ₘ ∅ +ₘ (Ξₑ₂ +ₘ Ξ)
            ≡⟨ cong (λ h -> m ×ₘ h +ₘ (Ξₑ₂ +ₘ Ξ)) (emp-e1'0) ⟩
              m ×ₘ (Ξₑ₁' +ₘ Ξ₀) +ₘ (Ξₑ₂ +ₘ Ξ)
            ≡⟨ cong (_+ₘ _) (×ₘ-dist m Ξₑ₁' Ξ₀) ⟩
              m ×ₘ Ξₑ₁' +ₘ m ×ₘ Ξ₀ +ₘ (Ξₑ₂ +ₘ Ξ)
            ≡⟨ +ₘ-transpose (m ×ₘ Ξₑ₁') (m ×ₘ Ξ₀) Ξₑ₂ Ξ ⟩
              (m ×ₘ Ξₑ₁' +ₘ Ξₑ₂) +ₘ ((m ×ₘ Ξ₀) +ₘ Ξ)
            ∎
      in Dmap (substV lemma) (eval i ano-e2 θ₂ t)
   }

  eval {Θ} {Ξₑ} {Γ} i ano θ (pair {Δ₁ = Δ₁} {Δ₂} {Ξ₁ = Ξ₁} {Ξ₂} t₁ t₂)
    with separateEnv {Γ} Δ₁ Δ₂ θ
  ... | tup Ξₑ₁ Ξₑ₂ refl θ₁ θ₂
    with subst all-no-omega (+ₘ-transpose Ξₑ₁ Ξₑ₂ Ξ₁ _) ano
  ... | ano'
    with all-no-omega-dist (Ξₑ₁ +ₘ Ξ₁) _ ano'
  ... | ano-e11 , ano-e22
    with eval i ano-e11 θ₁ t₁ | eval i ano-e22 θ₂ t₂
  ... | T₁ | T₂ = Bind T₁ λ v₁ ->
                  Bind T₂ λ v₂ -> Now (pair (+ₘ-transpose Ξₑ₁ Ξ₁ Ξₑ₂ _) v₁ v₂)

  eval {Θ} {Ξₑ} {Γ} i ano θ (letpair {Δ₀ = Δ₀} {Δ} {Ξ₀ = Ξ₀} {Ξ} m t₀ t)
    with separateEnv {Γ} (m ×ₘ Δ₀) Δ θ
  ... | tup Ξₑ₁ Ξₑ₂ refl θ₁ θ₂
    with un×ₘ-valEnv Γ θ₁
  ... | Ξₑ₁' , θ₁' , refl
    with subst all-no-omega (+ₘ-transpose (m ×ₘ Ξₑ₁') Ξₑ₂ (m ×ₘ Ξ₀) Ξ) ano
  ... | ano'
    with all-no-omega-dist (m ×ₘ Ξₑ₁' +ₘ m ×ₘ Ξ₀) _ ano'
  ... | ano-me1'm0 , ano-e2-
    with subst all-no-omega (sym (×ₘ-dist m Ξₑ₁' _)) ano-me1'm0
  ... | ano-m[e1'0]
    with all-no-omega-dist-×ₘ m _ ano-m[e1'0]
  ... | ano-e1'0
    with eval i ano-e1'0 θ₁' t₀
  ... | T₀  = Bind T₀ λ { (pair {Ξ₁ = Ξ₁} {Ξ₂} spΞ v₁ v₂) →
                   let ano-m[12] : all-no-omega (m ×ₘ (Ξ₁ +ₘ Ξ₂))
                       ano-m[12] = subst all-no-omega (cong (m ×ₘ_) (sym spΞ)) ano-m[e1'0]

                       ano-m1m2 : all-no-omega (m ×ₘ Ξ₁ +ₘ m ×ₘ Ξ₂)
                       ano-m1m2 = subst all-no-omega (×ₘ-dist m Ξ₁ Ξ₂) ano-m[12]

                       an : all-no-omega (m ×ₘ Ξ₁) × all-no-omega (m ×ₘ Ξ₂)
                       an = all-no-omega-dist (m ×ₘ Ξ₁) _ ano-m1m2

                       eq : m ×ₘ Ξ₁ +ₘ (m ×ₘ Ξ₂ +ₘ Ξₑ₂) ≡ m ×ₘ Ξₑ₁' +ₘ m ×ₘ Ξ₀ +ₘ Ξₑ₂
                       eq = begin
                              m ×ₘ Ξ₁ +ₘ (m ×ₘ Ξ₂ +ₘ Ξₑ₂)
                            ≡⟨ sym (+ₘ-assoc (m ×ₘ Ξ₁) (m ×ₘ Ξ₂) _) ⟩
                              m ×ₘ Ξ₁ +ₘ m ×ₘ Ξ₂ +ₘ Ξₑ₂
                            ≡⟨ cong (_+ₘ Ξₑ₂) (sym (×ₘ-dist m Ξ₁ Ξ₂)) ⟩
                              m ×ₘ (Ξ₁ +ₘ Ξ₂) +ₘ Ξₑ₂
                            ≡⟨ cong (_+ₘ Ξₑ₂) (cong (m ×ₘ_) spΞ) ⟩
                              m ×ₘ (Ξₑ₁' +ₘ Ξ₀) +ₘ Ξₑ₂
                            ≡⟨ cong (_+ₘ Ξₑ₂) (×ₘ-dist m _ _) ⟩
                              m ×ₘ Ξₑ₁' +ₘ m ×ₘ Ξ₀ +ₘ Ξₑ₂
                            ∎

                       θ' : ValEnv (_ ∷ _ ∷ Γ) (M→M₀ m ∷ M→M₀ m ∷ Δ) Θ (m ×ₘ Ξₑ₁' +ₘ m ×ₘ Ξ₀ +ₘ Ξₑ₂)
                       θ' = tup (m ×ₘ Ξ₁) _ eq (value-to-multM (proj₁ an) v₁)
                                  (tup (m ×ₘ Ξ₂) Ξₑ₂ refl (value-to-multM (proj₂ an) v₂) θ₂)

                       eq' : m ×ₘ Ξₑ₁' +ₘ m ×ₘ Ξ₀ +ₘ Ξₑ₂ +ₘ Ξ ≡ (m ×ₘ Ξₑ₁' +ₘ Ξₑ₂) +ₘ (m ×ₘ Ξ₀ +ₘ Ξ)
                       eq' = begin
                              m ×ₘ Ξₑ₁' +ₘ m ×ₘ Ξ₀ +ₘ Ξₑ₂ +ₘ Ξ
                             ≡⟨ +ₘ-assoc (m ×ₘ Ξₑ₁' +ₘ m ×ₘ Ξ₀) Ξₑ₂ _ ⟩
                              m ×ₘ Ξₑ₁' +ₘ m ×ₘ Ξ₀ +ₘ (Ξₑ₂ +ₘ Ξ)
                             ≡⟨ +ₘ-transpose (m ×ₘ Ξₑ₁') (m ×ₘ Ξ₀) Ξₑ₂ _ ⟩
                              (m ×ₘ Ξₑ₁' +ₘ Ξₑ₂) +ₘ (m ×ₘ Ξ₀ +ₘ Ξ)
                             ∎
                           -- solve 4 (λ a b c d ->
                           --                 ((a ⊞ b) ⊞ c) ⊞ d ⊜
                           --                 (a ⊞ c) ⊞ (b ⊞ d)) refl (m ×ₘ Ξₑ₁') (m ×ₘ Ξ₀) Ξₑ₂ Ξ
                   in Dmap (substV eq') (eval i (subst all-no-omega (sym eq') ano) θ' t)
              }

  eval {Θ} {Ξₑ} {Γ} i ano θ (many m t) = do
    (Ξₑ' , θ' , refl) <- un×ₘ-valEnv Γ θ
    ano-m[e'-] <- subst all-no-omega (sym (×ₘ-dist m Ξₑ' _)) ano
    ano-e'- <- all-no-omega-dist-×ₘ m _ ano-m[e'-]
    Bind (eval i ano-e'- θ' t) λ v ->
      Now (many m (×ₘ-dist m Ξₑ' _) v)

  eval {Θ} {Ξₑ} {Γ} i ano θ (unmany {Δ₀ = Δ₀} {Δ} {Ξ₀ = Ξ₀} {Ξ} {m₀ = m₀} {A} m t₀ t) = do
    tup Ξₑ₁ Ξₑ₂ refl θ₁ θ₂  <- separateEnv {Γ} (m ×ₘ Δ₀) Δ θ
    Ξₑ₁' , θ₁' , refl <-  un×ₘ-valEnv Γ θ₁
    ano' <- subst all-no-omega (+ₘ-transpose (m ×ₘ Ξₑ₁') Ξₑ₂ (m ×ₘ Ξ₀) Ξ) ano
    ano-me1'm0 , ano-e2 <-  all-no-omega-dist (m ×ₘ Ξₑ₁' +ₘ m ×ₘ Ξ₀) _ ano'
    ano-m[e1'0] <- subst all-no-omega (sym (×ₘ-dist m Ξₑ₁' _)) ano-me1'm0
    ano-e1'0    <- all-no-omega-dist-×ₘ m _ ano-m[e1'0]
    Bind (eval i ano-e1'0 θ₁' t₀ ) λ where
      (many {Ξ₀ = Ξ''} .m₀ sp v₀) -> do
        let ano-mm₀[e1'0] : all-no-omega (m ×ₘ m₀ ×ₘ Ξ'')
            ano-mm₀[e1'0] = subst all-no-omega (cong (m ×ₘ_) (sym sp)) ano-m[e1'0]

            ano-mul[e1'0] : all-no-omega (mul m m₀ ×ₘ Ξ'')
            ano-mul[e1'0] = subst all-no-omega (sym (mul-×ₘ m m₀ Ξ'')) ano-mm₀[e1'0]

            eq : m ×ₘ Ξₑ₁' +ₘ m ×ₘ Ξ₀ +ₘ (Ξₑ₂ +ₘ Ξ) ≡ mul m m₀ ×ₘ Ξ'' +ₘ Ξₑ₂ +ₘ Ξ
            eq =
              begin
                m ×ₘ Ξₑ₁' +ₘ m ×ₘ Ξ₀ +ₘ (Ξₑ₂ +ₘ Ξ)
                ≡⟨ cong (_+ₘ _) (sym (×ₘ-dist m Ξₑ₁' _)) ⟩
                m ×ₘ (Ξₑ₁' +ₘ Ξ₀) +ₘ (Ξₑ₂ +ₘ Ξ)
                ≡⟨ cong (λ e -> m ×ₘ e +ₘ _) (sym sp) ⟩
                m ×ₘ m₀ ×ₘ Ξ'' +ₘ (Ξₑ₂ +ₘ Ξ)
                ≡⟨ cong (_+ₘ _) (sym (mul-×ₘ m m₀ Ξ'')) ⟩
                mul m m₀ ×ₘ Ξ'' +ₘ (Ξₑ₂ +ₘ Ξ)
                ≡⟨ sym (+ₘ-assoc _ _ _) ⟩
                mul m m₀ ×ₘ Ξ'' +ₘ Ξₑ₂ +ₘ Ξ
              ∎

            ano'' : all-no-omega (mul m m₀ ×ₘ Ξ'' +ₘ Ξₑ₂ +ₘ Ξ)
            ano'' = subst all-no-omega eq ano'

            θ' : ValEnv (A ∷ Γ) (M→M₀ (mul m m₀) ∷ Δ) Θ (mul m m₀ ×ₘ Ξ'' +ₘ Ξₑ₂)
            θ' = tup _ Ξₑ₂ refl (value-to-multM ano-mul[e1'0] v₀) θ₂
        Bind (eval i ano'' θ' t) λ v -> Now (substV (trans (sym eq) (sym (+ₘ-transpose (m ×ₘ Ξₑ₁') Ξₑ₂ (m ×ₘ Ξ₀) Ξ))) v)

  eval i ano θ (inl t) = Dmap inl (eval i ano θ t)
  eval i ano θ (inr t) = Dmap inr (eval i ano θ t)
  eval {Θ} {Ξₑ = Ξₑ} {Γ} i ano θ (case {Δ₀ = Δ₀} {Δ} {Ξ₀ = Ξ₀} {Ξ} m t₀ t₁ t₂)
    with separateEnv {Γ} (m ×ₘ Δ₀) Δ θ
  ... | tup Ξₑ₁ Ξₑ₂ refl θ₁ θ₂
    with un×ₘ-valEnv Γ θ₁
  ... | Ξₑ₁' , θ₁' , refl
    with subst all-no-omega (+ₘ-transpose (m ×ₘ Ξₑ₁') Ξₑ₂ (m ×ₘ Ξ₀) Ξ) ano
  ... | ano'
    with all-no-omega-dist (m ×ₘ Ξₑ₁' +ₘ m ×ₘ Ξ₀) _ ano'
  ... | ano-me1'm0 , ano-e2-
    with subst all-no-omega (sym (×ₘ-dist m Ξₑ₁' _)) ano-me1'm0
  ... | ano-m[e1'0]
    with all-no-omega-dist-×ₘ m _ ano-m[e1'0]
  ... | ano-e1'0
    with eval i ano-e1'0 θ₁' t₀
  ... | T₀ =  Bind T₀ λ {
                (inl v) →
                  let θ' : ValEnv (_ ∷ Γ) (M→M₀ m ∷ Δ) Θ (m ×ₘ (Ξₑ₁' +ₘ Ξ₀) +ₘ Ξₑ₂)
                      θ' = tup (m ×ₘ (Ξₑ₁' +ₘ Ξ₀)) Ξₑ₂ refl (value-to-multM ano-m[e1'0] v) θ₂
                  in Dmap (substV lemma) (eval i (subst all-no-omega (sym lemma) ano) θ' t₁) ;
                (inr v) →
                  let θ' : ValEnv (_ ∷ Γ) (M→M₀ m ∷ Δ) Θ (m ×ₘ (Ξₑ₁' +ₘ Ξ₀) +ₘ Ξₑ₂)
                      θ' = tup (m ×ₘ (Ξₑ₁' +ₘ Ξ₀)) Ξₑ₂ refl (value-to-multM ano-m[e1'0] v) θ₂
                  in Dmap (substV lemma) (eval i (subst all-no-omega (sym lemma) ano) θ' t₂)
              }
      where
        lemma : m ×ₘ (Ξₑ₁' +ₘ Ξ₀) +ₘ Ξₑ₂ +ₘ Ξ ≡
                (m ×ₘ Ξₑ₁' +ₘ Ξₑ₂) +ₘ (m ×ₘ Ξ₀ +ₘ Ξ)
        lemma =
          begin
            m ×ₘ (Ξₑ₁' +ₘ Ξ₀) +ₘ Ξₑ₂ +ₘ Ξ
          ≡⟨ cong (λ x -> x +ₘ Ξₑ₂ +ₘ Ξ) (×ₘ-dist m Ξₑ₁' _) ⟩
            m ×ₘ Ξₑ₁' +ₘ m ×ₘ Ξ₀ +ₘ Ξₑ₂ +ₘ Ξ
          ≡⟨ +ₘ-assoc (m ×ₘ Ξₑ₁' +ₘ m ×ₘ Ξ₀) Ξₑ₂ _ ⟩
            m ×ₘ Ξₑ₁' +ₘ m ×ₘ Ξ₀ +ₘ (Ξₑ₂ +ₘ Ξ)
          ≡⟨ +ₘ-transpose _ _ _ _ ⟩
           (m ×ₘ Ξₑ₁' +ₘ Ξₑ₂) +ₘ (m ×ₘ Ξ₀ +ₘ Ξ)
          ∎

  eval i ano θ (roll t) = Dmap roll (eval i ano θ t)
  eval i ano θ (unroll t) =
   Bind (eval i ano θ t) λ { (roll v) → Later λ where .force -> Now v  }

  eval {Γ = Γ} i ano θ (unit● ad) with discardable-has-no-resources {Γ} θ ad
  ... | refl = Now (red (substR (sym (∅-lid _)) unit●))

  eval {Θ} {Ξₑ} {Γ} i ano θ (letunit● {Δ₀ = Δ₀} {Δ} {Ξ₀ = Ξ₀} {Ξ} t₀ t) = do
    tup Ξₑ₁ Ξₑ₂ refl θ₁ θ₂ <- separateEnv {Γ} Δ₀ Δ θ
    let lemma : Ξₑ₁ +ₘ Ξₑ₂ +ₘ (Ξ₀ +ₘ Ξ) ≡ Ξₑ₁ +ₘ Ξ₀ +ₘ (Ξₑ₂ +ₘ Ξ)
        lemma = +ₘ-transpose _ _ _ _
    let ano' = subst all-no-omega lemma ano
    ano-e10 , ano-e2- <- all-no-omega-dist (Ξₑ₁ +ₘ Ξ₀) _ ano'
    BindR (eval i ano-e10 θ₁ t₀) λ E₀ ->
     BindR (eval i ano-e2- θ₂ t) λ E ->
       Now (red (substR (sym lemma) (letunit● E₀ E)))

  eval {Θ} {Ξₑ} {Γ} i ano θ (pair● {Δ₁ = Δ₁} {Δ₂} {Ξ₁ = Ξ₁} {Ξ₂} t₁ t₂) = do
    tup Ξₑ₁ Ξₑ₂ refl θ₁ θ₂ <- separateEnv {Γ} Δ₁ Δ₂ θ
    let lemma : Ξₑ₁ +ₘ Ξₑ₂ +ₘ (Ξ₁ +ₘ Ξ₂) ≡ Ξₑ₁ +ₘ Ξ₁ +ₘ (Ξₑ₂ +ₘ Ξ₂)
        lemma = +ₘ-transpose _ _ _ _
    let ano' = subst all-no-omega lemma ano
    ano-e11 , ano-e22 <- all-no-omega-dist (Ξₑ₁ +ₘ Ξ₁) _ ano'
    BindR (eval i ano-e11 θ₁ t₁) λ E₁ ->
      BindR (eval i ano-e22 θ₂ t₂) λ E₂ ->
        Now (red (substR (sym lemma) (pair● E₁ E₂)))

  eval {Θ} {Ξₑ} {Γ} i ano θ (letpair● {Δ₀ = Δ₀} {Δ} {Ξ₀ = Ξ₀} {Ξ} t₀ t)
    with separateEnv {Γ} Δ₀ Δ θ
  ... | tup Ξₑ₁ Ξₑ₂ refl θ₁ θ₂
    with subst all-no-omega (+ₘ-transpose Ξₑ₁ Ξₑ₂ Ξ₀ _) ano
  ... | ano'
    with all-no-omega-dist (Ξₑ₁ +ₘ Ξ₀) _ ano'
  ... | ano-e10 , ano-e2-
    with eval i ano-e10 θ₁ t₀ | eval i (one ∷ one ∷ ano-e2-) (weakenΘ-valEnv Γ (compat-ext-here (compat-ext-here ext-id)) θ₂) t
  ... | T₁ | T =
    Bind T₁ λ { (red E₁) ->
     Bind T  λ { (red E ) ->
       Now (red (substR (+ₘ-transpose Ξₑ₁ Ξ₀ _ _) (letpair● E₁ E)))
     }}

  eval i ano θ (inl● t) =
    BindR (eval i ano θ t) λ E -> Now (red (inl● E))

  eval i ano θ (inr● t) =
    BindR (eval i ano θ t) λ E -> Now (red (inr● E))

  eval {Θ} {Ξₑ} {Γ} i ano θ (case● {Δ₀ = Δ₀} {Δ} {Δ'} {Ξ₀ = Ξ₀} {Ξ} {Ξ'} t t₁ t₂ t₃)
    with separateEnv {Γ} (Δ₀ +ₘ Δ) _ θ
  ... | tup Ξₑ₁₂ Ξₑ₃ refl θ' θ₃
    with discardable-has-no-resources {Γ} θ₃ (omega×ₘ-discardable Δ')
  ... | refl
    with un×ₘ-valEnv Γ θ₃
  ... | Ξₑ₃' , θ₃' , eq
    with omega×ₘ∅-inv Ξₑ₃' eq
  ... | refl
    with separateEnv {Γ} Δ₀ Δ θ'
  ... | tup Ξₑ₁ Ξₑ₂ refl θ₁ θ₂
    with subst all-no-omega lemma ano | lemma
    where
      open import Algebra.Solver.CommutativeMonoid (+ₘ-commutativeMonoid (length Θ))
                  renaming (_⊕_ to _⊞_)

      lemma : Ξₑ₁ +ₘ Ξₑ₂ +ₘ ∅ +ₘ (Ξ₀ +ₘ Ξ +ₘ omega ×ₘ Ξ')
              ≡ (Ξₑ₁ +ₘ Ξ₀) +ₘ (Ξₑ₂ +ₘ Ξ) +ₘ omega ×ₘ Ξ'
      lemma = solve 5 (\a b c d e -> ((a ⊞ b) ⊞ id) ⊞ ((c ⊞ d) ⊞ e)
                                     ⊜ ((a ⊞ c) ⊞ (b ⊞ d)) ⊞ e) refl Ξₑ₁ Ξₑ₂ Ξ₀ Ξ (omega ×ₘ Ξ')
  ... | ano' | lemma
    with all-no-omega-dist ((Ξₑ₁ +ₘ Ξ₀) +ₘ (Ξₑ₂ +ₘ Ξ)) _ ano'
  ... | ano'' , ano₃
    with all-no-omega-dist (Ξₑ₁ +ₘ Ξ₀) _ ano''
  ... | ano-e10 , ano-e2-
    with all-no-omega-omega×ₘ Ξ' ano₃
  ... | refl
    with eval i ano-e10 θ₁ t | eval i (subst all-no-omega (sym (∅-lid _)) all-no-omega-∅) θ₃' t₃
  ... | T | T₃ =
        Bind T λ { (red r) ->
        Bind T₃ λ { f ->
          Now (red (substR (trans lemma' (sym lemma))
            let f' = weakenΘ-value smashΘ (subst (λ x -> Value Θ x _) (∅-lid ∅) f)
            in (case● r refl θ₂ t₁ θ₂ t₂ f')))
        }
        }
      where
        lemma' : Ξₑ₁ +ₘ Ξ₀ +ₘ (Ξₑ₂ +ₘ Ξ)
                 ≡ Ξₑ₁ +ₘ Ξ₀ +ₘ (Ξₑ₂ +ₘ Ξ) +ₘ omega ×ₘ ∅
        lemma' =
          sym (trans (cong (λ x -> Ξₑ₁ +ₘ Ξ₀ +ₘ (Ξₑ₂ +ₘ Ξ) +ₘ x)
                           (×ₘ∅ omega))
                     (∅-rid (Ξₑ₁ +ₘ Ξ₀ +ₘ (Ξₑ₂ +ₘ Ξ) )))

  eval {Θ} {Ξₑ} {Γ} i ano θ (var● x ad ok)
    with discardable-has-no-resources {Γ} θ ad
  ... | refl = Now (red (substR (sym (∅-lid _)) (var● x ok)))

  eval {Θ} {Ξₑ} {Γ} i ano θ (pin {Δ₁ = Δ₁} {Δ₂} {Ξ₁ = Ξ₁} {Ξ₂} t₁ t₂) = do
    tup Ξₑ₁ Ξₑ₂ refl θ₁ θ₂  <- separateEnv {Γ} Δ₁ Δ₂ θ
    let ano' = subst all-no-omega (+ₘ-transpose Ξₑ₁ Ξₑ₂ Ξ₁ _) ano
    ano-e11 , ano-e22 <- all-no-omega-dist (Ξₑ₁ +ₘ Ξ₁) _ ano'
    BindR (eval i ano-e11 θ₁ t₁) λ r ->
      Bind (eval i ano-e22 θ₂ t₂) λ v ->
        Now (red (substR (+ₘ-transpose _ _ _ _) (pin r v)))

  eval {Γ = Γ} i ano θ (unlift e) = do
    Ξ' , θ' , refl <- un×ₘ-valEnv Γ θ
    ano₁ , ano₂  <- all-no-omega-dist _ _ ano
    refl <- all-no-omega-omega×ₘ _ ano₁
    refl <- all-no-omega-omega×ₘ _ ano₂
    Bind (eval i (subst all-no-omega (sym (∅-lid ∅)) all-no-omega-∅ ) θ' e) λ v ->
      BindR (apply i (one ∷ subst all-no-omega (sym lemma₁) all-no-omega-∅) (weakenΘ-value (compat-ext-here ext-id) v) (red var●₀)) λ r ->
        Now (substV (sym lemma₂) (inj refl (weakenΘ-residual (compat-skip smashΘ) (substR (cong (one ∷_) lemma₁) r) )))
    where
      open import Data.Vec.Properties using (map-id)
      lemma₁ : ∀ {n} -> ∅ +ₘ ∅ +ₘ Data.Vec.map (λ y -> y) ∅ ≡ ∅ {n}
      lemma₁ {n} rewrite map-id (∅ {n}) | ∅-rid {n} ∅ = ∅-lid ∅

      lemma₂ : ∀ {n} -> omega ×ₘ ∅ +ₘ omega ×ₘ ∅ ≡ ∅ {n}
      lemma₂ {n} rewrite ×ₘ∅ {n} omega | ∅-lid {n} ∅ = refl

  eval {Γ = Γ} i ano θ (fapp e₁ e₂) = do
    anoₑ , ano'  <- all-no-omega-dist _ _ ano
    ano₁ , ano'' <- all-no-omega-dist _ _ ano'
    refl <- all-no-omega-omega×ₘ _ ano''
    tup Ξₑ₁ Ξₑ₂ refl θ₁ θ₂  <- separateEnv {Γ} _ _ θ
    Ξₑ₂' , θ₂' , refl <- un×ₘ-valEnv Γ θ₂
    ano₁' , _ <- all-no-omega-dist _ _ (subst all-no-omega lemma' ano)
    Bind (eval i ano₁' θ₁ e₁) λ {
      (inj spΞ r) → do
        refl , refl <- ∅+ₘ∅-inv _ _ (sym spΞ)
        refl <- all-no-omega-omega×ₘ _ (subst all-no-omega (∅-lid _) anoₑ)
        Bind (eval i (subst all-no-omega (sym (∅-lid ∅)) all-no-omega-∅) θ₂' e₂) λ v -> Later λ { .force {j} ->
           Bind (Forward (evalR j (one ∷ all-no-omega-∅) r) (weakenΘ-value smashΘ (substV (∅-lid ∅) v) ∷ [])) λ v' ->
            Now (substV (sym lemma) (weakenΘ-value extendΘ v'))
         }
     }
    where
      lemma' : ∀ {n} {Ξₑ₁ Ξ₁ X Y : MultEnv n} -> Ξₑ₁ +ₘ X +ₘ (Ξ₁ +ₘ Y) ≡ Ξₑ₁ +ₘ Ξ₁ +ₘ (X +ₘ Y)
      lemma' {n} {A} {B} {C} {D} = +ₘ-transpose A C B D

      lemma : ∀ {n} -> ∅ +ₘ omega ×ₘ ∅ +ₘ (∅ +ₘ omega ×ₘ ∅) ≡ ∅ {n}
      lemma {n} rewrite ×ₘ∅ {n} omega | ∅-lid {n} ∅ = ∅-lid ∅

  eval {Γ = Γ} i ano θ (bapp e₁ e₂) = do
    anoₑ , ano'  <- all-no-omega-dist _ _ ano
    ano₁ , ano'' <- all-no-omega-dist _ _ ano'
    refl <- all-no-omega-omega×ₘ _ ano''
    tup Ξₑ₁ Ξₑ₂ refl θ₁ θ₂  <- separateEnv {Γ} _ _ θ
    Ξₑ₂' , θ₂' , refl <- un×ₘ-valEnv Γ θ₂
    ano₁' , _ <- all-no-omega-dist _ _ (subst all-no-omega lemma' ano)
    Bind (eval i ano₁' θ₁ e₁) λ {
      (inj spΞ r) → do
        refl , refl <- ∅+ₘ∅-inv _ _ (sym spΞ)
        refl <- all-no-omega-omega×ₘ _ (subst all-no-omega (∅-lid _) anoₑ)
        Bind (eval i (subst all-no-omega (sym (∅-lid ∅)) all-no-omega-∅) θ₂' e₂) λ v -> Later λ { .force {j} ->
          Bind (Backward (evalR j (one ∷ all-no-omega-∅) r) (weakenΘ-value smashΘ (substV (∅-lid ∅) v))) λ { (v' ∷ []) ->
             Now (substV (sym lemma) (weakenΘ-value extendΘ v'))
           }
         }
     }
    where
      lemma' : ∀ {n} {Ξₑ₁ Ξ₁ X Y : MultEnv n} -> Ξₑ₁ +ₘ X +ₘ (Ξ₁ +ₘ Y) ≡ Ξₑ₁ +ₘ Ξ₁ +ₘ (X +ₘ Y)
      lemma' {n} {A} {B} {C} {D} = +ₘ-transpose A C B D

      lemma : ∀ {n} -> ∅ +ₘ omega ×ₘ ∅ +ₘ (∅ +ₘ omega ×ₘ ∅) ≡ ∅ {n}
      lemma {n} rewrite ×ₘ∅ {n} omega | ∅-lid {n} ∅ = ∅-lid ∅

open Interpreter public

max_stars_repo_name: kztk-m/sparcl-agda

max_issues_repo_name: kztk-m/sparcl-agda

max_forks_repo_name: kztk-m/sparcl-agda


text:
module Oscar.Data.Equality.properties where

-- open import Relation.Binary.PropositionalEquality public using (cong; cong₂; cong-app; subst; subst₂; sym; trans)

-- open import Oscar.Data.Equality
-- open import Oscar.Function
-- open import Oscar.Level
-- open import Oscar.Relation

-- -- ≡̇-refl : ∀ {a} {A : Set a} {b} {B : A → Set b} (f : (x : A) → B x) → f ≡̇ f
-- -- ≡̇-refl _ _ = refl

-- -- ≡̇-sym : ∀ {a} {A : Set a} {b} {B : A → Set b} {f g : (x : A) → B x} → f ≡̇ g → g ≡̇ f
-- -- ≡̇-sym f≡̇g = sym ∘ f≡̇g

-- -- ≡̇-trans : ∀ {a} {A : Set a} {b} {B : A → Set b} {f g : (x : A) → B x} → f ≡̇ g → {h : (x : A) → B x} → g ⟨ _≡̇ h ⟩→ f
-- -- ≡̇-trans f≡̇g g≡̇h x = trans (f≡̇g x) (g≡̇h x)

-- -- -- open import Oscar.Category.Setoid

-- -- -- instance

-- -- --   IsEquivalencePropositionalEquality : ∀ {a} {A : Set a} → IsEquivalence (_≡_ {A = A})
-- -- --   IsEquivalence.reflexivity IsEquivalencePropositionalEquality _ = refl
-- -- --   IsEquivalence.symmetry IsEquivalencePropositionalEquality = sym
-- -- --   IsEquivalence.transitivity IsEquivalencePropositionalEquality = λ ‵ → trans ‵

-- -- --   IsEquivalenceIndexedPropositionalEquality : ∀ {a} {A : Set a} {b} {B : A → Set b} → IsEquivalence (_≡̇_ {B = B})
-- -- --   IsEquivalence.reflexivity IsEquivalenceIndexedPropositionalEquality = ≡̇-refl
-- -- --   IsEquivalence.symmetry IsEquivalenceIndexedPropositionalEquality = ≡̇-sym
-- -- --   IsEquivalence.transitivity IsEquivalenceIndexedPropositionalEquality = ≡̇-trans

-- -- -- instance

-- -- --   IsSetoidPropositionalEquality : ∀ {a} {A : Set a} → IsSetoid A a
-- -- --   IsSetoid._≋_ IsSetoidPropositionalEquality = _≡_

-- -- --   IsSetoidIndexedPropositionalEquality : ∀ {a} {A : Set a} {b} {B : A → Set b} → IsSetoid ((x : A) → B x) (a ⊔ b)
-- -- --   IsSetoid._≋_ IsSetoidIndexedPropositionalEquality = _≡̇_

-- -- -- setoidPropositionalEquality : ∀ {a} (A : Set a) → Setoid a a
-- -- -- Setoid.⋆ (setoidPropositionalEquality A) = A

-- -- -- setoidIndexedPropositionalEquality : ∀ {a} {A : Set a} {b} (B : A → Set b) → Setoid (a ⊔ b) (a ⊔ b)
-- -- -- Setoid.⋆ (setoidIndexedPropositionalEquality {A = A} B) = (x : A) → B x
-- -- -- Setoid.isSetoid (setoidIndexedPropositionalEquality B) = IsSetoidIndexedPropositionalEquality {B = B}

-- -- -- open import Oscar.Category.Action

-- -- -- actionΣ : ∀ {a} {A : Set a} {b} (B : A → Set b) → Action A b b
-- -- -- Action.𝔄 (actionΣ B) x = setoidPropositionalEquality (B x)

-- -- -- _⇒_ : ∀ {a} (A : Set a) {b} (B : Set b) → Setoid _ _
-- -- -- _⇒_ A B = setoidIndexedPropositionalEquality {A = A} λ _ → B

-- -- -- open import Oscar.Category.Semigroupoid
-- -- -- open import Oscar.Category.Morphism

-- -- -- ⇧ : ∀ {a} {A : Set a} {b} (B : A → A → Set b) → Morphism A b b
-- -- -- Morphism._⇒_ (⇧ B) x y = setoidPropositionalEquality (B x y)

-- -- -- _⇨_ : ∀ {a} {A : Set a} {b} (B : A → Set b) {c} (C : A → Set c) → Morphism A (b ⊔ c) (b ⊔ c)
-- -- -- Morphism._⇒_ (B ⇨ C) = λ m n → B m ⇒ C n

-- -- -- IsSemigroupoid⋆ : ∀ {a} {A : Set a} {b} {B : A → Set b} {c} {C : A → Set c}
-- -- --                     (let _↦_ = λ m n → B m → C n)
-- -- --                     (_∙_ : ∀ {y z} → y ↦ z → ∀ {x} → x ↦ y → x ↦ z) → Set (lsuc (a ⊔ b ⊔ c))
-- -- -- IsSemigroupoid⋆ _∙_ = IsSemigroupoid (_ ⇨ _) _∙_

-- -- -- Semigroupoid⋆ :
-- -- --   ∀ {a} {A : Set a} {b} {B : A → Set b} {c} {C : A → Set c}
-- -- --                     (let _↦_ = λ m n → B m → C n)
-- -- --                     (_∙_ : ∀ {y z} → y ↦ z → ∀ {x} → x ↦ y → x ↦ z)
-- -- --     ⦃ _ : IsSemigroupoid⋆ _∙_ ⦄
-- -- --     → Semigroupoid _ _ _
-- -- -- Semigroupoid⋆ _∙_ = _ ⇨ _ , _∙_

-- -- -- open import Oscar.Category.Semigroupoid

-- -- -- instance

-- -- --   isSemigroupoidFunctions≡̇ : ∀ {a} {A : Set a} {b} {B : A → Set b} → IsSemigroupoid (B ⇨ B) (λ g f → g ∘ f)
-- -- --   IsSemigroupoid.extensionality isSemigroupoidFunctions≡̇ {f₂ = f₂} f₁≡̇f₂ g₁≡̇g₂ x rewrite f₁≡̇f₂ x = g₁≡̇g₂ (f₂ x)
-- -- --   IsSemigroupoid.associativity isSemigroupoidFunctions≡̇ _ _ _ _ = refl

-- -- -- semigroupoidFunction : ∀ {a} {A : Set a} {b} (B : A → Set b) → Semigroupoid _ _ _
-- -- -- semigroupoidFunction B = B ⇨ B , (λ ‵ → _∘_ ‵)

-- -- -- open import Oscar.Category.Category

-- -- -- instance

-- -- --   isCategoryFunctions≡̇ : ∀ {a} {A : Set a} {b} {B : A → Set b} → IsCategory (semigroupoidFunction B) id
-- -- --   IsCategory.left-identity isCategoryFunctions≡̇ _ _ = refl
-- -- --   IsCategory.right-identity isCategoryFunctions≡̇ _ _ = refl

-- -- -- categoryFunction : ∀ {a} {A : Set a} {b} (B : A → Set b) → Category _ _ _
-- -- -- categoryFunction B = semigroupoidFunction B , id

-- -- -- -- -- open import Oscar.Property.Reflexivity

-- -- -- -- -- instance Reflexivity≡ : ∀ {a} {A : Set a} → Reflexivity (_≡_ {A = A})
-- -- -- -- -- Reflexivity.reflexivity Reflexivity≡ _ = refl

-- -- -- -- -- instance Reflexivity≡̇ : ∀ {a} {A : Set a} {b} {B : A → Set b} → Reflexivity (_≡̇_ {B = B})
-- -- -- -- -- Reflexivity.reflexivity Reflexivity≡̇ _ _ = refl

-- -- -- -- -- open import Oscar.Property.Symmetry

-- -- -- -- -- instance Symmetry≡ : ∀ {a} {A : Set a} → Symmetry (_≡_ {A = A})
-- -- -- -- -- Symmetry.symmetry Symmetry≡ = sym

-- -- -- -- -- instance Symmetry≡̇ : ∀ {a} {A : Set a} {b} {B : A → Set b} → Symmetry (_≡̇_ {B = B})
-- -- -- -- -- Symmetry.symmetry Symmetry≡̇ = ≡̇-sym

-- -- -- -- -- open import Oscar.Property.Transitivity

-- -- -- -- -- instance Transitivity≡ : ∀ {a} {A : Set a} → Transitivity (_≡_ {A = A})
-- -- -- -- -- Transitivity.transitivity Transitivity≡ x≡y = trans x≡y

-- -- -- -- -- instance Transitivity≡̇ : ∀ {a} {A : Set a} {b} {B : A → Set b} → Transitivity (_≡̇_ {B = B})
-- -- -- -- -- Transitivity.transitivity Transitivity≡̇ = ≡̇-trans

-- -- -- -- -- -- {-
-- -- -- -- -- -- _∘₂_ : ∀ {a b c}
-- -- -- -- -- --         {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
-- -- -- -- -- --         (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
-- -- -- -- -- --         ((x : A) → C (g x))
-- -- -- -- -- -- f ∘₂ g = λ x → f (g x)
-- -- -- -- -- -- -}

-- -- -- -- -- -- open import Oscar.Class.Equivalence

-- -- -- -- -- -- instance ReflexivityPropositional : ∀ {a} {A : Set a} → Reflexivity (_≡_ {A = A})
-- -- -- -- -- -- Reflexivity.reflexivity ReflexivityPropositional = refl

-- -- -- -- -- -- instance SymmetryPropositional : ∀ {a} {A : Set a} → Symmetry (_≡_ {A = A})
-- -- -- -- -- -- Symmetry.symmetry SymmetryPropositional = sym

-- -- -- -- -- -- instance TransitivityPropositional : ∀ {a} {A : Set a} → Transitivity (_≡_ {A = A})
-- -- -- -- -- -- Transitivity.transitivity TransitivityPropositional = trans

-- -- -- -- -- -- open import Prelude using (it)

-- -- -- -- -- -- instance Equivalence⋆ : ∀ {a} {A : Set a} {ℓ} {_≋_ : A → A → Set ℓ} ⦃ _ : Reflexivity _≋_ ⦄ ⦃ _ : Symmetry _≋_ ⦄ ⦃ _ : Transitivity _≋_ ⦄ → Equivalence _≋_
-- -- -- -- -- -- Equivalence.reflexivityI Equivalence⋆ = it
-- -- -- -- -- -- Equivalence.symmetryI Equivalence⋆ = it
-- -- -- -- -- -- Equivalence.transitivityI Equivalence⋆ = it

-- -- -- -- -- -- -- -- {-
-- -- -- -- -- -- -- -- instance EquivalencePropositional : ∀ {a} {A : Set a} → Equivalence (_≡_ {A = A})
-- -- -- -- -- -- -- -- Equivalence.reflexivity EquivalencePropositional = refl
-- -- -- -- -- -- -- -- Equivalence.symmetry EquivalencePropositional = sym
-- -- -- -- -- -- -- -- Equivalence.transitivity EquivalencePropositional = trans

-- -- -- -- -- -- -- -- instance EquivalencePointwise : ∀ {a} {A : Set a} {b} {B : A → Set b} → Equivalence (_≡̇_ {B = B})
-- -- -- -- -- -- -- -- Equivalence.reflexivity EquivalencePointwise x = refl
-- -- -- -- -- -- -- -- Equivalence.symmetry EquivalencePointwise = ≡̇-sym
-- -- -- -- -- -- -- -- Equivalence.transitivity EquivalencePointwise = ≡̇-trans
-- -- -- -- -- -- -- -- -}

-- -- -- -- -- -- instance CongruousEquivalencesPropositional : ∀ {a} {A : Set a} {b} {B : Set b} → CongruousEquivalences (_≡_ {A = A}) (_≡_ {A = B})
-- -- -- -- -- -- CongruousEquivalences.equivalence₁ CongruousEquivalencesPropositional = it
-- -- -- -- -- -- CongruousEquivalences.equivalence₂ CongruousEquivalencesPropositional = it
-- -- -- -- -- -- CongruousEquivalences.congruity CongruousEquivalencesPropositional = cong

-- -- -- -- -- -- postulate
-- -- -- -- -- --   FunctionName : Set

-- -- -- -- -- -- open import Oscar.Data.Nat
-- -- -- -- -- -- open import Oscar.Data.Fin
-- -- -- -- -- -- open import Oscar.Data.Term FunctionName
-- -- -- -- -- -- open import Oscar.Data.Term.Injectivity FunctionName

-- -- -- -- -- -- instance InjectiveEquivalencesTermI : ∀ {m : Nat} → InjectiveEquivalences (_≡_ {A = Fin m}) (_≡_ {A = Term m}) Term.i Term.i
-- -- -- -- -- -- InjectiveEquivalences.equivalence₁ InjectiveEquivalencesTermI = it
-- -- -- -- -- -- InjectiveEquivalences.equivalence₂ InjectiveEquivalencesTermI = it
-- -- -- -- -- -- InjectiveEquivalences.injectivity InjectiveEquivalencesTermI refl = reflexivity

-- -- -- -- -- -- instance InjectiveEquivalencesTermLeft : ∀ {m : Nat} {r₁ r₂ : Term m} → InjectiveEquivalences _≡_ _≡_ (_fork r₁) (_fork r₂)
-- -- -- -- -- -- InjectiveEquivalences.equivalence₁ InjectiveEquivalencesTermLeft = it
-- -- -- -- -- -- InjectiveEquivalences.equivalence₂ InjectiveEquivalencesTermLeft = it
-- -- -- -- -- -- InjectiveEquivalences.injectivity InjectiveEquivalencesTermLeft refl = reflexivity

-- -- -- -- -- -- instance InjectiveEquivalencesTermRight : ∀ {m : Nat} {l₁ l₂ : Term m} → InjectiveEquivalences _≡_ _≡_ (l₁ fork_) (l₂ fork_)
-- -- -- -- -- -- InjectiveEquivalences.equivalence₁ InjectiveEquivalencesTermRight = it
-- -- -- -- -- -- InjectiveEquivalences.equivalence₂ InjectiveEquivalencesTermRight = it
-- -- -- -- -- -- InjectiveEquivalences.injectivity InjectiveEquivalencesTermRight refl = reflexivity

-- -- -- -- -- -- injectivity' :
-- -- -- -- -- --   ∀ {a} {A : Set a} {ℓ₁} {_≋₁_ : A → A → Set ℓ₁}
-- -- -- -- -- --     {b} {B : Set b}
-- -- -- -- -- --     {f : A → B}
-- -- -- -- -- --     {g : A → B}
-- -- -- -- -- --     ⦃ _ : InjectiveEquivalences _≋₁_ _≡_ f g ⦄ →
-- -- -- -- -- --   ∀ {x y} → f x ≡ g y → x ≋₁ y
-- -- -- -- -- -- injectivity' x = injectivity {_≋₂_ = _≡_} x

-- -- -- -- -- -- Term-forkLeft-inj' : ∀ {n} {l₁ r₁ l₂ r₂ : Term n} → l₁ fork r₁ ≡ l₂ fork r₂ → l₁ ≡ l₂
-- -- -- -- -- -- Term-forkLeft-inj' {n} {l₁} {r₁} {l₂} {r₂} x = injectivity' x
-- -- -- -- -- -- --Term-forkLeft-inj' {n} {l₁} {r₁} {l₂} {r₂} x = injectivity {_≋₂_ = _≡_} x
-- -- -- -- -- -- -- injectivity {_≋₁_ = {!_≡_!}} {_≋₂_ = {!_≡_!}} ⦃ InjectiveEquivalencesTermLeft ⦄ x

-- -- -- -- -- -- Term-forkRight-inj' : ∀ {n} {l₁ r₁ l₂ r₂ : Term n} → l₁ fork r₁ ≡ l₂ fork r₂ → r₁ ≡ r₂
-- -- -- -- -- -- Term-forkRight-inj' {n} {l₁} {r₁} {l₂} {r₂} x = injectivity' x
-- -- -- -- -- -- --Term-forkLeft-inj' {n} {l₁} {r₁} {l₂} {r₂} x = injectivity {_≋₂_ = _≡_} x
-- -- -- -- -- -- -- injectivity {_≋₁_ = {!_≡_!}} {_≋₂_ = {!_≡_!}} ⦃ InjectiveEquivalencesTermLeft ⦄ x


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

module Agda.Builtin.Equality.Erase where

open import Agda.Builtin.Equality

primitive primEraseEquality : ∀ {a} {A : Set a} {x y : A} → x ≡ y → x ≡ y

max_stars_repo_name: bennn/agda

max_issues_repo_name: bennn/agda

max_forks_repo_name: bennn/agda