text:
module Structure.Operator.IntegralDomain where

open import Functional
import      Lvl
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Operator.Properties
open import Structure.Operator.Ring
open import Type

-- Rng with no non-zero zero divisors.
record Domain {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_+_  : T → T → T) (_⋅_  : T → T → T) ⦃ rng : Rng(_+_)(_⋅_) ⦄ : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  open Rng(rng)
  field
    no-zero-divisors  : ∀{x y} → (x ⋅ y ≡ 𝟎) → ((x ≡ 𝟎) ∨ (y ≡ 𝟎))

  zero-zero-divisorₗ : ∀{x} → ZeroDivisorₗ(x) → (x ≡ 𝟎)
  zero-zero-divisorₗ {x} ([∃]-intro y ⦃ [∧]-intro y𝟎 xy𝟎 ⦄) = [∨]-elim id ([⊥]-elim ∘ y𝟎) (no-zero-divisors xy𝟎)

  zero-zero-divisorᵣ : ∀{x} → ZeroDivisorᵣ(x) → (x ≡ 𝟎)
  zero-zero-divisorᵣ {x} ([∃]-intro y ⦃ [∧]-intro y𝟎 xy𝟎 ⦄) = [∨]-elim ([⊥]-elim ∘ y𝟎) id (no-zero-divisors xy𝟎)

  zero-zero-divisor : ∀{x} → ZeroDivisor(x) → (x ≡ 𝟎)
  zero-zero-divisor {x} ([∃]-intro y ⦃ [∧]-intro y𝟎 ([∧]-intro xy𝟎 yx𝟎) ⦄) = [∨]-elim id ([⊥]-elim ∘ y𝟎) (no-zero-divisors xy𝟎)

-- Non-trivial commutative ring and domain.
record IntegralDomain {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_+_  : T → T → T) (_⋅_  : T → T → T) : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  field
    ⦃ ring ⦄              : Ring(_+_)(_⋅_)
    ⦃ domain ⦄            : Domain(_+_)(_⋅_)
    ⦃ [⋅]-commutativity ⦄ : Commutativity(_⋅_)
  open Ring  (ring)   public
  open Domain(domain) public

  field
    ⦃ distinct-identities ⦄ : DistinctIdentities

record IntegralDomainObject {ℓ ℓₑ} : Stmt{Lvl.𝐒(ℓ Lvl.⊔ ℓₑ)} where
  constructor intro
  field
    {T} : Type{ℓ}
    ⦃ equiv ⦄ : Equiv{ℓₑ}(T)
    _+_ : T → T → T
    _⋅_ : T → T → T
    ⦃ integralDomain ⦄ : IntegralDomain(_+_)(_⋅_)
  open IntegralDomain(integralDomain) public

ext: agda

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, 2019-03-17, issue #3638
-- Making rewriting in interactive goals work in parametrized modules.

{-# OPTIONS --rewriting #-}

-- {-# OPTIONS -v rewriting:100 #-}
-- {-# OPTIONS -v tc.sig.param:60 #-}
-- {-# OPTIONS -v interactive.meta:10 #-}

open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-}

module _ (A : Set) where

postulate
  a b c : A
  eq  : a ≡ b
  rew : c ≡ b

{-# REWRITE rew #-}

goal : a ≡ c
goal = {! eq !}  -- C-u C-u C-c C-.

-- Displays:
-- Goal: a ≡ c
-- Have: a ≡ b

-- Expected: Rewrite rule rew should be applied.
-- Goal: a ≡ b

-- Works now.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Common.Sum where

open import Common.Level

data _⊎_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Sessions.Semantics.Runtime {E : Set} (delay : E) where

open import Prelude

open import Relation.Unary hiding (Empty; _∈_)
open import Relation.Unary.PredicateTransformer using (Pt)
open import Relation.Ternary.Separation.Construct.Market
open import Relation.Ternary.Separation.Construct.Product
open import Relation.Ternary.Separation.Morphisms
open import Relation.Ternary.Separation.Monad

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

open import Sessions.Semantics.Commands
open import Relation.Ternary.Separation.Monad
open import Relation.Ternary.Separation.Monad.Error
open import Relation.Ternary.Separation.Monad.State

open StateWithErr {C = RCtx} E
open ExceptMonad {A = RCtx} E
open Monads.Monad {{...}}

private
  module _ {C : Set} {{ r : RawSep C }} {u} {{ _ : IsUnitalSep r u }} where
    -- open Monads.Monad (err-monad {A = C}) public
    open Monads using (str) public

module _ where
  data _⇜_ : SType → SType → Pred RCtx 0ℓ where
    emp  : ∀ {α} → (α ⇜ α) ε
    cons : ∀ {a} → ∀[ Val a ✴ (β ⇜ γ) ⇒ ((a ¿ β) ⇜ γ) ]

  _⇝_ = flip _⇜_

  private
    -- It is crucial for type-safety that this is evident
    send-lemma : ∀[ ((a ! β) ⇜ γ) ⇒ Empty (γ ≡ a ! β) ]
    send-lemma emp = emp refl

  record Link (α γ : SType) Φ : Set where
    constructor link
    field
      {β₁ β₂} : SType
      duals   : β₂ ≡ β₁ ⁻¹
      buffers : (α ⇜ β₁ ✴ β₂ ⇝ γ) Φ

  revLink : ∀[ Link α γ ⇒ Link γ α ]
  revLink (link refl buffers) = link (sym dual-involutive) (✴-swap buffers)

  push : ∀[ Val a ✴ γ ⇜ (a ¿ β) ⇒ γ ⇜ β ]
  push (v ×⟨ σ₁ ⟩ emp) = cons (v ×⟨ σ₁ ⟩ emp)
  push (v ×⟨ σ₁ ⟩ cons (w ×⟨ σ₂ ⟩ b)) with ⊎-assoc σ₂ (⊎-comm σ₁)
  ... | _ , σ₃ , σ₄ with push (v ×⟨ ⊎-comm σ₄ ⟩ b)
  ... | b' = cons (w ×⟨ σ₃ ⟩ b')

  pull : ∀[ γ ⇝ (a ¿ β) ⇒ Except E (Val a ✴ γ ⇝ β) ]
  pull emp                  = error delay
  pull (cons (v ×⟨ σ ⟩ vs)) = return (v ×⟨ σ ⟩ vs)

  send-into : ∀[ Val a ✴ Link α (a ! β) ⇒ Link α β ]
  send-into (v ×⟨ σ ⟩ link {x ¿ β₁} refl (px ×⟨ σ₁ ⟩ emp)) rewrite ⊎-id⁻ʳ σ₁ =
    link refl ((push (v ×⟨ σ ⟩ px)) ×⟨ ⊎-idʳ ⟩ emp)

  recvₗ : ∀[ Link (a ¿ β) γ ⇒ Except E (Val a ✴ Link β γ) ]
  recvₗ c@(link refl (bₗ ×⟨ τ ⟩ bᵣ)) = do
    v ×⟨ σ ⟩ l ← mapM (pull bₗ &⟨ τ ⟩ bᵣ) ✴-assocᵣ
    return (v ×⟨ σ ⟩ link refl l)

  recvᵣ : ∀[ Link γ (a ¿ β) ⇒ Except E (Val a ✴ Link γ β) ]
  recvᵣ l = do
    v ×⟨ σ ⟩ l' ← recvₗ (revLink l)
    return (v ×⟨ σ ⟩ revLink l')

  data Recipient : SType → Set where
    rec : Recipient (a ¿ β)
    end : Recipient end

  data Channel : Runtype → Pred RCtx 0ℓ where
    twosided : ∀[ Link α β ⇒ Channel (chan α β) ]
    onesided : ∀[ end ⇝ β  ⇒ Channel (endp β) ]

  Channels' = Allstar Channel
  Channels = uncurry Channels'

  emptyLink : ε[ Link α (α ⁻¹) ]
  emptyLink = link refl (emp ×⟨ ⊎-∙ ⟩ emp)

  emptyChannel : ε[ Channel (chan α (α ⁻¹)) ]
  emptyChannel = twosided (link refl (emp ×⟨ ⊎-∙ ⟩ emp))

  flipChan : ∀ {τ} → ∀[ Channel τ ⇒ Channel (flipped τ) ]
  flipChan (twosided x) = twosided (revLink x)
  flipChan (onesided x) = onesided x

  {- Updating a known endpoint of a channel type -}
  _≔ₑ_ : ∀ {τ} → End α τ → SType → Runtype
  (endp β ∷ [] , divide lr []) ≔ₑ α = chan α β
  (endp β ∷ [] , divide rl []) ≔ₑ α = chan β α
  (         [] , to-left _)    ≔ₑ α = endp α

  onesided-recipient : ∀ {Φ} → (end ⇝ α) Φ → Recipient α
  onesided-recipient emp      = end
  onesided-recipient (cons x) = rec

  {- Receiving on any receiving end of a channel -}
  chan-receive : ∀ {τ} → (e : End (a ¿ α) τ) →
                 ∀[ Channel τ ⇒ Except E (Val a ✴ Channel (e ≔ₑ α)) ]

  chan-receive (._ , divide lr []) (twosided l) = do
    v ×⟨ σ ⟩ l' ← recvₗ l
    return (v ×⟨ σ ⟩ twosided l')

  chan-receive (._ , divide rl []) (twosided l) = do
    v ×⟨ σ ⟩ l' ← recvᵣ l
    return (v ×⟨ σ ⟩ twosided l')

  chan-receive (fst₁ , to-left []) (onesided b) = do
    v ×⟨ σ ⟩ b' ← pull b
    return (v ×⟨ σ ⟩ onesided b')

  {- Sending on any sending end of a channel -}
  chan-send : ∀ {τ} → (e : End (a ! α) τ) →
              ∀[ Channel τ ⇒ Val a ─✴ Channel (e ≔ₑ α) ]

  app (chan-send (_ , divide lr []) (twosided l)) v σ =
    let l' = send-into (v ×⟨ ⊎-comm σ ⟩ revLink l)
    in twosided (revLink l')

  app (chan-send (_ , divide rl []) (twosided l)) v σ =
    let l' = send-into (v ×⟨ ⊎-comm σ ⟩ l)
    in twosided l'

  -- cannot be onesided
  app (chan-send (_ , to-left []  ) (onesided b)) v σ with onesided-recipient b
  ... | ()


text:
module Issue22 where

postulate
  D   : Set
  _≡_ : D → D → Set
  d e : D

foo : ∀ x → x ≡ x
foo x = bar
  where
  postulate
    d≡e : d ≡ e

  postulate
    bar : x ≡ x
  {-# ATP prove bar d≡e #-}

-- $ apia Bug.agda
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/Apia/Utils/AgdaAPI/Interface.hs:307

-- The error occurs because the dead code analysis removes `d≡e` from
-- the the interfase file.

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module Terminal where

open import Agda.Builtin.Word
open import BasicIO
open import Data.Bool
open import Data.Char hiding (show)
open import Data.List hiding (_++_)
open import Data.String hiding (show)
open import Data.Unit
open import ByteCount
open import Int
open import Function
open import Pair
open import Show

{-# FOREIGN GHC import System.Posix.IO #-}
{-# FOREIGN GHC import System.Posix.Terminal #-}
{-# FOREIGN GHC import System.Posix.Types #-}

data TerminalState : Set where
  immediately : TerminalState
  whenDrained : TerminalState
  whenFlushed : TerminalState

{-# COMPILE GHC TerminalState =
  data TerminalState (Immediately | WhenDrained | WhenFlushed)
#-}

data TerminalMode : Set where
  interruptOnBreak : TerminalMode
  mapCRtoLF : TerminalMode
  ignoreBreak : TerminalMode
  ignoreCR : TerminalMode
  ignoreParityErrors : TerminalMode
  mapLFtoCR : TerminalMode
  checkParity : TerminalMode
  stripHighBit : TerminalMode
  startStopInput : TerminalMode
  startStopOutput : TerminalMode
  markParityErrors : TerminalMode
  processOutput : TerminalMode
  localMode : TerminalMode
  readEnable : TerminalMode
  twoStopBits : TerminalMode
  hangupOnClose : TerminalMode
  enableParity : TerminalMode
  oddParity : TerminalMode
  enableEcho : TerminalMode
  echoErase : TerminalMode
  echoKill : TerminalMode
  echoLF : TerminalMode
  processInput : TerminalMode
  extendedFunctions : TerminalMode
  keyboardInterrupts : TerminalMode
  noFlushOnInterrupt : TerminalMode
  backgroundWriteInterrupt : TerminalMode

{-# COMPILE GHC TerminalMode =
  data TerminalMode
  ( InterruptOnBreak
  | MapCRtoLF
  | IgnoreBreak
  | IgnoreCR
  | IgnoreParityErrors
  | MapLFtoCR
  | CheckParity
  | StripHighBit
  | StartStopInput
  | StartStopOutput
  | MarkParityErrors
  | ProcessOutput
  | LocalMode
  | ReadEnable
  | TwoStopBits
  | HangupOnClose
  | EnableParity
  | OddParity
  | EnableEcho
  | EchoErase
  | EchoKill
  | EchoLF
  | ProcessInput
  | ExtendedFunctions
  | KeyboardInterrupts
  | NoFlushOnInterrupt
  | BackgroundWriteInterrupt
  )
#-}

postulate
  Fd : Set
  TerminalAttributes : Set

  stdInput : Fd
  stdOutput : Fd
  getTerminalAttributes : Fd → IO TerminalAttributes
  setTerminalAttributes : Fd → TerminalAttributes → TerminalState → IO ⊤
  withoutMode : TerminalAttributes → TerminalMode → TerminalAttributes
  inputTime : TerminalAttributes → Int
  withTime : TerminalAttributes → Int → TerminalAttributes
  minInput : TerminalAttributes → Int
  withMinInput : TerminalAttributes → Int → TerminalAttributes
  fdRead : Fd → ByteCount → IO (List Char , ByteCount)
  fdWrite : Fd → List Char → IO ByteCount

{-# COMPILE GHC Fd = type Fd #-}
{-# COMPILE GHC TerminalAttributes = type TerminalAttributes #-}

{-# COMPILE GHC stdInput = stdInput #-}
{-# COMPILE GHC stdOutput = stdOutput #-}
{-# COMPILE GHC getTerminalAttributes = getTerminalAttributes #-}
{-# COMPILE GHC setTerminalAttributes = setTerminalAttributes #-}
{-# COMPILE GHC withoutMode = withoutMode #-}
{-# COMPILE GHC inputTime = inputTime #-}
{-# COMPILE GHC withTime = withTime #-}
{-# COMPILE GHC minInput = minInput #-}
{-# COMPILE GHC withMinInput = withMinInput #-}
{-# COMPILE GHC fdRead = fdRead #-}
{-# COMPILE GHC fdWrite = fdWrite #-}

clearScreen : String
clearScreen = "\^[[2J"

showCursor : String
showCursor = "\^[[?25h"

hideCursor : String
hideCursor = "\^[[?25l"

altScreenEnable : String
altScreenEnable = "\^[[?1049h"

altScreenDisable : String
altScreenDisable = "\^[[?1049l"

withUpdatedAttributes :
  {A : Set} → (TerminalAttributes → TerminalAttributes) → IO A → IO A
withUpdatedAttributes {A} updateFn actions =
  bracket (getTerminalAttributes stdOutput) setAttrs updateAndRun
    where
      setAttrs : TerminalAttributes → IO ⊤
      setAttrs attrs = setTerminalAttributes stdOutput attrs immediately

      updateAndRun : TerminalAttributes → IO A
      updateAndRun attrs = do
        _ ← setAttrs (updateFn attrs)
        actions

readMaxChars : ByteCount
readMaxChars = mkCSize (primWord64FromNat 1024)

termRead : IO String
termRead = fdRead stdInput readMaxChars >>= (return ∘ fromList ∘ fst)

termWrite : String → IO ByteCount
termWrite = fdWrite stdOutput ∘ toList

printAttrs : TerminalAttributes → IO ⊤
printAttrs attrs =
  do _ ← termWrite (formatField "inputTime" (inputTime attrs))
     _ ← termWrite (formatField "minInput" (minInput attrs))
     return tt
  where
    formatField : String → Int → String
    formatField name value = name ++ " = " ++ show value ++ "\n"

max_stars_repo_name: cruhland/agda-editor

max_issues_repo_name: cruhland/agda-editor

max_forks_repo_name: cruhland/agda-editor


text:
-- Deriving TreeEncoding. Note: only for non-dependent datatypes.

module Tactic.Deriving.TreeEncoding where

open import Prelude
open import Tactic.Reflection
open import Tactic.Deriving
open import Tactic.Reflection
open import Tactic.Reflection.Quote
open import Data.TreeRep
open import Container.Traversable

private
  mapIx : ∀ {a b} {A : Set a} {B : Set b} → (Nat → A → B) → List A → List B
  mapIx f []       = []
  mapIx f (x ∷ xs) = f 0 x ∷ mapIx (f ∘ suc) xs

  -- encode (ci x₁ .. xn) = node i (treeEncode x₁) .. (treeEncode xn)
  encodeClause : Nat → Nat → Name → TC Clause
  encodeClause np i c = do
    args ← drop np <$> argTel c
    let xs = reverse (mapIx const args)
    return (clause [ vArg (con c (map (var "x" <$_) args)) ]
                   (con₂ (quote node)
                         (lit (nat i))
                         (quoteList (map (λ i → def₁ (quote treeEncode) (var i [])) xs))))

  quoteListP : List Pattern → Pattern
  quoteListP = foldr (λ p ps → con₂ (quote List._∷_) p ps) (con₀ (quote List.[]))

  qAp : Term → Term → Term
  qAp f x = def₂ (quote _<*>′_) f x

  -- decode (node i x₁ .. xn) = ⦇ cᵢ (treeDecode x₁) .. (treeDecode xn) ⦈
  decodeClause : Nat → Nat → Name → TC Clause
  decodeClause np i c = do
    args ← drop np <$> argTel c
    let xs = reverse (mapIx const args)
    pure (clause [ vArg (con₂ (quote node) (lit (nat i)) (quoteListP (map (λ _ → var "x") args))) ]
                 (foldl qAp (con₁ (quote just) (con₀ c))
                            (map (λ i → def₁ (quote treeDecode) (var i [])) xs)))

  encodeClauses : Name → TC (List Clause)
  encodeClauses d = do
    cs ← getConstructors d
    np ← getParameters d
    traverse id (mapIx (encodeClause np) cs)

  decodeClauses : Name → TC (List Clause)
  decodeClauses d = do
    cs ← getConstructors d
    np ← getParameters d
    cs ← traverse id (mapIx (decodeClause np) cs)
    pure (cs ++ clause (vArg (var "_") ∷ []) (con₀ (quote nothing)) ∷ [])

  proofClause : Nat → Nat → Name → TC Clause
  proofClause np i c = do
    args ← drop np <$> argTel c
    let xs = reverse (mapIx const args)
    pure (clause [ vArg (con c (map (var "x" <$_) args)) ]
                 (foldl (λ eq eq₁ → def₂ (quote _=*=′_) eq eq₁)
                        (con₀ (quote refl))
                        (map (λ i → def₁ (quote isTreeEmbedding) (var i [])) xs)))

  proofClauses : Name → TC (List Clause)
  proofClauses d = do
    cs ← getConstructors d
    np ← getParameters d
    traverse id (mapIx (proofClause np) cs)

  makeProjection : Name → Clause → Clause
  makeProjection f (clause ps b)      = clause (vArg (proj f) ∷ ps) b
  makeProjection f (absurd-clause ps) = absurd-clause (vArg (proj f) ∷ ps)

  instanceClauses : Name → TC (List Clause)
  instanceClauses d = do
    enc ← encodeClauses d
    dec ← decodeClauses d
    prf ← proofClauses d
    pure (map (makeProjection (quote TreeEncoding.treeEncode)) enc ++
          map (makeProjection (quote TreeEncoding.treeDecode)) dec ++
          map (makeProjection (quote TreeEncoding.isTreeEmbedding)) prf)

deriveTreeEncoding : Name → Name → TC ⊤
deriveTreeEncoding iname dname = do
  declareDef (iArg iname) =<< instanceType dname (quote TreeEncoding)
  defineFun iname =<< instanceClauses dname

-- unquoteDecl EncodeList = deriveTreeEncoding EncodeList (quote List)

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


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

module Math.Combinatorics.IntegerFunction.Properties.Lemma where

open import Data.Integer
open import Data.Integer.Solver
open import Relation.Binary.PropositionalEquality

lemma₁ : ∀ a b c d → a * b * (c * d) ≡ (a * c) * (b * d)
lemma₁ = solve 4 (λ a b c d → a :* b :* (c :* d) := (a :* c) :* (b :* d) ) refl
  where open +-*-Solver

lemma₂ : ∀ n → n ≡ 1ℤ + (n - 1ℤ)
lemma₂ = solve 1 (λ n → n := con 1ℤ :+ (n :- con 1ℤ)) refl
  where open +-*-Solver

lemma₃ : ∀ m n → m ≡ n + (m - n)
lemma₃ = solve 2 (λ m n → m := n :+ (m :- n)) refl
  where open +-*-Solver


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

open import Cubical.Algebra.CommRing.Base public

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


text:
{-

A parameterized family of structures S can be combined into a single structure:
X ↦ (a : A) → S a X

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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.RelationalStructure
open import Cubical.Functions.FunExtEquiv
open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation
open import Cubical.HITs.SetQuotients

open import Cubical.Structures.Parameterized

private
  variable
    ℓ ℓ₀ ℓ₁ ℓ₁' ℓ₁'' : Level

-- Structured relations

module _ (A : Type ℓ₀) where

  ParamRelStr : {S : A → Type ℓ → Type ℓ₁}
    → (∀ a → StrRel (S a) ℓ₁')
    → StrRel (ParamStructure A S) (ℓ-max ℓ₀ ℓ₁')
  ParamRelStr ρ R s t =
    (a : A) → ρ a R (s a) (t a)

  paramSuitableRel : {S : A → Type ℓ → Type ℓ₁} {ρ : ∀ a → StrRel (S a) ℓ₁'}
    → (∀ a → SuitableStrRel (S a) (ρ a))
    → SuitableStrRel (ParamStructure A S) (ParamRelStr ρ)
  paramSuitableRel {ρ = ρ} θ .quo (X , f) R r .fst .fst a =
    θ a .quo (X , f a) R (r a) .fst .fst
  paramSuitableRel {ρ = ρ} θ .quo (X , f) R r .fst .snd a =
    θ a .quo (X , f a) R (r a) .fst .snd
  paramSuitableRel {ρ = ρ} θ .quo (X , f) R r .snd (q , c) i .fst a =
    θ a .quo (X , f a) R (r a) .snd (q a , c a) i .fst
  paramSuitableRel {ρ = ρ} θ .quo (X , f) R r .snd (q , c) i .snd a =
    θ a .quo (X , f a) R (r a) .snd (q a , c a) i .snd
  paramSuitableRel {ρ = ρ} θ .symmetric R r a =
    θ a .symmetric R (r a)
  paramSuitableRel {ρ = ρ} θ .transitive R R' r r' a =
    θ a .transitive R R' (r a) (r' a)
  paramSuitableRel {ρ = ρ} θ .set setX =
    isSetΠ λ a → θ a .set setX
  paramSuitableRel {ρ = ρ} θ .prop propR s t =
    isPropΠ λ a → θ a .prop propR (s a) (t a)

  paramRelMatchesEquiv : {S : A → Type ℓ → Type ℓ₁}
    (ρ : ∀ a → StrRel (S a) ℓ₁') {ι : ∀ a → StrEquiv (S a) ℓ₁''}
    → (∀ a → StrRelMatchesEquiv (ρ a) (ι a))
    → StrRelMatchesEquiv (ParamRelStr ρ) (ParamEquivStr A ι)
  paramRelMatchesEquiv ρ μ _ _ e = equivΠCod λ a → μ a _ _ e

  paramRelAction : {S : A → Type ℓ → Type ℓ₁} {ρ : ∀ a → StrRel (S a) ℓ₁'}
    → (∀ a → StrRelAction (ρ a))
    → StrRelAction (ParamRelStr ρ)
  paramRelAction α .actStr f s a = α a .actStr f (s a)
  paramRelAction α .actStrId s = funExt λ a → α a .actStrId (s a)
  paramRelAction α .actRel h _ _ r a = α a .actRel h _ _ (r a)

  -- Detransitivity of ParamRelStr would depend on choice in general, so
  -- we don't get positivity

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some code related to the W type that relies on the K rule
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.W.WithK where

open import Data.Product
open import Data.Container.Core
open import Data.W
open import Agda.Builtin.Equality

module _ {s p} {C : Container s p}
         {s : Shape C} {f : Position C s → W C} where

 sup-injective₂ : ∀ {g} → sup (s , f) ≡ sup (s , g) → f ≡ g
 sup-injective₂ refl = refl


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

module Cubical.Data.Strict2Group.Explicit where

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import Util.PKCS
open import Util.Prelude
import      Yasm.Base   as YB
import      Yasm.System as YS

-- This module provides a single import for all Yasm modules

module Yasm.Yasm
   (ℓ-PeerState : Level)
   (ℓ-VSFP      : Level)
   (parms       : YB.SystemTypeParameters ℓ-PeerState)
   (iiah        : YB.SystemInitAndHandlers ℓ-PeerState parms)
   (ValidSenderForPK        : YS.WithInitAndHandlers.ValidSenderForPK-type        ℓ-PeerState ℓ-VSFP parms iiah)
   (ValidSenderForPK-stable : YS.WithInitAndHandlers.ValidSenderForPK-stable-type ℓ-PeerState ℓ-VSFP parms iiah ValidSenderForPK)
  where
 open YB.SystemTypeParameters  parms
 open YB.SystemInitAndHandlers iiah
 open import Yasm.Base                                                                              public
 open import Yasm.Types                                                                             public
 open import Yasm.System     ℓ-PeerState ℓ-VSFP parms                                               public
 open import Yasm.Properties ℓ-PeerState ℓ-VSFP parms iiah ValidSenderForPK ValidSenderForPK-stable public
 open        WithInitAndHandlers iiah                                                                        public
 open import Util.FunctionOverride    PeerId _≟PeerId_                                                       public


text:
-- There was a bug where Confuse and confusing were considered
-- projection-like even though they have absurd clauses.
module _ (A : Set) where

data D : Set where
  d : D

data P : D → Set where

Confuse : (d : D) (p : P d) → Set
Confuse x ()

confusing : (d : D) (p : P d) → Confuse d p
confusing x ()

test : (x : P d) → Set
test x with confusing d x
test x | e = A


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Unit

module Oscar.Class.Leftunit where

module Leftunit
  {𝔞 𝔟} {𝔄 : Ø 𝔞} {𝔅 : Ø 𝔟}
  {𝔢} {𝔈 : Ø 𝔢}
  {𝔞𝔟}
  (_↤_ : 𝔅 → 𝔄 → Ø 𝔞𝔟) (let _↤_ = _↤_; infix 4 _↤_)
  (ε : 𝔈)
  (_◃_ : 𝔈 → 𝔄 → 𝔅) (let _◃_ = _◃_; infix 16 _◃_)
  (x : 𝔄)
  = ℭLASS (ε , _◃_ , _↤_) (ε ◃ x ↤ x)

module _
  {𝔞} {𝔄 : Ø 𝔞} {𝔢} {𝔈 : Ø 𝔢} {ℓ}
  {_↦_ : 𝔄 → 𝔄 → Ø ℓ}
  {ε : 𝔈}
  {_◃_ : 𝔈 → 𝔄 → 𝔄}
  {x : 𝔄}
  where
  leftunit = Leftunit.method _↦_ ε _◃_ x

open import Oscar.Class.Reflexivity
open import Oscar.Class.Surjection
open import Oscar.Class.Smap

module Leftunit,smaparrow
  {𝔵₁ 𝔵₂ 𝔭₁ 𝔭₂ 𝔯 𝔭̇₁₂} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  (ℜ : π̂² 𝔯 𝔛₁)
  (𝔓₁ : π̂ 𝔭₁ 𝔛₂)
  (𝔓₂ : π̂ 𝔭₂ 𝔛₂)
  (ε : Reflexivity.type ℜ)
  (surjection : Surjection.type 𝔛₁ 𝔛₂)
  (smaparrow : Smaparrow.type ℜ 𝔓₁ 𝔓₂ surjection surjection)
  (𝔓̇₁₂ : ∀ {x} → 𝔓₁ (surjection x) → 𝔓₂ (surjection x) → Ø 𝔭̇₁₂)
  where
  class = ∀ {x} {p : 𝔓₁ (surjection x)} → Leftunit.class (flip 𝔓̇₁₂) ε smaparrow p
  type = ∀ {x} {p : 𝔓₁ (surjection x)} → Leftunit.type (flip 𝔓̇₁₂) ε smaparrow p
  method : ⦃ _ : class ⦄ → type
  method {x} {p} = Leftunit.method (flip 𝔓̇₁₂) ε smaparrow p

module Leftunit,smaparrow!
  {𝔵₁ 𝔵₂ 𝔭₁ 𝔭₂ 𝔯 𝔭̇₁₂} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  (ℜ : π̂² 𝔯 𝔛₁)
  (𝔓₁ : π̂ 𝔭₁ 𝔛₂)
  (𝔓₂ : π̂ 𝔭₂ 𝔛₂)
  ⦃ _ : Reflexivity.class ℜ ⦄
  ⦃ _ : Surjection.class 𝔛₁ 𝔛₂ ⦄
  ⦃ _ : Smaparrow!.class ℜ 𝔓₁ 𝔓₂ ⦄
  (𝔓̇₁₂ : ∀ {x} → 𝔓₁ (surjection x) → 𝔓₂ (surjection x) → Ø 𝔭̇₁₂)
  = Leftunit,smaparrow ℜ 𝔓₁ 𝔓₂ ε surjection smaparrow 𝔓̇₁₂

module Leftunit,smaphomarrow
  {𝔵₁ 𝔵₂ 𝔭 𝔯 𝔭̇} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  (ℜ : π̂² 𝔯 𝔛₁)
  (𝔓 : π̂ 𝔭 𝔛₂)
  (ε : Reflexivity.type ℜ)
  (surjection : Surjection.type 𝔛₁ 𝔛₂)
  (smaparrow : Smaphomarrow.type ℜ 𝔓 surjection)
  (𝔓̇ : ∀ {x} → 𝔓 (surjection x) → 𝔓 (surjection x) → Ø 𝔭̇)
  = Leftunit,smaparrow ℜ 𝔓 𝔓 ε surjection smaparrow 𝔓̇

module Leftunit,smaphomarrow!
  {𝔵₁ 𝔵₂ 𝔭 𝔯 𝔭̇} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  (ℜ : π̂² 𝔯 𝔛₁)
  (𝔓 : π̂ 𝔭 𝔛₂)
  ⦃ _ : Reflexivity.class ℜ ⦄
  ⦃ _ : Surjection.class 𝔛₁ 𝔛₂ ⦄
  ⦃ _ : Smaphomarrow!.class ℜ 𝔓 ⦄
  (𝔓̇ : ∀ {x} → 𝔓 (surjection x) → 𝔓 (surjection x) → Ø 𝔭̇)
  = Leftunit,smaphomarrow ℜ 𝔓 ε surjection smaparrow 𝔓̇

open import Oscar.Class.HasEquivalence

module Leftunit,equivalence,smaphomarrow!
  {𝔵₁ 𝔵₂ 𝔭 𝔯 𝔭̇} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  (ℜ : π̂² 𝔯 𝔛₁)
  (𝔓 : π̂ 𝔭 𝔛₂)
  ⦃ _ : Reflexivity.class ℜ ⦄
  ⦃ _ : Surjection.class 𝔛₁ 𝔛₂ ⦄
  ⦃ _ : Smaphomarrow!.class ℜ 𝔓 ⦄
  ⦃ _ : ∀ {x} → HasEquivalence (𝔓 x) 𝔭̇ ⦄
  = Leftunit,smaphomarrow! ℜ 𝔓 _≈_


text:
-- There was a problem with module instantiation if a definition
-- was in scope under more than one name. For instance, constructors
-- or non-private local modules being open publicly. In this case
-- the module instantiation incorrectly generated two separate names
-- for this definition.
module Issue263 where

module M where
  data D : Set where
    d : D
  -- 'M.D.d' is in scope both as 'd' and 'D.d'

  module E where
    postulate X : Set

  open E public
  -- 'M.E.X' is in scope as 'X' and 'E.X'

module M′ = M

bar = M′.E.X  -- this panicked
foo = M′.D.d  -- and this as well


text:
-- Basic intuitionistic propositional calculus, without ∨ or ⊥.
-- Kripke-style semantics with contexts as concrete worlds, and glueing for α and ▻.
-- Implicit syntax.

module BasicIPC.Semantics.KripkeConcreteGluedImplicit where

open import BasicIPC.Syntax.Common public
open import Common.Semantics public

open ConcreteWorlds (Ty) public

-- Partial intuitionistic Kripke models.

record Model : Set₁ where
  infix 3 _⊩ᵅ_
  field
    -- Forcing for atomic propositions; monotonic.
    _⊩ᵅ_   : World → Atom → Set
    mono⊩ᵅ : ∀ {P w w′} → w ≤ w′ → w ⊩ᵅ P → w′ ⊩ᵅ P

open Model {{…}} public

module ImplicitSyntax
    (_[⊢]_   : Cx Ty → Ty → Set)
    (mono[⊢] : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ [⊢] A → Γ′ [⊢] A)
  where

  -- Forcing in a particular world of a particular model.

  module _ {{_ : Model}} where
    infix 3 _⊩_
    _⊩_ : World → Ty → Set
    w ⊩ α P   = Glue (unwrap w [⊢] (α P)) (w ⊩ᵅ P)
    w ⊩ A ▻ B = Glue (unwrap w [⊢] (A ▻ B)) (∀ {w′} → w ≤ w′ → w′ ⊩ A → w′ ⊩ B)
    w ⊩ A ∧ B = w ⊩ A × w ⊩ B
    w ⊩ ⊤    = 𝟙

    infix 3 _⊩⋆_
    _⊩⋆_ : World → Cx Ty → Set
    w ⊩⋆ ∅     = 𝟙
    w ⊩⋆ Ξ , A = w ⊩⋆ Ξ × w ⊩ A

  -- Monotonicity with respect to context inclusion.

  module _ {{_ : Model}} where
    mono⊩ : ∀ {A w w′} → w ≤ w′ → w ⊩ A → w′ ⊩ A
    mono⊩ {α P}   ξ s = mono[⊢] (unwrap≤ ξ) (syn s) ⅋ mono⊩ᵅ ξ (sem s)
    mono⊩ {A ▻ B} ξ s = mono[⊢] (unwrap≤ ξ) (syn s) ⅋ λ ξ′ → sem s (trans≤ ξ ξ′)
    mono⊩ {A ∧ B} ξ s = mono⊩ {A} ξ (π₁ s) , mono⊩ {B} ξ (π₂ s)
    mono⊩ {⊤}    ξ s = ∙

    mono⊩⋆ : ∀ {Ξ w w′} → w ≤ w′ → w ⊩⋆ Ξ → w′ ⊩⋆ Ξ
    mono⊩⋆ {∅}     ξ ∙        = ∙
    mono⊩⋆ {Ξ , A} ξ (ts , t) = mono⊩⋆ {Ξ} ξ ts , mono⊩ {A} ξ t

  -- Additional useful equipment.

  module _ {{_ : Model}} where
    _⟪$⟫_ : ∀ {A B w} → w ⊩ A ▻ B → w ⊩ A → w ⊩ B
    s ⟪$⟫ a = sem s refl≤ a

    ⟪S⟫ : ∀ {A B C w} → w ⊩ A ▻ B ▻ C → w ⊩ A ▻ B → w ⊩ A → w ⊩ C
    ⟪S⟫ s₁ s₂ a = (s₁ ⟪$⟫ a) ⟪$⟫ (s₂ ⟪$⟫ a)

  -- Forcing in a particular world of a particular model, for sequents.

  module _ {{_ : Model}} where
    infix 3 _⊩_⇒_
    _⊩_⇒_ : World → Cx Ty → Ty → Set
    w ⊩ Γ ⇒ A = w ⊩⋆ Γ → w ⊩ A

    infix 3 _⊩_⇒⋆_
    _⊩_⇒⋆_ : World → Cx Ty → Cx Ty → Set
    w ⊩ Γ ⇒⋆ Ξ = w ⊩⋆ Γ → w ⊩⋆ Ξ

  -- Entailment, or forcing in all worlds of all models, for sequents.

  infix 3 _⊨_
  _⊨_ : Cx Ty → Ty → Set₁
  Γ ⊨ A = ∀ {{_ : Model}} {w : World} → w ⊩ Γ ⇒ A

  infix 3 _⊨⋆_
  _⊨⋆_ : Cx Ty → Cx Ty → Set₁
  Γ ⊨⋆ Ξ = ∀ {{_ : Model}} {w : World} → w ⊩ Γ ⇒⋆ Ξ

  -- Additional useful equipment, for sequents.

  module _ {{_ : Model}} where
    lookup : ∀ {A Γ w} → A ∈ Γ → w ⊩ Γ ⇒ A
    lookup top     (γ , a) = a
    lookup (pop i) (γ , b) = lookup i γ

    _⟦$⟧_ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A ▻ B → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ B
    (s₁ ⟦$⟧ s₂) γ = s₁ γ ⟪$⟫ s₂ γ

    ⟦S⟧ : ∀ {A B C Γ w} → w ⊩ Γ ⇒ A ▻ B ▻ C → w ⊩ Γ ⇒ A ▻ B → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ C
    ⟦S⟧ s₁ s₂ a γ = ⟪S⟫ (s₁ γ) (s₂ γ) (a γ)

    _⟦,⟧_ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ B → w ⊩ Γ ⇒ A ∧ B
    (a ⟦,⟧ b) γ = a γ , b γ

    ⟦π₁⟧ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A ∧ B → w ⊩ Γ ⇒ A
    ⟦π₁⟧ s γ = π₁ (s γ)

    ⟦π₂⟧ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A ∧ B → w ⊩ Γ ⇒ B
    ⟦π₂⟧ s γ = π₂ (s γ)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


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

open import lib.Basics
open import lib.types.Group
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Truncation
open import lib.groups.GroupProduct
open import lib.groups.Homomorphisms

module lib.groups.TruncationGroup where

module _ {i} {El : Type i} (GS : GroupStructure El) where

  Trunc-group-struct : GroupStructure (Trunc 0 El)
  Trunc-group-struct = record {
    ident = [ ident GS ];
    inv = Trunc-fmap (inv GS);
    comp = _⊗_;
    unitl = t-unitl;
    unitr = t-unitr;
    assoc = t-assoc;
    invl = t-invl;
    invr = t-invr}
    where
    open GroupStructure
    infix 80 _⊗_
    _⊗_ = Trunc-fmap2 (comp GS)

    abstract
      t-unitl : (t : Trunc 0 El) → [ ident GS ] ⊗ t == t
      t-unitl = Trunc-elim (λ _ → =-preserves-level _ Trunc-level)
        (ap [_] ∘ unitl GS)

      t-unitr : (t : Trunc 0 El) → t ⊗ [ ident GS ] == t
      t-unitr = Trunc-elim (λ _ → =-preserves-level _ Trunc-level)
        (ap [_] ∘ unitr GS)

      t-assoc : (t₁ t₂ t₃ : Trunc 0 El) → (t₁ ⊗ t₂) ⊗ t₃ == t₁ ⊗ (t₂ ⊗ t₃)
      t-assoc = Trunc-elim
        (λ _ → Π-level (λ _ → Π-level (λ _ → =-preserves-level _ Trunc-level)))
        (λ a → Trunc-elim
          (λ _ → Π-level (λ _ → =-preserves-level _ Trunc-level))
          (λ b → Trunc-elim
             (λ _ → =-preserves-level _ Trunc-level)
             (λ c → ap [_] (assoc GS a b c))))

      t-invl : (t : Trunc 0 El) → Trunc-fmap (inv GS) t ⊗ t == [ ident GS ]
      t-invl = Trunc-elim (λ _ → =-preserves-level _ Trunc-level)
        (ap [_] ∘ invl GS)

      t-invr : (t : Trunc 0 El) → t ⊗ Trunc-fmap (inv GS) t == [ ident GS ]
      t-invr = Trunc-elim (λ _ → =-preserves-level _ Trunc-level)
        (ap [_] ∘ invr GS)

  Trunc-group : Group i
  Trunc-group = record {
    El = Trunc 0 El;
    El-level = Trunc-level;
    group-struct = Trunc-group-struct }

Trunc-group-× : ∀ {i j} {A : Type i} {B : Type j}
  (GS : GroupStructure A) (HS : GroupStructure B)
  → Trunc-group (×-group-struct GS HS) == Trunc-group GS ×ᴳ Trunc-group HS
Trunc-group-× GS HS = group-ua
  (record {
    f = Trunc-rec (×-level Trunc-level Trunc-level)
          (λ {(a , b) → ([ a ] , [ b ])});
    pres-comp =
      Trunc-elim
        (λ _ → (Π-level (λ _ → =-preserves-level _
                                 (×-level Trunc-level Trunc-level))))
        (λ a → Trunc-elim
          (λ _ → =-preserves-level _ (×-level Trunc-level Trunc-level))
          (λ b → idp))} ,
   is-eq _
    (uncurry (Trunc-rec (→-level Trunc-level)
               (λ a → Trunc-rec Trunc-level (λ b → [ a , b ]))))
    (uncurry (Trunc-elim
               (λ _ → Π-level (λ _ → =-preserves-level _
                                       (×-level Trunc-level Trunc-level)))
               (λ a → Trunc-elim
                        (λ _ → =-preserves-level _
                                 (×-level Trunc-level Trunc-level))
                        (λ b → idp))))
    (Trunc-elim (λ _ → =-preserves-level _ Trunc-level) (λ _ → idp)))

Trunc-group-hom : ∀ {i j} {A : Type i} {B : Type j}
  {GS : GroupStructure A} {HS : GroupStructure B} (f : A → B)
  → ((a₁ a₂ : A) → f (GroupStructure.comp GS a₁ a₂)
                   == GroupStructure.comp HS (f a₁) (f a₂))
  → (Trunc-group GS →ᴳ Trunc-group HS)
Trunc-group-hom {A = A} {GS = GS} {HS = HS} f p =
  record {f = Trunc-fmap f; pres-comp = pres-comp}
  where
  abstract
    pres-comp : (t₁ t₂ : Trunc 0 A) →
      Trunc-fmap f (Trunc-fmap2 (GroupStructure.comp GS) t₁ t₂)
      == Trunc-fmap2 (GroupStructure.comp HS)
           (Trunc-fmap f t₁) (Trunc-fmap f t₂)
    pres-comp =
      Trunc-elim (λ _ → Π-level (λ _ → =-preserves-level _ Trunc-level))
        (λ a₁ → Trunc-elim (λ _ → =-preserves-level _ Trunc-level)
          (λ a₂ → ap [_] (p a₁ a₂)))

Trunc-group-iso : ∀ {i} {A B : Type i}
  {GS : GroupStructure A} {HS : GroupStructure B} (f : A → B)
  → ((a₁ a₂ : A) → f (GroupStructure.comp GS a₁ a₂)
                   == GroupStructure.comp HS (f a₁) (f a₂))
  → is-equiv f → Trunc-group GS ≃ᴳ Trunc-group HS
Trunc-group-iso f pres-comp ie =
  (Trunc-group-hom f pres-comp ,
   is-eq _ (Trunc-fmap (is-equiv.g ie))
     (Trunc-elim (λ _ → =-preserves-level _ Trunc-level)
       (λ b → ap [_] (is-equiv.f-g ie b)))
     (Trunc-elim (λ _ → =-preserves-level _ Trunc-level)
       (λ a → ap [_] (is-equiv.g-f ie a))))

Trunc-group-abelian : ∀ {i} {A : Type i} (GS : GroupStructure A)
  → ((a₁ a₂ : A) → GroupStructure.comp GS a₁ a₂ == GroupStructure.comp GS a₂ a₁)
  → is-abelian (Trunc-group GS)
Trunc-group-abelian GS ab =
  Trunc-elim (λ _ → Π-level (λ _ → =-preserves-level _ Trunc-level)) $
    λ a₁ → Trunc-elim (λ _ → =-preserves-level _ Trunc-level) $
      λ a₂ → ap [_] (ab a₁ a₂)

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use the
-- Relation.Binary.Reasoning.MultiSetoid module directly.
------------------------------------------------------------------------

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

module Relation.Binary.SetoidReasoning where

open import Relation.Binary.Reasoning.MultiSetoid public


text:
module Prelude.Bool where

data Bool : Set where
  true  : Bool
  false : Bool

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  true  #-}
{-# BUILTIN FALSE false #-}

not : Bool -> Bool
not true  = false
not false = true

notnot : Bool -> Bool
notnot true  = not (not true)
notnot false = not (not false)

infix 90 if_then_else_
infix 90 if'_then_else_

if_then_else_ : ∀{ P : Bool -> Set} -> (b : Bool) -> P true -> P false -> P b
if true  then a else b = a
if false then a else b = b

if'_then_else_ : ∀{ P : Set} -> (b : Bool) -> P -> P  -> P
if' true  then a else b = a
if' false then a else b = b


text:
------------------------------------------------------------------------
-- Many properties which hold for _∼_ also hold for _∼_ on₁ f
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.On {A B : Set} (f : B → A) where

open import Data.Function
open import Data.Product

implies : ∀ ≈ ∼ → ≈ ⇒ ∼ → (≈ on₁ f) ⇒ (∼ on₁ f)
implies _ _ impl = impl

reflexive : ∀ ∼ → Reflexive ∼ → Reflexive (∼ on₁ f)
reflexive _ refl = refl

irreflexive : ∀ ≈ ∼ → Irreflexive ≈ ∼ → Irreflexive (≈ on₁ f) (∼ on₁ f)
irreflexive _ _ irrefl = irrefl

symmetric : ∀ ∼ → Symmetric ∼ → Symmetric (∼ on₁ f)
symmetric _ sym = sym

transitive : ∀ ∼ → Transitive ∼ → Transitive (∼ on₁ f)
transitive _ trans = trans

antisymmetric : ∀ ≈ ≤ →
                Antisymmetric ≈ ≤ → Antisymmetric (≈ on₁ f) (≤ on₁ f)
antisymmetric _ _ antisym = antisym

asymmetric : ∀ < → Asymmetric < → Asymmetric (< on₁ f)
asymmetric _ asym = asym

respects : ∀ ∼ P → P Respects ∼ → (P ∘₀ f) Respects (∼ on₁ f)
respects _ _ resp = resp

respects₂ : ∀ ∼₁ ∼₂ → ∼₁ Respects₂ ∼₂ → (∼₁ on₁ f) Respects₂ (∼₂ on₁ f)
respects₂ _ _ (resp₁ , resp₂) =
  ((λ {_} {_} {_} → resp₁) , λ {_} {_} {_} → resp₂)

decidable : ∀ ∼ → Decidable ∼ → Decidable (∼ on₁ f)
decidable _ dec = λ x y → dec (f x) (f y)

total : ∀ ∼ → Total ∼ → Total (∼ on₁ f)
total _ tot = λ x y → tot (f x) (f y)

trichotomous : ∀ ≈ < →
               Trichotomous ≈ < → Trichotomous (≈ on₁ f) (< on₁ f)
trichotomous _ _ compare = λ x y → compare (f x) (f y)

isEquivalence : ∀ {≈} → IsEquivalence ≈ → IsEquivalence (≈ on₁ f)
isEquivalence {≈} eq = record
  { refl  = reflexive  ≈ Eq.refl
  ; sym   = symmetric  ≈ Eq.sym
  ; trans = transitive ≈ Eq.trans
  }
  where module Eq = IsEquivalence eq

isPreorder : ∀ {≈ ∼} → IsPreorder ≈ ∼ → IsPreorder (≈ on₁ f) (∼ on₁ f)
isPreorder {≈} {∼} pre = record
  { isEquivalence = isEquivalence Pre.isEquivalence
  ; reflexive     = implies ≈ ∼ Pre.reflexive
  ; trans         = transitive ∼ Pre.trans
  ; ∼-resp-≈      = respects₂ ∼ ≈ Pre.∼-resp-≈
  }
  where module Pre = IsPreorder pre

isDecEquivalence : ∀ {≈} →
                   IsDecEquivalence ≈ → IsDecEquivalence (≈ on₁ f)
isDecEquivalence {≈} dec = record
  { isEquivalence = isEquivalence Dec.isEquivalence
  ; _≟_           = decidable ≈ Dec._≟_
  }
  where module Dec = IsDecEquivalence dec

isPartialOrder : ∀ {≈ ≤} →
                 IsPartialOrder ≈ ≤ →
                 IsPartialOrder (≈ on₁ f) (≤ on₁ f)
isPartialOrder {≈} {≤} po = record
  { isPreorder = isPreorder Po.isPreorder
  ; antisym    = antisymmetric ≈ ≤ Po.antisym
  }
  where module Po = IsPartialOrder po

isStrictPartialOrder : ∀ {≈ <} →
                       IsStrictPartialOrder ≈ < →
                       IsStrictPartialOrder (≈ on₁ f) (< on₁ f)
isStrictPartialOrder {≈} {<} spo = record
  { isEquivalence = isEquivalence Spo.isEquivalence
  ; irrefl        = irreflexive ≈ < Spo.irrefl
  ; trans         = transitive < Spo.trans
  ; <-resp-≈      = respects₂ < ≈ Spo.<-resp-≈
  }
  where module Spo = IsStrictPartialOrder spo

isTotalOrder : ∀ {≈ ≤} →
               IsTotalOrder ≈ ≤ →
               IsTotalOrder (≈ on₁ f) (≤ on₁ f)
isTotalOrder {≈} {≤} to = record
  { isPartialOrder = isPartialOrder To.isPartialOrder
  ; total          = total ≤ To.total
  }
  where module To = IsTotalOrder to

isDecTotalOrder : ∀ {≈ ≤} →
                  IsDecTotalOrder ≈ ≤ →
                  IsDecTotalOrder (≈ on₁ f) (≤ on₁ f)
isDecTotalOrder {≈} {≤} dec = record
  { isTotalOrder = isTotalOrder Dec.isTotalOrder
  ; _≟_          = decidable ≈ Dec._≟_
  ; _≤?_         = decidable ≤ Dec._≤?_
  }
  where module Dec = IsDecTotalOrder dec

isStrictTotalOrder : ∀ {≈ <} →
                     IsStrictTotalOrder ≈ < →
                       IsStrictTotalOrder (≈ on₁ f) (< on₁ f)
isStrictTotalOrder {≈} {<} sto = record
  { isEquivalence = isEquivalence Sto.isEquivalence
  ; trans         = transitive < Sto.trans
  ; compare       = trichotomous ≈ < Sto.compare
  ; <-resp-≈      = respects₂ < ≈ Sto.<-resp-≈
  }
  where module Sto = IsStrictTotalOrder sto

max_issues_repo_name: larrytheliquid/Lemmachine


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

open import Agda.Primitive.Cubical
open import Agda.Builtin.Bool

-- With --omega-in-omega we are allowed to split on Setω datatypes.
-- Andrea 22/05/2020: in the future we might be allowed even without --omega-in-omega.

-- This test makes sure the interval I is still special cased and splitting is forbidden.

bad : I → Bool
bad i0 = true
bad i1 = false


text:
{-# OPTIONS --without-K  #-}
module sets.fin.properties where

open import sum
open import decidable
open import equality
open import function.core
open import function.extensionality
open import function.isomorphism
open import function.overloading
open import sets.core
open import sets.nat.core
  hiding (_≟_; pred)
open import sets.nat.ordering
open import sets.fin.core
open import sets.empty
open import sets.properties
open import hott.level.core
open import hott.level.closure
open import hott.level.sets

pred : ∀ {n}(i : Fin (suc n))
     → ¬ (i ≡ zero) → Fin n
pred zero u = ⊥-elim (u refl)
pred (suc j) _ = j

pred-β : ∀ {n}(i : Fin (suc n))
       → (u : ¬ (i ≡ zero))
       → suc (pred i u) ≡ i
pred-β zero u = ⊥-elim (u refl)
pred-β (suc i) u = refl

pred-inj : ∀ {n}{i j : Fin (suc n)}
         → (u : ¬ (i ≡ zero))
         → (v : ¬ (j ≡ zero))
         → pred i u ≡ pred j v
         → i ≡ j
pred-inj {n} {zero} u v p = ⊥-elim (u refl)
pred-inj {n} {suc i} {zero} u v p = ⊥-elim (v refl)
pred-inj {n} {suc i} {suc j} u v p = ap suc p

toℕ : ∀ {n} → Fin n → ℕ
toℕ zero = 0
toℕ (suc i) = suc (toℕ i)

toℕ-sound : ∀ {n}(i : Fin n) → suc (toℕ i) ≤ n
toℕ-sound {zero} ()
toℕ-sound {suc n} zero = s≤s z≤n
toℕ-sound {suc n} (suc i) = s≤s (toℕ-sound i)

fromℕ : ∀ {n i} → (suc i ≤ n) → Fin n
fromℕ {zero} ()
fromℕ {suc n} {0} _ = zero
fromℕ {suc n} {suc i} (s≤s p) = suc (fromℕ p)

toℕ-iso : ∀ {n} → Fin n ≅ (Σ ℕ λ i → suc i ≤ n)
toℕ-iso {n} = record
  { to = λ i → toℕ i , toℕ-sound i
  ; from = λ { (_ , p) → fromℕ p }
  ; iso₁ = α
  ; iso₂ = λ { (i , p) → unapΣ (β i p , h1⇒prop ≤-level _ _) } }
  where
    α : ∀ {n} (i : Fin n) → fromℕ (toℕ-sound i) ≡ i
    α zero = refl
    α (suc i) = ap suc (α i)

    β : ∀ {n} (i : ℕ)(p : suc i ≤ n) → toℕ (fromℕ p) ≡ i
    β {0} _ ()
    β {suc n} 0 _ = refl
    β {suc n} (suc i) (s≤s p) = ap suc (β i p)

toℕ-inj : ∀ {n} → injective (toℕ {n = n})
toℕ-inj p = iso⇒inj toℕ-iso (unapΣ (p , h1⇒prop ≤-level _ _))

#_ : ∀ {n} i {p : True (suc i ≤? n)} → Fin n
#_ {n} i {p} = fromℕ (witness p)

transpose : ∀ {n} → Fin n → Fin n → Fin n → Fin n
transpose i j k with i ≟ k
... | yes _ = j
... | no _ with j ≟ k
... | yes _ = i
... | no _ = k

transpose-β₂ : ∀ {n}(i j : Fin n)
             → transpose i j j ≡ i
transpose-β₂ i j with i ≟ j
... | yes p = sym p
... | no u with j ≟ j
... | yes p = refl
... | no v = ⊥-elim (v refl)

abstract
  transpose-invol : ∀ {n}(i j k : Fin n)
                  → transpose i j (transpose i j k) ≡ k
  transpose-invol i j k with i ≟ k
  transpose-invol i j k | yes p with i ≟ j
  transpose-invol i j k | yes p | yes p' = sym p' · p
  transpose-invol i j k | yes p | no u with j ≟ j
  transpose-invol i j k | yes p | no u | yes p' = p
  transpose-invol i j k | yes p | no u | no v = ⊥-elim (v refl)
  transpose-invol i j k | no u with j ≟ k
  transpose-invol i j k | no u | yes p with i ≟ i
  transpose-invol i j k | no u | yes p | yes p' = p
  transpose-invol i j k | no u | yes p | no v = ⊥-elim (v refl)
  transpose-invol i j k | no u | no v with i ≟ k
  transpose-invol i j k | no u | no v | yes p = ⊥-elim (u p)
  transpose-invol i j k | no u | no v | no w with j ≟ k
  transpose-invol i j k | no u | no v | no w | yes p = ⊥-elim (v p)
  transpose-invol i j k | no u | no v | no w | no z = refl

transpose-iso : ∀ {n}(i j : Fin n) → Fin n ≅ Fin n
transpose-iso i j = record
  { to = transpose i j
  ; from = transpose i j
  ; iso₁ = transpose-invol i j
  ; iso₂ = transpose-invol i j }

fin-remove₀-iso : ∀ {n} → (Fin (suc n) minus zero) ≅ Fin n
fin-remove₀-iso = record
  { to = uncurry pred
  ; from = λ i → suc i , λ p → fin-disj _ (sym p)
  ; iso₁ = λ { (i , u) → unapΣ (pred-β _ u , h1⇒prop ¬-h1 _ _) }
  ; iso₂ = λ _ → refl }

fin-remove-iso : ∀ {n}(i : Fin (suc n))
               → (Σ (Fin (suc n)) λ j → ¬ (j ≡ i))
               ≅ Fin n
fin-remove-iso {n} i = begin
    (Σ (Fin (suc n)) λ j → ¬ (j ≡ i))
  ≅⟨ ( Σ-ap-iso (transpose-iso zero i) λ _
     → Π-ap-iso lem λ _ → refl≅ ) ⟩
    (Σ (Fin (suc n)) λ j → ¬ (j ≡ zero))
  ≅⟨ fin-remove₀-iso ⟩
    Fin n
  ∎
  where
    open ≅-Reasoning

    lem : ∀ {x} → (x ≡ i) ≅ (transpose zero i x ≡ zero)
    lem {x} = begin
        (x ≡ i)
      ≅⟨ iso≡ (transpose-iso zero i) ⟩
        ( transpose zero i x ≡ transpose zero i i )
      ≅⟨ trans≡-iso' (transpose-β₂ zero i) ⟩
        ( transpose zero i x ≡ zero )
      ∎ where open ≅-Reasoning

transpose-inj : ∀ {n m}(i j : Fin m)
              → (f : Fin n → Fin m)
              → injective f
              → injective (transpose i j ∘' f)
transpose-inj i j f inj = inj ∘' iso⇒inj (transpose-iso i j)

transpose-inj-iso' : ∀ {n} (i j : Fin n)
                   → (Fin n ↣ Fin n)
                   ≅ (Fin n ↣ Fin n)
transpose-inj-iso' {n} i j
  = Σ-ap-iso (Π-ap-iso refl≅ λ _ → tiso) λ f
  → mk-prop-iso (inj-level f (fin-set _))
                (inj-level _ (fin-set _))
                (transpose-inj i j f)
                (λ inj p → inj (ap (apply tiso) p))
   where
     tiso : Fin n ≅ Fin n
     tiso = transpose-iso i j

transpose-inj-iso : ∀ {n} (i j : Fin n)
                  → (Fin n ↣ Fin n)
                  ≅ (Fin n ↣ Fin n)
transpose-inj-iso {n} i j
  = Σ-ap-iso (Π-ap-iso tiso λ _ → refl≅) λ f
  → mk-prop-iso (inj-level f (fin-set _))
                (inj-level _ (fin-set _))
                (λ inj → iso⇒inj tiso ∘' inj)
                (λ inj p → iso⇒inj tiso (inj (
                           ap f (_≅_.iso₁ tiso _)
                         · p
                         · sym (ap f (_≅_.iso₁ tiso _)))))
   where
     tiso : Fin n ≅ Fin n
     tiso = transpose-iso i j

inj-nonsurj : ∀ {n i}{A : Set i}
            → (f : A → Fin (suc n))
            → injective f
            → {i : Fin (suc n)}
            → ((x : A) → ¬ (f x ≡ i))
            → A ↣ Fin n
inj-nonsurj {n}{i}{A} f inj {z} u = g , g-inj
 where
   f' : A → Σ (Fin (suc n)) λ k → ¬ (k ≡ z)
   f' i = f i , u i

   inj' : injective f'
   inj' p = inj (ap proj₁ p)

   abstract
    φ : (Σ (Fin (suc n)) λ k → ¬ (k ≡ z)) ≅ Fin n
    φ = fin-remove-iso z

   g : A → Fin n
   g = apply φ ∘' f'

   g-inj : injective g
   g-inj p = inj' (iso⇒inj φ p)

preimage : ∀ {i n}{A : Set i}
         → (f : Fin n → A)
         → (dec : (x y : A) → Dec (x ≡ y))
         → (x : A)
         → ( (Σ (Fin n) λ i → f i ≡ x)
            ⊎ ((i : Fin n) → ¬ (f i ≡ x)) )
preimage {n = 0} f dec x = inj₂ (λ ())
preimage {n = suc n} f dec x with dec (f zero) x
... | yes p = inj₁ (zero , p)
... | no u with preimage (λ i → f (suc i)) dec x
... | inj₁ (i , p) = inj₁ (suc i , p)
... | inj₂ v = inj₂ λ { zero → u ; (suc i) → v i }

fin-inj-remove₀ : ∀ {n m}
                → (f : Fin (suc n) ↣ Fin (suc m))
                → (apply f zero ≡ zero)
                → Fin n ↣ Fin m
fin-inj-remove₀ {n}{m} (f , inj) p = g , g-inj
  where
    nz : {i : Fin n} → ¬ (f (suc i) ≡ zero)
    nz q = fin-disj _ (inj (p · sym q))

    g : Fin n → Fin m
    g i = pred (f (suc i)) nz

    g-inj : injective g
    g-inj q = fin-suc-inj (inj (pred-inj nz nz q))

fin-inj-remove : ∀ {n m}
               → (Fin (suc n) ↣ Fin (suc m))
               → (Fin n ↣ Fin m)
fin-inj-remove {n}{m} (f , f-inj)
  = fin-inj-remove₀
      ( transpose zero (f zero) ∘' f
      , transpose-inj zero (f zero) f f-inj)
      ( transpose-β₂ zero (f zero))

fin-inj-add : ∀ {n m}
            → (Fin n ↣ Fin m)
            → (Fin (suc n) ↣ Fin (suc m))
fin-inj-add {n}{m} (f , f-inj) = g , g-inj
  where
    g : Fin (suc n) → Fin (suc m)
    g zero = zero
    g (suc i) = suc (f i)

    g-inj : injective g
    g-inj {zero} {zero} p = refl
    g-inj {zero} {suc x'} p = ⊥-elim (fin-disj _ p)
    g-inj {suc x} {zero} p = ⊥-elim (fin-disj _ (sym p))
    g-inj {suc x} {suc x'} p = ap suc (f-inj (fin-suc-inj p))

fin-lt : ∀ {n m}(f : Fin n ↣ Fin m) → n ≤ m
fin-lt {0} _ = z≤n
fin-lt {suc n} {0} (f , _) with f zero
... | ()
fin-lt {suc n}{suc m} f = s≤s (fin-lt (fin-inj-remove f))

inj⇒retr : ∀ {n}(f : Fin n → Fin n)
         → injective f
         → retraction f
inj⇒retr {0} f inj ()
inj⇒retr {suc n} f inj y with preimage f _≟_ y
... | inj₁ t = t
... | inj₂ u = ⊥-elim (suc≰ (fin-lt (inj-nonsurj f inj u)))

inj⇒iso : ∀ {n}(f : Fin n → Fin n)
         → injective f
         → Fin n ≅ Fin n
inj⇒iso f inj = inj+retr⇒iso f inj (inj⇒retr f inj)

Fin-inj : ∀ {n m} → Fin n ≅ Fin m → n ≡ m
Fin-inj {n}{m} isoF
  = antisym≤ (fin-lt (_ , iso⇒inj isoF))
             (fin-lt (_ , iso⇒inj (sym≅ isoF)))

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module StateSizedIO.IOObject where

open import Data.Product

open import Size

open import SizedIO.Base
open import StateSizedIO.Object

-- ---
-- ---
-- ---  FILE IS DELETED !!!
-- ---
-- ---

-- An IO object is like a simple object,
-- but the method returns IO applied to the result type of a simple object
-- which means the method returns an IO program which when terminating
-- returns the result of the simple object

{- NOTE   IOObject is now replaced by IOObjectˢ as defined in
          StateSizedIO.Base
-}

{-
module _  (ioi  : IOInterface)  (let C = Command ioi)  (let R = Response ioi)
          (oi   : Interfaceˢ)    (let S = Stateˢ oi)     (let M  = Methodˢ oi)
                                (let Rt  = Resultˢ oi) (let next = nextˢ oi)

  where

  record IOObject (i : Size) (s : S) : Set where
    coinductive
    field
      method : ∀{j : Size< i} (m : M s) → IO ioi ∞ (Σ[ r ∈ Rt s m ] IOObject j (next s m r) )

open IOObject public
-}

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
module A.B where

{-# NON_TERMINATING #-}

easy : (A : Set) → A
easy = easy

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
data D : Set where
  zero : D
  suc  : D → D

postulate
  f : D → D

{-# COMPILE GHC f = \ x -> x #-}


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

module Algebra.Construct.Free.Semilattice.Eliminators where

open import Algebra.Construct.Free.Semilattice.Definition
open import Prelude
open import Algebra

record _⇘_ {a p} (A : Type a) (P : 𝒦 A → Type p) : Type (a ℓ⊔ p) where
  no-eta-equality
  constructor elim
  field
    ⟦_⟧-set : ∀ {xs} → isSet (P xs)
    ⟦_⟧[] : P []
    ⟦_⟧_∷_⟨_⟩ : ∀ x xs → P xs → P (x ∷ xs)
  private z = ⟦_⟧[]; f = ⟦_⟧_∷_⟨_⟩
  field
    ⟦_⟧-com : ∀ x y xs pxs →
      f x (y ∷ xs) (f y xs pxs) ≡[ i ≔ P (com x y xs i) ]≡
      f y (x ∷ xs) (f x xs pxs)
    ⟦_⟧-dup : ∀ x xs pxs →
      f x (x ∷ xs) (f x xs pxs) ≡[ i ≔ P (dup x xs i) ]≡
      f x xs pxs
  ⟦_⟧⇓ : ∀ xs → P xs
  ⟦ [] ⟧⇓ = z
  ⟦ x ∷ xs ⟧⇓ = f x xs ⟦ xs ⟧⇓
  ⟦ com x y xs i ⟧⇓ = ⟦_⟧-com x y xs ⟦ xs ⟧⇓  i
  ⟦ dup x xs i ⟧⇓ = ⟦_⟧-dup x xs ⟦ xs ⟧⇓ i
  ⟦ trunc xs ys x y i j ⟧⇓ =
      isOfHLevel→isOfHLevelDep 2
        (λ xs → ⟦_⟧-set {xs})
        ⟦ xs ⟧⇓ ⟦ ys ⟧⇓
        (cong ⟦_⟧⇓ x) (cong ⟦_⟧⇓ y)
        (trunc xs ys x y)
        i j
  {-# INLINE ⟦_⟧⇓ #-}
open _⇘_ public

infixr 0 ⇘-syntax
⇘-syntax = _⇘_
syntax ⇘-syntax A (λ xs → Pxs) = xs ∈𝒦 A ⇒ Pxs

record _⇲_ {a p} (A : Type a) (P : 𝒦 A  → Type p) : Type (a ℓ⊔ p) where
  no-eta-equality
  constructor elim-prop
  field
    ∥_∥-prop : ∀ {xs} → isProp (P xs)
    ∥_∥[] : P []
    ∥_∥_∷_⟨_⟩ : ∀ x xs → P xs → P (x ∷ xs)
  private z = ∥_∥[]; f = ∥_∥_∷_⟨_⟩
  ∥_∥⇑ = elim
          (λ {xs} → isProp→isSet (∥_∥-prop {xs}))
          z f
          (λ x y xs pxs → toPathP (∥_∥-prop (transp (λ i → P (com x y xs i)) i0 (f x (y ∷ xs) (f y xs pxs))) (f y (x ∷ xs) (f x xs pxs))))
          (λ x xs pxs → toPathP (∥_∥-prop (transp (λ i → P (dup x xs i)) i0 (f x (x ∷ xs) (f x xs pxs))) (f x xs pxs) ))
  ∥_∥⇓ = ⟦ ∥_∥⇑ ⟧⇓
  {-# INLINE ∥_∥⇑ #-}
  {-# INLINE ∥_∥⇓ #-}

open _⇲_ public
elim-prop-syntax : ∀ {a p} → (A : Type a) → (𝒦 A → Type p) → Type (a ℓ⊔ p)
elim-prop-syntax = _⇲_

syntax elim-prop-syntax A (λ xs → Pxs) = xs ∈𝒦 A ⇒∥ Pxs ∥

record _↘∥_∥ {a p} (A : Type a) (P : 𝒦 A → Type p) : Type (a ℓ⊔ p) where
  no-eta-equality
  constructor elim-to-prop
  field
    ∣_∣[] : P []
    ∣_∣_∷_⟨_⟩ : ∀ x xs → P xs → P (x ∷ xs)
  private z = ∣_∣[]; f = ∣_∣_∷_⟨_⟩
  open import HITs.PropositionalTruncation.Sugar
  open import HITs.PropositionalTruncation

  ∣_∣⇑ : xs ∈𝒦 A ⇒∥ ∥ P xs ∥ ∥
  ∣_∣⇑ = elim-prop squash ∣ z ∣ λ x xs ∣Pxs∣ → f x xs ∥$∥ ∣Pxs∣
  ∣_∣⇓ = ∥ ∣_∣⇑ ∥⇓

open _↘∥_∥ public
elim-to-prop-syntax : ∀ {a p} → (A : Type a) → (𝒦 A → Type p) → Type (a ℓ⊔ p)
elim-to-prop-syntax = _↘∥_∥

syntax elim-to-prop-syntax A (λ xs → Pxs) = xs ∈𝒦 A ⇒∣ Pxs ∣

infixr 0 _↘_
record _↘_ {a b} (A : Type a) (B : Type b) : Type (a ℓ⊔ b) where
  no-eta-equality
  constructor rec
  field
    [_]-set  : isSet B
    [_]_∷_   : A → B → B
    [_][]    : B
  private f = [_]_∷_; z = [_][]
  field
    [_]-dup  : ∀ x xs → f x (f x xs) ≡ f x xs
    [_]-com : ∀ x y xs → f x (f y xs) ≡ f y (f x xs)
  [_]↑ = elim
            [_]-set
            z
            (λ x _ xs → f x xs)
            (λ x y xs → [_]-com x y)
            (λ x xs → [_]-dup x)
  [_]↓ = ⟦ [_]↑ ⟧⇓
  {-# INLINE [_]↑ #-}
  {-# INLINE [_]↓ #-}
open _↘_ public

module _ {a p} {A : Type a} {P : 𝒦 A → Type p} where
    𝒦-elim-prop : (∀ {xs} → isProp (P xs)) →
                  (∀ x xs → P xs → P (x ∷ xs)) →
                  (P []) →
                  ∀ xs → P xs
    𝒦-elim-prop isPropB f n = go
      where
      go : ∀ xs → P xs
      go [] = n
      go (x ∷ xs) = f x xs (go xs)
      go (com x y xs j) = toPathP {A = λ i → P (com x y xs i)} (isPropB (transp (λ i → P (com x y xs i)) i0 (f x (y ∷ xs) (f y xs (go xs)))) (f y (x ∷ xs) (f x xs (go xs)))) j
      go (dup x xs j) = toPathP {A = λ i → P (dup x xs i)} (isPropB (transp (λ i → P (dup x xs i)) i0 (f x (x ∷ xs) (f x xs (go xs)))) (f x xs (go xs)) ) j
      go (trunc xs ys x y i j) =
        isOfHLevel→isOfHLevelDep 2
          (λ xs → isProp→isSet (isPropB {xs}))
          (go xs) (go ys)
          (cong go x) (cong go y)
          (trunc xs ys x y)
          i j

module _ {a b} {A : Type a} {B : Type b} where
  𝒦-rec : isSet B →
          (f : A → B → B) →
          (n : B) →
          (fdup : ∀ x xs → f x (f x xs) ≡ f x xs) →
          (fcom : ∀ x y xs → f x (f y xs) ≡ f y (f x xs)) →
          𝒦 A →
          B
  𝒦-rec isSetB f n fdup fcom = go
    where
    go : 𝒦 A → B
    go [] = n
    go (x ∷ xs) = f x (go xs)
    go (com x y xs i) = fcom x y (go xs) i
    go (dup x xs i) = fdup x (go xs) i
    go (trunc xs ys x y i j) =
      isOfHLevel→isOfHLevelDep 2
        (λ xs → isSetB)
        (go xs) (go ys)
        (cong go x) (cong go y)
        (trunc xs ys x y)
        i j

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Instantiates the ring solver, using the natural numbers as the
-- coefficient "ring"
------------------------------------------------------------------------

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

open import Algebra
import Algebra.Operations.Semiring as SemiringOps
open import Data.Maybe.Base using (Maybe; just; nothing; map)

module Algebra.Solver.Ring.NaturalCoefficients
         {r₁ r₂}
         (R : CommutativeSemiring r₁ r₂)
         (dec : let open CommutativeSemiring R
                    open SemiringOps semiring in
                ∀ m n → Maybe (m × 1# ≈ n × 1#)) where

import Algebra.Solver.Ring
open import Algebra.Solver.Ring.AlmostCommutativeRing
open import Data.Nat.Base as ℕ
open import Data.Product using (module Σ)
open import Function

open CommutativeSemiring R
open SemiringOps semiring
open import Relation.Binary.Reasoning.Setoid setoid

private

  -- The coefficient "ring".

  ℕ-ring : RawRing _
  ℕ-ring = record
    { Carrier = ℕ
    ; _+_     = ℕ._+_
    ; _*_     = ℕ._*_
    ; -_      = id
    ; 0#      = 0
    ; 1#      = 1
    }

  -- There is a homomorphism from ℕ to R.
  --
  -- Note that _×′_ is used rather than _×_. If _×_ were used, then
  -- Function.Related.TypeIsomorphisms.test would fail to type-check.

  homomorphism :
    ℕ-ring -Raw-AlmostCommutative⟶ fromCommutativeSemiring R
  homomorphism = record
    { ⟦_⟧    = λ n → n ×′ 1#
    ; +-homo = ×′-homo-+ 1#
    ; *-homo = ×′1-homo-*
    ; -‿homo = λ _ → refl
    ; 0-homo = refl
    ; 1-homo = refl
    }

  -- Equality of certain expressions can be decided.

  dec′ : ∀ m n → Maybe (m ×′ 1# ≈ n ×′ 1#)
  dec′ m n = map to (dec m n)
    where
    to : m × 1# ≈ n × 1# → m ×′ 1# ≈ n ×′ 1#
    to m≈n = begin
      m ×′ 1#  ≈⟨ sym $ ×≈×′ m 1# ⟩
      m ×  1#  ≈⟨ m≈n ⟩
      n ×  1#  ≈⟨ ×≈×′ n 1# ⟩
      n ×′ 1#  ∎

-- The instantiation.

open Algebra.Solver.Ring _ _ homomorphism dec′ public


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

open import BBHeap _≤_
open import Bound.Lower A
open import BTree.Equality {A} renaming (_≃_ to _≃'_)
open import BTree.Complete.Alternative {A} renaming (_⋘_ to _⋘'_ ; _⋙_ to _⋙'_ ;  _⋗_ to _⋗'_)

lemma-forget≃ : {b b' : Bound}{l : BBHeap b}{r : BBHeap b'} → l ≃ r → forget l ≃' forget r
lemma-forget≃ ≃lf = ≃lf
lemma-forget≃ (≃nd {x = x} {x' = x'} _ _ _ _ l≃r l'≃r' l≃l') = ≃nd x x' (lemma-forget≃ l≃r) (lemma-forget≃ l≃l') (lemma-forget≃ l'≃r')

lemma-forget⋗ : {b b' : Bound}{l : BBHeap b}{r : BBHeap b'} → l ⋗ r → forget l ⋗' forget r
lemma-forget⋗ (⋗lf {x = x} _) = ⋗lf x
lemma-forget⋗ (⋗nd {x = x} {x' = x'} _ _ _ _ l≃r l'≃r' l⋗l') = ⋗nd x x' (lemma-forget≃ l≃r) (lemma-forget≃ l'≃r') (lemma-forget⋗ l⋗l')

mutual
  lemma-forget⋘ : {b b' : Bound}{l : BBHeap b}{r : BBHeap b'} → l ⋘ r → forget l ⋘' forget r
  lemma-forget⋘ lf⋘ = lf⋘
  lemma-forget⋘ (ll⋘ {x = x} {x' = x'} _ _ l⋘r l'⋘r' l'≃r' r≃l') = ll⋘ x x' (lemma-forget⋘ l⋘r) (lemma-forget≃ l'≃r') (lemma-forget≃ r≃l')
  lemma-forget⋘ (lr⋘ {x = x} {x' = x'} _ _ l⋙r l'⋘r' l'≃r' l⋗l') = lr⋘ x x' (lemma-forget⋙ l⋙r) (lemma-forget≃ l'≃r') (lemma-forget⋗ l⋗l')

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

lemma-bbheap-complete : {b : Bound}(h : BBHeap b) → Complete (forget h)
lemma-bbheap-complete leaf = leaf
lemma-bbheap-complete (left {x = x} {l = l} {r = r} _ l⋘r) = left x (lemma-bbheap-complete l) (lemma-bbheap-complete r) (lemma-forget⋘ l⋘r)
lemma-bbheap-complete (right {x = x} {l = l} {r = r} _ l⋙r) = right x  (lemma-bbheap-complete l) (lemma-bbheap-complete r) (lemma-forget⋙ l⋙r)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
------------------------------------------------------------------------------
-- Existential quantifier on the inductive PA universe
------------------------------------------------------------------------------

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

module PA.Inductive.Existential where

infix 2 ∃

------------------------------------------------------------------------------
-- PA universe
open import PA.Inductive.Base.Core

-- The existential quantifier type on M.
data ∃ (A : ℕ → Set) : Set where
  _,_ : (x : ℕ) → A x → ∃ A

-- Sugar syntax for the existential quantifier.
syntax ∃ (λ x → e) = ∃[ x ] e

-- 2012-03-05: We avoid to use the existential elimination or the
-- existential projections because we use pattern matching (and the
-- Agda's with constructor).

-- The existential elimination.
--
-- NB. We do not use the usual type theory elimination with two
-- projections because we are working in first-order logic where we do
-- not need extract a witness from an existence proof.
-- ∃-elim : {A : ℕ → Set}{B : Set} → ∃ A → (∀ {x} → A x → B) → B
-- ∃-elim (_ , Ax) h = h Ax

-- The existential proyections.
-- ∃-proj₁ : ∀ {A} → ∃ A → M
-- ∃-proj₁ (x , _) = x

-- ∃-proj₂ : ∀ {A} → (h : ∃ A) → A (∃-proj₁ h)
-- ∃-proj₂ (_ , Ax) = Ax

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to setoid list membership
------------------------------------------------------------------------

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

module Data.List.Membership.Setoid.Properties where

open import Algebra.FunctionProperties using (Op₂; Selective)
open import Data.Fin using (Fin; zero; suc)
open import Data.List
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
import Data.List.Relation.Unary.Any.Properties as Any
import Data.List.Membership.Setoid as Membership
import Data.List.Relation.Binary.Equality.Setoid as Equality
open import Data.Nat using (suc; z≤n; s≤s; _≤_; _<_)
open import Data.Nat.Properties using (≤-trans; n≤1+n)
open import Data.Product as Prod using (∃; _×_; _,_ ; ∃₂)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_$_; flip; _∘_; id)
open import Relation.Binary hiding (Decidable)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Unary using (Decidable; Pred)
open import Relation.Nullary using (¬_; yes; no)
open import Relation.Nullary.Negation using (contradiction)
open Setoid using (Carrier)

------------------------------------------------------------------------
-- Equality properties

module _ {c ℓ} (S : Setoid c ℓ) where

  open Setoid S
  open Equality S
  open Membership S

  -- _∈_ respects the underlying equality

  ∈-resp-≈ : ∀ {xs} → (_∈ xs) Respects _≈_
  ∈-resp-≈ x≈y x∈xs = Any.map (trans (sym x≈y)) x∈xs

  ∉-resp-≈ : ∀ {xs} → (_∉ xs) Respects _≈_
  ∉-resp-≈ v≈w v∉xs w∈xs = v∉xs (∈-resp-≈ (sym v≈w) w∈xs)

  ∈-resp-≋ : ∀ {x} → (x ∈_) Respects _≋_
  ∈-resp-≋ = Any.lift-resp (flip trans)

  ∉-resp-≋ : ∀ {x} → (x ∉_) Respects _≋_
  ∉-resp-≋ xs≋ys v∉xs v∈ys = v∉xs (∈-resp-≋ (≋-sym xs≋ys) v∈ys)

------------------------------------------------------------------------
-- mapWith∈

module _ {c₁ c₂ ℓ₁ ℓ₂} (S₁ : Setoid c₁ ℓ₁) (S₂ : Setoid c₂ ℓ₂) where

  open Setoid S₁ renaming (Carrier to A₁; _≈_ to _≈₁_; refl to refl₁)
  open Setoid S₂ renaming (Carrier to A₂; _≈_ to _≈₂_; refl to refl₂)
  open Equality S₁ using ([]; _∷_) renaming (_≋_ to _≋₁_)
  open Equality S₂ using () renaming (_≋_ to _≋₂_)
  open Membership S₁

  mapWith∈-cong : ∀ {xs ys} → xs ≋₁ ys →
                  (f : ∀ {x} → x ∈ xs → A₂) →
                  (g : ∀ {y} → y ∈ ys → A₂) →
                  (∀ {x y} → x ≈₁ y → (x∈xs : x ∈ xs) (y∈ys : y ∈ ys) →
                     f x∈xs ≈₂ g y∈ys) →
                  mapWith∈ xs f ≋₂ mapWith∈ ys g
  mapWith∈-cong []            f g cong = []
  mapWith∈-cong (x≈y ∷ xs≋ys) f g cong =
    cong x≈y (here refl₁) (here refl₁) ∷
    mapWith∈-cong xs≋ys (f ∘ there) (g ∘ there)
      (λ x≈y x∈xs y∈ys → cong x≈y (there x∈xs) (there y∈ys))

  mapWith∈≗map : ∀ f xs → mapWith∈ xs (λ {x} _ → f x) ≋₂ map f xs
  mapWith∈≗map f []       = []
  mapWith∈≗map f (x ∷ xs) = refl₂ ∷ mapWith∈≗map f xs

module _ {c ℓ} (S : Setoid c ℓ) where

  open Setoid S
  open Membership S

  length-mapWith∈ : ∀ {a} {A : Set a} xs {f : ∀ {x} → x ∈ xs → A} →
                    length (mapWith∈ xs f) ≡ length xs
  length-mapWith∈ []       = P.refl
  length-mapWith∈ (x ∷ xs) = P.cong suc (length-mapWith∈ xs)

------------------------------------------------------------------------
-- map

module _ {c₁ c₂ ℓ₁ ℓ₂} (S₁ : Setoid c₁ ℓ₁) (S₂ : Setoid c₂ ℓ₂) where

  open Setoid S₁ renaming (Carrier to A₁; _≈_ to _≈₁_; refl to refl₁)
  open Setoid S₂ renaming (Carrier to A₂; _≈_ to _≈₂_)
  private module M₁ = Membership S₁; open M₁ using (find) renaming (_∈_ to _∈₁_)
  private module M₂ = Membership S₂; open M₂ using () renaming (_∈_ to _∈₂_)

  ∈-map⁺ : ∀ {f} → f Preserves _≈₁_ ⟶ _≈₂_ → ∀ {v xs} →
            v ∈₁ xs → f v ∈₂ map f xs
  ∈-map⁺ pres x∈xs = Any.map⁺ (Any.map pres x∈xs)

  ∈-map⁻ : ∀ {v xs f} → v ∈₂ map f xs →
           ∃ λ x → x ∈₁ xs × v ≈₂ f x
  ∈-map⁻ x∈map = find (Any.map⁻ x∈map)

  map-∷= : ∀ {f} (f≈ : f Preserves _≈₁_ ⟶ _≈₂_)
           {xs x v} → (x∈xs : x ∈₁ xs) →
           map f (x∈xs M₁.∷= v) ≡ ∈-map⁺ f≈ x∈xs M₂.∷= f v
  map-∷= f≈ (here x≈y)   = P.refl
  map-∷= f≈ (there x∈xs) = P.cong (_ ∷_) (map-∷= f≈ x∈xs)

------------------------------------------------------------------------
-- _++_

module _ {c ℓ} (S : Setoid c ℓ) where

  open Membership S using (_∈_)
  open Setoid S
  open Equality S using (_≋_; _∷_; ≋-refl)

  ∈-++⁺ˡ : ∀ {v xs ys} → v ∈ xs → v ∈ xs ++ ys
  ∈-++⁺ˡ = Any.++⁺ˡ

  ∈-++⁺ʳ : ∀ {v} xs {ys} → v ∈ ys → v ∈ xs ++ ys
  ∈-++⁺ʳ = Any.++⁺ʳ

  ∈-++⁻ : ∀ {v} xs {ys} → v ∈ xs ++ ys → (v ∈ xs) ⊎ (v ∈ ys)
  ∈-++⁻ = Any.++⁻

  ∈-insert : ∀ xs {ys v w} → v ≈ w → v ∈ xs ++ [ w ] ++ ys
  ∈-insert xs = Any.++-insert xs

  ∈-∃++ : ∀ {v xs} → v ∈ xs → ∃₂ λ ys zs → ∃ λ w →
          v ≈ w × xs ≋ ys ++ [ w ] ++ zs
  ∈-∃++ (here px)                  = [] , _ , _ , px , ≋-refl
  ∈-∃++ (there {d} v∈xs) with ∈-∃++ v∈xs
  ... | hs , _ , _ , v≈v′ , eq = d ∷ hs , _ , _ , v≈v′ , refl ∷ eq

------------------------------------------------------------------------
-- concat

module _ {c ℓ} (S : Setoid c ℓ) where

  open Setoid S using (_≈_)
  open Membership S using (_∈_)
  open Equality S using (≋-setoid)
  open Membership ≋-setoid using (find) renaming (_∈_ to _∈ₗ_)

  ∈-concat⁺ : ∀ {v xss} → Any (v ∈_) xss → v ∈ concat xss
  ∈-concat⁺ = Any.concat⁺

  ∈-concat⁻ : ∀ {v} xss → v ∈ concat xss → Any (v ∈_) xss
  ∈-concat⁻ = Any.concat⁻

  ∈-concat⁺′ : ∀ {v vs xss} → v ∈ vs → vs ∈ₗ xss → v ∈ concat xss
  ∈-concat⁺′ v∈vs = ∈-concat⁺ ∘ Any.map (flip (∈-resp-≋ S) v∈vs)

  ∈-concat⁻′ : ∀ {v} xss → v ∈ concat xss → ∃ λ xs → v ∈ xs × xs ∈ₗ xss
  ∈-concat⁻′ xss v∈c[xss] with find (∈-concat⁻ xss v∈c[xss])
  ... | xs , t , s = xs , s , t

------------------------------------------------------------------------
-- applyUpTo

module _ {c ℓ} (S : Setoid c ℓ) where

  open Setoid S using (_≈_; refl)
  open Membership S using (_∈_)

  ∈-applyUpTo⁺ : ∀ f {i n} → i < n → f i ∈ applyUpTo f n
  ∈-applyUpTo⁺ f = Any.applyUpTo⁺ f refl

  ∈-applyUpTo⁻ : ∀ {v} f {n} → v ∈ applyUpTo f n →
                 ∃ λ i → i < n × v ≈ f i
  ∈-applyUpTo⁻ = Any.applyUpTo⁻

------------------------------------------------------------------------
-- tabulate

module _ {c ℓ} (S : Setoid c ℓ) where

  open Setoid S using (_≈_; refl) renaming (Carrier to A)
  open Membership S using (_∈_)

  ∈-tabulate⁺ : ∀ {n} {f : Fin n → A} i → f i ∈ tabulate f
  ∈-tabulate⁺ i = Any.tabulate⁺ i refl

  ∈-tabulate⁻ : ∀ {n} {f : Fin n → A} {v} →
                v ∈ tabulate f → ∃ λ i → v ≈ f i
  ∈-tabulate⁻ = Any.tabulate⁻

------------------------------------------------------------------------
-- filter

module _ {c ℓ p} (S : Setoid c ℓ) {P : Pred (Carrier S) p}
         (P? : Decidable P) (resp : P Respects (Setoid._≈_ S)) where

  open Setoid S using (_≈_; sym)
  open Membership S using (_∈_)

  ∈-filter⁺ : ∀ {v xs} → v ∈ xs → P v → v ∈ filter P? xs
  ∈-filter⁺ {xs = x ∷ _} (here v≈x) Pv with P? x
  ... | yes _   = here v≈x
  ... | no  ¬Px = contradiction (resp v≈x Pv) ¬Px
  ∈-filter⁺ {xs = x ∷ _} (there v∈xs) Pv with P? x
  ... | yes _ = there (∈-filter⁺ v∈xs Pv)
  ... | no  _ = ∈-filter⁺ v∈xs Pv

  ∈-filter⁻ : ∀ {v xs} → v ∈ filter P? xs → v ∈ xs × P v
  ∈-filter⁻ {xs = []}     ()
  ∈-filter⁻ {xs = x ∷ xs} v∈f[x∷xs] with P? x
  ... | no  _  = Prod.map there id (∈-filter⁻ v∈f[x∷xs])
  ... | yes Px with v∈f[x∷xs]
  ...   | here  v≈x   = here v≈x , resp (sym v≈x) Px
  ...   | there v∈fxs = Prod.map there id (∈-filter⁻ v∈fxs)

------------------------------------------------------------------------
-- length

module _ {c ℓ} (S : Setoid c ℓ) where

  open Membership S using (_∈_)

  ∈-length : ∀ {x xs} → x ∈ xs → 1 ≤ length xs
  ∈-length (here px)    = s≤s z≤n
  ∈-length (there x∈xs) = ≤-trans (∈-length x∈xs) (n≤1+n _)

------------------------------------------------------------------------
-- lookup

module _ {c ℓ} (S : Setoid c ℓ) where

  open Setoid S using (refl)
  open Membership S using (_∈_)

  ∈-lookup : ∀ xs i → lookup xs i ∈ xs
  ∈-lookup []       ()
  ∈-lookup (x ∷ xs) zero    = here refl
  ∈-lookup (x ∷ xs) (suc i) = there (∈-lookup xs i)

------------------------------------------------------------------------
-- foldr

module _ {c ℓ} (S : Setoid c ℓ) {_•_ : Op₂ (Carrier S)} where

  open Setoid S using (_≈_; refl; sym; trans)
  open Membership S using (_∈_)

  foldr-selective : Selective _≈_ _•_ → ∀ e xs →
                    (foldr _•_ e xs ≈ e) ⊎ (foldr _•_ e xs ∈ xs)
  foldr-selective •-sel i [] = inj₁ refl
  foldr-selective •-sel i (x ∷ xs) with •-sel x (foldr _•_ i xs)
  ... | inj₁ x•f≈x = inj₂ (here x•f≈x)
  ... | inj₂ x•f≈f with foldr-selective •-sel i xs
  ...   | inj₁ f≈i  = inj₁ (trans x•f≈f f≈i)
  ...   | inj₂ f∈xs = inj₂ (∈-resp-≈ S (sym x•f≈f) (there f∈xs))

------------------------------------------------------------------------
-- _∷=_

module _ {c ℓ} (S : Setoid c ℓ) where

  open Setoid S
  open Membership S

  ∈-∷=⁺-updated : ∀ {xs x v} (x∈xs : x ∈ xs) → v ∈ (x∈xs ∷= v)
  ∈-∷=⁺-updated (here  px)  = here refl
  ∈-∷=⁺-updated (there pxs) = there (∈-∷=⁺-updated pxs)

  ∈-∷=⁺-untouched : ∀ {xs x y v} (x∈xs : x ∈ xs) → (¬ x ≈ y) → y ∈ xs → y ∈ (x∈xs ∷= v)
  ∈-∷=⁺-untouched (here  x≈z)  x≉y (here  y≈z)  = contradiction (trans x≈z (sym y≈z)) x≉y
  ∈-∷=⁺-untouched (here  x≈z)  x≉y (there y∈xs) = there y∈xs
  ∈-∷=⁺-untouched (there x∈xs) x≉y (here  y≈z)  = here y≈z
  ∈-∷=⁺-untouched (there x∈xs) x≉y (there y∈xs) = there (∈-∷=⁺-untouched x∈xs x≉y y∈xs)

  ∈-∷=⁻ : ∀ {xs x y v} (x∈xs : x ∈ xs) → (¬ y ≈ v) → y ∈ (x∈xs ∷= v) → y ∈ xs
  ∈-∷=⁻ (here x≈z)   y≉v (here y≈v) = contradiction y≈v y≉v
  ∈-∷=⁻ (here x≈z)   y≉v (there y∈) = there y∈
  ∈-∷=⁻ (there x∈xs) y≉v (here y≈z) = here y≈z
  ∈-∷=⁻ (there x∈xs) y≉v (there y∈) = there (∈-∷=⁻ x∈xs y≉v y∈)


text:
-- Operators used in the wrong way.
module NoParseForApplication where

postulate
  X : Set
  _! : X -> X

right : X -> X
right x = x !

wrong : X -> X
wrong x = ! x

max_issues_repo_name: cruhland/agda