text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- AVL trees
------------------------------------------------------------------------

-- AVL trees are balanced binary search trees.

-- The search tree invariant is specified using the technique
-- described by Conor McBride in his talk "Pivotal pragmatism".

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

module Data.AVL
  {k v ℓ}
  {Key : Set k} (Value : Key → Set v)
  {_<_ : Rel Key ℓ}
  (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_)
  where

open import Data.Bool
import Data.DifferenceList as DiffList
open import Data.Empty
open import Data.List as List using (List)
open import Data.Maybe hiding (map)
open import Data.Nat hiding (_<_; compare; _⊔_)
open import Data.Product hiding (map)
open import Data.Unit
open import Function
open import Level using (_⊔_; Lift; lift)

open IsStrictTotalOrder isStrictTotalOrder

------------------------------------------------------------------------
-- Extended keys

module Extended-key where

  -- The key type extended with a new minimum and maximum.

  data Key⁺ : Set k where
    ⊥⁺ ⊤⁺ : Key⁺
    [_]   : (k : Key) → Key⁺

  -- An extended strict ordering relation.

  infix 4 _<⁺_

  _<⁺_ : Key⁺ → Key⁺ → Set ℓ
  ⊥⁺    <⁺ [ _ ] = Lift ⊤
  ⊥⁺    <⁺ ⊤⁺    = Lift ⊤
  [ x ] <⁺ [ y ] = x < y
  [ _ ] <⁺ ⊤⁺    = Lift ⊤
  _     <⁺ _     = Lift ⊥

  -- A pair of ordering constraints.

  infix 4 _<_<_

  _<_<_ : Key⁺ → Key → Key⁺ → Set ℓ
  l < x < u = l <⁺ [ x ] × [ x ] <⁺ u

  -- _<⁺_ is transitive.

  trans⁺ : ∀ l {m u} → l <⁺ m → m <⁺ u → l <⁺ u

  trans⁺ [ l ] {m = [ m ]} {u = [ u ]} l<m m<u = trans l<m m<u

  trans⁺ ⊥⁺    {u = [ _ ]} _ _ = _
  trans⁺ ⊥⁺    {u = ⊤⁺}    _ _ = _
  trans⁺ [ _ ] {u = ⊤⁺}    _ _ = _

  trans⁺ _     {m = ⊥⁺}    {u = ⊥⁺}    _ (lift ())
  trans⁺ _     {m = [ _ ]} {u = ⊥⁺}    _ (lift ())
  trans⁺ _     {m = ⊤⁺}    {u = ⊥⁺}    _ (lift ())
  trans⁺ [ _ ] {m = ⊥⁺}    {u = [ _ ]} (lift ()) _
  trans⁺ [ _ ] {m = ⊤⁺}    {u = [ _ ]} _ (lift ())
  trans⁺ ⊤⁺    {m = ⊥⁺}                (lift ()) _
  trans⁺ ⊤⁺    {m = [ _ ]}             (lift ()) _
  trans⁺ ⊤⁺    {m = ⊤⁺}                (lift ()) _

------------------------------------------------------------------------
-- Types and functions which are used to keep track of height
-- invariants

module Height-invariants where

  -- Bits. (I would use Fin 2 instead if Agda had "defined patterns",
  -- so that I could pattern match on 1# instead of suc zero; the text
  -- "suc zero" takes up a lot more space.)

  data ℕ₂ : Set where
    0# : ℕ₂
    1# : ℕ₂

  -- Addition.

  infixl 6 _⊕_

  _⊕_ : ℕ₂ → ℕ → ℕ
  0# ⊕ n = n
  1# ⊕ n = 1 + n

  -- i ⊕ n -1 = pred (i ⊕ n).

  _⊕_-1 : ℕ₂ → ℕ → ℕ
  i ⊕ zero  -1 = 0
  i ⊕ suc n -1 = i ⊕ n

  infix 4 _∼_

  -- If m ∼ n, then the difference between m and n is at most 1. _∼_
  -- is used to record the balance factor of the AVL trees, and also
  -- to ensure that the absolute value of the balance factor is never
  -- more than 1.

  data _∼_ : ℕ → ℕ → Set where
    ∼+ : ∀ {n} →     n ∼ 1 + n
    ∼0 : ∀ {n} →     n ∼ n
    ∼- : ∀ {n} → 1 + n ∼ n

  -- The maximum of m and n.

  max : ∀ {m n} → m ∼ n → ℕ
  max (∼+ {n}) = 1 + n
  max (∼0 {n}) =     n
  max (∼- {n}) = 1 + n

  -- Some lemmas.

  1+ : ∀ {m n} → m ∼ n → 1 + m ∼ 1 + n
  1+ ∼+ = ∼+
  1+ ∼0 = ∼0
  1+ ∼- = ∼-

  max∼ : ∀ {i j} (bal : i ∼ j) → max bal ∼ i
  max∼ ∼+ = ∼-
  max∼ ∼0 = ∼0
  max∼ ∼- = ∼0

  ∼max : ∀ {i j} (bal : i ∼ j) → j ∼ max bal
  ∼max ∼+ = ∼0
  ∼max ∼0 = ∼0
  ∼max ∼- = ∼+

  max∼max : ∀ {i j} (bal : i ∼ j) → max (max∼ bal) ∼ max (∼max bal)
  max∼max ∼+ = ∼0
  max∼max ∼0 = ∼0
  max∼max ∼- = ∼0

  max-lemma : ∀ {m n} (bal : m ∼ n) →
              1 + max (1+ (max∼max bal)) ≡ 2 + max bal
  max-lemma ∼+ = P.refl
  max-lemma ∼0 = P.refl
  max-lemma ∼- = P.refl

------------------------------------------------------------------------
-- AVL trees

-- Key/value pairs.

KV : Set (k ⊔ v)
KV = Σ Key Value

module Indexed where

  open Extended-key
  open Height-invariants

  -- The trees have three parameters/indices: a lower bound on the
  -- keys, an upper bound, and a height.
  --
  -- (The bal argument is the balance factor.)

  data Tree (l u : Key⁺) : ℕ → Set (k ⊔ v ⊔ ℓ) where
    leaf : (l<u : l <⁺ u) → Tree l u 0
    node : ∀ {hˡ hʳ}
           (k : KV)
           (lk : Tree l [ proj₁ k ] hˡ)
           (ku : Tree [ proj₁ k ] u hʳ) (bal : hˡ ∼ hʳ) →
           Tree l u (1 + max bal)

  -- Cast operations. Logarithmic in the size of the tree, if we don't
  -- count the time needed to construct the new proofs in the leaf
  -- cases. (The same kind of caveat applies to other operations
  -- below.)
  --
  -- Perhaps it would be worthwhile changing the data structure so
  -- that the casts could be implemented in constant time (excluding
  -- proof manipulation). However, note that this would not change the
  -- worst-case time complexity of the operations below (up to Θ).

  castˡ : ∀ {l m u h} → l <⁺ m → Tree m u h → Tree l u h
  castˡ {l} l<m (leaf m<u)         = leaf (trans⁺ l l<m m<u)
  castˡ     l<m (node k mk ku bal) = node k (castˡ l<m mk) ku bal

  castʳ : ∀ {l m u h} → Tree l m h → m <⁺ u → Tree l u h
  castʳ {l} (leaf l<m)         m<u = leaf (trans⁺ l l<m m<u)
  castʳ     (node k lk km bal) m<u = node k lk (castʳ km m<u) bal

  -- Various constant-time functions which construct trees out of
  -- smaller pieces, sometimes using rotation.

  joinˡ⁺ : ∀ {l u hˡ hʳ} →
           (k : KV) →
           (∃ λ i → Tree l [ proj₁ k ] (i ⊕ hˡ)) →
           Tree [ proj₁ k ] u hʳ →
           (bal : hˡ ∼ hʳ) →
           ∃ λ i → Tree l u (i ⊕ (1 + max bal))
  joinˡ⁺ k₆ (1# , node k₂ t₁
                    (node k₄ t₃ t₅ bal)
                                ∼+) t₇ ∼-  = (0# , P.subst (Tree _ _) (max-lemma bal)
                                                     (node k₄
                                                           (node k₂ t₁ t₃ (max∼ bal))
                                                           (node k₆ t₅ t₇ (∼max bal))
                                                           (1+ (max∼max bal))))
  joinˡ⁺ k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼-  = (0# , node k₂ t₁ (node k₄ t₃ t₅ ∼0) ∼0)
  joinˡ⁺ k₄ (1# , node k₂ t₁ t₃ ∼0) t₅ ∼-  = (1# , node k₂ t₁ (node k₄ t₃ t₅ ∼-) ∼+)
  joinˡ⁺ k₂ (1# , t₁)               t₃ ∼0  = (1# , node k₂ t₁ t₃ ∼-)
  joinˡ⁺ k₂ (1# , t₁)               t₃ ∼+  = (0# , node k₂ t₁ t₃ ∼0)
  joinˡ⁺ k₂ (0# , t₁)               t₃ bal = (0# , node k₂ t₁ t₃ bal)

  joinʳ⁺ : ∀ {l u hˡ hʳ} →
           (k : KV) →
           Tree l [ proj₁ k ] hˡ →
           (∃ λ i → Tree [ proj₁ k ] u (i ⊕ hʳ)) →
           (bal : hˡ ∼ hʳ) →
           ∃ λ i → Tree l u (i ⊕ (1 + max bal))
  joinʳ⁺ k₂ t₁ (1# , node k₆
                       (node k₄ t₃ t₅ bal)
                                t₇ ∼-) ∼+  = (0# , P.subst (Tree _ _) (max-lemma bal)
                                                     (node k₄
                                                           (node k₂ t₁ t₃ (max∼ bal))
                                                           (node k₆ t₅ t₇ (∼max bal))
                                                           (1+ (max∼max bal))))
  joinʳ⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+) ∼+  = (0# , node k₄ (node k₂ t₁ t₃ ∼0) t₅ ∼0)
  joinʳ⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0) ∼+  = (1# , node k₄ (node k₂ t₁ t₃ ∼+) t₅ ∼-)
  joinʳ⁺ k₂ t₁ (1# , t₃)               ∼0  = (1# , node k₂ t₁ t₃ ∼+)
  joinʳ⁺ k₂ t₁ (1# , t₃)               ∼-  = (0# , node k₂ t₁ t₃ ∼0)
  joinʳ⁺ k₂ t₁ (0# , t₃)               bal = (0# , node k₂ t₁ t₃ bal)

  joinˡ⁻ : ∀ {l u} hˡ {hʳ} →
           (k : KV) →
           (∃ λ i → Tree l [ proj₁ k ] (i ⊕ hˡ -1)) →
           Tree [ proj₁ k ] u hʳ →
           (bal : hˡ ∼ hʳ) →
           ∃ λ i → Tree l u (i ⊕ max bal)
  joinˡ⁻ zero    k₂ (0# , t₁) t₃ bal = (1# , node k₂ t₁ t₃ bal)
  joinˡ⁻ zero    k₂ (1# , t₁) t₃ bal = (1# , node k₂ t₁ t₃ bal)
  joinˡ⁻ (suc _) k₂ (0# , t₁) t₃ ∼+  = joinʳ⁺ k₂ t₁ (1# , t₃) ∼+
  joinˡ⁻ (suc _) k₂ (0# , t₁) t₃ ∼0  = (1# , node k₂ t₁ t₃ ∼+)
  joinˡ⁻ (suc _) k₂ (0# , t₁) t₃ ∼-  = (0# , node k₂ t₁ t₃ ∼0)
  joinˡ⁻ (suc _) k₂ (1# , t₁) t₃ bal = (1# , node k₂ t₁ t₃ bal)

  joinʳ⁻ : ∀ {l u hˡ} hʳ →
           (k : KV) →
           Tree l [ proj₁ k ] hˡ →
           (∃ λ i → Tree [ proj₁ k ] u (i ⊕ hʳ -1)) →
           (bal : hˡ ∼ hʳ) →
           ∃ λ i → Tree l u (i ⊕ max bal)
  joinʳ⁻ zero    k₂ t₁ (0# , t₃) bal = (1# , node k₂ t₁ t₃ bal)
  joinʳ⁻ zero    k₂ t₁ (1# , t₃) bal = (1# , node k₂ t₁ t₃ bal)
  joinʳ⁻ (suc _) k₂ t₁ (0# , t₃) ∼-  = joinˡ⁺ k₂ (1# , t₁) t₃ ∼-
  joinʳ⁻ (suc _) k₂ t₁ (0# , t₃) ∼0  = (1# , node k₂ t₁ t₃ ∼-)
  joinʳ⁻ (suc _) k₂ t₁ (0# , t₃) ∼+  = (0# , node k₂ t₁ t₃ ∼0)
  joinʳ⁻ (suc _) k₂ t₁ (1# , t₃) bal = (1# , node k₂ t₁ t₃ bal)

  -- Extracts the smallest element from the tree, plus the rest.
  -- Logarithmic in the size of the tree.

  headTail : ∀ {l u h} → Tree l u (1 + h) →
             ∃ λ (k : KV) → l <⁺ [ proj₁ k ] ×
                            ∃ λ i → Tree [ proj₁ k ] u (i ⊕ h)
  headTail (node k₁ (leaf l<k₁) t₂ ∼+) = (k₁ , l<k₁ , 0# , t₂)
  headTail (node k₁ (leaf l<k₁) t₂ ∼0) = (k₁ , l<k₁ , 0# , t₂)
  headTail (node {hˡ = suc _} k₃ t₁₂ t₄ bal) with headTail t₁₂
  ... | (k₁ , l<k₁ , t₂) = (k₁ , l<k₁ , joinˡ⁻ _ k₃ t₂ t₄ bal)

  -- Extracts the largest element from the tree, plus the rest.
  -- Logarithmic in the size of the tree.

  initLast : ∀ {l u h} → Tree l u (1 + h) →
             ∃ λ (k : KV) → [ proj₁ k ] <⁺ u ×
                            ∃ λ i → Tree l [ proj₁ k ] (i ⊕ h)
  initLast (node k₂ t₁ (leaf k₂<u) ∼-) = (k₂ , k₂<u , (0# , t₁))
  initLast (node k₂ t₁ (leaf k₂<u) ∼0) = (k₂ , k₂<u , (0# , t₁))
  initLast (node {hʳ = suc _} k₂ t₁ t₃₄ bal) with initLast t₃₄
  ... | (k₄ , k₄<u , t₃) = (k₄ , k₄<u , joinʳ⁻ _ k₂ t₁ t₃ bal)

  -- Another joining function. Logarithmic in the size of either of
  -- the input trees (which need to have almost equal heights).

  join : ∀ {l m u hˡ hʳ} →
         Tree l m hˡ → Tree m u hʳ → (bal : hˡ ∼ hʳ) →
         ∃ λ i → Tree l u (i ⊕ max bal)
  join t₁ (leaf m<u) ∼0 = (0# , castʳ t₁ m<u)
  join t₁ (leaf m<u) ∼- = (0# , castʳ t₁ m<u)
  join {hʳ = suc _} t₁ t₂₃ bal with headTail t₂₃
  ... | (k₂ , m<k₂ , t₃) = joinʳ⁻ _ k₂ (castʳ t₁ m<k₂) t₃ bal

  -- An empty tree.

  empty : ∀ {l u} → l <⁺ u → Tree l u 0
  empty = leaf

  -- A singleton tree.

  singleton : ∀ {l u} (k : Key) → Value k → l < k < u → Tree l u 1
  singleton k v (l<k , k<u) = node (k , v) (leaf l<k) (leaf k<u) ∼0

  -- Inserts a key into the tree, using a function to combine any
  -- existing value with the new value. Logarithmic in the size of the
  -- tree (assuming constant-time comparisons and a constant-time
  -- combining function).

  insertWith : ∀ {l u h} → (k : Key) → Value k →
               (Value k → Value k → Value k) →  -- New → old → result.
               Tree l u h → l < k < u →
               ∃ λ i → Tree l u (i ⊕ h)
  insertWith k v f (leaf l<u) l<k<u = (1# , singleton k v l<k<u)
  insertWith k v f (node (k′ , v′) lp pu bal) (l<k , k<u) with compare k k′
  ... | tri< k<k′ _ _ = joinˡ⁺ (k′ , v′) (insertWith k v f lp (l<k , k<k′)) pu bal
  ... | tri> _ _ k′<k = joinʳ⁺ (k′ , v′) lp (insertWith k v f pu (k′<k , k<u)) bal
  ... | tri≈ _ k≡k′ _ rewrite P.sym k≡k′ = (0# , node (k , f v v′) lp pu bal)

  -- Inserts a key into the tree. If the key already exists, then it
  -- is replaced. Logarithmic in the size of the tree (assuming
  -- constant-time comparisons).

  insert : ∀ {l u h} → (k : Key) → Value k → Tree l u h → l < k < u →
           ∃ λ i → Tree l u (i ⊕ h)
  insert k v = insertWith k v const

  -- Deletes the key/value pair containing the given key, if any.
  -- Logarithmic in the size of the tree (assuming constant-time
  -- comparisons).

  delete : ∀ {l u h} → Key → Tree l u h →
           ∃ λ i → Tree l u (i ⊕ h -1)
  delete k (leaf l<u)         = (0# , leaf l<u)
  delete k (node p lp pu bal) with compare k (proj₁ p)
  ... | tri< _ _ _ = joinˡ⁻ _ p (delete k lp) pu bal
  ... | tri> _ _ _ = joinʳ⁻ _ p lp (delete k pu) bal
  ... | tri≈ _ _ _ = join lp pu bal

  -- Looks up a key. Logarithmic in the size of the tree (assuming
  -- constant-time comparisons).

  lookup : ∀ {l u h} → (k : Key) → Tree l u h → Maybe (Value k)
  lookup k (leaf _)                  = nothing
  lookup k (node (k′ , v) lk′ k′u _) with compare k k′
  ... | tri< _ _  _ = lookup k lk′
  ... | tri> _ _  _ = lookup k k′u
  ... | tri≈ _ eq _ rewrite eq = just v

  -- Maps a function over all values in the tree.

  map : (∀ {k} → Value k → Value k) →
        ∀ {l u h} → Tree l u h → Tree l u h
  map f (leaf l<u)             = leaf l<u
  map f (node (k , v) l r bal) = node (k , f v) (map f l) (map f r) bal

  -- Converts the tree to an ordered list. Linear in the size of the
  -- tree.

  open DiffList

  toDiffList : ∀ {l u h} → Tree l u h → DiffList KV
  toDiffList (leaf _)       = []
  toDiffList (node k l r _) = toDiffList l ++ k ∷ toDiffList r

------------------------------------------------------------------------
-- Types and functions with hidden indices

data Tree : Set (k ⊔ v ⊔ ℓ) where
  tree : let open Extended-key in
         ∀ {h} → Indexed.Tree ⊥⁺ ⊤⁺ h → Tree

empty : Tree
empty = tree (Indexed.empty _)

singleton : (k : Key) → Value k → Tree
singleton k v = tree (Indexed.singleton k v _)

insert : (k : Key) → Value k → Tree → Tree
insert k v (tree t) = tree $ proj₂ $ Indexed.insert k v t _

insertWith : (k : Key) → Value k → (Value k → Value k → Value k) →
             Tree → Tree
insertWith k v f (tree t) = tree $ proj₂ $ Indexed.insertWith k v f t _

delete : Key → Tree → Tree
delete k (tree t) = tree $ proj₂ $ Indexed.delete k t

lookup : (k : Key) → Tree → Maybe (Value k)
lookup k (tree t) = Indexed.lookup k t

map : ({k : Key} → Value k → Value k) → Tree → Tree
map f (tree t) = tree $ Indexed.map f t

_∈?_ : Key → Tree → Bool
k ∈? t = is-just (lookup k t)

headTail : Tree → Maybe (KV × Tree)
headTail (tree (Indexed.leaf _)) = nothing
headTail (tree {h = suc _} t)    with Indexed.headTail t
... | (k , _ , _ , t′) = just (k , tree (Indexed.castˡ _ t′))

initLast : Tree → Maybe (Tree × KV)
initLast (tree (Indexed.leaf _)) = nothing
initLast (tree {h = suc _} t)    with Indexed.initLast t
... | (k , _ , _ , t′) = just (tree (Indexed.castʳ t′ _) , k)

-- The input does not need to be ordered.

fromList : List KV → Tree
fromList = List.foldr (uncurry insert) empty

-- Returns an ordered list.

toList : Tree → List KV
toList (tree t) = DiffList.toList (Indexed.toDiffList t)

-- Naive implementations of union.

unionWith : (∀ {k} → Value k → Value k → Value k) →
            -- Left → right → result.
            Tree → Tree → Tree
unionWith f t₁ t₂ =
  List.foldr (λ { (k , v) → insertWith k v f }) t₂ (toList t₁)

-- Left-biased.

union : Tree → Tree → Tree
union = unionWith const

unionsWith : (∀ {k} → Value k → Value k → Value k) → List Tree → Tree
unionsWith f ts = List.foldr (unionWith f) empty ts

-- Left-biased.

unions : List Tree → Tree
unions = unionsWith const

ext: agda


text:
module Issue4260.M where

postulate
  F : Set → Set

syntax F X = G X

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

open import Light.Library.Data.Integer as ℤ using (ℤ ; zero ; successor)
open import Light.Package using (Package)

module Light.Literals.Integer ⦃ package : Package record { ℤ } ⦄ where

open import Light.Literals.Definition.Natural using (FromNatural)
open import Light.Literals.Definition.Negative using (FromNegative)
open FromNatural using (convert)
open import Light.Library.Relation.Decidable using (if_then_else_)
open import Light.Library.Relation.Binary.Equality using (_≈_)
import Light.Library.Data.Natural as ℕ
import Light.Library.Relation.Binary.Equality.Decidable

instance from‐natural : FromNatural ℤ
convert from‐natural n =
      if n ≈ ℕ.zero
      then zero
      else successor (convert from‐natural (ℕ.predecessor n))

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Int.Base where

open import Cubical.Core.Everything

open import Cubical.Data.Nat

data Int : Type₀ where
  pos    : (n : ℕ) → Int
  negsuc : (n : ℕ) → Int

sucInt : Int → Int
sucInt (pos n)          = pos (suc n)
sucInt (negsuc zero)    = pos zero
sucInt (negsuc (suc n)) = negsuc n

predInt : Int → Int
predInt (pos zero)    = negsuc zero
predInt (pos (suc n)) = pos n
predInt (negsuc n)    = negsuc (suc n)

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
open import Relation.Binary.PropositionalEquality using
  ( _≡_ ; refl ; sym ; trans ; subst ; subst₂ ; cong ; cong₂ )

open import AssocFree.Util using ( δsubst₂ )

import AssocFree.STLambdaC.Typ
import AssocFree.STLambdaC.Exp
import AssocFree.STLambdaC.NF
import AssocFree.STLambdaC.Redn

module AssocFree.STLambdaC.Eval
  (TConst : Set)
  (Const : AssocFree.STLambdaC.Typ.Typ TConst → Set) where

open Relation.Binary.PropositionalEquality.≡-Reasoning using ( begin_ ; _≡⟨_⟩_ ; _∎ )

open module Typ = AssocFree.STLambdaC.Typ TConst using
  ( Typ ; Ctxt ; const ; _⇝_ ; [_] ; [] ; _∷_ ; _++_ ; _∈_ ; uniq
  ; Case ; case ; inj₁ ; inj₂ ; case-≫ ; _≪_ ; _≫_ )

open module Exp = AssocFree.STLambdaC.Exp TConst Const using
  ( Exp ; exp ; const ; abs ; app ; var ; var₀
  ; Substn ; substn+ ; substn* ; xsubstn+ ; weaken+ ; weaken* ; weakens*
  ; ⟨_⟩ ; choose ; _◁_ ; id
  ; weaken*-[] ; weaken*-++ ; substn*-◁ ; substn*-id )

open module NF = AssocFree.STLambdaC.NF TConst Const using
  ( Atom ; NF ; var ; const ; app ; abs ; atom ; atom₀ ; aweaken* )

open module Redn = AssocFree.STLambdaC.Redn TConst Const using
  ( _⇒_ ; _⇓ ; _⇓′ ; eta ; beta ; lhs ; atom ; nf ; redn ; tgt ; ⇓abs ; ⇓app ; rweaken* )

-- Values

data cVal {Γ C} : Exp Γ (const C) → Set where
  atom : ∀ {M} → Atom M → cVal M
  redn : ∀ {M N} → (M ⇒ N) → cVal N → cVal M

data fVal {Γ T U} (F : ∀ {Γ} → Exp Γ T → Set) (G : ∀ {Γ} → Exp Γ U → Set) : Exp Γ (T ⇝ U) → Set where
  fun : ∀ {M} → (∀ Δ → {N : Exp (Δ ++ Γ) T} → F N → G (app (weaken* Δ {Γ} M) N)) → fVal F G M
  redn : ∀ {M N} → (M ⇒ N) → fVal F G N → fVal F G M

Val : ∀ {Γ T} → Exp Γ T → Set
Val {Γ} {const C} M = cVal M
Val {Γ} {T ⇝ U}   M = fVal Val Val M

-- Values are closed under reduction and application

vredn : ∀ {Γ T} {M N : Exp Γ T} → (M ⇒ N) → Val N → Val M
vredn {Γ} {const C} = redn
vredn {Γ} {T ⇝ U}   = redn

vapp : ∀ {Γ T U} {M : Exp Γ (T ⇝ U)} {N : Exp Γ T} → Val M → Val N → Val (app M N)
vapp {Γ} {T} {U} {M} {N} (fun f) W = subst (λ X → Val (app X N)) (weaken*-[] M) (f [] W)
vapp                (redn M⇒N V) W = vredn (lhs M⇒N) (vapp V W)

-- Reification and reflection

mutual

  reify : ∀ {Γ T} {M : Exp Γ T} → Val M → (M ⇓)
  reify {Γ} {const C}   (atom N)     = nf (atom N)
  reify {Γ} {const C}   (redn M⇒N V) = redn M⇒N (reify V)
  reify {Γ} {T ⇝ U} {M} (fun f)      = redn (eta M) (⇓abs {Γ} T (reify (f [ T ] (reflect (atom (atom₀ {Γ}))))))
  reify {Γ} {T ⇝ U}     (redn M⇒N V) = redn M⇒N (reify V)

  reflect : ∀ {Γ T} {M : Exp Γ T} → (M ⇓′) → Val M
  reflect {Γ} {const C} (atom M) = atom M
  reflect {Γ} {T ⇝ U}   (atom M) = fun (λ Δ V → reflect (⇓app (atom (aweaken* Δ M)) (reify V)))
  reflect          (redn M⇒N N⇓) = vredn M⇒N (reflect N⇓)

-- Value substitutions

Vals : ∀ {Γ Δ} → Substn (exp var) Γ Δ → Set
Vals {Γ} {Δ} σ = ∀ {T} (x : T ∈ Δ) → Val (σ x)

⟪_⟫ : ∀ {Γ T} {N : Exp Γ T} → Val N → Vals ⟨ N ⟩
⟪ V ⟫ x = δsubst₂ (λ X Y → Val {T = X} Y) (uniq x) refl V

vchoose : ∀ {Γ Δ E} {σ : Substn (exp var) Γ Δ} {τ : Substn (exp var) Γ E} → Vals σ → Vals τ →
  ∀ {T} (x : Case T Δ E) → Val (choose σ τ x)
vchoose Vs Ws (inj₁ x) = Vs x
vchoose Vs Ws (inj₂ x) = Ws x

_◂_ : ∀ {Γ Δ T} {N : Exp Γ T} {σ : Substn (exp var) Γ Δ} → Val N → Vals σ → Vals (N ◁ σ)
_◂_ {Γ} {Δ} {T} V Vs x = vchoose ⟪ V ⟫ Vs (case [ T ] Δ x)

-- Weakening

vweaken* : ∀ {Γ} Δ {U} {M : Exp Γ U} → Val M → Val (weaken* Δ M)
vweaken* Δ {const C}   (atom N)     = atom (aweaken* Δ N)
vweaken* Δ {const C}   (redn M⇒N V) = redn (rweaken* Δ M⇒N) (vweaken* Δ V)
vweaken* Δ {T ⇝ U} {M} (fun f)      = fun (λ Φ {N} V → subst (λ X → Val (app X N)) (sym (weaken*-++ Φ Δ _ M)) (f (Φ ++ Δ) V))
vweaken* Δ {T ⇝ U}     (redn M⇒N V) = redn (rweaken* Δ M⇒N) (vweaken* Δ V)

vweakens* : ∀ {Γ Δ} E {σ : Substn (exp var) Γ Δ} → Vals σ → Vals (weakens* E σ)
vweakens* E {σ} Vs x = vweaken* E (Vs x)

-- Evaluation

eval : ∀ {Γ Δ T} (M : Exp Γ T) → {σ : Substn (exp var) Δ Γ} →
  Vals σ → Val (substn* σ M)
eval (const {T} c) Vs = reflect (atom (const c))
eval {Γ} {Δ} (var x) {σ} Vs =
  subst Val (begin
    σ x
  ≡⟨ sym (weaken*-[] (σ x)) ⟩
    weaken* [] (σ x)
  ≡⟨ cong (xsubstn+ [] Δ Γ σ) (sym (case-≫ [] x)) ⟩
    substn* σ (var x)
  ∎) (Vs x)
eval {Γ} {Δ} (abs T M) {σ} Vs =
  fun (λ E {N} V →
    vredn (beta {E ++ Δ} (weaken+ [ T ] E Δ (substn+ [ T ] Δ Γ σ M)) N)
      (subst Val
        (substn*-◁ Γ Δ E M N σ)
        (eval M (V ◂ vweakens* E {σ} Vs))))
eval (app M N) Vs = vapp (eval M Vs) (eval N Vs)

vid : ∀ Γ → Vals (id Γ)
vid Γ x = reflect (atom (var x))

normalize : ∀ {Γ T} → (M : Exp Γ T) → (M ⇓)
normalize {Γ} M = reify (subst Val (substn*-id M) (eval M (vid Γ)))

normal : ∀ {Γ T} → Exp Γ T → Exp Γ T
normal M = tgt (normalize M)

max_stars_repo_name: agda/agda-assoc-free

max_issues_repo_name: agda/agda-assoc-free

max_forks_repo_name: agda/agda-assoc-free


text:
module Duploid.Functor where

open import Preduploid
open import Duploid
import Preduploid.Functor as PF

open import Level

record Functor {o₁ ℓ₁ o₂ ℓ₂} (𝒞 : Duploid o₁ ℓ₁) (𝒟 : Duploid o₂ ℓ₂)
  : Set (levelOfTerm 𝒞 ⊔ levelOfTerm 𝒟) where
  private
    module 𝒞 = Duploid.Duploid 𝒞
    module 𝒟 = Duploid.Duploid 𝒟

  open 𝒟

  field
    F : PF.Functor 𝒞.𝒟 𝒟.𝒟

  open PF.Functor F

  field
    F-wrap-Thunkable : forall {N : 𝒞.Ob ⊝} -> Thunkable (F₁ (𝒞.wrap {N = N}))
    F-force-Linear : forall {P : 𝒞.Ob +} -> Linear (F₁ (𝒞.force {P = P}))

max_stars_repo_name: elpinal/duploids

max_issues_repo_name: elpinal/duploids

max_forks_repo_name: elpinal/duploids


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

module Cubical.Structures.Ring where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma

open import Cubical.Foundations.SIP renaming (SNS-PathP to SNS)

open import Cubical.Structures.NAryOp
open import Cubical.Structures.Monoid hiding (⟨_⟩)
open import Cubical.Structures.AbGroup hiding (⟨_⟩)
open import Cubical.Structures.Pointed

private
  variable
    ℓ ℓ' : Level

raw-ring-structure : Type ℓ → Type ℓ
raw-ring-structure X = (X → X → X) × X × (X → X → X)

-- Maybe this is not the best way? (Suggestions welcome, maybe having raw-monoid-iso defined?)
raw-ring-is-SNS : SNS {ℓ} raw-ring-structure _
raw-ring-is-SNS = join-SNS (nAryFunIso 2) (nAryFunSNS 2)
                           (join-iso pointed-iso (nAryFunIso 2))
                           (join-SNS pointed-iso pointed-is-SNS (nAryFunIso 2) (nAryFunSNS 2))

ring-axioms : (X : Type ℓ) (s : raw-ring-structure X) → Type ℓ
ring-axioms X (_+_ , ₁ , _·_) = abelian-group-axioms X _+_ ×
                                monoid-axioms X (₁ , _·_) ×
                                ((x y z : X) → x · (y + z) ≡ (x · y) + (x · z)) ×
                                ((x y z : X) → (x + y) · z ≡ (x · z) + (y · z))

ring-structure : Type ℓ → Type ℓ
ring-structure = add-to-structure raw-ring-structure ring-axioms

Ring : Type (ℓ-suc ℓ)
Ring {ℓ} = TypeWithStr ℓ ring-structure

ring-iso : StrIso ring-structure ℓ
ring-iso = add-to-iso (join-iso (nAryFunIso 2) (join-iso pointed-iso (nAryFunIso 2))) ring-axioms

ring-axioms-isProp : (X : Type ℓ) (s : raw-ring-structure X) → isProp (ring-axioms X s)
ring-axioms-isProp X (_+_ , ₁ , _·_) = isPropΣ (abelian-group-axioms-isProp X _+_)
                                      λ _ → isPropΣ (monoid-axioms-are-Props X (₁ , _·_))
                                      λ { (isSetX , _) → isPropΣ (isPropΠ3 (λ _ _ _ → isSetX _ _))
                                      λ _ → isPropΠ3 (λ _ _ _ → isSetX _ _)}

ring-is-SNS : SNS {ℓ} ring-structure ring-iso
ring-is-SNS = add-axioms-SNS _ ring-axioms-isProp raw-ring-is-SNS

RingPath : (M N : Ring {ℓ}) → (M ≃[ ring-iso ] N) ≃ (M ≡ N)
RingPath = SIP ring-is-SNS

-- Rings have an abelian group

Ring→AbGroup : Ring {ℓ} → AbGroup {ℓ}
Ring→AbGroup (R , (_+_ , _) , +AbGroup , _) = R , _+_ , +AbGroup

-- Rings have a monoid

Ring→Monoid : Ring {ℓ} → Monoid {ℓ}
Ring→Monoid (R , (_ , ₁ , _·_) , _ , ·Monoid , _) = R , (₁ , _·_) , ·Monoid

-- Ring extractors

⟨_⟩ : Ring {ℓ} → Type ℓ
⟨ R , _ ⟩ = R

module _ (R : Ring {ℓ}) where
  ring+-operation = abgroup-operation (Ring→AbGroup R)

  ring-is-set = abgroup-is-set (Ring→AbGroup R)

  ring+-assoc = abgroup-assoc (Ring→AbGroup R)

  ring+-id = abgroup-id (Ring→AbGroup R)

  ring+-rid = abgroup-rid (Ring→AbGroup R)

  ring+-lid = abgroup-lid (Ring→AbGroup R)

  ring+-inv = abgroup-inv (Ring→AbGroup R)

  ring+-rinv = abgroup-rinv (Ring→AbGroup R)

  ring+-linv = abgroup-linv (Ring→AbGroup R)

  ring+-comm = abgroup-comm (Ring→AbGroup R)

  ring·-operation = monoid-operation (Ring→Monoid R)

  ring·-assoc = monoid-assoc (Ring→Monoid R)

  ring·-id = monoid-id (Ring→Monoid R)

  ring·-rid = monoid-rid (Ring→Monoid R)

  ring·-lid = monoid-lid (Ring→Monoid R)

module ring-syntax where

  ring+-operation-syntax : (R : Ring {ℓ}) → ⟨ R ⟩ → ⟨ R ⟩ → ⟨ R ⟩
  ring+-operation-syntax R = ring+-operation R

  infixr 14 ring+-operation-syntax
  syntax ring+-operation-syntax R x y = x +⟨ R ⟩ y

  ring·-operation-syntax : (R : Ring {ℓ}) → ⟨ R ⟩ → ⟨ R ⟩ → ⟨ R ⟩
  ring·-operation-syntax R = ring·-operation R

  infixr 18 ring·-operation-syntax
  syntax ring·-operation-syntax R x y = x ·⟨ R ⟩ y

open ring-syntax

ring-rdist : (R : Ring {ℓ}) (x y z : ⟨ R ⟩) → x ·⟨ R ⟩ (y +⟨ R ⟩ z) ≡ (x ·⟨ R ⟩ y) +⟨ R ⟩ (x ·⟨ R ⟩ z)
ring-rdist (_ , _ , _ , _ , P , _) = P

ring-ldist : (R : Ring {ℓ}) (x y z : ⟨ R ⟩) → (x +⟨ R ⟩ y) ·⟨ R ⟩ z ≡ (x ·⟨ R ⟩ z) +⟨ R ⟩ (y ·⟨ R ⟩ z)
ring-ldist (_ , _ , _ , _ , _ , P) = P

-- Ring ·syntax

module ring-·syntax (R : Ring {ℓ}) where

  infixr 14 _+_
  infixr 18 _·_
  infix  15 -_

  _+_ = ring+-operation R

  _·_ = ring·-operation R

  ₀ = ring+-id R

  ₁ = ring·-id R

  -_ = ring+-inv R


text:
open import Common.Prelude hiding (_>>=_)
open import Common.Reflection
open import Common.Equality
open import Agda.Builtin.Sigma

record Functor (F : Set → Set) : Set₁ where
  field
    fmap : ∀ {A B} → (A → B) → F A → F B

IdF : Functor (λ A → A)
unquoteDef IdF =
  defineFun IdF (clause (("x" , vArg unknown) ∷ ("f" , vArg unknown) ∷ [])
                        (vArg (projP (quote Functor.fmap)) ∷ vArg (var 1) ∷ vArg (var 0) ∷ [])
                        (var 1 (vArg (var 0 []) ∷ [])) ∷ [])

check : ∀ {A B} (f : A → B) (x : A) → Functor.fmap IdF f x ≡ f x
check f x = refl

open Functor {{...}}

instance
  InstF : Functor (λ A → A)
  unquoteDef InstF =
    defineFun InstF (clause (("x" , vArg unknown) ∷ ("f" , vArg unknown) ∷ [])
                            (iArg (projP (quote fmap)) ∷ vArg (var 1) ∷ vArg (var 0) ∷ [])
                            (var 1 (vArg (var 0 []) ∷ [])) ∷ [])

check₁ : ∀ {A B} (f : A → B) (x : A) → fmap f x ≡ f x
check₁ f x = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

infixr 4 _>>=_
_>>=_ = bindTC

login : String → String
login "secret" = "access granted"
login _        = "access denied"

macro
  getDef : Name → Term → TC ⊤
  getDef f hole =
    getDefinition f >>= λ def → quoteTC def >>= unify hole

test : Definition
test = getDef login


text:
module Everything where

import Prelude
import Category

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

-- The syntax of STLC.
import STLC.Syntax

-- A simplification of Coquand 2002,
-- with de Bruijn indices and implicit substitutions.
import STLC.Coquand.Renaming
import STLC.Coquand.Substitution
import STLC.Coquand.Normalisation   -- TODO: Fill postulates
import STLC.Coquand.Convertibility  -- TODO: Simplify β-reduction rule
import STLC.Coquand.Completeness    -- TODO: Fill postulates
import STLC.Coquand.Soundness       -- TODO: Fill postulates

-- A restyling of Kovacs 2017.
import STLC.Kovacs.Embedding
import STLC.Kovacs.Substitution
import STLC.Kovacs.NormalForm
import STLC.Kovacs.Normalisation
import STLC.Kovacs.Convertibility
import STLC.Kovacs.Completeness
import STLC.Kovacs.PresheafRefinement
import STLC.Kovacs.Soundness

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

-- The syntax of STLC, with simple products.
import STLC1.Syntax

-- An extension of Kovacs 2017.
import STLC1.Kovacs.Embedding
import STLC1.Kovacs.Substitution
import STLC1.Kovacs.NormalForm
import STLC1.Kovacs.Normalisation
import STLC1.Kovacs.Convertibility
import STLC1.Kovacs.Completeness
import STLC1.Kovacs.PresheafRefinement
import STLC1.Kovacs.Soundness

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

-- The syntax of STLC, with simple products and coproducts.
import STLC2.Syntax

-- An extension of Kovacs 2017.
import STLC2.Kovacs.Embedding
import STLC2.Kovacs.Substitution
import STLC2.Kovacs.NormalForm
import STLC2.Kovacs.Normalisation.SoundNotComplete
import STLC2.Kovacs.Normalisation.Experimental
import STLC2.Kovacs.Normalisation
import STLC2.Kovacs.Convertibility
import STLC2.Kovacs.Completeness           -- TODO: Finish this
-- import STLC2.Kovacs.PresheafRefinement  -- TODO: Start this
-- import STLC2.Kovacs.Soundness           -- TODO: Start this

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

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Implementation.Standard.Relation.Sets where

open import Light.Level using (_⊔_)
open import Light.Variable.Levels
open import Light.Variable.Sets
open import Light.Library.Relation using (Base ; Kind ; Style)
open import Light.Library.Data.Unit as Unit using (Unit ; unit)
open import Light.Library.Data.Empty as Empty using (Empty)
open import Light.Library.Data.Both as Both using (Both)
import Light.Library.Data.Product as Product
open import Light.Library.Data.These as These using (These)
import Light.Implementation.Standard.Data.Unit
import Light.Implementation.Standard.Data.Empty
import Light.Implementation.Standard.Data.Product
import Light.Implementation.Standard.Data.These

instance kind : Kind
kind = record { Proposition = λ ℓ → Set ℓ }

instance style : Style kind
style = record { Implementation }
      where
      module Implementation where
            true = Unit
            false = Empty

            ¬_ : Set ℓ → Set ℓ
            ¬ 𝕒 = 𝕒 → Empty

            _∧_ = Both
            _∨_ = These

            _⇢_ : Set aℓ → Set bℓ → Set (aℓ ⊔ bℓ)
            𝕒 ⇢ 𝕓 = 𝕒 → 𝕓

            True : Set ℓ → Set ℓ
            True 𝕒 = 𝕒
            False = ¬_

            true‐is‐true = unit
            false‐is‐false : _
            false‐is‐false ()

instance base : Base
base = record { kind = kind ; style = style }


text:
-- Agda program using the Iowa Agda library

open import bool

module PROOF-permlength
  (Choice : Set)
  (choose : Choice → 𝔹)
  (lchoice : Choice → Choice)
  (rchoice : Choice → Choice)
  where

open import eq
open import bool
open import nat
open import list
open import maybe

---------------------------------------------------------------------------
-- Translated Curry operations:

insert : {a : Set} → Choice → a → 𝕃 a → 𝕃 a
insert c1 x [] = x :: []
insert c1 y (z :: u) = if choose c1 then y :: (z :: u) else z :: (insert (lchoice c1) y u)

perm : {a : Set} → Choice → 𝕃 a → 𝕃 a
perm c1 [] = []
perm c1 (x :: y) = insert c1 x (perm (lchoice c1) y)

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

insert-inc-length : ∀ {a : Set} → (ch : Choice) (x : a) (xs : 𝕃 a)
                 → length (insert ch x xs) ≡ suc (length xs)
insert-inc-length ch x [] = refl
insert-inc-length ch x (y :: ys) with choose ch
... | tt = refl
... | ff rewrite insert-inc-length (lchoice ch) x ys = refl

permlength : {a : Set} → (c1 : Choice) → (x : 𝕃 a) → (length x) ≡ (length (perm c1 x))
permlength c1 [] = refl
permlength c1 (x :: xs)
 rewrite insert-inc-length c1 x (perm (lchoice c1) xs)
         | permlength (lchoice c1) xs
  = refl

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

max_stars_repo_name: phlummox/curry-tools

max_issues_repo_name: phlummox/curry-tools

max_forks_repo_name: phlummox/curry-tools


text:
module SHE-Prelude where

record Functor (T : Set -> Set) : Set1 where
  field
    -- OPERATIONS ----------------------------------------------
    map     : forall {X Y} -> (X -> Y) -> T X -> T Y

record Applicative (T : Set -> Set) : Set1 where
  field
    -- OPERATIONS ----------------------------------------------
    pure         : forall {X} -> X -> T X
    _<*>_        : forall {X Y} -> T (X -> Y) -> T X -> T Y

data Zero : Set where

magic : forall {l}{A : Set l} -> Zero -> A
magic ()

record One : Set where
  constructor <>
open One public
{-# COMPILED_DATA One () () #-}

max_stars_repo_name: iain-logan/she

max_issues_repo_name: iain-logan/she

max_forks_repo_name: iain-logan/she


text:
-- Note that this module assumes function extensionality
module guarded-recursion.prelude where

open import Level
              public
              using (_⊔_)
              renaming (zero to ₀
                       ;suc  to ₛ)
open import Function
              public
              using (id; _∘_; _∘′_)
open import Data.Nat
              public
              using (ℕ; _+_)
              renaming (zero to O
                       ;suc  to S)
open import Data.Bool
              public
              renaming (Bool  to 𝟚
                       ;false to 0₂
                       ;true  to 1₂)
open import Data.Sum
              public
              using (_⊎_; [_,_])
              renaming (inj₁ to inl
                       ;inj₂ to inr)
open import Data.Maybe
              public
              using (Maybe; nothing; just)
open import Data.Empty
              public
              renaming (⊥ to 𝟘
                       ;⊥-elim to 𝟘-elim)
open import Data.Unit
              public
              using ()
          --  using (Hidden; Unit; hide; reveal)
              renaming (⊤ to 𝟙)
open import Data.Unit.NonEta
              public
              using (Hidden; Unit; hide; reveal)
import      Data.Product
open        Data.Product
              public
              using (Σ; _×_; _,_; curry; <_,_>)
              renaming (proj₁ to fst
                       ;proj₂ to snd)
open import Relation.Binary
              public
              using (Reflexive)
import      Relation.Binary.PropositionalEquality
open        Relation.Binary.PropositionalEquality
              public
              using (_≡_)
              renaming (subst to transport
                       ;refl  to idp
                       ;sym   to !
                       ;cong  to ap)
import Relation.Binary.PropositionalEquality.TrustMe
module ThisIsUnsafeButPlease = Relation.Binary.PropositionalEquality.TrustMe

-- using stdlib only
infixr 8 _∙_
_∙_ = Relation.Binary.PropositionalEquality.trans

ℕ² = ℕ × ℕ

-- Let's rename "Set₀" as "Type" to avoid confusion with set-theory
Type = Set

-- Let's rename "Set ℓ" as "Type_ ℓ" to avoid confusion with set-theory
Type_ : ∀ ℓ → Set (ₛ ℓ)
Type_ ℓ = Set ℓ

-→- : ∀ {a b} → Type_ a → Type_ b → Type_ (a ⊔ b)
-→- A B = A → B

Endo : ∀ {a} → Type_ a → Type_ a
Endo A = A → A

Fix : ∀ {a} → Type_ a → Type_ a
Fix X = (X → X) → X

postulate
  funext : ∀ {a b}
             {A : Type_ a} {B : A → Type_ b}
             {f g : (x : A) → B x}
           → (∀ x → f x ≡ g x)
           → f ≡ g

𝟘-elim-uniq! : ∀ {a} {A : Type_ a} {f : 𝟘 → A} → 𝟘-elim ≡ f
𝟘-elim-uniq! = funext (λ())

[,]-uniq! : ∀ {a b c} {A : Type_ a} {B : Type_ b} {C : Type_ c}
              {f : (A ⊎ B) → C}
            → [ f ∘ inl , f ∘ inr ] ≡ f
[,]-uniq! = funext p
  where p : (_ : _ ⊎ _) → _
        p (inl _) = idp
        p (inr _) = idp

module Coe {ℓ} where
    coe : {A B : Type_ ℓ} → A ≡ B → A → B
    coe = transport id

    coe! : {A B : Type_ ℓ} → A ≡ B → B → A
    coe! = transport id ∘ !

    module _ {a} {A : Type_ a} {P Q : A → Type_ ℓ} (p : P ≡ Q) {x} where
        coe₁ : P x → Q x
        coe₁ = transport (λ P → P x) p

        coe₁! : Q x → P x
        coe₁! = transport (λ P → P x) (! p)

    module _ {a b} {A : Type_ a} {B : Type_ b} {R S : A → B → Type_ ℓ} (p : R ≡ S) {x y} where
        coe₂ : R x y → S x y
        coe₂ = transport (λ R → R x y) p

        coe₂! : S x y → R x y
        coe₂! = transport (λ R → R x y) (! p)

[0:_1:_] : ∀ {a} {A : Type_ a} (a₀ a₁ : A) → 𝟚 → A
[0: a₀ 1: a₁ ] 0₂ = a₀
[0: a₀ 1: a₁ ] 1₂ = a₁

max_stars_repo_name: np/guarded-recursion

max_issues_repo_name: np/guarded-recursion

max_forks_repo_name: np/guarded-recursion


text:
module Categories.Terminal where

open import Library
open import Categories
open import Categories.Sets
open Cat

record Term {a b} (C : Cat {a}{b})(T : Obj C) : Set (a ⊔ b) where
  constructor term
  field t : ∀{X} → Hom C X T
        law : ∀{X}{f : Hom C X T} → t {X} ≅ f

OneSet : Term Sets ⊤
OneSet = record {t = λ _ → _; law = ext (λ _ → refl)}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

{- Addition -}

_+_ : ℕ → ℕ → ℕ
zero    + n =  n
(suc m) + n =  suc (m + n)

_ : 3 + 4 ≡ 7
_ =
  begin
    3 + 4
  ≡⟨⟩
    suc (2 + 4)
  ≡⟨⟩
    suc (suc (1 + 4))
  ≡⟨⟩
    suc (suc (suc (0 + 4)))
  ≡⟨⟩
    suc (suc (suc 4))
  ≡⟨⟩
    7
  ∎

_ : 1 + 1 ≡ 2
_ = refl

{- Multiplication -}

_*_ : ℕ → ℕ → ℕ
zero * n    = zero
(suc m) * n = n + (m * n)

_ : 2 * 2 ≡ 4
_ =
  begin
    2 * 2
  ≡⟨⟩
    2 + (1 * 2)
  ≡⟨⟩
    2 + (2 + (0 * 2))
  ≡⟨⟩
    2 + 2
  ≡⟨⟩
    4
  ∎

_ : 1 * 1 ≡ 1
_ = refl

{- Exponentiation -}

_^_ : ℕ → ℕ → ℕ
n ^ 0       = 1
n ^ (suc m) = n * (n ^ m)

_ : 2 ^ 3 ≡ 8
_ =
  begin
    2 ^ 3
  ≡⟨⟩
    2 * (2 ^ 2)
  ≡⟨⟩
    2 * (2 * (2 ^ 1))
  ≡⟨⟩
    2 * (2 * (2 * (2 ^ 0)))
  ≡⟨⟩
    2 * (2 * (2 * 1))
  ≡⟨⟩
    8
  ∎

_ : 42 ^ 0 ≡ 1
_ = refl

{- Monus -}

_∸_ : ℕ → ℕ → ℕ
m       ∸ zero    = m
zero    ∸ (suc n) = zero
(suc m) ∸ (suc n) = m ∸ n

_ : 2 ∸ 1 ≡ 1
_ =
  begin
    2 ∸ 1
  ≡⟨⟩
    1 ∸ 0
  ≡⟨⟩
    1
  ∎

_ : 7 ∸ 4 ≡ 3
_ = refl

_ : 4 ∸ 7 ≡ 0
_ = refl

max_stars_repo_name: anqurvanillapy/fpl

max_issues_repo_name: anqurvanillapy/fpl

max_forks_repo_name: anqurvanillapy/fpl


text:
module String where

import      Lvl
open import Data.Boolean
open import Data.List
open import Numeral.Natural
open import Type

postulate Char : Type{Lvl.𝟎}
{-# BUILTIN CHAR Char #-}

postulate String : Type{Lvl.𝟎}
{-# BUILTIN STRING String #-}

private
  module Primitives where
    primitive primStringToList   : String → List(Char)
    primitive primStringFromList : List(Char) → String
    primitive primStringAppend   : String → String → String
    primitive primStringEquality : String → String → Bool
    primitive primShowChar       : Char → String
    primitive primShowString     : String → String
    primitive primShowNat        : ℕ → String

    primitive primIsLower      : Char → Bool
    primitive primIsDigit      : Char → Bool
    primitive primIsAlpha      : Char → Bool
    primitive primIsSpace      : Char → Bool
    primitive primIsAscii      : Char → Bool
    primitive primIsLatin1     : Char → Bool
    primitive primIsPrint      : Char → Bool
    primitive primIsHexDigit   : Char → Bool
    primitive primToUpper      : Char → Char
    primitive primToLower      : Char → Char
    primitive primCharToNat    : Char → ℕ
    primitive primNatToChar    : ℕ → Char
    primitive primCharEquality : Char → Char → Bool

module String where
  open Primitives renaming
    ( primStringToList   to toList
    ; primStringFromList to fromList
    ; primStringAppend   to _++_
    ; primStringEquality to _==_
    ; primShowChar       to fromChar
    ; primShowNat        to fromℕ
    ) public

  {-
  open import Relator.Equals
  open import Relator.Equals.Proofs
  open import Syntax.Transitivity

  primitive primEraseEquality : ∀{ℓ}{A : Type{ℓ}}{x y : A} → (x ≡ y) → (x ≡ y)

  unsafeDefinitionalEquality : ∀{ℓ}{A : Type{ℓ}}{x y : A} → (x ≡ y)
  unsafeDefinitionalEquality {x = x}{y = y} = primEraseEquality xy where
    postulate xy : x ≡ y

  toList-fromList-of-[⊰] : ∀{x}{l} → (toList(fromList(x ⊰ l)) ≡ x ⊰ toList(fromList(l)))
  toList-fromList-of-[⊰] = unsafeDefinitionalEquality

  fromList-toList-inverse : ∀{s} → (fromList(toList(s)) ≡ s)
  fromList-toList-inverse = unsafeDefinitionalEquality

  toList-fromList-inverse : ∀{l} → (toList(fromList(l)) ≡ l)
  toList-fromList-inverse {∅}     = [≡]-intro
  toList-fromList-inverse {x ⊰ l} = toList-fromList-of-[⊰] 🝖 [≡]-with(x ⊰_) (toList-fromList-inverse {l})
  -}

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:
{- This file describes properties of computable relations. -}

open import bool
open import level
open import eq
open import product
open import product-thms

module relations {ℓ ℓ' : level}{A : Set ℓ} (_≥A_ : A → A → Set ℓ') where

reflexive : Set (ℓ ⊔ ℓ')
reflexive = ∀ {a : A} → a ≥A a

transitive : Set (ℓ ⊔ ℓ')
transitive = ∀ {a b c : A} → a ≥A b → b ≥A c → a ≥A c

preorder : Set (ℓ ⊔ ℓ')
preorder = reflexive ∧ transitive

_iso_ : A → A → Set ℓ'
d iso d' = d ≥A d' ∧ d' ≥A d

iso-intro : ∀{x y : A} → x ≥A y → y ≥A x → x iso y
iso-intro p1 p2 = p1 , p2

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


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

module Cubical.Categories.Type where

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

open Precategory

module _ ℓ where
  TYPE : Precategory (ℓ-suc ℓ) ℓ
  TYPE .ob = Type ℓ
  TYPE .Hom[_,_] A B = A → B
  TYPE .id A  = λ x → x
  TYPE ._⋆_ f g = λ x → g (f x)
  TYPE .⋆IdL f = refl
  TYPE .⋆IdR f = refl
  TYPE .⋆Assoc f g h = refl


text:
{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
            --no-subtyping #-}

module Agda.Builtin.Reflection.Properties where

open import Agda.Builtin.Reflection
open import Agda.Builtin.Equality

primitive

  primMetaToNatInjective : ∀ a b → primMetaToNat a ≡ primMetaToNat b → a ≡ b
  primQNameToWord64sInjective : ∀ a b → primQNameToWord64s a ≡ primQNameToWord64s b → a ≡ b


text:
------------------------------------------------------------------------
-- Some theory of equivalences with erased "proofs", developed using
-- Cubical Agda
------------------------------------------------------------------------

-- This module instantiates and reexports code from
-- Equivalence.Erased.

{-# OPTIONS --erased-cubical --safe #-}

import Equality.Path as P

module Equivalence.Erased.Cubical
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Erased.Cubical eq

import Equivalence.Erased
open Equivalence.Erased equality-with-J public
  hiding (module []-cong)
open Equivalence.Erased.[]-cong
  equality-with-J instance-of-[]-cong-axiomatisation
  public

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

-- Defines Restriction Category
--   https://ncatlab.org/nlab/show/restriction+category
-- but see also
--   https://github.com/jmchapman/restriction-categories

-- Notation choice: one of the interpretations is that the
-- restriction structure captures the "domain of definedness"
-- of a morphism, as a (partial) identity. As this is positive
-- information, we will use f ↓ (as a postfix operation) to
-- denote this. Note that computability theory uses the same
-- notation to mean definedness.

-- Note, as we're working in Setoid-Enriched Categories, we need
-- to add an explicit axiom, that ↓ preserves ≈
module Categories.Category.Restriction where

open import Level using (Level; _⊔_)

open import Categories.Category.Core using (Category)

private
  variable
    o ℓ e : Level

record Restriction (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
  open Category C using (Obj; _⇒_; _∘_; _≈_; id)

  field
    _↓ :  {A B : Obj} → A ⇒ B → A ⇒ A
    -- partial identity on the right
    pidʳ : {A B : Obj} {f : A ⇒ B} → f ∘ f ↓ ≈ f
    -- the domain-of-definition arrows commute
    ↓-comm : {A B C : Obj} {f : A ⇒ B} {g : A ⇒ C} → f ↓ ∘ g ↓ ≈ g ↓ ∘ f ↓
    -- domain-of-definition denests (on the right)
    ↓-denestʳ : {A B C : Obj} {f : A ⇒ B} {g : A ⇒ C} → (g ∘ f ↓) ↓ ≈ g ↓ ∘ f ↓
    -- domain-of-definition has a skew-commutative law
    ↓-skew-comm : {A B C : Obj} {g : A ⇒ B} {f : C ⇒ A} → g ↓ ∘ f ≈ f ∘ (g ∘ f) ↓
    -- and the new axiom, ↓ is a congruence
    ↓-cong : {A B : Obj} {f g : A ⇒ B} → f ≈ g → f ↓ ≈ g ↓

  -- it is convenient to define the total predicate in this context
  total : {A B : Obj} (f : A ⇒ B) → Set e
  total f = f ↓ ≈ id

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:
module Formalization.LambdaCalculus where

import      Lvl
open import Data
open import Numeral.Natural
open import Numeral.Finite
open import Syntax.Number
open import Type

-- A lambda term (A term in the language of lambda calculus).
-- This is encoded with an abstraction depth which ensures that every term is well-formed.
-- `Term(𝟎)` is the type of closed terms, terms that have no unbound variables.
--   In this representation, it means that there are no occurrences of `Var(_)` in a term.
-- `Term(𝐒(n))` for some `n` is the types of open terms with possibly `n` number of different variables, terms that have unbound variables.
--   In this representation, it means that there can be `Var(i)` for `i < n` in a term.
data Term : ℕ → Type{0} where
  -- The term which represents applying the second term on the first term.
  -- Representation in function notation:
  --   (Apply f(x)) is f(x)
  Apply : ∀{d} → Term(d) → Term(d) → Term(d)

  -- The term which represents bounding a new variable (introducing a variable).
  -- Representation in function notation:
  --   (Abstract{n} term) is (xₙ ↦ term)
  Abstract : ∀{d} → Term(𝐒(d)) → Term(d)

  -- The term which represents a specific variable in scope.
  -- Representation in function notation:
  --   (Var(n)) is xₙ
  Var : ∀{d} → 𝕟(d) → Term(d)

-- An expression in the language of lambda calculus is a closed term.
Expression : Type{0}
Expression = Term(0)

module VarNumeralSyntax where
  -- Syntax for writing Var as a numeral.
  instance
    Term-from-ℕ : ∀{N} → Numeral(Term(N))
    Numeral.restriction-ℓ ( Term-from-ℕ {N} ) = Numeral.restriction-ℓ ( 𝕟-from-ℕ {N} )
    Numeral.restriction   ( Term-from-ℕ {N} ) = Numeral.restriction ( 𝕟-from-ℕ {N} )
    num                   ⦃ Term-from-ℕ {N} ⦄ (n) ⦃ proof ⦄ = Var(num n)

module OperSyntax where
  open VarNumeralSyntax public

  infixr 100 _↦_
  infixl 101 _←_

  pattern _↦_ d expr = Term.Abstract{d} expr
  pattern _←_ a b    = Term.Apply a b

module ExplicitLambdaSyntax where
  open VarNumeralSyntax public

  infixl 101 _←_

  pattern 𝜆 d expr = Term.Abstract{d} expr
  pattern _←_ a b  = Term.Apply a b


text:
module ctxt-types where

open import lib
open import cedille-types
open import general-util
open import syntax-util

location : Set
location = string × posinfo -- file path and starting position in the file

-- file path and starting / ending position in file
span-location = string × posinfo × posinfo

-- missing locations
missing-location : location
missing-location = ("missing" , "missing")

missing-span-location : span-location
missing-span-location = ("missing" , "missing" , "missing")

{- we will generally keep classifiers of variables in hnf in the ctxt, although
   we will not necessarily unfold recursive type definitions. -}

defScope : Set
defScope = 𝔹
pattern localScope = tt
pattern globalScope = ff
pattern concrete-datatype = globalScope
pattern abstract-datatype = localScope

defParams : Set
defParams = maybe params

data ctxt-info : Set where
  -- for defining a datatype
--  datatype-def : defParams → (ind reg : kind) → ctrs → ctxt-info

  -- for defining a datatype constructor
  ctr-def : params → type → (ctrs-length ctr-index ctr-unerased-arrows : ℕ) → ctxt-info

  -- for declaring the type that proves a type is a datatype (X/Mu)
--  mu-def : defParams → var → kind → ctxt-info

  -- for declaring a variable to have a given type (with no definition)
  term-decl : type → ctxt-info

  -- for defining a variable to equal a term with a given type
  -- maybe term, because datatype X/Mu and X/mu have params, etc... but no def
  term-def : defParams → opacity → maybe term → type → ctxt-info

  -- for untyped term definitions
  term-udef : defParams → opacity → term → ctxt-info

  -- for declaring a variable to have a given kind (with no definition)
  type-decl : kind → ctxt-info

  -- for defining a variable to equal a type with a given kind
  type-def : defParams → opacity → maybe type → kind → ctxt-info

  -- for defining a variable to equal a kind
  kind-def : params → kind → ctxt-info

  -- to rename a variable at any level to another
  rename-def : var → ctxt-info

  -- representing a declaration of a variable with no other information about it
  var-decl : ctxt-info

sym-info : Set
sym-info = ctxt-info × location

-- module filename, name, parameters, and qualifying substitution
mod-info : Set
mod-info = string × string × params × qualif

is-term-level : ctxt-info → 𝔹
is-term-level (term-decl _) = tt
is-term-level (term-def _ _ _ _) = tt
is-term-level (term-udef _ _ _) = tt
is-term-level (ctr-def _ _ _ _ _ ) = tt
is-term-level _ = ff

data ctxt : Set where
  mk-ctxt : (mod : mod-info) →                     -- current module
            (syms : trie (string × 𝕃 string) × trie string × trie params × trie ℕ × Σ ℕ (𝕍 string)) →    -- map each filename to its module name and the symbols declared in that file, map each module name to its filename and params, and file ID's for use in to-string.agda
            (i : trie sym-info) →                  -- map symbols (from Cedille files) to their ctxt-info and location
            (sym-occurrences : trie (𝕃 (var × posinfo × string))) →  -- map symbols to a list of definitions they occur in (and relevant file info)
            (Δ : trie (params × kind × kind × ctrs) × trie (var × var × args) × trie var) → -- datatype info: (concrete/global datatypes × abstract/local datatypes × datatype/Mu map)
            ctxt

ctxt-binds-var : ctxt → var → 𝔹
ctxt-binds-var (mk-ctxt (_ , _ , _ , q) _ i _ _) x = trie-contains q x || trie-contains i x

ctxt-var-decl : var → ctxt → ctxt
ctxt-var-decl v (mk-ctxt (fn , mn , ps , q) syms i symb-occs Δ) =
  mk-ctxt (fn , mn , ps , (trie-insert q v (v , []))) syms (trie-insert i v (var-decl , "missing" , "missing")) symb-occs Δ

ctxt-var-decl-loc : posinfo → var → ctxt → ctxt
ctxt-var-decl-loc pi v (mk-ctxt (fn , mn , ps , q) syms i symb-occs Δ) =
  mk-ctxt (fn , mn , ps , (trie-insert q v (v , []))) syms (trie-insert i v (var-decl , fn , pi)) symb-occs Δ

qualif-var : ctxt → var → var
qualif-var (mk-ctxt (_ , _ , _ , q) _ _ _ _) v with trie-lookup q v
...| just (v' , _) = v'
...| nothing = v

start-modname : start → string
start-modname (File _ _ _ mn _ _ _) = mn

ctxt-get-current-filename : ctxt → string
ctxt-get-current-filename (mk-ctxt (fn , _) _ _ _ _) = fn

ctxt-get-current-mod : ctxt → mod-info
ctxt-get-current-mod (mk-ctxt m _ _ _ _) = m

ctxt-get-current-modname : ctxt → string
ctxt-get-current-modname (mk-ctxt (_ , mn , _ , _) _ _ _ _) = mn

ctxt-get-current-params : ctxt → params
ctxt-get-current-params (mk-ctxt (_ , _ , ps , _) _ _ _ _) = ps

ctxt-get-symbol-occurrences : ctxt → trie (𝕃 (var × posinfo × string))
ctxt-get-symbol-occurrences (mk-ctxt _ _ _ symb-occs _) = symb-occs

ctxt-set-symbol-occurrences : ctxt → trie (𝕃 (var × posinfo × string)) → ctxt
ctxt-set-symbol-occurrences (mk-ctxt fn syms i symb-occs Δ) new-symb-occs = mk-ctxt fn syms i new-symb-occs Δ

max_stars_repo_name: CarlOlson/cedille

max_issues_repo_name: CarlOlson/cedille

max_forks_repo_name: CarlOlson/cedille


text:
-- {-# OPTIONS -v tc.cover.split.con:100 #-}

{-# OPTIONS --show-implicit #-}

data D : Set where
  d : {x : D} → D

f : D → Set
f y = {!!}


text:
open import Sec2
data Vec (A : Set) : ℕ → Set where
  [] : Vec A Z
  _∷_ : {n : ℕ} → A → Vec A n → Vec A (S n)

head : {A : Set} → {n : ℕ} → Vec A (S n) → A
head (x ∷ vs) = x

tail : {A : Set} → {n : ℕ} → Vec A (S n) → Vec A n
tail (x ∷ vs) = vs

map : {A B : Set} → {n : ℕ} → (f : A → B) → Vec A n → Vec B n
map f [] = []
map f (x ∷ vs) = f x ∷ map f vs

zip : {A B : Set} → {n : ℕ} → Vec A n → Vec B n → Vec (A Π B) n
zip [] [] = []
zip (x ∷ xs) (x₁ ∷ ys) = < x , x₁ > ∷ zip xs ys


text:
module x02-842Induction-hc-2 where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)

-- PLFA coverage of identity, associativity, commutativity, distributivity.

-- + associative
_ : (3 + 4) + 5 ≡ 3 + (4 + 5)
_ =
  begin
  (3 + 4) + 5 ≡⟨⟩
       7  + 5 ≡⟨⟩
           12 ≡⟨⟩
   3 +  9     ≡⟨⟩
   3 + (4 + 5)
  ∎

+-identityᴸ : ∀ (m : ℕ) → zero + m ≡ m
+-identityᴸ m = refl

0+ : ∀ (m : ℕ) → zero + m ≡ m
0+ = +-identityᴸ

+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ  zero   = refl
+-identityʳ (suc m) = cong suc (+-identityʳ m)

+0 : ∀ (m : ℕ) → m + zero ≡ m
+0 = +-identityʳ

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc  zero   n p = refl
+-assoc (suc m) n p = cong suc (+-assoc m n p)

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc  zero   n = refl
+-suc (suc m) n = cong suc (+-suc m n)

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm  zero   n          --   zero + n  ≡ n + zero
                          --          n  ≡ n + zero
  rewrite +-identityʳ n   --          n  ≡ n
  = refl
+-comm (suc m) n          -- suc  m + n  ≡ n + suc m
                          -- suc (m + n) ≡ n + suc m
  rewrite +-suc n m       -- suc (m + n) ≡ suc (n + m)
  | cong suc (+-comm m n) -- suc (n + m) ≡ suc (n + m)
  = refl

-- without using induction/recursion
+-swap : ∀ (m n p : ℕ) → (m + n) + p ≡ n + (m + p)
+-swap  zero   n p = refl
+-swap (suc m) n p      -- suc  m + n + p  ≡ n + (suc m + p)
                        -- suc (m + n + p) ≡ n + suc (m + p)
  rewrite
    +-suc n (m + p)     -- suc (m + n + p) ≡ suc (n + (m + p))
  | sym (+-assoc n m p) -- suc (m + n + p) ≡ suc (n +  m + p)
  | +-comm m n          -- suc (n + m + p) ≡ suc (n +  m + p)
  = refl

*-+-rdistrib : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-+-rdistrib  zero   n p = refl
*-+-rdistrib (suc m) n p       -- (suc m + n)    * p  ≡ suc  m * p + n * p
                               -- p + (m + n)    * p  ≡ p +  m * p + n * p
  rewrite
    *-+-rdistrib m n p         -- p + (m * p + n * p) ≡ p +  m * p + n * p
  | +-assoc p (m * p) (n * p)  -- p + (m * p + n * p) ≡ p + (m * p + n * p)
  = refl

*-assoc : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
*-assoc  zero   n p = refl
*-assoc (suc m) n p            -- suc  m * n    * p ≡     suc m * (n * p)
                               -- (n + m * n)   * p ≡ n * p + m * (n * p)
  rewrite
    *-+-rdistrib n (m * n) p   -- n * p + m * n * p ≡ n * p + m * (n * p)
  | sym (*-assoc m n p)        -- n * p + m * n * p ≡ n * p + m *  n * p
  = refl

*0 : ∀ (m : ℕ) → m * zero ≡ zero
*0  zero   = refl
*0 (suc m) = *0 m

*1 : ∀ (m : ℕ) → m * suc zero ≡ m
*1  zero   = refl
*1 (suc m) = cong suc (*1 m)

-- like addition, helper lemmas needed
*-comm : ∀ (m n : ℕ) → m * n ≡ n * m
*-comm  zero   n rewrite *0 n = refl
*-comm  m   zero rewrite *0 m = refl
*-comm (suc m) (suc n)        -- suc       m * suc n   ≡ suc      n * suc m
                              -- suc (n +  m * suc n)  ≡ suc (m + n * suc m)
  rewrite
    *-comm m (suc n)          -- suc (n + (m + n * m)) ≡ suc (m +  n * suc m)
  | *-comm n (suc m)          -- suc (n + (m + n * m)) ≡ suc (m + (n + m * n))
  | sym (+-assoc n m (n * m)) -- suc (n +  m + n * m)  ≡ suc (m + (n + m * n))
  | sym (+-assoc m n (m * n)) -- suc (n +  m + n * m)  ≡ suc (m +  n + m * n)
  |      +-swap  n m (n * m)  -- suc (m + (n + n * m)) ≡ suc (m +  n + m * n)
  | sym (+-assoc m n (n * m)) -- suc (m +  n + n * m)  ≡ suc (m +  n + m * n)
  | *-comm m n                -- suc (m +  n + n * m)  ≡ suc (m +  n + n * m)
  = refl

0∸n≡0 : ∀ (m : ℕ) → zero ∸ m ≡ zero
0∸n≡0  zero   = refl
0∸n≡0 (suc m) rewrite 0∸n≡0 m = refl

m∸0≡m : ∀ (m : ℕ) → m ∸ zero ≡ m
m∸0≡m m = refl

∸-+-assoc : ∀ (m n p : ℕ) → m ∸ n ∸ p ≡ m ∸ (n + p)
∸-+-assoc  zero        n       p      -- zero ∸ n ∸ p  ≡ zero ∸ (n + p)
  rewrite
    0∸n≡0 (n + p)                     -- 0 ∸ n ∸ p     ≡ 0
  | 0∸n≡0 n                           -- 0     ∸ p     ≡ 0
  | 0∸n≡0 p                           -- 0             ≡ 0
  = refl
∸-+-assoc      m    zero       p
  = refl
∸-+-assoc      m       n    zero      -- m ∸ n ∸ zero  ≡ m ∸ (n + zero)
  rewrite
    +0 n                              -- m ∸ n         ≡ m ∸  n
  = refl
∸-+-assoc (suc m) (suc n) (suc p)     -- m ∸ n ∸ suc p ≡ m ∸ (n + suc p)
  rewrite sym (∸-+-assoc m n (suc p)) -- m ∸ n ∸ suc p ≡ m ∸  n ∸ suc p
  = refl

------------------------------------------------------------------------------
-- Properties of binary representation.

-----
-- BEGIN : copied from x01-842Naturals-hc-2.agda

data Bin-ℕ : Set where
  bits : Bin-ℕ
  _x0 : Bin-ℕ → Bin-ℕ
  _x1 : Bin-ℕ → Bin-ℕ
bin-zero : Bin-ℕ
bin-zero = bits

bin-one : Bin-ℕ
bin-one = bits x1     -- 1 in binary

bin-two : Bin-ℕ
bin-two = bits x1 x0  -- 10 in binary

inc : Bin-ℕ → Bin-ℕ
inc  bits  = bits x1
inc (m x0) = m    x1
inc (m x1) = (inc m) x0

dbl : ℕ → ℕ
dbl zero = zero
dbl (suc m) = suc (suc (dbl m))

tob : ℕ → Bin-ℕ
tob  zero   = bits
tob (suc m) = inc (tob m)

fromb : Bin-ℕ → ℕ
fromb  bits  = zero
fromb (n x0) =      dbl (fromb n)
fromb (n x1) = suc (dbl (fromb n))

_bin-+_ : Bin-ℕ → Bin-ℕ → Bin-ℕ
bits   bin-+     n  =                    n
m      bin-+  bits  =            m
(m x0) bin-+ (n x0) =           (m bin-+ n) x0
(m x0) bin-+ (n x1) =      inc ((m bin-+ n) x0)
(m x1) bin-+ (n x0) =      inc ((m bin-+ n) x0)
(m x1) bin-+ (n x1) = inc (inc ((m bin-+ n) x0))

-- END : copied from x01-842Naturals-hc-2.agda
-----

-- Bin-ℕ version of dbl. Do not use tob/fromb.

dblb : Bin-ℕ → Bin-ℕ
dblb  bits  = bits
dblb (m x0) =           (dblb m) x0
dblb (m x1) = inc (inc ((dblb m) x0))

_ : dblb  bits ≡ bits
_ = refl
_ : dblb (bits       x0) ≡ bits          x0
_ = refl
_ : dblb (bits       x1) ≡ bits       x1 x0
_ = refl
_ : dblb (bits    x1 x0) ≡ bits    x1 x0 x0
_ = refl
_ : dblb (bits    x1 x1) ≡ bits    x1 x1 x0
_ = refl
_ : dblb (bits x1 x0 x0) ≡ bits x1 x0 x0 x0
_ = refl
_ : dblb (bits x1 x0 x1) ≡ bits x1 x0 x1 x0
_ = refl

from∘inc : ∀ (m : Bin-ℕ) → fromb (inc m) ≡ suc (fromb m)
from∘inc  bits  = refl
from∘inc (m x0) = refl
from∘inc (m x1) --       fromb (inc (m x1))  ≡ suc (fromb (m x1))
                --      dbl (fromb (inc m))  ≡ suc (suc (dbl (fromb m)))
  rewrite
    from∘inc m  --      dbl (suc (fromb m))  ≡ suc (suc (dbl (fromb m)))
                -- suc (suc (dbl (fromb m))) ≡ suc (suc (dbl (fromb m)))
  = refl

from∘tob : ∀ (m : ℕ) → fromb (tob m) ≡ m
from∘tob  zero   = refl
from∘tob (suc m)     -- fromb (tob (suc m)) ≡ suc m
                     -- fromb (inc (tob m)) ≡ suc m
  rewrite
    from∘inc (tob m) -- suc (fromb (tob m)) ≡ suc m
  | from∘tob m       -- suc             m   ≡ suc m
  = refl

-- ∀ (m : Bin-ℕ) → tob (fromb m) ≡ m cannot be proved.
-- Because there are multiple representations of ZERO.
-- This restriction can be proved.

to/from-corr : ∀ (b : Bin-ℕ) (n : ℕ) → b ≡ tob n → fromb b ≡ n
to/from-corr .bits  zero   refl = refl
to/from-corr .(inc (tob n)) (suc n) refl -- fromb (tob (suc n)) ≡ suc n
                                         -- fromb (inc (tob n)) ≡ suc n
  rewrite
    from∘inc (tob n)                     -- suc (fromb (tob n)) ≡ suc n
  | to/from-corr (tob n) n refl          -- suc             n   ≡ suc n
  = refl

dblb∘inc : ∀ (b : Bin-ℕ) → dblb (inc b) ≡ inc (inc (dblb b))
dblb∘inc  bits  = refl
dblb∘inc (b x0) = refl
dblb∘inc (b x1)  --       dblb (inc (b   x1)) ≡  inc (inc (dblb (b x1)))
                 --      (dblb (inc  b)  x0)  ≡ (inc (inc (dblb  b)) x0)
  rewrite
    dblb∘inc b   --  (inc (inc (dblb b)) x0)  ≡ (inc (inc (dblb  b)) x0)
  = refl

to∘dbl : ∀ (m : ℕ) → tob (dbl m) ≡ dblb (tob m)
to∘dbl  zero   = refl
to∘dbl (suc m)       --      tob (dbl  (suc m))  ≡      dblb (tob (suc m))
                     -- inc (inc (tob  (dbl m))) ≡      dblb (inc (tob m))
  rewrite
    to∘dbl m         -- inc (inc (dblb (tob m))) ≡      dblb (inc (tob m))
  | dblb∘inc (tob m) -- inc (inc (dblb (tob m))) ≡ inc (inc (dblb (tob m)))
  = refl

from∘dblb : ∀ (b : Bin-ℕ) → fromb (dblb b) ≡ dbl (fromb b)
from∘dblb  bits  = refl
from∘dblb (b x0)      --             fromb (dblb (b x0)) ≡ dbl (fromb (b x0))
                      --            dbl (fromb (dblb b)) ≡ dbl (dbl (fromb b))
  rewrite
    from∘dblb b       --            dbl  (dbl (fromb b)) ≡ dbl (dbl (fromb b))
  = refl
from∘dblb (b x1)      --             fromb (dblb (b x1)) ≡ dbl (fromb (b x1))
                      --     dbl (fromb (inc (dblb b)))  ≡ suc (suc (dbl (dbl (fromb b))))
  rewrite
    from∘inc (dblb b) --     dbl (suc (fromb (dblb b)))  ≡ suc (suc (dbl (dbl (fromb b))))
  | from∘dblb b       -- suc (suc (dbl (dbl (fromb b)))) ≡ suc (suc (dbl (dbl (fromb b))))
  = refl

-- lemma
-- second case for unary addition
--     suc m + n = suc (m + n)
-- into binary setting.
-- Induction on both m and n is needed.

bin-+-linc : ∀ (m n : Bin-ℕ) → (inc m) bin-+ n ≡ inc (m bin-+ n)
bin-+-linc bits    bits  = refl
bin-+-linc bits   (n x0) = refl
bin-+-linc bits   (n x1) = refl
bin-+-linc (m x0)  bits  = refl
bin-+-linc (m x0) (n x0) = refl
bin-+-linc (m x0) (n x1) = refl
bin-+-linc (m x1)  bits  = refl
bin-+-linc (m x1) (n x0) rewrite bin-+-linc m n = refl
bin-+-linc (m x1) (n x1) rewrite bin-+-linc m n = refl

-- theorem relates unary and binary addition
to∘+ : ∀ (m n : ℕ) → tob (m + n) ≡ tob m bin-+ tob n
to∘+  zero   n = refl
to∘+ (suc m) n                 --  tob (suc m + n)        ≡ (tob (suc m) bin-+ tob n)
                               -- inc (tob (m + n))       ≡ (inc (tob m) bin-+ tob n)
  rewrite
    bin-+-linc (tob m) (tob n) -- inc (tob (m + n))       ≡ inc (tob m bin-+ tob n)
  | to∘+ m n                   -- inc (tob m bin-+ tob n) ≡ inc (tob m bin-+ tob n)
  = refl

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

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

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


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Instance.Groupoids where

-- The category of groupoids.
--
-- This category should maybe be called "Ho(Groupoids)" or "Ho(Gpd)"
-- instead.  The "homsets" are not the "usual" ones consisting of
-- functors, but consist instead of equivalence classes of functors up
-- to natural isomorphism.  This is because homsets here are really
-- hom-setoids and we pick natural isomorphism as the equivalence
-- relation for these setoids.
--
-- See https://ncatlab.org/nlab/show/Ho%28Cat%29

open import Level
open import Categories.Category
open import Categories.Category.Groupoid
open import Categories.Functor as Fctr using (Functor; _∘F_)
open import Categories.Functor.Properties using ([_]-resp-Iso)
import Categories.Morphism.IsoEquiv as IsoEquiv
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism; associator; unitorˡ; unitorʳ; unitor²; isEquivalence; _ⓘₕ_; sym)
private
  variable
    o ℓ e : Level

open Groupoid using (category)

-- The category of groupoids.

Groupoids : ∀ o ℓ e → Category (suc (o ⊔ ℓ ⊔  e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
Groupoids o ℓ e = record
  { Obj       = Groupoid o ℓ e
  ; _⇒_       = λ G H → Functor (category G) (category H)
  ; _≈_       = NaturalIsomorphism
  ; id        = Fctr.id
  ; _∘_       = _∘F_
  ; assoc     = λ {_ _ _ _ F G H} → associator F G H
  ; sym-assoc = λ {_ _ _ _ F G H} → sym (associator F G H)
  ; identityˡ = unitorˡ
  ; identityʳ = unitorʳ
  ; identity² = unitor²
  ; equiv     = isEquivalence
  ; ∘-resp-≈  = _ⓘₕ_
  }

module _ {o ℓ e o′ ℓ′ e′} {G : Groupoid o ℓ e} {H : Groupoid o′ ℓ′ e′}
         (F : Functor (category G) (category H))
         where

  private
    module G = Groupoid G
    module H = Groupoid H
  open Functor F
  open IsoEquiv (category H) using (to-unique)

  -- Functors preserve inverses

  F-resp-⁻¹ : ∀ {A B} (f : A G.⇒ B) → F₁ (f G.⁻¹) H.≈ (F₁ f) H.⁻¹
  F-resp-⁻¹ f = to-unique ([ F ]-resp-Iso G.iso) H.iso H.Equiv.refl


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.DistLattice where

open import Cubical.Algebra.DistLattice.Base public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
-- Andreas, 2016-04-14 Issue 1821
-- pts rule for SizeUniv not implemented properly

open import Common.Size
open import Common.Equality

record Reveal_·_is_  {A : Set} {B : A → Set}
                    (f : (x : A) → B x) (x : A) (y : B x) :
                    Set where
  constructor [_]
  field eq : f x ≡ y

inspect : ∀ {A : Set} {B : A → Set}
          (f : (x : A) → B x) (x : A) → Reveal f · x is f x
inspect f x = [ refl ]

record Co i : Set where
  coinductive
  field force : ∀{j : Size< i} → Co j

test : ∀ (n : Co ∞) → Set
(test n) with inspect Co.force n
(test n) | n' = Co ∞

-- Error WAS:
-- SizeUniv != Set
-- when checking that the type
-- ...
-- of the generated with function is well-formed

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Functions.Definition
open import Numbers.Naturals.Definition
open import Sets.FinSet.Definition
open import Setoids.Setoids

module Setoids.Cardinality.Infinite.Definition where

InfiniteSetoid : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → Set (a ⊔ b)
InfiniteSetoid {A = A} S = (n : ℕ) → (f : FinSet n → A) → (SetoidBijection (reflSetoid (FinSet n)) S f) → False

record DedekindInfiniteSetoid {a b : _} {A : Set a} (S : Setoid {a} {b} A) : Set (a ⊔ b) where
  field
    inj : ℕ → A
    isInjection : SetoidInjection (reflSetoid ℕ) S inj


text:
module Properties.Dec where

data ⊥ : Set where

data Dec(A : Set) : Set where
  yes : A → Dec A
  no : (A → ⊥) → Dec A

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Functions.Embedding

open import Cubical.Algebra

private
  variable
    m n : Level

IsMagmaHom : (M : Magma m) (N : Magma n) → (⟨ M ⟩ → ⟨ N ⟩) → Type (ℓ-max m n)
IsMagmaHom M N fun = Homomorphic₂ fun (Magma._•_ M) (Magma._•_ N)

record MagmaHom (M : Magma m) (N : Magma n) : Type (ℓ-max m n) where
  constructor magmahom
  field
    fun : ⟨ M ⟩ → ⟨ N ⟩
    isHom : IsMagmaHom M N fun

record MagmaEquiv (M : Magma m) (N : Magma n) : Type (ℓ-max m n) where
  constructor magmaequiv
  field
    eq : ⟨ M ⟩ ≃ ⟨ N ⟩
    isHom : IsMagmaHom M N (equivFun eq)

  hom : MagmaHom M N
  hom = record { isHom = isHom }

instance
  MagmaHomOperators : HomOperators (Magma m) (Magma n) (ℓ-max m n)
  MagmaHomOperators = record { _⟶ᴴ_ = MagmaHom; _≃ᴴ_ = MagmaEquiv }


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

module Piston where

open import Data.Fin     using (#_)
open import Data.List    using (List; map; _∷_; []; concatMap; zip; drop; length; replicate; intercalate)
open import Data.Maybe   using (Maybe; fromMaybe)
open import Data.Nat     using (ℕ)
open import Data.Product using (_×_; proj₁; proj₂)
open import Data.Vec     using (Vec; fromList; _∷_; []; toList)
open import Function     using (_∘_)

open import Counterpoint
open import Harmony
open import Note
open import Music
open import MidiEvent
open import Pitch
open import Interval
open import Util

-- 3/4 time
melodyAs : List Note
melodyAs =
  tone dhalf (c 6) ∷
  tone qtr (d 6) ∷ tone qtr (c 6) ∷ tone qtr (e 6) ∷
  tone half (f 6) ∷ tone qtr (f 6) ∷
  tone qtr (g 6) ∷ tone qtr (f 6) ∷ tone qtr (d 6) ∷
  tone half (c 6) ∷ tone qtr (a 5) ∷
  tone qtr (b♭ 5) ∷ tone half (g 5) ∷
  tone dhalf (f 5) ∷ []

-- 4/4 time
melodyBs : List Note
melodyBs =
  tone half (c 6) ∷ tone qtr (b 5) ∷ tone qtr (c 6) ∷
  tone half (d 6) ∷ tone qtr (e 6) ∷ tone qtr (c 6) ∷
  tone half (f 6) ∷ tone half (d 6) ∷
  tone half (b 5) ∷ tone qtr (c 6) ∷ tone qtr (d 6) ∷
  tone half (b 5) ∷ tone half (b 5) ∷
  tone half (c 6) ∷ tone half (c 6) ∷ []

-- 4/4 time
melodyCs : List Note
melodyCs =
  tone qtr (g♯ 5) ∷ tone qtr (g♯ 5) ∷ tone qtr (a 5) ∷ tone qtr (f♯ 5) ∷
  tone half (g♯ 5) ∷ tone qtr (g♯ 5) ∷ tone qtr (c♯ 6) ∷
  tone half (b 5) ∷ tone qtr (g♯ 5) ∷ tone qtr (a 5) ∷
  tone half (f♯ 5) ∷ tone half (f♯ 5) ∷
  tone qtr (g♯ 5) ∷ tone qtr (g♯ 5) ∷ tone qtr (a 5) ∷ tone qtr (b 5) ∷
  tone half (c♯ 6) ∷ tone half (b 5) ∷
  tone qtr (b 5) ∷ tone qtr (d♯ 5) ∷ tone qtr (e 5) ∷ tone qtr (f♯ 5) ∷
  tone whole (e 5) ∷ []

-- This is example 9-1 in the 5th edition of Piston.
-- It was example 117 in a previous edition used in the FHARM paper.
-- 4/4 time
melody117s : List Note
melody117s =
  rest half ∷ tone half (g 5) ∷
  tone half (e 5) ∷ tone half (g 5) ∷
  tone half (a 5) ∷ tone half (c 6) ∷
  tone half (b 5) ∷ tone half (a 5) ∷
  tone whole (g 5) ∷ []

melody117a : List Note
melody117a =
  tone whole (b 4) ∷
  tone half (c 5) ∷ tone half (e 5) ∷
  tone half (f 5) ∷ tone half (e 5) ∷
  tone half (g 5) ∷ tone half (f 5) ∷
  tone whole (d 5) ∷ []

melody117t : List Note
melody117t =
  tone dwhole (g 4) ∷ tone half (c 5) ∷
  tone whole (c 5) ∷
  tone half (e 5) ∷ tone half (c 5) ∷
  tone whole (b 4) ∷ []

melody117b : List Note
melody117b =
  tone whole (g 3) ∷
  tone whole (c 4) ∷
  tone half (f 4) ∷ tone half (a 4) ∷
  tone half (e 4) ∷ tone half (f 4) ∷
  tone whole (g 4) ∷ []

----

piano marimba : InstrumentNumber-1
piano   = # 0
marimba = # 12

channel1 channel2 : Channel-1
channel1 = # 0
channel2 = # 1

tempo : ℕ
tempo = 120

mVelocity cVelocity : Velocity
mVelocity = # 60
cVelocity = # 60

melodyAsTrack : MidiTrack
melodyAsTrack = track "Melody A S" piano channel1 tempo (notes→events mVelocity melodyAs)

melodyATracks : List MidiTrack
melodyATracks =  melodyAsTrack ∷ []

melodyBsTrack : MidiTrack
melodyBsTrack = track "Melody B S" piano channel1 tempo (notes→events mVelocity melodyBs)

melodyBTracks : List MidiTrack
melodyBTracks =  melodyBsTrack ∷ []

melodyCsTrack : MidiTrack
melodyCsTrack = track "Melody C S" piano channel1 tempo (notes→events mVelocity melodyCs)

melodyCTracks : List MidiTrack
melodyCTracks =  melodyCsTrack ∷ []

melody117sTrack : MidiTrack
melody117sTrack = track "Melody 117 S" piano channel1 tempo (notes→events mVelocity melody117s)

melody117aTrack : MidiTrack
melody117aTrack = track "Melody 117 A" piano channel1 tempo (notes→events mVelocity melody117a)

melody117tTrack : MidiTrack
melody117tTrack = track "Melody 117 T" piano channel1 tempo (notes→events mVelocity melody117t)

melody117bTrack : MidiTrack
melody117bTrack = track "Melody 117 B" piano channel1 tempo (notes→events mVelocity melody117b)

melody117Tracks : List MidiTrack
melody117Tracks =  melody117sTrack ∷ melody117aTrack ∷ melody117tTrack ∷ melody117bTrack ∷ []

-----

-- Harmonization of Piston's example 9-1 (117).

pitches117s : Vec Pitch 9
pitches117s = g 5 ∷ g 5 ∷ e 5 ∷ g 5 ∷ a 5 ∷ c 6 ∷ b 5 ∷ a 5 ∷ g 5 ∷ []

vhs117 : List (Vec (Vec Pitch 4) 9)
vhs117 = voicedHarmonizations pitches117s

best : Maybe (List (Vec Pitch 4))
best = Data.Maybe.map toList (listMin (length ∘ motionErrors) vhs117)

vh117 : List (Vec Pitch 4)
vh117 = fromMaybe [] best

chordsPoints117 : List (Vec Point 4)
chordsPoints117 = map (Data.Vec.map tone) vh117

harm117 : Harmony 4 (length vh117)
harm117 = harmony (fromList (map chord chordsPoints117))

testHTrack : MidiTrack
testHTrack = track "Test Harm" piano channel1 tempo (harmony→events mVelocity harm117)

testHTracks : List MidiTrack
testHTracks = testHTrack ∷ []

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
module A where

postulate A : Set

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Data.Any where

import      Lvl
open import Type

-- A type that can hold a value of any type.
record Any {ℓ} : Type{Lvl.𝐒(ℓ)} where
  constructor intro
  field
    {type} : Type{ℓ}
    value  : type

  map : ∀{T : Type{ℓ}} → (type → T) → Any{ℓ}
  map f = record{value = f(value)}

-- A type that can hold a value of any type in any universe.
record UniversalAny : Typeω where
  constructor intro
  field
    {level} : Lvl.Level
    {type} : Type{level}
    value  : type

  map : ∀{ℓ}{T : Type{ℓ}} → (type → T) → UniversalAny
  map f = record{value = f(value)}


text:
module List.Permutation.Base.Equivalence (A : Set) where

open import List.Permutation.Base A
open import Data.List
open import Data.Product renaming (_×_ to _∧_)

refl∼ : {xs : List A} → xs ∼ xs
refl∼ {[]}     = ∼[]
refl∼ {x ∷ xs} = ∼x /head /head refl∼

sym∼ : {xs ys : List A} → xs ∼ ys → ys ∼ xs
sym∼ ∼[] = ∼[]
sym∼ (∼x xs/x⟶xs' ys/x⟶ys' xs'∼ys') = ∼x ys/x⟶ys' xs/x⟶xs' (sym∼ xs'∼ys')

lemma// : {x y : A}{xs ys zs : List A} → xs / x ⟶ ys → ys / y ⟶ zs → ∃ (λ ws → xs / y ⟶ ws ∧ ws / x ⟶ zs)
lemma//  (/head {x = x}) (/head {xs = xs}) = x ∷ xs , /tail /head , /head
lemma// (/head {x = x}) (/tail {x = u} {ys = us'} us/y⟶us') = x ∷ u ∷ us' , /tail (/tail us/y⟶us') , /head
lemma// (/tail {xs = us} us/x⟶us') /head = us , /head , us/x⟶us'
lemma// (/tail {x = u} us/x⟶us') (/tail us'/y⟶us'')
    with lemma// us/x⟶us' us'/y⟶us''
... | ws' , us/y⟶ws' , ws'/x⟶us'' = u ∷ ws' , /tail us/y⟶ws' ,  /tail ws'/x⟶us''

lemma∼/∷ : {x : A}{xs ys : List A} → (x ∷ xs) ∼ ys → ∃ (λ ys' → ys / x ⟶ ys' ∧ xs ∼ ys')
lemma∼/∷  (∼x {ys' = vs'} /head ys/x⟶vs' xs∼vs') = vs' , ys/x⟶vs' , xs∼vs'
lemma∼/∷  (∼x (/tail xs/u⟶us') ys/u⟶vs' x∷us'∼vs')
    with lemma∼/∷ x∷us'∼vs'
... | _ , vs'/x⟶zs , us'∼zs
    with lemma// ys/u⟶vs' vs'/x⟶zs
... | ws , ys/x⟶ws , ws/u⟶zs = ws , ys/x⟶ws , ∼x xs/u⟶us' ws/u⟶zs us'∼zs

lemma∼/ : {x : A}{xs xs' ys : List A} → xs ∼ ys → xs / x  ⟶ xs' →
                   ∃ (λ ys' → ys / x ⟶ ys' ∧ xs' ∼ ys')
lemma∼/ u∷us∼ys /head = lemma∼/∷ u∷us∼ys
lemma∼/ u∷us∼ys (/tail us/x⟶xs')
    with lemma∼/∷ u∷us∼ys
... | _ , ys/u⟶ys' , us∼ys'
    with lemma∼/ us∼ys' us/x⟶xs'
... | _ , ys'/x⟶vs , xs'∼vs
    with lemma// ys/u⟶ys' ys'/x⟶vs
... | ws , ys/x⟶ws , ws/u⟶vs = ws , ys/x⟶ws , ∼x /head ws/u⟶vs xs'∼vs

trans∼ : {xs ys zs : List A} → xs ∼ ys → ys ∼ zs → xs ∼ zs
trans∼ ∼[] ∼[] = ∼[]
trans∼ ∼[] (∼x .{xs = []} () zs/x⟶zs' ys'∼zs')
trans∼ {zs = zs} (∼x {ys = ys} xs/x⟶xs' ys/x⟶ys' xs'∼ys') ys∼zs
    with lemma∼/ {xs = ys} ys∼zs ys/x⟶ys'
... | _ , zs/x⟶us , ys'∼us = ∼x xs/x⟶xs' zs/x⟶us (trans∼ xs'∼ys' ys'∼us)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-

This file contains:
    - the abelianization of groups as a HIT as proposed in https://arxiv.org/abs/2007.05833

The definition of the abelianization is not as a set-quotient, since the relation of
abelianization is cumbersome to work with.

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

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

open import Cubical.Data.Sigma

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
  using (isPropIsGroupHom; compGroupHom; idGroupHom)

open import Cubical.Algebra.AbGroup.Base

open import Cubical.Algebra.Group.Abelianization.Base

private
  variable
    ℓ : Level

module _ (G : Group ℓ) where
  open GroupStr {{...}}
  open GroupTheory G
  private
    instance
      _ = snd G

  -- Some helpful lemmas, similar to those in Cubical/HITs/SetQuotients/Properties.agda
  elimProp : {B : Abelianization G → Type ℓ}
        → (Bprop : (x : Abelianization G) → isProp (B x))
        → (f : (g : fst G) → B (η g))
        → (x : Abelianization G)
        → B x
  elimProp Bprop f (η g) = f g
  elimProp {B = B} Bprop f (comm a b c i) =
    isProp→PathP (λ i → Bprop (comm a b c i)) (f (a · (b · c))) (f (a · (c · b))) i
  elimProp Bprop f (isset x y p q i j) =
    isOfHLevel→isOfHLevelDep
      2 (λ x → isProp→isSet (Bprop x)) (g x) (g y) (cong g p) (cong g q) (isset x y p q) i j
    where
    g = elimProp Bprop f

  elimProp2 : {C : Abelianization G → Abelianization G → Type ℓ}
        → (Cprop : (x y : Abelianization G) → isProp (C x y))
        → (f : (a b : fst G) → C (η a) (η b))
        → (x y : Abelianization G)
        → C x y
  elimProp2 Cprop f = elimProp (λ x → isPropΠ (λ y → Cprop x y))
                               (λ x → elimProp (λ y → Cprop (η x) y) (f x))

  elimProp3 : {D : Abelianization G → Abelianization G → Abelianization G → Type ℓ}
        → (Dprop : (x y z : Abelianization G) → isProp (D x y z))
        → ((a b c : fst G) → D (η a) (η b) (η c))
        → (x y z : Abelianization G)
        → D x y z
  elimProp3 Dprop f = elimProp (λ x → isPropΠ2 (λ y z → Dprop x y z))
                               (λ x → elimProp2 (λ y z → Dprop (η x) y z) (f x))

  elimContr : {B : Abelianization G → Type ℓ}
        → (Bcontr : ∀ (a : fst G) → isContr (B (η a)))
        → (x : Abelianization G)
        → B x
  elimContr Bcontr = elimProp (elimProp (λ _ → isPropIsProp) λ _ → isContr→isProp (Bcontr _))
                              λ _ → Bcontr _ .fst

  elimContr2 : {C : Abelianization G → Abelianization G → Type ℓ}
        → (Ccontr : ∀ (a b : fst G) → isContr (C (η a) (η b)))
        → (x y : Abelianization G)
        → C x y
  elimContr2 Ccontr = elimContr λ _ → isOfHLevelΠ 0
                     (elimContr λ _ → inhProp→isContr (Ccontr _ _) isPropIsContr)

  rec : {M : Type ℓ}
        (Mset : isSet M)
        (f : fst G → M)
        (fcomm : (a b c : fst G) → f (a · (b · c)) ≡ f (a · (c · b)))
      → Abelianization G → M
  rec Mset f fcomm (η g) = f g
  rec Mset f fcomm (comm a b c i) = fcomm a b c i
  rec Mset f fcomm (isset a b p q i j) = Mset (g a) (g b) (cong g p) (cong g q) i j
    where
    g = rec Mset f fcomm

  rec2 : {M : Type ℓ}
        (Mset : isSet M)
        (f : fst G → fst G → M)
        (fcomml : (a b c d : fst G) → f (a · (b · c)) d ≡ f (a · (c · b)) d)
        (fcommr : (a b c d : fst G) → f a (b · (c · d)) ≡ f a (b · (d · c)))
      → Abelianization G → Abelianization G → M
  rec2 Mset f fcomml fcommr =
    rec
      (isSetΠ (λ _ → Mset))
      (λ g → rec Mset (λ h → f g h) (fcommr g))
      (λ a b c → funExt (elimProp (λ _ → Mset _ _) (λ d → fcomml a b c d)))

module AbelianizationGroupStructure (G : Group ℓ) where
  open GroupStr {{...}}
  open GroupTheory G
  private
    instance
      _ = snd G

  {-
    Definition of the group structure on the abelianization. Here the generality of the comm
    relation is used.
  -}
  _·Ab_ : Abelianization G → Abelianization G → Abelianization G
  _·Ab_ =
    (rec2 G)
      isset
      (λ x y → η (x · y))
      (λ a b c d → η ((a · (b · c)) · d) ≡⟨ cong η (cong (λ x → (x · d)) (assoc _ _ _)) ⟩
                   η (((a · b) · c) · d) ≡⟨ cong η (sym (assoc (a · b) c d)) ⟩
                   η ((a · b) · (c · d)) ≡⟨ comm (a · b) c d ⟩
                   η ((a · b) · (d · c)) ≡⟨ cong η (sym (assoc _ _ _)) ⟩
                   η (a · (b · (d · c))) ≡⟨ cong η (cong (λ x → (a · x)) (assoc _ _ _)) ⟩
                   η (a · ((b · d) · c)) ≡⟨ comm a (b · d) c ⟩
                   η (a · (c · (b · d))) ≡⟨ cong η (cong (λ x → (a · x)) (assoc _ _ _)) ⟩
                   η (a · ((c · b) · d)) ≡⟨ cong η (assoc a (c · b) d) ⟩
                   η ((a · (c · b)) · d) ∎)
      (λ a b c d → η (a · (b · (c · d))) ≡⟨ cong η (assoc _ _ _) ⟩
                   η ((a · b) · (c · d)) ≡⟨ comm (a · b) c d ⟩
                   η ((a · b) · (d · c)) ≡⟨ cong η (sym (assoc _ _ _)) ⟩
                   η (a · (b · (d · c))) ∎)

  1Ab : Abelianization G
  1Ab = η 1g

  invAb : Abelianization G → Abelianization G
  invAb =
    (rec G)
      isset
      ((λ x → η (inv x)))
      (λ a b c → η (inv (a · (b · c)))         ≡⟨ cong η (invDistr a (b · c)) ⟩
      η ((inv (b · c)) · (inv a))              ≡⟨ cong (λ x → η (x · (inv a))) (invDistr b c) ⟩
      η (((inv c) · (inv b)) · (inv a))        ≡⟨ cong
                                                    η
                                                    ((sym (lid (((inv c) · (inv b)) · (inv a))))) ⟩
      η (1g · (((inv c) · (inv b)) · (inv a))) ≡⟨ comm 1g ((inv c) · (inv b)) (inv a) ⟩
      η (1g · ((inv a) · ((inv c) · (inv b)))) ≡⟨ cong η (lid ((inv a) · ((inv c) · (inv b)))) ⟩
      η ((inv a) · ((inv c) · (inv b)))        ≡⟨ comm (inv a) (inv c) (inv b) ⟩
      η ((inv a) · ((inv b) · (inv c)))        ≡⟨ cong
                                                    η
                                                    ((sym (lid ((inv a) · ((inv b) · (inv c)))))) ⟩
      η (1g · ((inv a) · ((inv b) · (inv c)))) ≡⟨ comm 1g (inv a) ((inv b) · (inv c)) ⟩
      η (1g · (((inv b) · (inv c)) · (inv a))) ≡⟨ cong η (lid (((inv b) · (inv c)) · (inv a))) ⟩
      η (((inv b) · (inv c)) · (inv a))        ≡⟨ cong
                                                    (λ x → η (x · (inv a)))
                                                    (sym (invDistr c b)) ⟩
      η ((inv (c · b)) · (inv a))              ≡⟨ cong η (sym (invDistr a (c · b))) ⟩
      η (inv (a · (c · b))) ∎)

  assocAb : (x y z : Abelianization G) → x ·Ab (y ·Ab z) ≡ (x ·Ab y) ·Ab z
  assocAb =
    (elimProp3 G)
      (λ x y z → isset (x ·Ab (y ·Ab z)) ((x ·Ab y) ·Ab z))
      (λ x y z → cong η (assoc x y z))

  ridAb : (x : Abelianization G) → x ·Ab 1Ab ≡ x
  ridAb =
    (elimProp G)
      (λ x → isset (x ·Ab 1Ab) x)
      (λ x → cong η (rid x))

  rinvAb : (x : Abelianization G) → x ·Ab (invAb x) ≡ 1Ab
  rinvAb =
    (elimProp G)
      (λ x → isset (x ·Ab (invAb x)) 1Ab)
      (λ x → (η x) ·Ab (invAb (η x)) ≡⟨ refl ⟩
             (η x) ·Ab (η (inv x))   ≡⟨ refl ⟩
             η (x · (inv x))         ≡⟨ cong η (fst (inverse x)) ⟩
             η 1g                    ≡⟨ refl ⟩
             1Ab ∎)

  commAb : (x y : Abelianization G) → x ·Ab y ≡ y ·Ab x
  commAb =
    (elimProp2 G)
      (λ x y → isset (x ·Ab y) (y ·Ab x))
      (λ x y → (η x) ·Ab (η y)  ≡⟨ refl ⟩
               η (x · y)        ≡⟨ cong η (sym (lid (x · y))) ⟩
               η (1g · (x · y)) ≡⟨ comm 1g x y ⟩
               η (1g · (y · x)) ≡⟨ cong η (lid (y · x)) ⟩
               η (y · x)        ≡⟨ refl ⟩
               (η y) ·Ab (η x) ∎)

  -- The proof that the abelianization is in fact an abelian group.
  asAbelianGroup : AbGroup ℓ
  asAbelianGroup = makeAbGroup 1Ab _·Ab_ invAb isset assocAb ridAb rinvAb commAb

  -- The proof that η can be seen as a group homomorphism
  ηAsGroupHom : GroupHom G (AbGroup→Group asAbelianGroup)
  ηAsGroupHom = f , fIsHom
    where
    f = λ x → η x
    fIsHom : IsGroupHom (snd G) f (snd (AbGroup→Group asAbelianGroup))
    IsGroupHom.pres· fIsHom = λ x y → refl
    IsGroupHom.pres1 fIsHom = refl
    IsGroupHom.presinv fIsHom = λ x → refl

AbelianizationAbGroup : (G : Group ℓ) → AbGroup ℓ
AbelianizationAbGroup G = AbelianizationGroupStructure.asAbelianGroup G

AbelianizationHom : (G : Group ℓ) → GroupHom G (AbGroup→Group (AbelianizationAbGroup G))
AbelianizationHom G = AbelianizationGroupStructure.ηAsGroupHom G

module UniversalProperty (G : Group ℓ) where
  open GroupStr {{...}}
  open GroupTheory G
  open AbelianizationGroupStructure G
  private
    instance
      _ = snd G
  abstract
    {- The proof of the universal property of the abelianization.

    G --η--> abelianization
    \         .
      \       .
        f   ∃! inducedHom
          \   .
            \ .
              H
    commuting diagram
    -}
    inducedHom : (H : AbGroup ℓ)
               → (f : GroupHom G (AbGroup→Group H))
               → AbGroupHom asAbelianGroup H
    inducedHom H f = g , gIsHom
      where open IsGroupHom
            instance
              _ : GroupStr (fst H)
              _ = snd (AbGroup→Group H)
            f' : fst G → fst H
            f' = fst f
            g : Abelianization G → fst H
            g = (rec G)
                  (isSetAbGroup H)
                  (λ x → (f') x)
                  (λ a b c → f' (a · b · c)           ≡⟨ (snd f).pres· a (b · c) ⟩
                             (f' a) · (f' (b · c))    ≡⟨ cong
                                                           (λ x → (f' a) · x)
                                                           ((snd f).pres· b c) ⟩
                             (f' a) · (f' b) · (f' c) ≡⟨ cong
                                                           (λ x → (f' a) · x)
                                                           ((snd H).AbGroupStr.comm (f' b) (f' c)) ⟩
                             (f' a) · (f' c) · (f' b) ≡⟨ cong
                                                           (λ x → (f' a) · x)
                                                           (sym ((snd f).pres· c b)) ⟩
                             (f' a) · (f' (c · b))    ≡⟨ sym ((snd f).pres· a (c · b)) ⟩
                             f' (a · c · b) ∎)
            gIsHom : IsGroupHom (snd (AbGroup→Group asAbelianGroup)) g (snd (AbGroup→Group H))
            pres· gIsHom =
              (elimProp2 G)
                (λ x y → isSetAbGroup H _ _)
                ((snd f).pres·)
            pres1 gIsHom = (snd f).pres1
            presinv gIsHom =
              (elimProp G)
                (λ x → isSetAbGroup H _ _)
                ((snd f).presinv)

    commutativity : (H : AbGroup ℓ)
                  → (f : GroupHom G (AbGroup→Group H))
                  → (compGroupHom ηAsGroupHom (inducedHom H f) ≡ f)
    commutativity H f =
        Σ≡Prop
          (λ _ → isPropIsGroupHom _ _)
          (λ i x → q x i)
      where q : (x : fst  G)
              → fst (compGroupHom ηAsGroupHom (inducedHom H f)) x ≡ fst f x
            q = (λ x → refl)

    uniqueness : (H : AbGroup ℓ)
               → (f : GroupHom G (AbGroup→Group H))
               → (g : AbGroupHom asAbelianGroup H)
               → (p : compGroupHom ηAsGroupHom g ≡ f)
               → (g ≡ inducedHom H f)
    uniqueness H f g p =
        Σ≡Prop
          (λ _ → isPropIsGroupHom _ _)
          (λ i x →  q x i)
      where q : (x : Abelianization G)
                →  fst g x ≡ fst (inducedHom H f) x
            q = (elimProp G)
                  (λ _ → isSetAbGroup H _ _)
                  (λ x → fst g (η x) ≡⟨ cong (λ f → f x) (cong fst p) ⟩
                         (fst f) x   ≡⟨ refl ⟩
                         fst (inducedHom H f) (η x)∎)

max_stars_repo_name: gmagaf/cubical

max_issues_repo_name: gmagaf/cubical

max_forks_repo_name: gmagaf/cubical


text:
{-# OPTIONS --copatterns #-}

module IOExampleGraphicsMovingText where

--
--  not yet updated for new SizedIO library
--  not yet updated to change with IOInterface Record of Commands / Responses
--

{-

open import SizedIO.General
open import SizedIO.IOGraphicsLib -- TODO

open import Data.Bool.Base
open import Data.Char.Base
open import Data.Nat.Base
open import Data.List.Base hiding (_++_)
open import Data.Integer.Base hiding (_+_;suc)
open import Data.String.Base
open import Data.Maybe.Base

open import Function
open import Size

width :  ℕ
width = 125

height :  ℕ
height = 20

myBox : Point  → Graphic
myBox p  = withColor black (polygon  ( point x y
                                      ∷ point (x +IntNat width) y
                                      ∷ point (x +IntNat width) (y +IntNat height)
                                      ∷ point x (y +IntNat height)
                                      ∷ [] ) )
               where x = proj1Point p
                     y = proj2Point p

record State : Set where
  constructor state
  field oldpoint : Maybe Point
        newpoint : Maybe Point
open State

module _ (w : Window) where

  -- If there was a mouse movement since the last invokation of refresh
  -- overwrite old text and place text at new mouse position.
  refresh : ∀{i} → State → IOGraphics i State
  refresh s =  case newpoint s of
    λ{ nothing → return s
     ; (just lastMousePoint) →
         {- case there was a new mouse movement. -}
         (whenJust (oldpoint s) λ p →
              exec1 (drawInWindow w (myBox p)) >>
              exec1 (drawInWindow w (withColor white (text lastMousePoint ("1st :some Text")))))
           >> return (state (just lastMousePoint) nothing)
     }

  processEvent : ∀{i} → State → IOGraphics+ i (Maybe State)
  processEvent s =
    exec (getWindowEvent w)
      λ{ {- key event: check whether this was equal to 'x'; if yes, terminate, otherwise return to loop -}
         (Key c t) →
           if (c ==CharBool 'x') then return nothing else return (just s)

         {- mouse event: if this was the first ever event, ignore it, but
             record that the next mouse event is no longer the first one.
            If it was not the first ever event: set newpoint to the position of the mouse p -}
       ; (MouseMove p) →
           return (just record s{ newpoint = just p })

         {- otherwise just go back to start -}
       ; _ →
           return (just s)
       }

  loop : ∀{i} → State → IOGraphics i Unit
  force (loop s) = processEvent s >>=+'  -- maybe′ loop (return _)
    λ{ nothing   → return _
     ; (just s') → refresh s' >>= loop
     }

myProgram : ∀{i} → IOGraphics i Unit
force myProgram =
  exec   (openWindowEx "Hello World" nothing (just (natSize 1000 1000)) nativeDrawGraphic nothing) λ window →
  loop window (state nothing nothing)

main : NativeIO Unit
main = nativeRunGraphics (translateIOGraphics myProgram)
-}

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
open import Data.Empty
open import Data.List renaming (_∷_ to _∷ₗ_ ; [_] to [_]ₗ)
open import Data.Maybe
open import Data.Product
open import Data.Sum
open import Data.Unit

open import AEff
open import AwaitingComputations
open import EffectAnnotations
open import Preservation
open import ProcessPreservation
open import Progress
open import Renamings
open import Substitutions
open import Types

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

module ProcessProgress where

-- PROCESS RESULTS

data ParResult⟨_⟩ : {o : O} {PP : PType o} → [] ⊢P⦂ PP → Set where

  run    : {X : VType}
           {o : O}
           {i : I} →
           {M : [] ⊢M⦂ X ! (o , i)} →
           RunResult⟨ [] ∣ M ⟩ →
           --------------------------
           ParResult⟨ run M ⟩

  par    : {o o' : O}
           {PP : PType o}
           {QQ : PType o'}
           {P : [] ⊢P⦂ PP}
           {Q : [] ⊢P⦂ QQ} →
           ParResult⟨ P ⟩ →
           ParResult⟨ Q ⟩ →
           ------------------
           ParResult⟨ P ∥ Q ⟩

data ProcResult⟨_⟩ : {o : O} {PP : PType o} → [] ⊢P⦂ PP → Set where

  proc   : {o : O}
           {PP : PType o}
           {P : [] ⊢P⦂ PP} →
           ParResult⟨ P ⟩ →
           -----------------
           ProcResult⟨ P ⟩

  signal : {o : O}
           {PP : PType o}
           {op : Σₛ}
           {p : op ∈ₒ o}
           {V : [] ⊢V⦂ ``(payload op)}
           {P : [] ⊢P⦂ PP} →
           ProcResult⟨ P ⟩ →
           ---------------------------
           ProcResult⟨ ↑ op p V P ⟩

-- PROGRESS THEOREM FOR PROCESSES

{- THEOREM 4.3 -}

proc-progress : {o : O}
                {PP : PType o} →
                (P : [] ⊢P⦂ PP) →
                -------------------------------------------------------------------------------
                (Σ[ o' ∈ O ] Σ[ QQ ∈ PType o' ] Σ[ r ∈ PP ⇝ QQ ] Σ[ Q ∈ [] ⊢P⦂ QQ ] (P [ r ]↝ Q)
                 ⊎
                 ProcResult⟨ P ⟩)

proc-progress (run {X} {o} {i} M) with progress M
... | inj₁ (M' , r) =
  inj₁ (_ , _ , _ , _ , run r)
... | inj₂ (comp R) =
  inj₂ (proc (run R))
... | inj₂ (signal {_} {_} {_} {_} {p} {V} {Q} R) =
  inj₁ (_ , _ , _ , _ , ↑ p V Q)
proc-progress (P ∥ Q) with proc-progress P
... | inj₁ (o' , PP' , r , P' , r') =
  inj₁ (_ , _ , _ , _ , context ([-] ∥ₗ Q) r')
... | inj₂ R with proc-progress Q
... | inj₁ (o' , QQ' , r , Q' , r') =
  inj₁ (_ , _ , _ , _ , context (P ∥ᵣ [-]) r')
proc-progress (P ∥ Q) | inj₂ (proc R) | inj₂ (proc R') =
  inj₂ (proc (par R R'))
proc-progress (P ∥ .(↑ _ _ _ _)) | inj₂ R | inj₂ (signal {_} {_} {_} {p} {V} {Q} R') =
  inj₁ (_ , _ , _ , _ , ↑-∥ᵣ p V P Q)
proc-progress (.(↑ _ _ _ _) ∥ Q) | inj₂ (signal {_} {_} {_} {p} {V} {P} R) | inj₂ R' =
  inj₁ (_ , _ , _ , _ , ↑-∥ₗ p V P Q)
proc-progress (↑ op p V P) with proc-progress P
... | inj₁ (o' , PP' , r , P' , r') =
  inj₁ (_ , _ , _ , _ , context (↑ op p V [-]) r')
... | inj₂ R =
  inj₂ (signal R)
proc-progress (↓ op V P) with proc-progress P
... | inj₁ (o' , OO' , r , P' , r') =
  inj₁ (_ , _ , _ , _ , context (↓ op V [-]) r')
... | inj₂ (proc (run {_} {_} {_} {M} R)) =
  inj₁ (_ , _ , _ , _ , ↓-run V M)
... | inj₂ (proc (par {_} {_} {_} {_} {Q} {Q'} R R')) =
  inj₁ (_ , _ , _ , _ , ↓-∥ V Q Q')
... | inj₂ (signal {_} {_} {_} {p} {W} {Q} R) =
  inj₁ (_ , _ , _ , _ , ↓-↑ p V W Q)

max_stars_repo_name: danelahman/aeff-agda

max_issues_repo_name: danelahman/aeff-agda

max_forks_repo_name: danelahman/aeff-agda