text:
------------------------------------------------------------------------
-- A correct implementation of tree sort
------------------------------------------------------------------------

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

-- The algorithm and the treatment of ordering information is taken
-- from Conor McBride's talk "Pivotal pragmatism".

-- The module is parametrised by a total relation.

open import Equality
open import Prelude hiding (id; _∘_; lower)

module Tree-sort.Full
  {c⁺}
  (eq : ∀ {a p} → Equality-with-J a p c⁺)
  {A : Type}
  (le : A → A → Type)
  (total : ∀ x y → le x y ⊎ le y x)
  where

open Derived-definitions-and-properties eq

open import Bag-equivalence eq using () renaming (Any to AnyL)
open import Bijection eq using (_↔_)
open import Function-universe eq hiding (Kind; module Kind)
open import List eq

------------------------------------------------------------------------
-- Extending the order with new minimum and maximum elements

-- A extended with a new minimum and maximum.

data Extended : Type where
  min max : Extended
  [_]     : (x : A) → Extended

infix 4 _≤_

_≤_ : Extended → Extended → Type
min   ≤ y     = ⊤
[ x ] ≤ [ y ] = le x y
x     ≤ max   = ⊤
_     ≤ _     = ⊥

-- A pair of ordering constraints (written as a record type to aid
-- type inference).

infix 4 _,_

record _≤[_]≤_ (l : Extended) (x : A) (u : Extended) : Type where
  constructor _,_
  field
    lower : l ≤ [ x ]
    upper : [ x ] ≤ u

------------------------------------------------------------------------
-- Ordered lists

data Ordered-list (l u : Extended) : Type where
  nil  : (l≤u : l ≤ u) → Ordered-list l u
  cons : (x : A) (xs : Ordered-list [ x ] u) (l≤x : l ≤ [ x ]) →
         Ordered-list l u

-- Conversion to ordinary lists.

to-list : ∀ {l u} → Ordered-list l u → List A
to-list (nil l≤u)       = []
to-list (cons x xs l≤x) = x ∷ to-list xs

------------------------------------------------------------------------
-- Unbalanced binary search trees

infix 5 node

syntax node x lx xu = lx -[ x ]- xu

data Search-tree (l u : Extended) : Type where
  leaf : (l≤u : l ≤ u) → Search-tree l u
  node : (x : A) (lx : Search-tree l [ x ]) (xu : Search-tree [ x ] u) →
         Search-tree l u

-- Any.

AnyT : ∀ {l u} → (A → Type) → Search-tree l u → Type
AnyT P (leaf _)     = ⊥
AnyT P (node x l r) = AnyT P l ⊎ P x ⊎ AnyT P r

------------------------------------------------------------------------
-- An ad-hoc universe consisting of lists, ordered lists and search
-- trees

-- The purpose of this universe is to allow overloading of Any, _∈_
-- and _≈-bag_.

-- Codes.

data Kind : Type where
  list ordered-list search-tree : Kind

-- Index type.
--
-- Note that Agda infers values of type ⊤ automatically.

Index : Kind → Type
Index list = ⊤
Index _    = Extended

-- Interpretation.

⟦_⟧ : (k : Kind) → (Index k → Index k → Type)
⟦ list         ⟧ _ _ = List A
⟦ ordered-list ⟧ l u = Ordered-list l u
⟦ search-tree  ⟧ l u = Search-tree l u

-- Any.

Any : ∀ {k l u} → (A → Type) → (⟦ k ⟧ l u → Type)
Any {list}         = AnyL
Any {ordered-list} = λ P → AnyL P ∘ to-list
Any {search-tree}  = AnyT

-- Membership.

infix 4 _∈_

_∈_ : ∀ {k l u} → A → ⟦ k ⟧ l u → Type
x ∈ xs = Any (λ y → x ≡ y) xs

-- Bag equivalence.

infix 4 _≈-bag_

_≈-bag_ : ∀ {k₁ k₂ l₁ u₁ l₂ u₂} → ⟦ k₁ ⟧ l₁ u₁ → ⟦ k₂ ⟧ l₂ u₂ → Type
xs ≈-bag ys = ∀ z → z ∈ xs ↔ z ∈ ys

------------------------------------------------------------------------
-- Singleton trees

singleton : ∀ {l u} (x : A) → l ≤[ x ]≤ u → Search-tree l u
singleton x (l≤x , x≤u) = leaf l≤x -[ x ]- leaf x≤u

-- Any lemma for singleton.

Any-singleton : ∀ (P : A → Type) {l u x} (l≤x≤u : l ≤[ x ]≤ u) →
                Any P (singleton x l≤x≤u) ↔ P x
Any-singleton P {x = x} l≤x≤u =
  Any P (singleton x l≤x≤u)  ↔⟨⟩
  ⊥ ⊎ P x ⊎ ⊥                ↔⟨ ⊎-left-identity ⟩
  P x ⊎ ⊥                    ↔⟨ ⊎-right-identity ⟩
  P x                        □

------------------------------------------------------------------------
-- Insertion into a search tree

insert : ∀ {l u} (x : A) → Search-tree l u → l ≤[ x ]≤ u →
         Search-tree l u
insert x (leaf _)        l≤x≤u       = singleton x l≤x≤u
insert x (ly -[ y ]- yu) (l≤x , x≤u) with total x y
... | inj₁ x≤y = insert x ly (l≤x , x≤y) -[ y ]- yu
... | inj₂ y≤x = ly -[ y ]- insert x yu (y≤x , x≤u)

-- Any lemma for insert.

Any-insert : ∀ (P : A → Type) {l u} x t (l≤x≤u : l ≤[ x ]≤ u) →
             Any P (insert x t l≤x≤u) ↔ P x ⊎ Any P t
Any-insert P {l} {u} x (leaf l≤u) l≤x≤u =
  Any P (singleton x l≤x≤u)               ↔⟨ Any-singleton P l≤x≤u ⟩
  P x                                     ↔⟨ inverse ⊎-right-identity ⟩
  P x ⊎ ⊥                                 ↔⟨⟩
  P x ⊎ Any P (leaf {l = l} {u = u} l≤u)  □
Any-insert P x (ly -[ y ]- yu) (l≤x , x≤u) with total x y
... | inj₁ x≤y =
  Any P (insert x ly (l≤x , x≤y)) ⊎ P y ⊎ Any P yu  ↔⟨ Any-insert P x ly (l≤x , x≤y) ⊎-cong id ⟩
  (P x ⊎ Any P ly) ⊎ P y ⊎ Any P yu                 ↔⟨ inverse ⊎-assoc ⟩
  P x ⊎ Any P ly ⊎ P y ⊎ Any P yu                   □
... | inj₂ y≤x =
  Any P ly ⊎ P y ⊎ Any P (insert x yu (y≤x , x≤u))  ↔⟨ id ⊎-cong id ⊎-cong Any-insert P x yu (y≤x , x≤u) ⟩
  Any P ly ⊎ P y ⊎ P x ⊎ Any P yu                   ↔⟨ lemma _ _ _ _ ⟩
  P x ⊎ Any P ly ⊎ P y ⊎ Any P yu                   □
  where

  -- The following lemma is easy to prove automatically (for
  -- instance by using a ring solver).

  lemma : (A B C D : Type) → A ⊎ B ⊎ C ⊎ D ↔ C ⊎ A ⊎ B ⊎ D
  lemma A B C D =
    A ⊎ B ⊎ C ⊎ D      ↔⟨ id ⊎-cong ⊎-assoc ⟩
    A ⊎ (B ⊎ C) ⊎ D    ↔⟨ id ⊎-cong ⊎-comm ⊎-cong id ⟩
    A ⊎ (C ⊎ B) ⊎ D    ↔⟨ ⊎-assoc ⟩
    (A ⊎ C ⊎ B) ⊎ D    ↔⟨ ⊎-assoc ⊎-cong id ⟩
    ((A ⊎ C) ⊎ B) ⊎ D  ↔⟨ (⊎-comm ⊎-cong id) ⊎-cong id ⟩
    ((C ⊎ A) ⊎ B) ⊎ D  ↔⟨ inverse ⊎-assoc ⊎-cong id ⟩
    (C ⊎ A ⊎ B) ⊎ D    ↔⟨ inverse ⊎-assoc ⟩
    C ⊎ (A ⊎ B) ⊎ D    ↔⟨ id ⊎-cong inverse ⊎-assoc ⟩
    C ⊎ A ⊎ B ⊎ D      □

------------------------------------------------------------------------
-- Turning an unordered list into a search tree

to-search-tree : List A → Search-tree min max
to-search-tree = foldr (λ x t → insert x t _) (leaf _)

-- No elements are added or removed.

to-search-tree-lemma : ∀ xs → to-search-tree xs ≈-bag xs
to-search-tree-lemma [] = λ z →
  z ∈ leaf {l = min} {u = max} _  ↔⟨⟩
  z ∈ []                          □
to-search-tree-lemma (x ∷ xs) = λ z →
  z ∈ insert x (to-search-tree xs) _  ↔⟨ Any-insert (λ x → z ≡ x) _ _ _ ⟩
  z ≡ x ⊎ z ∈ to-search-tree xs       ↔⟨ id ⊎-cong to-search-tree-lemma xs z ⟩
  z ∈ x ∷ xs                          □

------------------------------------------------------------------------
-- Appending two ordered lists with an extra element in between

infixr 5 append

syntax append x lx xu = lx -⁅ x ⁆- xu

append : ∀ {l u} (x : A) →
         Ordered-list l [ x ] → Ordered-list [ x ] u → Ordered-list l u
nil l≤x       -⁅ x ⁆- xu = cons x xu l≤x
cons y yx l≤y -⁅ x ⁆- xu = cons y (yx -⁅ x ⁆- xu) l≤y

-- Any lemma for append.

Any-append : ∀ (P : A → Type) {l u} x
             (lx : Ordered-list l [ x ]) (xu : Ordered-list [ x ] u) →
             Any P (lx -⁅ x ⁆- xu) ↔ Any P lx ⊎ P x ⊎ Any P xu
Any-append P x (nil l≤x) xu =
  P x ⊎ Any P xu      ↔⟨ inverse ⊎-left-identity ⟩
  ⊥ ⊎ P x ⊎ Any P xu  □
Any-append P x (cons y yx l≤y) xu =
  P y ⊎ Any P (append x yx xu)       ↔⟨ id ⊎-cong Any-append P x yx xu ⟩
  P y ⊎ Any P yx ⊎ P x ⊎ Any P xu    ↔⟨ ⊎-assoc ⟩
  (P y ⊎ Any P yx) ⊎ P x ⊎ Any P xu  □

------------------------------------------------------------------------
-- Inorder flattening of a tree

flatten : ∀ {l u} → Search-tree l u → Ordered-list l u
flatten (leaf l≤u)    = nil l≤u
flatten (l -[ x ]- r) = flatten l -⁅ x ⁆- flatten r

-- Flatten does not add or remove any elements.

flatten-lemma : ∀ {l u} (t : Search-tree l u) → flatten t ≈-bag t
flatten-lemma {l} {u} (leaf l≤u) = λ z →
  z ∈ nil  {l = l} {u = u} l≤u  ↔⟨⟩
  z ∈ leaf {l = l} {u = u} l≤u  □
flatten-lemma (l -[ x ]- r) = λ z →
  z ∈ flatten l -⁅ x ⁆- flatten r        ↔⟨ Any-append (λ x → z ≡ x) _ _ _ ⟩
  z ∈ flatten l ⊎ z ≡ x ⊎ z ∈ flatten r  ↔⟨ flatten-lemma l z ⊎-cong id ⊎-cong flatten-lemma r z ⟩
  z ∈ l ⊎ z ≡ x ⊎ z ∈ r                  ↔⟨⟩
  z ∈ l -[ x ]- r                        □

------------------------------------------------------------------------
-- Sorting

-- Sorts a list.

tree-sort : List A → Ordered-list min max
tree-sort = flatten ∘ to-search-tree

-- The result is a permutation of the input.

tree-sort-permutes : ∀ xs → tree-sort xs ≈-bag xs
tree-sort-permutes xs = λ z →
  z ∈ tree-sort xs                 ↔⟨⟩
  z ∈ flatten (to-search-tree xs)  ↔⟨ flatten-lemma (to-search-tree xs) _ ⟩
  z ∈ to-search-tree xs            ↔⟨ to-search-tree-lemma xs _ ⟩
  z ∈ xs                           □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Issue734a where

module M₁ (Z : Set₁) where

  postulate
    P : Set
    Q : Set → Set

module M₂ (X Y : Set) where

  module M₁′ = M₁ Set
  open M₁′

  p : P
  p = {!!}

  -- Previous and current agda2-goal-and-context:

  -- Y : Set
  -- X : Set
  -- ---------
  -- Goal: P

  q : Q X
  q = {!!}

  -- Previous and current agda2-goal-and-context:

  -- Y : Set
  -- X : Set
  -- -----------
  -- Goal: Q X

postulate X : Set

pp : M₂.M₁′.P X X
pp = {!!}

  -- Previous agda2-goal-and-context:

  -- ----------------
  -- Goal: M₁.P Set

  -- Current agda2-goal-and-context:

  -- --------------------
  -- Goal: M₂.M₁′.P X X

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Examples.Gcd where

open import Examples.Gcd.Euclid public
open import Examples.Gcd.Clocked public
open import Examples.Gcd.Spec public
open import Examples.Gcd.Refine public

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.GradedRing.Instances.Polynomials where

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

open import Cubical.Data.Unit
open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.Vec
open import Cubical.Data.Vec.OperationsNat
open import Cubical.Data.Sigma

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Monoid.Instances.NatVec
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.AbGroup.Instances.Unit
open import Cubical.Algebra.DirectSum.DirectSumHIT.Base
open import Cubical.Algebra.Ring
open import Cubical.Algebra.GradedRing.Base
open import Cubical.Algebra.GradedRing.DirectSumHIT

private variable
  ℓ : Level

open Iso
open GradedRing-⊕HIT-index
open GradedRing-⊕HIT-⋆

module _
  (ARing@(A , Astr) : Ring ℓ)
  (n : ℕ)
  where

  open RingStr Astr
  open RingTheory ARing

  PolyGradedRing : GradedRing ℓ-zero ℓ
  PolyGradedRing = makeGradedRingSelf
                   (NatVecMonoid n)
                   (λ _ → A)
                   (λ _ → snd (Ring→AbGroup ARing))
                   1r _·_ 0LeftAnnihilates 0RightAnnihilates
                   (λ a b c → ΣPathP ((+n-vec-assoc _ _ _) , (·Assoc _ _ _)))
                   (λ a → ΣPathP ((+n-vec-rid _) , (·IdR _)))
                   (λ a → ΣPathP ((+n-vec-lid _) , (·IdL _)))
                   ·DistR+
                   ·DistL+

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module std-lib where

open import IO using (IO; run; putStrLn; _>>_)
open import Data.Unit using (⊤)
open import Codata.Musical.Notation using (♯_)
import Agda.Builtin.IO using (IO)
open import Function using (_$_)

main1 : Agda.Builtin.IO.IO ⊤
main1 = run (♯ putStrLn "hallo" >> ♯ putStrLn "welt")

main2 : Agda.Builtin.IO.IO ⊤
main2 = run (do
  ♯ putStrLn "hallo"
  ♯ putStrLn "welt"
  )

main3 : Agda.Builtin.IO.IO ⊤
main3 = run $ do
  ♯ putStrLn "hallo"
  ♯ putStrLn "welt"

main4 : Agda.Builtin.IO.IO ⊤
main4 = run $ do
  ♯ putStrLn "hallo"
  ♯ (do
    ♯ putStrLn "welt"
    ♯ putStrLn "!")

main : Agda.Builtin.IO.IO ⊤
main = main3

max_stars_repo_name: neosimsim/merkdas

max_issues_repo_name: neosimsim/merkdas

max_forks_repo_name: neosimsim/merkdas


text:
module Sessions.Syntax.Values where

open import Prelude hiding (both)
open import Relation.Unary
open import Data.Maybe
open import Data.List.Properties using (++-isMonoid)
import Data.List as List

open import Sessions.Syntax.Types
open import Sessions.Syntax.Expr

open import Relation.Ternary.Separation.Morphisms

data Runtype : Set where
  endp : SType → Runtype
  chan : SType → SType → Runtype

flipped : Runtype → Runtype
flipped (endp x)   = endp x
flipped (chan α β) = chan β α

data Ends : Runtype → Runtype → Runtype → Set where
  lr : ∀ {a b} → Ends (endp a) (endp b) (chan a b)
  rl : ∀ {a b} → Ends (endp b) (endp a) (chan a b)

instance
  ≺-raw-sep : RawSep Runtype
  RawSep._⊎_≣_ ≺-raw-sep = Ends

  ≺-has-sep : IsSep ≺-raw-sep
  IsSep.⊎-comm ≺-has-sep lr = rl
  IsSep.⊎-comm ≺-has-sep rl = lr
  IsSep.⊎-assoc ≺-has-sep lr ()
  IsSep.⊎-assoc ≺-has-sep rl ()

RCtx = List Runtype
open import Relation.Ternary.Separation.Construct.ListOf Runtype public

End : SType → Runtype → Set
End α τ = [ endp α ] ≤ [ τ ]

ending : ∀ {ys} → Ends (endp γ) ys (chan α β) → End γ (chan α β)
ending lr = -, divide lr ⊎-idˡ
ending rl = -, divide rl ⊎-idˡ

mutual
  Env = Allstar Val

  data Closure : Type → Type → Pred RCtx 0ℓ where
    clos : ∀ {a} → Exp b (a ∷ Γ) → ∀[ Env Γ ⇒ Closure a b ]

  Endptr = Just ∘ endp

  data Val : Type → Pred RCtx 0ℓ where
    tt    : ε[ Val unit ]
    cref  : ∀[ Endptr α ⇒ Val (cref α)   ]
    pairs : ∀[ Val a ✴ Val b  ⇒ Val (prod a b) ]
    clos  : Exp b (a ∷ Γ) → ∀[ Env Γ ⇒ Val (a ⊸ b) ]


text:
-- Jesper, 2018-10-16: When solving constraints produces a term which
-- contains the same unsolved metavariable twice, only the first
-- occurrence should be turned into an interaction hole.

open import Agda.Builtin.Equality

postulate Id : (A : Set) → A → A → Set

allq : (∀ m n → Id _ m n) ≡ {!!}
allq = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Products
------------------------------------------------------------------------

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

module Data.Product where

open import Function
open import Level
open import Relation.Nullary
open import Agda.Builtin.Equality

infixr 4 _,′_
infix  4 -,_
infixr 2 _×_ _-×-_ _-,-_

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

open import Agda.Builtin.Sigma hiding (module Σ) public renaming (fst to proj₁; snd to proj₂)

module Σ = Agda.Builtin.Sigma.Σ renaming (fst to proj₁; snd to proj₂)

-- The syntax declaration below is attached to Σ-syntax, to make it
-- easy to import Σ without the special syntax.

infix 2 Σ-syntax

Σ-syntax : ∀ {a b} (A : Set a) → (A → Set b) → Set (a ⊔ b)
Σ-syntax = Σ

syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

∃ : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
∃ = Σ _

∃-syntax : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
∃-syntax = ∃

syntax ∃-syntax (λ x → B) = ∃[ x ] B

∄ : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
∄ P = ¬ ∃ P

∄-syntax : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
∄-syntax = ∄

syntax ∄-syntax (λ x → B) = ∄[ x ] B

∃₂ : ∀ {a b c} {A : Set a} {B : A → Set b}
     (C : (x : A) → B x → Set c) → Set (a ⊔ b ⊔ c)
∃₂ C = ∃ λ a → ∃ λ b → C a b

_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b)
A × B = Σ[ x ∈ A ] B

_,′_ : ∀ {a b} {A : Set a} {B : Set b} → A → B → A × B
_,′_ = _,_

------------------------------------------------------------------------
-- Unique existence

-- Parametrised on the underlying equality.

∃! : ∀ {a b ℓ} {A : Set a} →
     (A → A → Set ℓ) → (A → Set b) → Set (a ⊔ b ⊔ ℓ)
∃! _≈_ B = ∃ λ x → B x × (∀ {y} → B y → x ≈ y)

------------------------------------------------------------------------
-- Functions

-- Sometimes the first component can be inferred.

-,_ : ∀ {a b} {A : Set a} {B : A → Set b} {x} → B x → ∃ B
-, y = _ , y

<_,_> : ∀ {a b c} {A : Set a} {B : A → Set b} {C : ∀ {x} → B x → Set c}
        (f : (x : A) → B x) → ((x : A) → C (f x)) →
        ((x : A) → Σ (B x) C)
< f , g > x = (f x , g x)

map : ∀ {a b p q}
      {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q} →
      (f : A → B) → (∀ {x} → P x → Q (f x)) →
      Σ A P → Σ B Q
map f g (x , y) = (f x , g y)

map₁ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
       (A → B) → A × C → B × C
map₁ f = map f id

map₂ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : A → Set c} →
       (∀ {x} → B x → C x) → Σ A B → Σ A C
map₂ f = map id f

zip : ∀ {a b c p q r}
        {A : Set a} {B : Set b} {C : Set c}
        {P : A → Set p} {Q : B → Set q} {R : C → Set r} →
      (_∙_ : A → B → C) →
      (∀ {x y} → P x → Q y → R (x ∙ y)) →
      Σ A P → Σ B Q → Σ C R
zip _∙_ _∘_ (a , p) (b , q) = ((a ∙ b) , (p ∘ q))

swap : ∀ {a b} {A : Set a} {B : Set b} → A × B → B × A
swap (x , y) = (y , x)

_-×-_ : ∀ {a b i j} {A : Set a} {B : Set b} →
        (A → B → Set i) → (A → B → Set j) → (A → B → Set _)
f -×- g = f -[ _×_ ]- g

_-,-_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
        (A → B → C) → (A → B → D) → (A → B → C × D)
f -,- g = f -[ _,_ ]- g

curry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
        ((p : Σ A B) → C p) →
        ((x : A) → (y : B x) → C (x , y))
curry f x y = f (x , y)

curry′ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
         (A × B → C) → (A → B → C)
curry′ = curry

uncurry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
          ((x : A) → (y : B x) → C (x , y)) →
          ((p : Σ A B) → C p)
uncurry f (x , y) = f x y

uncurry′ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
           (A → B → C) → (A × B → C)
uncurry′ = uncurry


text:
module New where

module _ where

  open import Agda.Primitive

  record IsBottom {ℓ-⊥} (⊥ : Set ℓ-⊥) ℓ-elim : Set (lsuc ℓ-elim ⊔ ℓ-⊥) where
    field
      ⊥-elim : ⊥ → {A : Set ℓ-elim} → A

  open IsBottom ⦃ … ⦄ public

  record Bottom ℓ-⊥ ℓ-elim : Set (lsuc (ℓ-elim ⊔ ℓ-⊥)) where
    field
      ⊥ : Set ℓ-⊥
      instance ⦃ isBottom ⦄ : IsBottom ⊥ ℓ-elim

    ¬_ : ∀ {a} → Set a → Set (a ⊔ ℓ-⊥)
    ¬_ p = p → ⊥

  open Bottom ⦃ … ⦄ public

  record IsEquivalence {a} {A : Set a} {ℓ} (_≈_ : A → A → Set ℓ) : Set (a ⊔ ℓ) where
    field
      reflexivity : ∀ x → x ≈ x
      symmetry : ∀ x y → x ≈ y → y ≈ x
      transitivity : ∀ x y z → x ≈ y → y ≈ z → x ≈ z

  open IsEquivalence ⦃ … ⦄ public

  record Equivalence {a} (A : Set a) ℓ : Set (a ⊔ lsuc ℓ) where
    infix 4 _≈_
    field
      _≈_ : A → A → Set ℓ
      ⦃ isEquivalence ⦄ : IsEquivalence _≈_

  open Equivalence ⦃ … ⦄ public

  {-# DISPLAY Equivalence._≈_ _ = _≈_ #-}

  infix 4 _≉_
  _≉_ : ∀ {a} {A : Set a} {ℓ} ⦃ _ : Equivalence A ℓ ⦄ {b} ⦃ _ : Bottom b ℓ  ⦄ → A → A → Set (b ⊔ ℓ)
  _≉_ {ℓ = ℓ} x y = ¬ (x ≈ y)

  record _and_ {ℓ} (A : Set ℓ) (B : Set ℓ) : Set ℓ where
    field
      and₁ : A
      and₂ : B

  record _NOR_ {ℓ} (A : Set ℓ) (B : Set ℓ) : Set (lsuc ℓ) where
    field
      ⦃ bottom ⦄ : Bottom ℓ ℓ
      nor₁ : A → ⊥
      nor₂ : B → ⊥

  NOT : ∀ {ℓ} (A : Set ℓ) → Set (lsuc ℓ)
  NOT A = A NOR A

  _AND_ : ∀ {ℓ} (A B : Set ℓ) → Set (lsuc (lsuc ℓ))
  _AND_ A B = (NOT A) NOR (NOT B)

  _OR_ : ∀ {ℓ} (A B : Set ℓ) → Set (lsuc (lsuc ℓ))
  _OR_ A B = NOT (A NOR B)

  record Natlike {a} (A : Set a) ℓ b : Set (lsuc (b ⊔ a ⊔ ℓ)) where
    field
      zero : A
      suc : A → A
      ⦃ equivalence ⦄ : Equivalence A ℓ
      ⦃ bottom ⦄ : Bottom b ℓ
      suc-inj : ∀ {x} {y} → suc x ≈ suc y → x ≈ y
      cong-suc : ∀ {x y} → x ≈ y → suc x ≈ suc y
      zero≉one : zero ≉ suc zero
      zero-is-bottommost : ∀ x → suc x ≉ zero

    break-suc1 : suc zero ≉ suc (suc zero)
    break-suc1 x = zero≉one (suc-inj x)

    break-suc : ∀ x → suc x ≉ suc (suc x)
    break-suc x x₁ = {!suc-inj x₁!}

  record Isomorphic {a} (A : Set a) ℓᵃ ⦃ _ : Equivalence A ℓᵃ ⦄ {b} (B : Set b) ℓᵇ ⦃ _ : Equivalence B ℓᵇ ⦄ : Set (a ⊔ ℓᵃ ⊔ b ⊔ ℓᵇ) where
    field
      toB : A → B
      toA : B → A
      isoA : ∀ x → toA (toB x) ≈ x
      isoB : ∀ x → toB (toA x) ≈ x

  open import Agda.Builtin.Nat
  open import Agda.Builtin.Equality
  instance IsEquivalence≡ : ∀ {a} {A : Set a} → IsEquivalence {a} {A} _≡_
  IsEquivalence.reflexivity IsEquivalence≡ x = refl
  IsEquivalence.symmetry IsEquivalence≡ x .x refl = refl
  IsEquivalence.transitivity IsEquivalence≡ x .x z refl x₂ = x₂

  module _ where
    open import Prelude using (it)

    instance EquivalenceNat : Equivalence Nat lzero
    Equivalence._≈_ EquivalenceNat = _≡_

  record NatIso {a} (A : Set a) ℓ : Set (a ⊔ lsuc ℓ) where
    field
      ⦃ equivalence ⦄ : Equivalence A ℓ
      isoNat : Isomorphic A ℓ Nat lzero

  record Op₂ {a} (A : Set a) : Set a where
    infixl 6 _∙_
    field
      _∙_ : A → A → A

  open Op₂ ⦃ … ⦄ public

  record Op₀ {a} (A : Set a) : Set a where
    field
      ε : A

  open Op₀ ⦃ … ⦄ public

  record MonoidWithSuc {a} (A : Set a) : Set a where
    field
      instance op2 : Op₂ A
      op0 : Op₀ A
      ¡ : A → A

  open MonoidWithSuc ⦃ … ⦄ public

  private
   module ZC where
    private
      module ASD where
        open import Prelude.Nat using ()

  instance MonoidWithSucLevel : MonoidWithSuc Level
  Op₂._∙_ (MonoidWithSuc.op2 MonoidWithSucLevel) = _⊔_
  Op₀.ε (MonoidWithSuc.op0 MonoidWithSucLevel) = lzero
  MonoidWithSuc.¡ MonoidWithSucLevel = lsuc

module _ where

  open import Agda.Builtin.Nat

  instance MonoidWithSucNat : MonoidWithSuc Nat
  Op₂._∙_ (MonoidWithSuc.op2 MonoidWithSucNat) = _+_
  Op₀.ε (MonoidWithSuc.op0 MonoidWithSucNat) = 0
  MonoidWithSuc.¡ MonoidWithSucNat = suc

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

instance op0fromm : ∀ {a} {A : Set a} ⦃ _ : MonoidWithSuc A ⦄ → Op₀ A
op0fromm = op0

module _ where
 private
  foo : Nat → Set (¡ ε)
  foo x = x ∙ x ≡ x → Set

  bar : 4 ∙ 2 ≡ Nat.suc 5
  bar = refl

module _ where

  open import Agda.Primitive

  infix -65536 ℞_
  ℞_ : ∀ ℓ → Set (lsuc ℓ)
  ℞_ ℓ = Set ℓ

module _ where

  open import Agda.Primitive


text:
-- Andreas, 2022-06-10
-- A failed attempt to break Prop ≤ Set.
-- See https://github.com/agda/agda/issues/5761#issuecomment-1151336715

{-# OPTIONS --prop --cumulativity #-}

data   ⊥ : Set where
record ⊤ : Set where
  constructor tt

data Fool : Prop where
  true false : Fool

Bool : Set
Bool = Fool

True : Bool → Set
True true  = ⊤
True false = ⊥

X : Fool → Set

true≡false : X true → X false
true≡false x = x

X = True

-- Now we have  True true → True false  which looks dangerous...
-- But we cannot exploit it:

fails : ⊥
fails = true≡false tt

-- ERROR:
-- ⊤ !=< (True _)
-- when checking that the expression tt has type X _


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

-- | Exclusive option. Exactly one of the options holds at the same time.
module Dodo.Nullary.XOpt where

-- Stdlib imports
open import Level using (Level; _⊔_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Relation.Nullary using (¬_; Dec; yes; no)

-- # XOpt₂

data XOpt₂ {a b : Level} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  xopt₁ : ( a :   A) → (¬b : ¬ B) → XOpt₂ A B
  xopt₂ : (¬a : ¬ A) → ( b :   B) → XOpt₂ A B

xopt₂-apply : {a b c : Level} {A : Set a} {B : Set b} {C : Set c}
  → ( A → C )
  → ( B → C )
    -----------------
  → ( XOpt₂ A B → C )
xopt₂-apply f g (xopt₁ a _) = f a
xopt₂-apply f g (xopt₂ _ b) = g b

xopt₂-dec₁ : {a b : Level} {A : Set a} {B : Set b} → XOpt₂ A B → Dec A
xopt₂-dec₁ (xopt₁  a ¬b) = yes a
xopt₂-dec₁ (xopt₂ ¬a  b) = no ¬a

xopt₂-dec₂ : {a b : Level} {A : Set a} {B : Set b} → XOpt₂ A B → Dec B
xopt₂-dec₂ (xopt₁  a ¬b) = no ¬b
xopt₂-dec₂ (xopt₂ ¬a  b) = yes b

xopt₂-elim₁ : {a b : Level} {A : Set a} {B : Set b} → ¬ A → XOpt₂ A B → B
xopt₂-elim₁ ¬a (xopt₁  a ¬b) = ⊥-elim (¬a a)
xopt₂-elim₁ _  (xopt₂ ¬a  b) = b

xopt₂-elim₂ : {a b : Level} {A : Set a} {B : Set b} → ¬ B → XOpt₂ A B → A
xopt₂-elim₂ _  (xopt₁  a ¬b) = a
xopt₂-elim₂ ¬b (xopt₂ ¬a  b) = ⊥-elim (¬b b)

xopt₂-select₁ : {a b : Level} {A : Set a} {B : Set b} → A → XOpt₂ A B → ¬ B
xopt₂-select₁ _ (xopt₁ _ ¬b) = ¬b
xopt₂-select₁ a (xopt₂ ¬a _) = ⊥-elim (¬a a)

xopt₂-select₂ : {a b : Level} {A : Set a} {B : Set b} → B → XOpt₂ A B → ¬ A
xopt₂-select₂ b (xopt₁ _ ¬b) = ⊥-elim (¬b b)
xopt₂-select₂ b (xopt₂ ¬a _) = ¬a

xopt₂-sum : {a b : Level} {A : Set a} {B : Set b} → XOpt₂ A B → A ⊎ B
xopt₂-sum (xopt₁ a _) = inj₁ a
xopt₂-sum (xopt₂ _ b) = inj₂ b

-- # XOpt₃

data XOpt₃ {a b c : Level} (A : Set a) (B : Set b) (C : Set c) : Set (a ⊔ b ⊔ c) where
  xopt₁ : ( a :   A) → (¬b : ¬ B) → (¬c : ¬ C) → XOpt₃ A B C
  xopt₂ : (¬a : ¬ A) → ( b :   B) → (¬c : ¬ C) → XOpt₃ A B C
  xopt₃ : (¬a : ¬ A) → (¬b : ¬ B) → ( c :   C) → XOpt₃ A B C

xopt₃-apply : {a b c d : Level} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
  → ( A → D )
  → ( B → D )
  → ( C → D )
    -------------------
  → ( XOpt₃ A B C → D )
xopt₃-apply f g h (xopt₁ a _ _) = f a
xopt₃-apply f g h (xopt₂ _ b _) = g b
xopt₃-apply f g h (xopt₃ _ _ c) = h c

xopt₃-dec₁ : {a b c : Level} {A : Set a} {B : Set b} {C : Set c} → XOpt₃ A B C → Dec A
xopt₃-dec₁ (xopt₁  a _ _) = yes  a
xopt₃-dec₁ (xopt₂ ¬a _ _) = no ¬a
xopt₃-dec₁ (xopt₃ ¬a _ _) = no ¬a

xopt₃-dec₂ : {a b c : Level} {A : Set a} {B : Set b} {C : Set c} → XOpt₃ A B C → Dec B
xopt₃-dec₂ (xopt₁ _ ¬b _) = no ¬b
xopt₃-dec₂ (xopt₂ _  b _) = yes b
xopt₃-dec₂ (xopt₃ _ ¬b _) = no ¬b

xopt₃-dec₃ : {a b c : Level} {A : Set a} {B : Set b} {C : Set c} → XOpt₃ A B C → Dec C
xopt₃-dec₃ (xopt₁ _ _ ¬c) = no ¬c
xopt₃-dec₃ (xopt₂ _ _ ¬c) = no ¬c
xopt₃-dec₃ (xopt₃ _ _  c) = yes c

xopt₃-elim₁ : {a b c : Level} {A : Set a} {B : Set b} {C : Set c} → ¬ A → XOpt₃ A B C → XOpt₂ B C
xopt₃-elim₁ ¬a (xopt₁ a  _  _) = ⊥-elim (¬a a)
xopt₃-elim₁ _  (xopt₂ _  b ¬c) = xopt₁  b ¬c
xopt₃-elim₁ _  (xopt₃ _ ¬b  c) = xopt₂ ¬b  c

xopt₃-elim₂ : {a b c : Level} {A : Set a} {B : Set b} {C : Set c} → ¬ B → XOpt₃ A B C → XOpt₂ A C
xopt₃-elim₂ ¬b (xopt₁  a  _ ¬c) = xopt₁  a ¬c
xopt₃-elim₂ ¬b (xopt₂  _  b  _) = ⊥-elim (¬b b)
xopt₃-elim₂ ¬b (xopt₃ ¬a  _  c) = xopt₂ ¬a  c

xopt₃-elim₃ : {a b c : Level} {A : Set a} {B : Set b} {C : Set c} → ¬ C → XOpt₃ A B C → XOpt₂ A B
xopt₃-elim₃ _  (xopt₁  a ¬b  _) = xopt₁  a ¬b
xopt₃-elim₃ _  (xopt₂ ¬a  b  _) = xopt₂ ¬a  b
xopt₃-elim₃ ¬c (xopt₃  _  _  c) = ⊥-elim (¬c c)

xopt₃-select₁ : {a b c : Level} {A : Set a} {B : Set b} {C : Set c} → A → XOpt₃ A B C → ¬ B × ¬ C
xopt₃-select₁ a (xopt₁  _ ¬b ¬c) = ¬b , ¬c
xopt₃-select₁ a (xopt₂ ¬a  _  _) = ⊥-elim (¬a a)
xopt₃-select₁ a (xopt₃ ¬a  _  _) = ⊥-elim (¬a a)

xopt₃-select₂ : {a b c : Level} {A : Set a} {B : Set b} {C : Set c} → B → XOpt₃ A B C → ¬ A × ¬ C
xopt₃-select₂ b (xopt₁  _ ¬b  _) = ⊥-elim (¬b b)
xopt₃-select₂ b (xopt₂ ¬a  _ ¬c) = ¬a , ¬c
xopt₃-select₂ b (xopt₃  _ ¬b  _) = ⊥-elim (¬b b)

xopt₃-select₃ : {a b c : Level} {A : Set a} {B : Set b} {C : Set c} → C → XOpt₃ A B C → ¬ A × ¬ B
xopt₃-select₃ c (xopt₁  _  _ ¬c) = ⊥-elim (¬c c)
xopt₃-select₃ c (xopt₂  _  _ ¬c) = ⊥-elim (¬c c)
xopt₃-select₃ c (xopt₃ ¬a ¬b  _) = ¬a , ¬b

xopt₃-select₁₂ : {a b c : Level} {A : Set a} {B : Set b} {C : Set c} → A → B → XOpt₃ A B C → ⊥
xopt₃-select₁₂ a b x = proj₁ (xopt₃-select₁ a x) b

xopt₃-select₂₃ : {a b c : Level} {A : Set a} {B : Set b} {C : Set c} → B → C → XOpt₃ A B C → ⊥
xopt₃-select₂₃ b c x = proj₂ (xopt₃-select₂ b x) c

xopt₃-select₁₃ : {a b c : Level} {A : Set a} {B : Set b} {C : Set c} → A → C → XOpt₃ A B C → ⊥
xopt₃-select₁₃ a c x = proj₂ (xopt₃-select₁ a x) c

xopt₃-sum : {a b c : Level} {A : Set a} {B : Set b} {C : Set c} → XOpt₃ A B C → A ⊎ B ⊎ C
xopt₃-sum (xopt₁ a _ _) = inj₁ a
xopt₃-sum (xopt₂ _ b _) = inj₂ (inj₁ b)
xopt₃-sum (xopt₃ _ _ c) = inj₂ (inj₂ c)

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
module Issue2486.Haskell where

{-# FOREIGN GHC

data MyList a = Nil | Cons a (MyList a)

#-}


text:
------------------------------------------------------------------------------
-- Property <→◁
------------------------------------------------------------------------------

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

-- The <→◁ property proves that the recursive calls of the McCarthy 91
-- function are on smaller arguments.

module FOTC.Program.McCarthy91.WF-Relation.LT2WF-RelationATP where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.PropertiesATP using ( S∸S )
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesATP using ( x<0→⊥ )
open import FOTC.Data.Nat.Inequalities.PropertiesATP
  using ( x<y→x≤y
        ; x≥y→y>0→x∸y<x
        ; x∸y<Sx
        ; x<y∨x≥y
        ; Sx≯y→x≯y
        ; x≯y→x≤y
        ; x≤y→x∸y≡0
        ; x<y→0<y∸x
        )
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Data.Nat.UnaryNumbers.TotalityATP
  using ( 100-N
        ; 101-N
        )
open import FOTC.Program.McCarthy91.WF-Relation

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

<→◁-helper : ∀ {n m k} → N n → N m → N k →
             m < n → succ₁ n < k →
             succ₁ m < k →
             k ∸ n < k ∸ m →
             k ∸ succ₁ n < k ∸ succ₁ m
<→◁-helper nzero Nm Nk p qn qm h = ⊥-elim (x<0→⊥ Nm p)
<→◁-helper (nsucc Nn) Nm nzero p qn qm h = ⊥-elim (x<0→⊥ (nsucc Nm) qm)
<→◁-helper (nsucc {n} Nn) nzero (nsucc {k} Nk) p qn qm h = prfS0S
  where
  postulate
    k≥Sn   : k ≥ succ₁ n
    k∸Sn<k : k ∸ (succ₁ n) < k
    prfS0S : succ₁ k ∸ succ₁ (succ₁ n) < succ₁ k ∸ succ₁ zero
  {-# ATP prove k≥Sn x<y→x≤y #-}
  {-# ATP prove k∸Sn<k k≥Sn x≥y→y>0→x∸y<x #-}
  {-# ATP prove prfS0S k∸Sn<k S∸S #-}

<→◁-helper (nsucc {n} Nn) (nsucc {m} Nm) (nsucc {k} Nk) p qn qm h =
  k∸Sn<k∸Sm→Sk∸SSn<Sk∸SSm (<→◁-helper Nn Nm Nk m<n Sn<k Sm<k k∸n<k∸m)
  where
  postulate
    k∸Sn<k∸Sm→Sk∸SSn<Sk∸SSm : k ∸ succ₁ n < k ∸ succ₁ m →
                              succ₁ k ∸ succ₁ (succ₁ n) < succ₁ k ∸ succ₁ (succ₁ m)
  {-# ATP prove k∸Sn<k∸Sm→Sk∸SSn<Sk∸SSm S∸S #-}

  postulate
    m<n     : m < n
    Sn<k    : succ₁ n < k
    Sm<k    : succ₁ m < k
    k∸n<k∸m : k ∸ n < k ∸ m
  {-# ATP prove m<n #-}
  {-# ATP prove Sn<k #-}
  {-# ATP prove Sm<k #-}
  {-# ATP prove k∸n<k∸m S∸S #-}

<→◁ : ∀ {n m} → N n → N m → m ≯ 100' → m < n → n ◁ m
<→◁ nzero          Nm    p h = ⊥-elim (x<0→⊥ Nm h)
<→◁ (nsucc {n} Nn) nzero p h = prfS0
  where
  postulate prfS0 : succ₁ n ◁ zero
  {-# ATP prove prfS0 x∸y<Sx S∸S #-}

<→◁ (nsucc {n} Nn) (nsucc {m} Nm) p h with x<y∨x≥y Nn 100-N
... | inj₁ n<100 = <→◁-helper Nn Nm 101-N m<n Sn≤101 Sm≤101
                              (<→◁ Nn Nm m≯100 m<n)
  where
  postulate
    m≯100  : m ≯ 100'
    m<n    : m < n
    Sn≤101 : succ₁ n < 101'
    Sm≤101 : succ₁ m < 101'
  {-# ATP prove m≯100 Sx≯y→x≯y #-}
  {-# ATP prove m<n #-}
  {-# ATP prove Sn≤101 #-}
  {-# ATP prove Sm≤101 x≯y→x≤y #-}
... | inj₂ n≥100 = prf-n≥100
  where
  postulate
    0≡101∸Sn : zero ≡ 101' ∸ succ₁ n
    0<101∸Sm : zero < 101' ∸ succ₁ m
  {-# ATP prove 0≡101∸Sn x≤y→x∸y≡0 #-}
  {-# ATP prove 0<101∸Sm x≯y→x≤y x<y→0<y∸x #-}

  prf-n≥100 : succ₁ n ◁ succ₁ m
  prf-n≥100 = subst (λ t → t < 101' ∸ succ₁ m) 0≡101∸Sn 0<101∸Sm

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}

module Cubical.Algebra.Group.EilenbergMacLane.GroupStructure where

open import Cubical.Algebra.Group.EilenbergMacLane.Base
open import Cubical.Algebra.Group.EilenbergMacLane.WedgeConnectivity
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.AbGroup.Base

open import Cubical.Data.Nat

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.GroupoidLaws renaming (assoc to ∙assoc)
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Path

open import Cubical.Homotopy.Loopspace

open import Cubical.HITs.EilenbergMacLane1
open import Cubical.HITs.Truncation
  renaming (elim to trElim ; rec to trRec ; rec2 to trRec2)
open import Cubical.HITs.Susp

open import Cubical.Functions.Morphism

private
  variable ℓ : Level

module _ {G : AbGroup ℓ} where
  infixr 34 _+ₖ_
  infixr 34 _-ₖ_
  open AbGroupStr (snd G) renaming (_+_ to _+G_ ; -_ to -G_ ; +Assoc to +AssocG)

  private
    help : (n : ℕ) → n + (4 + n) ≡ (2 + n) + (2 + n)
    help n = +-suc n (3 + n) ∙ cong suc (+-suc n (suc (suc n)))

    hLevHelp : (n : ℕ) → isOfHLevel ((2 + n) + (2 + n)) (EM G (2 + n))
    hLevHelp n =
      transport (λ i → isOfHLevel (help n i) (EM G (2 + n)))
            (isOfHLevelPlus {n = 4 + n} n (isOfHLevelTrunc (4 + n)))

    helper : (g h : fst G)
      → PathP (λ i → Path (EM₁ (AbGroup→Group G))
               (emloop h i) (emloop h i)) (emloop g) (emloop g)
    helper g h =
      comm→PathP
        ((sym (emloop-comp _ h g)
          ∙∙ cong emloop (+Comm h g)
          ∙∙ emloop-comp _ g h))

  _+ₖ_ : {n : ℕ} → EM G n → EM G n → EM G n
  _+ₖ_ {n = zero} = _+G_
  _+ₖ_ {n = suc zero} =
    rec _ (isGroupoidΠ (λ _ → emsquash))
      (λ x → x)
      (λ x → funExt (looper x))
      λ g h i j x → el g h x i j
    where
    looper : fst G → (x : _) → x ≡ x
    looper g = (elimSet _ (λ _ → emsquash _ _)
                     (emloop g)
                     (helper g))

    el : (g h : fst G) (x : EM₁ (AbGroup→Group G))
      → Square (looper g x)
                (looper (g +G h) x)
                refl (looper h x)
    el g h =
      elimProp _ (λ _ → isOfHLevelPathP' 1 (emsquash _ _) _ _)
        (emcomp g h)

  _+ₖ_ {n = suc (suc n)} =
    trRec2 (isOfHLevelTrunc (4 + n))
      (wedgeConEM.fun G G (suc n) (suc n)
        (λ _ _ → hLevHelp n)
        ∣_∣ ∣_∣ refl)

  σ-EM : (n : ℕ) → EM-raw G (suc n) → Path (EM-raw G (2 + n)) ptEM-raw ptEM-raw
  σ-EM n x = merid x ∙ sym (merid ptEM-raw)

  -ₖ_ : {n : ℕ} → EM G n → EM G n
  -ₖ_ {n = zero} x = -G x
  -ₖ_ {n = suc zero} =
    rec _ emsquash
      embase
      (λ g → sym (emloop g))
      λ g h → sym (emloop-sym _ g)
            ◁ (flipSquare
                (flipSquare (emcomp (-G g) (-G h))
               ▷ emloop-sym _ h)
            ▷ (cong emloop (+Comm (-G g) (-G h)
                          ∙ sym (GroupTheory.invDistr (AbGroup→Group G) g h))
             ∙ emloop-sym _ (g +G h)))
  -ₖ_ {n = suc (suc n)} =
    map λ { north → north
          ; south → north
          ; (merid a i) → σ-EM n a (~ i)}

  _-ₖ_ : {n : ℕ} → EM G n → EM G n → EM G n
  _-ₖ_ {n = n} x y = _+ₖ_ {n = n} x (-ₖ_ {n = n} y)

  +ₖ-syntax : (n : ℕ) →  EM G n → EM G n → EM G n
  +ₖ-syntax n = _+ₖ_ {n = n}

  -ₖ-syntax : (n : ℕ) → EM G n → EM G n
  -ₖ-syntax n = -ₖ_ {n = n}

  -'ₖ-syntax : (n : ℕ) → EM G n → EM G n → EM G n
  -'ₖ-syntax n = _-ₖ_ {n = n}

  syntax +ₖ-syntax n x y = x +[ n ]ₖ y
  syntax -ₖ-syntax n x = -[ n ]ₖ x
  syntax -'ₖ-syntax n x y = x -[ n ]ₖ y

  lUnitₖ : (n : ℕ) (x : EM G n) → 0ₖ n +[ n ]ₖ x ≡ x
  lUnitₖ zero x = +IdL x
  lUnitₖ (suc zero) _ = refl
  lUnitₖ (suc (suc n)) =
    trElim (λ _ → isOfHLevelTruncPath {n = 4 + n})
      λ _ → refl

  rUnitₖ : (n : ℕ) (x : EM G n) → x +[ n ]ₖ 0ₖ n ≡ x
  rUnitₖ zero x = +IdR x
  rUnitₖ (suc zero) =
    elimSet _ (λ _ → emsquash _ _)
            refl
            λ _ _ → refl
  rUnitₖ (suc (suc n)) =
    trElim (λ _ → isOfHLevelTruncPath {n = 4 + n})
      (wedgeConEM.right G G (suc n) (suc n)
      (λ _ _ → hLevHelp n)
      ∣_∣ ∣_∣ refl)

  commₖ : (n : ℕ) (x y : EM G n) → x +[ n ]ₖ y ≡ y +[ n ]ₖ x
  commₖ zero = +Comm
  commₖ (suc zero) =
    wedgeConEM.fun G G 0 0 (λ _ _ → emsquash _ _)
      (λ x → sym (rUnitₖ 1 x))
      (rUnitₖ 1)
      refl
  commₖ (suc (suc n)) =
    elim2 (λ _ _ → isOfHLevelTruncPath {n = 4 + n})
      (wedgeConEM.fun G G _ _ (λ _ _ → isOfHLevelPath ((2 + n) + (2 + n)) (hLevHelp n) _ _)
      (λ x → sym (rUnitₖ (2 + n) ∣ x ∣))
      (λ x → rUnitₖ (2 + n) ∣ x ∣)
      refl)

  cong₂+₁ : (p q : typ (Ω (EM∙ G 1)))
          → cong₂ (λ x y → x +[ 1 ]ₖ y) p q ≡ p ∙ q
  cong₂+₁ p q =
      (cong₂Funct (λ x y → x +[ 1 ]ₖ y) p q)
   ∙ (λ i → (cong (λ x → rUnitₖ 1 x i) p) ∙ (cong (λ x → lUnitₖ 1 x i) q))

  cong₂+₂ : (n : ℕ) (p q : typ (Ω (EM∙ G  (suc (suc n)))))
          → cong₂ (λ x y → x +[ (2 + n) ]ₖ y) p q ≡ p ∙ q
  cong₂+₂ n p q =
      (cong₂Funct (λ x y → x +[ (2 + n) ]ₖ y) p q)
   ∙ (λ i → (cong (λ x → rUnitₖ (2 + n) x i) p) ∙ (cong (λ x → lUnitₖ (2 + n) x i) q))

  isCommΩEM : (n : ℕ) (p q : typ (Ω (EM∙ G  (suc n)))) → p ∙ q ≡ q ∙ p
  isCommΩEM zero p q =
       sym (cong₂+₁ p q)
    ∙∙ (λ i j → commₖ 1 (p j) (q j) i)
    ∙∙ cong₂+₁ q p
  isCommΩEM (suc n) p q =
       (sym (cong₂+₂ n p q)
    ∙∙ (λ i j → commₖ (suc (suc n)) (p j) (q j) i)
    ∙∙ cong₂+₂ n q p)

  cong-₁ : (p : typ (Ω (EM∙ G 1))) → cong (λ x → -[ 1 ]ₖ x) p ≡ sym p
  cong-₁ p = main embase p
    where
    decoder : (x : EM G 1) → embase ≡ x → x ≡ embase
    decoder =
      elimSet _
        (λ _ → isSetΠ λ _ → emsquash _ _)
        (λ p i → -[ 1 ]ₖ (p i))
        λ g → toPathP
          (funExt λ x →
            (λ i → transport (λ i → Path (EM G 1) (emloop g i) embase)
               (cong (-ₖ_ {n = 1})
                 (transp (λ j → Path (EM G 1) embase (emloop g (~ j ∧ ~ i))) i
                   (compPath-filler x (sym (emloop g)) i) )))
         ∙∙ (λ i → transp (λ j → Path (EM G 1) (emloop g (i ∨ j)) embase) i
                           (compPath-filler'
                             (sym (emloop g))
                             (cong-∙ (-ₖ_ {n = 1})
                                   x (sym (emloop g)) i) i))
      ∙∙ (cong (sym (emloop g) ∙_) (isCommΩEM 0 (cong (-ₖ_ {n = 1}) x) (emloop g)))
      ∙∙ ∙assoc _ _ _
      ∙∙ cong (_∙ (cong (-ₖ_ {n = 1}) x)) (lCancel (emloop g))
       ∙ sym (lUnit _))

    main : (x : EM G 1) (p : embase ≡ x) → decoder x p ≡ sym p
    main x = J (λ x p → decoder x p ≡ sym p) refl

  cong-₂ : (n : ℕ) (p : typ (Ω (EM∙ G (2 + n))))
    → cong (λ x → -[ 2 + n ]ₖ x) p ≡ sym p
  cong-₂ n p = main _ p
    where
    pp : (a : _)
      → PathP (λ i → 0ₖ (suc (suc n)) ≡ ∣ merid a i ∣ₕ → ∣ merid a i ∣ₕ ≡ 0ₖ (2 + n))
               (cong (λ x → -[ 2 + n ]ₖ x))
               λ p → cong ∣_∣ₕ (sym (merid ptEM-raw)) ∙ cong (λ x → -[ 2 + n ]ₖ x) p
    pp a =
      toPathP
        (funExt λ x →
          (λ k → transp (λ i → Path (EM G (2 + n)) ∣ merid a (i ∨ k) ∣ ∣ ptEM-raw ∣) k
                         (compPath-filler' (cong ∣_∣ₕ (sym (merid a)))
                          (cong (-ₖ-syntax (suc (suc n)))
                           (transp (λ j → Path (EM G (2 + n)) ∣ ptEM-raw ∣ ∣ merid a (~ j ∧ ~ k) ∣) k
                            (compPath-filler x (sym (cong ∣_∣ₕ (merid a))) k))) k))
               ∙∙ cong (cong ∣_∣ₕ (sym (merid a)) ∙_)
                       (cong-∙ (λ x → -[ 2 + n ]ₖ x) x (sym (cong ∣_∣ₕ (merid a)))
                      ∙ isCommΩEM (suc n) (cong (λ x → -[ 2 + n ]ₖ x) x) (cong ∣_∣ₕ (σ-EM n a)))
               ∙∙ (λ k → (λ i → ∣ merid a (~ i ∨ k) ∣)
                        ∙ (λ i → ∣ compPath-filler' (merid a) (sym (merid ptEM-raw)) (~ k) i ∣)
                        ∙ cong (λ x → -ₖ-syntax (suc (suc n)) x) x)
                ∙ sym (lUnit _))

    decoder : (x : EM G (2 + n))
            → 0ₖ (2 + n) ≡ x → x ≡ 0ₖ (2 + n)
    decoder =
      trElim (λ _ → isOfHLevelΠ (4 + n) λ _ → isOfHLevelTruncPath {n = 4 + n})
             λ { north → pp ptEM-raw i0
               ; south → pp ptEM-raw i1
               ; (merid a i) → pp a i}

    main : (x : EM G (2 + n)) (p : 0ₖ (2 + n) ≡ x) → decoder x p ≡ sym p
    main x = J (λ x p → decoder x p ≡ sym p) refl

  rCancelₖ : (n : ℕ) (x : EM G n) → x +[ n ]ₖ (-[ n ]ₖ x) ≡ 0ₖ n
  rCancelₖ zero x = +InvR x
  rCancelₖ (suc zero) =
    elimSet _ (λ _ → emsquash _ _)
      refl
      λ g → flipSquare (cong₂+₁ (emloop g) (λ i → -ₖ-syntax 1 (emloop g i))
           ∙ rCancel (emloop g))
  rCancelₖ (suc (suc n)) =
    trElim (λ _ → isOfHLevelTruncPath {n = 4 + n})
      λ { north → refl
        ; south i → +ₖ-syntax (suc (suc n)) ∣ merid ptEM-raw (~ i) ∣
                      (-ₖ-syntax (suc (suc n)) ∣ merid ptEM-raw (~ i) ∣)
        ; (merid a i) j
          → hcomp (λ r → λ { (i = i0) → 0ₖ (2 + n)
                             ; (i = i1) → ∣ merid ptEM-raw (~ j ∧ r) ∣ₕ -[ 2 + n ]ₖ ∣ merid ptEM-raw (~ j ∧ r) ∣
                             ; (j = i0) → ∣ compPath-filler (merid a) (sym (merid ptEM-raw)) (~ r) i ∣
                                        -[ 2 + n ]ₖ ∣ compPath-filler (merid a) (sym (merid ptEM-raw)) (~ r) i ∣
                             ; (j = i1) → 0ₖ (2 + n)})
                   (help' a j i) }
    where
    help' : (a : _)
      → cong₂ (λ x y → ∣ x ∣ -[ suc (suc n) ]ₖ ∣ y ∣) (σ-EM n a) (σ-EM n a) ≡ refl
    help' a =
         cong₂+₂ n (cong ∣_∣ₕ (σ-EM n a)) (cong (λ x → -[ 2 + n ]ₖ ∣ x ∣) (σ-EM n a))
      ∙∙ cong (cong ∣_∣ₕ (σ-EM n a) ∙_) (cong-₂ n (cong ∣_∣ₕ (σ-EM n a)))
      ∙∙ rCancel _

  lCancelₖ : (n : ℕ) (x : EM G n) → (-[ n ]ₖ x) +[ n ]ₖ x ≡ 0ₖ n
  lCancelₖ n x = commₖ n (-[ n ]ₖ x) x ∙ rCancelₖ n x

  assocₖ : (n : ℕ) (x y z : EM G n)
        → (x +[ n ]ₖ (y +[ n ]ₖ z) ≡ (x +[ n ]ₖ y) +[ n ]ₖ z)
  assocₖ zero = +AssocG
  assocₖ (suc zero) =
    elimSet _ (λ _ → isSetΠ2 λ _ _ → emsquash _ _)
      (λ _ _ → refl)
      λ g i y z k → lem g y z k i
    where
    lem : (g : fst G) (y z : _)
        → cong (λ x → x +[ suc zero ]ₖ (y +[ suc zero ]ₖ z)) (emloop g)
         ≡ cong (λ x → (x +[ suc zero ]ₖ y) +[ suc zero ]ₖ z) (emloop g)
    lem g =
      elimProp _ (λ _ → isPropΠ λ _ → emsquash _ _ _ _)
        (elimProp _ (λ _ → emsquash _ _ _ _)
          refl)
  assocₖ (suc (suc n)) =
    elim2 (λ _ _ → isOfHLevelΠ (4 + n) λ _ → isOfHLevelTruncPath {n = 4 + n})
      λ a b → trElim (λ _ → isOfHLevelTruncPath {n = 4 + n})
                (λ c → main c a b)
    where
    lem : (c : _) (a b : _)
      → PathP (λ i → (∣ a ∣ₕ +[ suc (suc n) ]ₖ (∣ b ∣ₕ +[ suc (suc n) ]ₖ ∣ merid c i ∣ₕ)
                    ≡ (∣ a ∣ₕ +[ suc (suc n) ]ₖ ∣ b ∣ₕ) +[ suc (suc n) ]ₖ ∣ merid c i ∣ₕ))
               (cong (λ x → ∣ a ∣ₕ +[ suc (suc n) ]ₖ x) (rUnitₖ (suc (suc n)) ∣ b ∣)
                   ∙ sym (rUnitₖ (suc (suc n)) (∣ a ∣ₕ +[ suc (suc n) ]ₖ ∣ b ∣ₕ)))
               ((λ i → ∣ a ∣ₕ +[ suc (suc n) ]ₖ (∣ b ∣ₕ +[ suc (suc n) ]ₖ ∣ merid ptEM-raw (~ i) ∣ₕ))
             ∙∙ cong (λ x → ∣ a ∣ₕ +[ suc (suc n) ]ₖ x) (rUnitₖ (suc (suc n)) ∣ b ∣)
                 ∙ sym (rUnitₖ (suc (suc n)) (∣ a ∣ₕ +[ suc (suc n) ]ₖ ∣ b ∣ₕ))
             ∙∙ λ i → (∣ a ∣ₕ +[ suc (suc n) ]ₖ ∣ b ∣ₕ) +[ suc (suc n) ]ₖ ∣ merid ptEM-raw i ∣ₕ)
    lem c =
      raw-elim G (suc n)
        (λ _ → isOfHLevelΠ (2 + n)
          (λ _ → isOfHLevelPathP' (2 + n) (isOfHLevelTrunc (4 + n) _ _) _ _))
           (raw-elim G (suc n)
            (λ _ → isOfHLevelPathP' (2 + n) (isOfHLevelTrunc (4 + n) _ _) _ _)
             ((sym (rUnit refl)
             ◁ λ _ → refl)
             ▷ (sym (lCancel (cong ∣_∣ₕ (merid ptEM-raw)))
             ∙ λ i → (λ j → ∣ merid ptEM-raw (~ j ∨ ~ i) ∣ₕ)
                   ∙∙ lUnit (λ j → ∣ merid ptEM-raw (~ j ∧ ~ i) ∣ₕ) i
                   ∙∙ cong ∣_∣ₕ (merid ptEM-raw))))
    main : (c a b : _)
      → (∣ a ∣ₕ +[ suc (suc n) ]ₖ (∣ b ∣ₕ +[ suc (suc n) ]ₖ ∣ c ∣ₕ)
       ≡ (∣ a ∣ₕ +[ suc (suc n) ]ₖ ∣ b ∣ₕ) +[ suc (suc n) ]ₖ ∣ c ∣ₕ)
    main north a b = lem ptEM-raw a b i0
    main south a b = lem ptEM-raw a b i1
    main (merid c i) a b = lem c a b i

  σ-EM' : (n : ℕ) (x : EM G (suc n))
        → Path (EM G (suc (suc n)))
                (0ₖ (suc (suc n)))
                (0ₖ (suc (suc n)))
  σ-EM' zero x = cong ∣_∣ₕ (σ-EM zero x)
  σ-EM' (suc n) =
    trElim (λ _ → isOfHLevelTrunc (5 + n) _ _)
      λ x → cong ∣_∣ₕ (σ-EM (suc n) x)

  σ-EM'-0ₖ : (n : ℕ) → σ-EM' n (0ₖ (suc n)) ≡ refl
  σ-EM'-0ₖ zero = cong (cong ∣_∣ₕ) (rCancel (merid ptEM-raw))
  σ-EM'-0ₖ (suc n) = cong (cong ∣_∣ₕ) (rCancel (merid ptEM-raw))

  private
    lUnit-rUnit-coh : ∀ {ℓ} {A : Type ℓ} {x : A} (p : x ≡ x) (r : refl ≡ p)
        → lUnit p ∙ cong (_∙ p) r
         ≡ rUnit p ∙ cong (p ∙_) r
    lUnit-rUnit-coh p =
      J (λ p r → lUnit p ∙ cong (_∙ p) r ≡ rUnit p ∙ cong (p ∙_) r) refl

  σ-EM'-hom : (n : ℕ) → (a b : _) → σ-EM' n (a +ₖ b) ≡ σ-EM' n a ∙ σ-EM' n b
  σ-EM'-hom zero =
    wedgeConEM.fun G G 0 0 (λ _ _ → isOfHLevelTrunc 4 _ _ _ _) l r p
    where
    l : _
    l x = cong (σ-EM' zero) (lUnitₖ 1 x)
        ∙∙ lUnit (σ-EM' zero x)
        ∙∙ cong (_∙ σ-EM' zero x) (sym (σ-EM'-0ₖ zero))

    r : _
    r x =
         cong (σ-EM' zero) (rUnitₖ 1 x)
      ∙∙ rUnit (σ-EM' zero x)
      ∙∙ cong (σ-EM' zero x ∙_) (sym (σ-EM'-0ₖ zero))

    p : _
    p = lUnit-rUnit-coh (σ-EM' zero embase) (sym (σ-EM'-0ₖ zero))
  σ-EM'-hom (suc n) =
    elim2 (λ _ _ → isOfHLevelPath (4 + n) (isOfHLevelTrunc (5 + n) _ _) _ _)
      (wedgeConEM.fun G G _ _
        (λ x y → transport (λ i → isOfHLevel (help n i)
                            ((σ-EM' (suc n) (∣ x ∣ₕ +ₖ ∣ y ∣ₕ)
                           ≡ σ-EM' (suc n) ∣ x ∣ₕ ∙ σ-EM' (suc n) ∣ y ∣ₕ)))
                    (isOfHLevelPlus {n = 4 + n} n
                      (isOfHLevelPath (4 + n)
                        (isOfHLevelTrunc (5 + n) _ _) _ _)))
        (λ x → cong (σ-EM' (suc n)) (lUnitₖ (suc (suc n)) ∣ x ∣)
            ∙∙ lUnit (σ-EM' (suc n) ∣ x ∣)
            ∙∙ cong (_∙ σ-EM' (suc n) ∣ x ∣) (sym (σ-EM'-0ₖ (suc n))))
        (λ x → cong (σ-EM' (suc n)) (rUnitₖ (2 + n) ∣ x ∣)
      ∙∙ rUnit (σ-EM' (suc n) ∣ x ∣)
      ∙∙ cong (σ-EM' (suc n) ∣ x ∣ ∙_) (sym (σ-EM'-0ₖ (suc n))))
        (lUnit-rUnit-coh (σ-EM' (suc n) (0ₖ (2 + n))) (sym (σ-EM'-0ₖ (suc n)))))

  σ-EM'-ₖ : (n : ℕ) → (a : _) → σ-EM' n (-ₖ a) ≡ sym (σ-EM' n a)
  σ-EM'-ₖ n =
    morphLemmas.distrMinus
      (λ x y → x +[ suc n ]ₖ y) (_∙_)
      (σ-EM' n) (σ-EM'-hom n)
      (0ₖ (suc n)) refl
      (λ x → -ₖ x) sym
      (λ x → sym (lUnit x)) (λ x → sym (rUnit x))
      (lCancelₖ (suc n)) rCancel
      ∙assoc (σ-EM'-0ₖ n)

  -Dist : (n : ℕ) (x y : EM G n) → -[ n ]ₖ (x +[ n ]ₖ y) ≡ (-[ n ]ₖ x) +[ n ]ₖ (-[ n ]ₖ y)
  -Dist zero x y = (GroupTheory.invDistr (AbGroup→Group G) x y) ∙ commₖ zero _ _
  -Dist (suc zero) = k
    where -- useless where clause. Needed for fast type checking for some reason.
    l : _
    l x = refl

    r : _
    r x = cong (λ z → -[ 1 ]ₖ z) (rUnitₖ 1 x) ∙ sym (rUnitₖ 1 (-[ 1 ]ₖ x))

    p : r ptEM-raw ≡ l ptEM-raw
    p = sym (rUnit refl)

    k = wedgeConEM.fun G G 0 0 (λ _ _ → emsquash _ _) l r (sym p)

  -Dist (suc (suc n)) =
    elim2 (λ _ _ → isOfHLevelTruncPath {n = 4 + n})
      (wedgeConEM.fun G G (suc n) (suc n)
        (λ _ _ → isOfHLevelPath ((2 + n) + (2 + n)) (hLevHelp n) _ _)
        (λ x → refl)
        (λ x → cong (λ z → -[ (suc (suc n)) ]ₖ z)
                     (rUnitₖ (suc (suc n)) ∣ x ∣ₕ)
                     ∙ sym (rUnitₖ (suc (suc n)) (-[ (suc (suc n)) ]ₖ ∣ x ∣ₕ)))
        (rUnit refl))

  addIso : (n : ℕ) (x : EM G n) → Iso (EM G n) (EM G n)
  Iso.fun (addIso n x) y = y +[ n ]ₖ x
  Iso.inv (addIso n x) y = y -[ n ]ₖ x
  Iso.rightInv (addIso n x) y =
       sym (assocₖ n y (-[ n ]ₖ x) x)
    ∙∙ cong (λ x → y +[ n ]ₖ x) (lCancelₖ n x)
    ∙∙ rUnitₖ n y
  Iso.leftInv (addIso n x) y =
    sym (assocₖ n y x (-[ n ]ₖ x))
    ∙∙ cong (λ x → y +[ n ]ₖ x) (rCancelₖ n x)
    ∙∙ rUnitₖ n y


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of functions, such as associativity and commutativity
------------------------------------------------------------------------

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

open import Level
open import Relation.Binary
open import Data.Sum

-- The properties are parameterised by the following "equality" relation

module Algebra.FunctionProperties
  {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where

open import Data.Product

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

open import Algebra.FunctionProperties.Core public

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

Associative : Op₂ A → Set _
Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))

Commutative : Op₂ A → Set _
Commutative _∙_ = ∀ x y → (x ∙ y) ≈ (y ∙ x)

LeftIdentity : A → Op₂ A → Set _
LeftIdentity e _∙_ = ∀ x → (e ∙ x) ≈ x

RightIdentity : A → Op₂ A → Set _
RightIdentity e _∙_ = ∀ x → (x ∙ e) ≈ x

Identity : A → Op₂ A → Set _
Identity e ∙ = (LeftIdentity e ∙) × (RightIdentity e ∙)

LeftZero : A → Op₂ A → Set _
LeftZero z _∙_ = ∀ x → (z ∙ x) ≈ z

RightZero : A → Op₂ A → Set _
RightZero z _∙_ = ∀ x → (x ∙ z) ≈ z

Zero : A → Op₂ A → Set _
Zero z ∙ = (LeftZero z ∙) × (RightZero z ∙)

LeftInverse : A → Op₁ A → Op₂ A → Set _
LeftInverse e _⁻¹ _∙_ = ∀ x → ((x ⁻¹) ∙ x) ≈ e

RightInverse : A → Op₁ A → Op₂ A → Set _
RightInverse e _⁻¹ _∙_ = ∀ x → (x ∙ (x ⁻¹)) ≈ e

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

LeftConical : A → Op₂ A → Set _
LeftConical e _∙_ = ∀ x y → (x ∙ y) ≈ e → x ≈ e

RightConical : A → Op₂ A → Set _
RightConical e _∙_ = ∀ x y → (x ∙ y) ≈ e → y ≈ e

Conical : A → Op₂ A → Set _
Conical e ∙ = (LeftConical e ∙) × (RightConical e ∙)

_DistributesOverˡ_ : Op₂ A → Op₂ A → Set _
_*_ DistributesOverˡ _+_ =
  ∀ x y z → (x * (y + z)) ≈ ((x * y) + (x * z))

_DistributesOverʳ_ : Op₂ A → Op₂ A → Set _
_*_ DistributesOverʳ _+_ =
  ∀ x y z → ((y + z) * x) ≈ ((y * x) + (z * x))

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

_IdempotentOn_ : Op₂ A → A → Set _
_∙_ IdempotentOn x = (x ∙ x) ≈ x

Idempotent : Op₂ A → Set _
Idempotent ∙ = ∀ x → ∙ IdempotentOn x

IdempotentFun : Op₁ A → Set _
IdempotentFun f = ∀ x → f (f x) ≈ f x

Selective : Op₂ A → Set _
Selective _∙_ = ∀ x y → (x ∙ y) ≈ x ⊎ (x ∙ y) ≈ y

_Absorbs_ : Op₂ A → Op₂ A → Set _
_∙_ Absorbs _∘_ = ∀ x y → (x ∙ (x ∘ y)) ≈ x

Absorptive : Op₂ A → Op₂ A → Set _
Absorptive ∙ ∘ = (∙ Absorbs ∘) × (∘ Absorbs ∙)

Involutive : Op₁ A → Set _
Involutive f = ∀ x → f (f x) ≈ x

LeftCancellative : Op₂ A → Set _
LeftCancellative _•_ = ∀ x {y z} → (x • y) ≈ (x • z) → y ≈ z

RightCancellative : Op₂ A → Set _
RightCancellative _•_ = ∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z

Cancellative : Op₂ A → Set _
Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_)

Congruent₁ : Op₁ A → Set _
Congruent₁ f = f Preserves _≈_ ⟶ _≈_

Congruent₂ : Op₂ A → Set _
Congruent₂ ∙ = ∙ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_

LeftCongruent : Op₂ A → Set _
LeftCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_

RightCongruent : Op₂ A → Set _
RightCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_


text:
module AbsToConDecl where

x where
    data D (A : Set) : Set where
      c : D A


text:
{-# OPTIONS --copatterns #-}
module Tree where

data Bool : Set where
  true false : Bool

record Tree (A : Set) : Set where
  field
    label : A
    child : Bool -> Tree A
open Tree

-- corecursive function defined by copattern matching
alternate : {A : Set}(a b : A) -> Tree A
-- deep copatterns:
label (child (alternate a b) false)       = b
child (child (alternate a b) false) true  = alternate a b
child (child (alternate a b) false) false = alternate a b
-- shallow copatterns
child {A = A} (alternate a b) true = alternate b a
label {A = A} (alternate a b)      = a

{- Delivers an infinite tree

                 a
            b        b
          a   a    a   a
         b b b b  b b b b
               ...
-}

infixr 5 _::_

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

collect : List Bool -> {A : Set} -> Tree A -> List A
collect []       t = []
collect (b :: l) t = label t :: collect l (child t b)

test : List Bool
test = collect (true :: true :: true :: []) (alternate true false)
-- should give true :: false : true :: []

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module SizedPolyIO.Base where

open import Data.Maybe.Base
open import Data.Sum renaming (inj₁ to left; inj₂ to right; [_,_]′ to either)

open import Function
open import Level using (_⊔_) renaming (suc to lsuc)
open import Size

open import NativePolyIO

record IOInterface γ ρ : Set (lsuc (γ ⊔ ρ)) where
  field
    Command   : Set γ
    Response  : (m : Command) → Set ρ
open IOInterface public

module _ {γ ρ} (I : IOInterface γ ρ) (let C = Command I) (let R = Response I) where

  mutual
    record IO (i : Size) {α} (A : Set α) : Set (α ⊔ γ ⊔ ρ) where
      coinductive
      constructor delay
      field
        force : {j : Size< i} → IO' j A

    data IO' (i : Size) {α} (A : Set α) : Set (α ⊔ γ ⊔ ρ) where
      do'      : (c : C) (f : R c → IO i A) → IO' i A
      return' : (a : A) → IO' i A

    data IO+ (i : Size) {α} (A : Set α) : Set (α ⊔ ρ ⊔ γ) where
      do' : (c : C) (f : R c → IO i A) → IO+ i A

open IO public

module _ {γ ρ} {I : IOInterface γ ρ} (let C = Command I) (let R = Response I) where

  return : ∀{i α}{A : Set α} (a : A) → IO I i A
  force (return a) = return' a

  do : ∀{i α}{A : Set α} (c : C) (f : R c → IO I i A) → IO I i A
  force (do c f) = do' c f

  do1 :  ∀{i} (c : C) → IO I i (R c)
  do1 c = do c return

  infixl 2 _>>=_ _>>='_ _>>_

  mutual
    _>>='_ : ∀{i α}{A B : Set α} (m : IO' I i A) (k : A → IO I (↑ i) B) → IO' I i B
    do' c f    >>=' k = do' c λ x → f x >>= k
    return' a >>=' k = force (k a)

    _>>=_ : ∀{i α}{A B : Set α} (m : IO I i A) (k : A → IO I i B) → IO I i B
    force (m >>= k) = force m >>=' k

  _>>_ : ∀{i α}{B : Set α} (m : IO I i Unit) (k : IO I i B) → IO I i B
  m >> k = m >>= λ _ → k

  {-# NON_TERMINATING #-}
  translateIO : ∀{α}{A : Set α}
    →  (translateLocal : (c : C) → NativeIO (R c))
    →  IO I ∞ A
    →  NativeIO A
  translateIO translateLocal m = case (force m {_}) of
    λ{ (do' c f)    → (translateLocal c) native>>= λ r →
         translateIO translateLocal (f r)
     ; (return' a) → nativeReturn a
     }

  -- Recursion

  -- trampoline provides a generic form of loop (generalizing while/repeat).
  -- Starting at state s : S, step function f is iterated until it returns
  -- a result in A.

  fromIO+' : ∀{i α}{A : Set α} → IO+ I i A → IO' I i A
  fromIO+' (do' c f) = do' c f

  fromIO+ : ∀{i α}{A : Set α} → IO+ I i A → IO I i A
  force (fromIO+ (do' c f)) = do' c f

  _>>=+'_ : ∀{i α}{A B : Set α} (m : IO+ I i A) (k : A → IO I i B) → IO' I i B
  do' c f >>=+' k = do' c λ x → f x >>= k

  _>>=+_ : ∀{i α}{A B : Set α} (m : IO+ I i A) (k : A → IO I i B) → IO I i B
  force (m >>=+ k) = m >>=+' k

  mutual

    _>>+_ : ∀{i α}{A B : Set α} (m : IO I i (A ⊎ B)) (k : A → IO I i B) → IO I i B
    force (m >>+ k) = force m >>+' k

    _>>+'_ : ∀{j α}{A B : Set α} (m : IO' I j (A ⊎ B)) (k : A → IO I (↑ j) B) → IO' I j B
    do' c f            >>+' k = do' c λ x → f x >>+ k
    return' (left  a) >>+' k = force (k a)
    return' (right b) >>+' k = return' b

   -- loop

  trampoline : ∀{i α}{A S : Set α} (f : S → IO+ I i (S ⊎ A)) (s : S) → IO I i A
  force (trampoline f s) = case (f s) of
    \{ (do' c k) → do' c λ r → k r >>+ trampoline f }

  -- simple infinite loop

  forever : ∀{i α}{A B : Set α} → IO+ I i A → IO I i B
  force (forever (do' c f)) = do' c λ r → f r >>= λ _ → forever (do' c f)

  whenJust : ∀{i α}{A : Set α} → Maybe A → (A → IO I i (Unit {α})) → IO I i Unit
  whenJust nothing  k = return _
  whenJust (just a) k = k a

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module Negative2 where

data Tree (A : Set) : Set where
    leaf : Tree A
    node : (A -> Tree A) -> Tree A

data Bad : Set where
    bad : Tree Bad -> Bad


text:
module Issue312 where

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

syntax Σ A (λ x → B) = Σ[ x ∶ A ] B

_×_ : Set → Set → Set
A × B = Σ[ _ ∶ A ] B

postulate
  T : Set → Set → Set
  equal : ∀ {A} → T A A
  _and_are_ : (A B : Set) → T A B → Set

  -- Check that it parses to the right thing
  check : ∀ A B → (A × B) and Σ A (λ x → B) are equal


text:
module sv20.class-exercise where

open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _≤_; s≤s; z≤n)

-- Subset definition taken from: https://agda.readthedocs.io/en/v2.6.1/language/irrelevance.html
-- Notice that irrelevance is not the same as function dot-pattern: https://agda.readthedocs.io/en/v2.6.1/language/function-definitions.html#dot-patterns

postulate
  .irrAx : ∀ {ℓ} {A : Set ℓ} -> .A -> A

record Subset (A : Set) (P : A -> Set) : Set where
  constructor _#_
  field
    elem         : A
    .certificate : P elem

.certificate : {A : Set}{P : A -> Set} -> (x : Subset A P) -> P (Subset.elem x)
certificate (a # p) = irrAx p

_ : Subset ℕ (_≤ 3)
_ = 3 # s≤s (s≤s (s≤s z≤n))
--_ = 0 # z≤n

--_∈_ : ?
--(a # p) ∈ s = ?


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

module Data.List.Kleene.Properties where

open import Data.List.Kleene.Base

open import Relation.Binary
open import Relation.Unary

open import Function

module _ {a r} {A : Set a} {R : Rel A r} where
  infix 4 _≈_
  _≈_ = R

  open import Algebra.FunctionProperties _≈_

  foldr-universal : Transitive _≈_
                  → ∀ {b} {B : Set b} (h : B ⋆ → A) f e
                  → ∀[ f ⊢ Congruent₁ ]
                  → (h [] ≈ e)
                  → (∀ x xs → h (∹ x & xs) ≈ f x (h xs))
                  → ∀ xs → h xs ≈ foldr⋆ f e xs
  foldr-universal trans h f e cong-f base cons [] = base
  foldr-universal trans h f e cong-f base cons (∹ x & xs) =
    (cons x xs) ⟨ trans ⟩ cong-f (foldr-universal trans h f e cong-f base cons xs)

  foldr-fusion : Transitive _≈_
               → Reflexive _≈_
               → ∀ {b c} {B : Set b} {C : Set c} (f : C → A) {_⊕_ : B → C → C} {_⊗_ : B → A → A} e
               → ∀[ _⊗_ ⊢ Congruent₁ ]
               → (∀ x y → f (x ⊕ y) ≈ x ⊗ f y)
               → ∀ xs → f (foldr⋆ _⊕_ e xs) ≈ foldr⋆ _⊗_ (f e) xs
  foldr-fusion trans refl h {f} {g} e cong-g fuse =
    foldr-universal trans (h ∘ foldr⋆ f e) g (h e) cong-g refl (λ x xs → fuse x (foldr⋆ f e xs))

max_stars_repo_name: oisdk/agda-kleene-lists

max_issues_repo_name: oisdk/agda-kleene-lists

max_forks_repo_name: oisdk/agda-kleene-lists


text:
------------------------------------------------------------------------------
-- Unary naturales numbers
------------------------------------------------------------------------------

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

module LTC-PCF.Data.Nat.UnaryNumbers where

open import LTC-PCF.Base

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

[0]  = zero
[1]  = succ₁ [0]
[2]  = succ₁ [1]
[3]  = succ₁ [2]
[4]  = succ₁ [3]
[5]  = succ₁ [4]
[6]  = succ₁ [5]
[7]  = succ₁ [6]
[8]  = succ₁ [7]
[9]  = succ₁ [8]


text:
module Category.Profunctor.Joker where
open import Agda.Primitive using (Level; _⊔_; lsuc)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Category.Functor using (RawFunctor; module RawFunctor)
open import Category.Functor.Lawful
open import Category.Profunctor
open import Category.Choice
open import Relation.Binary.PropositionalEquality using (refl)

Joker : ∀ {l₁ l₂ l₃} (F : Set l₂ → Set l₃) (A : Set l₁) (B : Set l₂) → Set l₃
Joker F _ B = F B

jokerProfunctor : ∀ {l₁ l₂} {F : Set l₁ → Set l₂} → RawFunctor F → ProfunctorImp (Joker F)
jokerProfunctor f = record
  { dimap = λ _ h g → h <$> g
  ; lmap  = λ _ g → g
  ; rmap  = λ h g → h <$> g
  } where open RawFunctor f

jokerLawfulProfunctor : ∀ {l₁ l₂} {F : Set l₁ → Set l₂} {FFunc : RawFunctor F} → LawfulFunctorImp FFunc → LawfulProfunctorImp (jokerProfunctor FFunc)
jokerLawfulProfunctor f = record
  { lmapId = refl
  ; rmapId = <$>-identity
  ; dimapLmapRmap = refl
  } where open LawfulFunctor f

jokerChoice : ∀ {l₁ l₂} {F : Set l₁ → Set l₂} → RawFunctor F → ChoiceImp (Joker F)
jokerChoice f  = record
  { isProfunctor = jokerProfunctor f
  ; left' = inj₁ <$>_
  ; right' = inj₂ <$>_
  }
  where open RawFunctor f

max_stars_repo_name: crisoagf/agda-optics

max_issues_repo_name: crisoagf/agda-optics

max_forks_repo_name: crisoagf/agda-optics


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- M-types (the dual of W-types)
------------------------------------------------------------------------

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

module Codata.Musical.M where

open import Codata.Musical.Notation
open import Level
open import Data.Product hiding (map)
open import Data.Container.Core as C hiding (map)

-- The family of M-types.

data M {s p} (C : Container s p) : Set (s ⊔ p) where
  inf : ⟦ C ⟧ (∞ (M C)) → M C

-- Projections.

module _ {s p} (C : Container s p) where

  head : M C → Shape C
  head (inf (x , _)) = x

  tail : (x : M C) → Position C (head x) → M C
  tail (inf (x , f)) b = ♭ (f b)

-- map

module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂}
         (m : C₁ ⇒ C₂) where

  map : M C₁ → M C₂
  map (inf (x , f)) = inf (shape m x , λ p → ♯ map (♭ (f (position m p))))

-- unfold

module _ {s p ℓ} {C : Container s p} (open Container C)
         {S : Set ℓ} (alg : S → ⟦ C ⟧ S) where

  unfold : S → M C
  unfold seed = let (x , f) = alg seed in
                inf (x , λ p → ♯ unfold (f p))

------------------------------------------------------------------------
-- Legacy

import Codata.M as M
open import Codata.Thunk
import Size

module _ {s p} {C : Container s p} where

  fromMusical : ∀ {i} → M C → M.M C i
  fromMusical (inf t) = M.inf (C.map rec t) where
    rec = λ x → λ where .force → fromMusical (♭ x)

  toMusical : M.M C Size.∞ → M C
  toMusical (M.inf (s , f)) = inf (s , λ p → ♯ toMusical (f p .force))


text:
-- Andreas, 2013-03-15 issue reported by Nisse

-- {-# OPTIONS -v tc.proj:40 -v tc.conv.elim:40 #-}
-- {-# OPTIONS -v tc.inj.check:45 #-}
-- {-# OPTIONS -v tc.proj.like:45 #-}

module Issue821 where

import Common.Level

data D (A : Set) : Set where
  c : D A → D A

-- f is projection like, but could also be injective!?
f : (A : Set) → D A → D A
f A (c x) = x

postulate
  A : Set
  P : D A → Set
  x : D A
  p : P x
  Q : P (f A x) → Set

Foo : Set₁
Foo = Q p

-- WAS:
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/Conversion.hs:466

-- Reason was that f is projection-like so the test x =?= f A x
-- actually becomes x =?= x .f with unequal spine shapes (empty vs. non-empty).
-- Agda thought this was impossible.

-- Expected error:
-- x != (f A x) of type (D A)
-- when checking that the expression p has type P (f A x)

-- Projection-likeness of f will turn this into:
-- x != (f _ x) of type (D A)


text:
module Examples where

-- The terms of AExp assign a binding time to each subterm. For
-- program specialization, we interpret terms with dynamic binding
-- time as the programs subject to specialization, and their subterms
-- with static binding time as statically known inputs. A partial
-- evaluation function (or specializer) then compiles the program into
-- a residual term for that is specialized for the static inputs. The
-- main complication when defining partial evaluation as a total,
-- primitively recursive function will be the treatment of the De
-- Bruijn variables of non-closed residual expressions.

-- Before diving into the precise definition, it is instructive to
-- investigate the expected result of partial evaluation on some
-- examples.

{-
module AExp-Examples where

  open import Data.Product

  -- (We pre-define some De Bruijn indices to improve
  -- readability of the examples:)
  x : ∀ {α Δ} → AExp (α ∷ Δ) α
  x = Var hd
  y : ∀ {α₁ α Δ} → AExp (α₁ ∷ α ∷ Δ) α
  y = Var (tl hd)
  z : ∀ {α₁ α₂ α Δ} → AExp (α₁ ∷ α₂ ∷ α ∷ Δ) α
  z = Var (tl (tl hd))

  -- A very simple case is the addition of three constants, where one
  -- is dynamically bound and two are bound statically:
  -- 5D +D (30S +S 7S)

  -- ex1 : AExp [] (D Int)
  -- ex1 = DAdd (DInt 5) (AAdd (AInt 30) (AInt 7))
  -- ex1' : AExp [] (D Int)
  -- ex1' = AApp (ALam (DAdd (DInt 5) x)) (AApp (ALam (DInt x) (AInt 30) (AInt 7)))

  -- TODO: this example does not work due to the very restrictive type
  -- off Add/DAdd. We could add a subsumption operator to AExp that
  -- turns a static expression into a dynamic one and then build a
  -- smart constructor for addition on top of that

  -- Note:This case is omitted in the same way as we impose the restriction that
  --      a dynamic function can only have components which are also dynamic.

  -- Another simple case is the specialization for a static identity
  -- function:
  -- (Sλ x → x) (42D)  ---specializes to--> 42D
  ex1 : AExp [] (D Int)
  ex1 = AApp (ALam (Var hd)) (DInt 42)

  ex1-spec : Exp [] Int
  ex1-spec = EInt 42

  -- The above example can be rewritten as an open AExp term that
  -- should be closed with a suitable environment. This representation
  -- does not only corresponds more directly with the notion of
  -- ``static inputs'', it also illustrates a typical situation when
  -- specializing the body of a lambda abstraction:

  -- The program ex1' takes an Int→Int function x as a static input.
  --ex1' : AExp [ AFun (D Int) (D Int) ] (D Int)
  --ex1' = AApp x (DInt 42)

  ---------------------
  -- Some more examples
  ---------------------
  ------------------
  -- Pairs
  ------------------
  ------------------
  -- a. Static Pairs
  ------------------
  ex2 : AExp [] (D Int)
  ex2 = Snd (AInt 42 , DInt 42)

  ex3 : AExp [] (D Int)
  ex3 = AApp (ALam (Snd (Var hd))) (AInt 42 , DInt 42)

  -- similar to ex1'
  --ex3' : AExp [ AFun (AInt • (D Int)) (D Int) ] (D Int)
  --ex3' = AApp x (AInt 42 , DInt 42)

  -------------------
  -- b. Dynamic Pairs
  -------------------
  ex4 : AExp [] (D Int)
  ex4 = AApp (ALam (DSnd (Var hd))) ( DInt 43 ḋ DInt 42)

  -- similar to ex1'
  --ex4' : AExp [ AFun (D (Int • Int)) (D Int) ] (D Int)
  --ex4' = AApp x (DInt 43 ḋ DInt 42)

  ---------------------
  -- Sums
  ---------------------
  -----------------
  -- a. Static Sums
  -----------------
  ex5 : AExp [] AInt
  ex5 = Case {α₂ = AInt} (Tl (AInt 0))  (Var hd) (Var hd)

  ex6 : AExp [] AInt
  ex6 = Case {α₁ = AInt} (Tr (AInt 0))  (Var hd) (AInt 10)

  ex7 : AExp [] (AFun AInt AInt)
  ex7 = Case {α₂ = AInt} (Tl (ALam (Var hd))) (Var hd) (ALam (Var hd))

  ------------------
  -- b. Dynamic Sums
  ------------------
  ex8 : AExp [] (D Int)
  ex8 = DCase {σ₂ = Int} (DTl (DInt 0)) (Var hd) (Var hd)

  ex9 : AExp [] (D Int)
  ex9 = DCase {σ₁ = Int} (DTr (DInt 0)) (Var hd) (DInt 10)

  ex10 : AExp [] (D (Fun Int Int))
  ex10 = DCase {σ₂ = Int} (DTl (DLam (Var hd))) (Var hd) (DLam (Var hd))

  -- The partial evaluation of ex1' requires an environment to look up
  -- the static input. As a first approximation, a single input of
  -- type α is just some annotated term of type type α:
  Input : ∀ α → Set
  Input α = (∃ λ Δ → AExp Δ α)

  ----------------------------
  -- alternative specification
  ----------------------------
  --record Sg  (S : Set) (T : S → Set) : Set where
  --  constructor _,_
  --  field
  --    ffst : S
  --    ssnd : T ffst
  --open Sg public
  --Input' : ∀ α → Set
  --Input' α = Sg ACtx \ x → AExp x α
  -- Note that [input'] should be equivalent to [input]

  -- (convenience constructor for Inputs)
  inp : ∀ {α Δ} → AExp Δ α → Input α
  inp {α} {Δ} e = Δ , e
  -- An environment is simply a list of inputs that agrees with a
  -- given typing context.
  data AEnv : ACtx → Set where
    [] : AEnv []
    _∷_ : ∀ {α Δ} → Input α → AEnv Δ → AEnv (α ∷ Δ)

  lookup : ∀ {α Δ} → AEnv Δ → α ∈ Δ → Input α
  lookup [] ()
  lookup (x ∷ env) hd = x
  lookup (x ∷ env) (tl id) = lookup env id

  -- Thus, an environment like ex1'-env should be able to close ex1'
  -- and a partial evaluation of the closure should yield the same
  -- result as in example ex1:
  --ex1'-env : AEnv [ AFun (D Int) (D Int) ]
  --ex1'-env = inp (ALam {[]} {D Int} (Var hd)) ∷ []

  -- Similarly, an environment like ex3'-env should be able to close ex3'
  -- and a partial evaluation of the closure should yield the same
  -- result as in example ex3:
  --ex3'-env : AEnv [ AFun (AInt • (D Int)) (D Int) ]
  --ex3'-env = inp (ALam {[]} {AInt • (D Int)} (Snd (Var hd))) ∷ []

  -- Also, an environment like ex4'-env should be able to close ex4'
  -- and a partial evaluation of the closure should yield the same
  -- result as in example ex4:
  --ex4'-env : AEnv [ AFun (D (Int • Int)) (D Int) ]
  --ex4'-env = inp (ALam {[]} {D (Int • Int)} (DSnd (Var hd))) ∷ []

  -- TODO: unit test
  ex1'-spec = ex1-spec
  ex3'-spec = ex1-spec
  ex4'-spec = ex1-spec

  -- (some definitions for the example)
  open import Data.Maybe
  _=<<_ : ∀ {A B : Set} → (A → Maybe B) → Maybe A → Maybe B
  f =<< mx = maybe′ f nothing mx
  liftM2 : ∀ {A B C : Set} → (A → B → Maybe C) → Maybe A → Maybe B → Maybe C
  liftM2 f mx my = (λ x → (λ y → f x y) =<< my) =<< mx

  -- The partial function ex1'-pe demonstrates the desired calculation
  -- for the specific case of ex1':
  ex1'-pe : ∀ {Δ} → AEnv Δ → AExp Δ (D Int) → Maybe (Exp [] Int)
  ex1'-pe {Δ} env (AApp ef ei)
    = liftM2 fromApp
             (fromInput =<< fromVar ef)
             (fromInt ei)

    where fromInput : ∀ {α} → Input α → Maybe (Exp [] Int → Exp [] Int)
          fromInput (_ , ALam {D Int} (Var hd)) = just (λ x → x)
          -- Sλ x/D → x
          fromInput _ = nothing
          fromVar : ∀ {α} → AExp Δ α → Maybe (Input α)
          fromVar (Var x) = just (lookup env x)
          fromVar _ = nothing
          fromApp : (Exp [] Int → Exp [] Int) → Exp [] Int → Maybe (Exp [] Int)
          fromApp f x = just (f x)
          fromInt : ∀ {α} → AExp Δ α → Maybe (Exp [] Int)
          fromInt (DInt i) = just (EInt {[]} i)
          fromInt _ = nothing
  ex1'-pe _ _ = nothing

  open import Relation.Binary.PropositionalEquality
  check-ex1'-pe : ex1'-pe ex1'-env ex1' ≡ just (ex1'-spec)
  check-ex1'-pe = refl

  -- Similarly the partial function ex3'-pe demonstrates the desired calculation
  -- for the specific case of ex3':

  ex3'-pe : ∀ {Δ} → AEnv Δ → AExp Δ (D Int) → Maybe (Exp [] Int)
  ex3'-pe {Δ} env (AApp ef ei)
    = liftM2 fromApp
             (fromInput =<< fromVar ef)
             (fromPair ei)

    where fromInput : ∀ {α} → Input α → Maybe ((ℕ * (Exp [] Int)) → Exp [] Int)
          fromInput (_ , ALam {AInt • (D Int)} (Snd (Var hd))) = just (λ x → (snd x))
          -- Sλ x/(S*D) → (snd x)
          fromInput _ = nothing
          fromVar : ∀ {α} → AExp Δ α → Maybe (Input α)
          fromVar (Var x) = just (lookup env x)
          fromVar _ = nothing
          fromApp : ((ℕ  * (Exp [] Int)) → Exp [] Int) → (ℕ * (Exp [] Int)) → Maybe (Exp [] Int)
          fromApp f x = just (f x)
          fromPair : ∀ {α} → AExp Δ α → Maybe (ℕ * (Exp [] Int))
          fromPair ((AInt j) , (DInt i)) = just (j , (EInt {[]} i))
          fromPair _ = nothing
  ex3'-pe _ _ = nothing

  open import Relation.Binary.PropositionalEquality
  check-ex3'-pe : ex3'-pe ex3'-env ex3' ≡ just (ex3'-spec)
  check-ex3'-pe = refl

  -- Similarly the partial function ex3'-pe demonstrates the desired calculation
  -- for the specific case of ex3':

  ex4'-pe : ∀ {Δ} → AEnv Δ → AExp Δ (D Int) → Maybe (Exp [] Int)
  ex4'-pe {Δ} env (AApp ef ei)
    = liftM2 fromApp
             (fromInput =<< fromVar ef)
             (fromDPair ei)

    where fromInput : ∀ {α} → Input α → Maybe (((Exp [] Int) * (Exp [] Int)) → Exp [] Int)
          fromInput (_ , ALam {D (Int • Int)} (DSnd (Var hd))) = just (λ x → (snd x))
          -- Sλ x/(S*D) → (snd x)
          fromInput _ = nothing
          fromVar : ∀ {α} → AExp Δ α → Maybe (Input α)
          fromVar (Var x) = just (lookup env x)
          fromVar _ = nothing
          fromApp : (((Exp [] Int)  * (Exp [] Int)) → Exp [] Int) → ((Exp [] Int) * (Exp [] Int)) → Maybe (Exp [] Int)
          fromApp f x = just (f x)
          fromDPair : ∀ {α} → AExp Δ α → Maybe ((Exp [] Int) * (Exp [] Int))
          fromDPair ((DInt j) ḋ (DInt i)) = just ((EInt {[]} j) , (EInt {[]} i))
          fromDPair _ = nothing
  ex4'-pe _ _ = nothing

  open import Relation.Binary.PropositionalEquality
  check-ex4'-pe : ex4'-pe ex4'-env ex4' ≡ just (ex4'-spec)
  check-ex4'-pe = refl

  -- The examples above show several problems for a total
  -- generalization to arbitrary term with the current datastructures:
  --  - the argument to fromApp is not primitive recursive

  -- What?

  --  - the result type of fromInput generates the context of the returned expression
  --    ``out of thin air''

  --  - Note "out of thin air" in a sense that the "typing context for the value" is only restricted by
  --    the value v itself thus any Δ which types v will do. Also note there is no connection between
  --    "typing context for the value" and the "typing context"

  -- TODO: continue

  -- Dλ y → let f = λ x → x D+ y in Dλ z → f z
  term1 : AExp [] (D (Fun Int (Fun Int Int)))
  term1 = DLam (AApp (ALam (DLam (AApp (ALam y) x)))
                     ((ALam (DAdd x y))))

-- Dλ y → let f = λ x → (Dλ w → x D+ y) in Dλ z → f z
-- Dλ y → (λ f → Dλ z → f z) (λ x → (Dλ w → x D+ y))
-- wrong
  term2 : AExp [] (D (Fun Int (Fun Int Int)))
  term2 = DLam (AApp (ALam (DLam (AApp (ALam y) x)))
                     ((ALam (DLam {σ₁ = Int} (DAdd y z)))))
-- ?
  term3 : AExp [] (D (Fun Int (Fun Int Int)))
  term3 = DLam (AApp (ALam (DLam (AApp (ALam y) x)))
                     (DInt 0))
  -- correct!
  term4 : AExp [] (D (Fun Int (Fun Int (Fun Int Int))))
  term4 = DLam (AApp (ALam (DLam (AApp y x)))
                     ((ALam (DLam {σ₁ = Int} (DAdd y z)))))
  ------------------
  -- Some more terms
  ------------------

-}

{-

module CheckExamples where
  open import Relation.Binary.PropositionalEquality
  open SimpleAEnv
  open AExp-Examples

  check-ex1 : pe ex1 [] ≡ ex1-spec
  check-ex1 = refl
  -------------
  -- Similarly
  ------------
  check-ex3 : pe ex3 [] ≡ ex1-spec
  check-ex3 = refl

  -------
  -- Also
  -------
  check-ex4 : pe {Γ = []} ex4 [] ≡ ESnd (EInt 43 , EInt 42)
  check-ex4 = refl

module Examples where
  open SimpleAEnv
  open import Relation.Binary.PropositionalEquality

  x : ∀ {α Δ} → AExp (α ∷ Δ) α
  x = Var hd
  y : ∀ {α₁ α Δ} → AExp (α₁ ∷ α ∷ Δ) α
  y = Var (tl hd)
  z : ∀ {α₁ α₂ α Δ} → AExp (α₁ ∷ α₂ ∷ α ∷ Δ) α
  z = Var (tl (tl hd))

-- Dλ y → let f = λ x → x D+ y in Dλ z → f z
  term1 : AExp [] (D (Fun Int (Fun Int Int)))
  term1 = DLam (AApp (ALam (DLam (AApp (ALam y) x)))
                     ((ALam (DAdd x y))))

-- Dλ y → let f = λ x → (Dλ w → x D+ y) in Dλ z → f z
-- Dλ y → (λ f → Dλ z → f z) (λ x → (Dλ w → x D+ y))
  term2 : AExp [] (D (Fun Int (Fun Int Int)))
  term2 = DLam (AApp (ALam (DLam (AApp (ALam y) x)))
                     ((ALam (DLam {σ₁ = Int} (DAdd y z)))))

  -- closed pe. In contrast to BTA5, it is now not clear what Γ is
  -- given an expression. So perhaps AEnv has it's merrits after all?
  pe[] : ∀ {α} → AExp [] α → Imp [] α
  pe[] e = pe e []

  ex-pe-term1 : pe[] term1 ≡ ELam (ELam (EVar hd))
  ex-pe-term1 = refl

  ex-pe-term2 : pe[] term2 ≡ ELam (ELam (EVar hd))
  ex-pe-term2 = refl

  --------------------------
  -- Tests on pairs and sums
  --------------------------

-}

max_stars_repo_name: luminousfennell/polybta

max_issues_repo_name: luminousfennell/polybta

max_forks_repo_name: luminousfennell/polybta


text:
open import Numeral.Natural
open import Type

module Formalization.ClassicalPredicateLogic.Syntax {ℓₚ ℓᵥ ℓₒ} (Prop : ℕ → Type{ℓₚ}) (Var : Type{ℓᵥ}) (Obj : ℕ → Type{ℓₒ}) where

open import Data.ListSized
import      Lvl
open import Functional using (_∘_ ; _∘₂_ ; swap)
open import Sets.PredicateSet using (PredSet)

private variable ℓ : Lvl.Level
private variable n : ℕ

data Term : Type{ℓᵥ Lvl.⊔ ℓₒ} where
  var  : Var → Term                -- Variables
  func : Obj(n) → List(Term)(n) → Term -- Constants/functions

-- Formulas.
-- Inductive definition of the grammatical elements of the language of predicate logic.
data Formula : Type{ℓₚ Lvl.⊔ ℓᵥ Lvl.⊔ ℓₒ} where
  _$_ : Prop(n) → List(Term)(n) → Formula -- Relations

  ⊤ : Formula -- Tautology (Top / True)
  ⊥ : Formula -- Contradiction (Bottom / False)

  _∧_ : Formula → Formula → Formula -- Conjunction (And)
  _∨_ : Formula → Formula → Formula -- Disjunction (Or)
  _⟶_ : Formula → Formula → Formula -- Implication

  Ɐ : Var → Formula → Formula
  ∃ : Var → Formula → Formula

infix  1011 _$_
infixr 1005 _∧_
infixr 1004 _∨_
infixr 1000 _⟶_

-- Negation
¬_ : Formula → Formula
¬_ = _⟶ ⊥

-- Double negation
¬¬_ : Formula → Formula
¬¬_ = (¬_) ∘ (¬_)

-- Reverse implication
_⟵_ : Formula → Formula → Formula
_⟵_ = swap(_⟶_)

-- Equivalence
_⟷_ : Formula → Formula → Formula
p ⟷ q = (p ⟵ q) ∧ (p ⟶ q)

-- (Nor)
_⊽_ : Formula → Formula → Formula
_⊽_ = (¬_) ∘₂ (_∨_)

-- (Nand)
_⊼_ : Formula → Formula → Formula
_⊼_ = (¬_) ∘₂ (_∧_)

-- (Exclusive or / Xor)
_⊻_ : Formula → Formula → Formula
_⊻_ = (¬_) ∘₂ (_⟷_)

infix  1010 ¬_ ¬¬_
infixl 1000 _⟵_ _⟷_

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:
-- Andreas, 2018-06-14, issue #2513, do not allow conflicting relevance info.

postulate
  Foo : {A : Set} → ..(@irrelevant A) → A

-- Should fail.  (Currently: parse error)


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

syntax Inception | IA

type
  L : 0-ary
  P : 0-ary
  A : 0-ary

term
  rec : L  P  ->  A
  inc : L.A  P.A  ->  A

theory
  (S) p : P   a : P.A |> inc (l. rec (l, p[]), x. a[x]) = a[p[]]
  (E) a : L.A  |> k : L |- inc (l. a[l], x. rec(k, x)) = a[k]
  (W) m : A  a : P.A  |> inc (l. m[], x. a[x]) = m[]
  (A) p : (L,L).A  a : (L,P).A  b : P.A |>         inc (l. inc (k. p[l, k], x. a[l,x]), y. b[y])       = inc (k. inc(l. p[l,k], y.b[y]), x. inc(l. a[l,x], y.b[y]))
-}

module Inception.Signature where

open import SOAS.Context

-- Type declaration
data IAT : Set where
  L : IAT
  P : IAT
  A : IAT

open import SOAS.Syntax.Signature IAT public
open import SOAS.Syntax.Build IAT public

-- Operator symbols
data IAₒ : Set where
  recₒ incₒ : IAₒ

-- Term signature
IA:Sig : Signature IAₒ
IA:Sig = sig λ
  {  recₒ  → (⊢₀ L) , (⊢₀ P) ⟼₂ A
  ;  incₒ  → (L ⊢₁ A) , (P ⊢₁ A) ⟼₂ A
  }

open Signature IA:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module Oscar.Data.Equality where

open import Agda.Builtin.Equality public using (_≡_; refl) public
open import Relation.Binary.PropositionalEquality public using (_≢_) public
open import Relation.Binary.PropositionalEquality public using (cong; cong₂; cong-app; subst; subst₂; sym; trans) public

open import Oscar.Level
open import Oscar.Function
open import Oscar.Relation

infix 4 _≡̇_
_≡̇_ : ∀ {a} {A : Set a} {b} {B : A → Set b} → ((x : A) → B x) → ((x : A) → B x) → Set (a ⊔ b)
f ≡̇ g = ∀ x → f x ≡ g x

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

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

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

open import Oscar.Category

≡-setoid : ∀ {a} (A : Set a) → Setoid A a
Setoid._≋_ (≡-setoid A) = _≡_
Setoid.≋-reflexivity (≡-setoid A) = refl
Setoid.≋-symmetry (≡-setoid A) = sym
Setoid.≋-transitivity (≡-setoid A) x≡y = trans x≡y

≡̇-setoid : ∀ {a} {A : Set a} {b} (B : A → Set b) → Setoid ((x : A) → B x) (a ⊔ b)
Setoid._≋_ (≡̇-setoid B) = _≡̇_
Setoid.≋-reflexivity (≡̇-setoid B) = ≡̇-refl _
Setoid.≋-symmetry (≡̇-setoid B) = ≡̇-sym
Setoid.≋-transitivity (≡̇-setoid B) = ≡̇-trans


text:
module Example where

open import Base
open import Nat
open import univ

-- Application

_#_ : {A : S}{F : El A -> S}{pF : Map _==_ _=S_ F} ->
      El (pi A F pF) -> (x : El A) -> El (F x)
el < f , pf > # x = f x

-- Projection

π₀ : {A : S}{F : El A -> S}{pF : Map _==_ _=S_ F} ->
     El (sigma A F pF) -> El A
π₀ (el < x , Fx >) = x

π₁ : {A : S}{F : El A -> S}{pF : Map _==_ _=S_ F} ->
     (p : El (sigma A F pF)) -> El (F (π₀ p))
π₁ (el < x , Fx >) = Fx