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

--------------------------------------------------------------------------------
-- Simple implementation of sets of ℕ.
--------------------------------------------------------------------------------

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

module Data.Nat.Table where

open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.List as List using (List; _∷_; [])
open import Function

Table : Set
Table = List ℕ

para : ∀ {a b} {A : Set a} {B : Set b} → (A → List A → B → B) → B → List A → B
para f b [] = b
para f b (x ∷ xs) = f x xs (para f b xs)

insert : ℕ → Table → Table
insert x xs = para (go zero) (_∷ []) xs x
  where
  go : ℕ → ℕ → Table → (ℕ → Table) → ℕ → Table
  go k zero    xs g zero    = k ∷ xs
  go k zero    xs g (suc i) = k ∷ g i
  go k (suc x) xs g zero    = k ∷ x ∷ xs
  go k (suc x) xs g (suc i) = go (suc k) x xs g i

open import Data.Maybe as Maybe using (Maybe; just; nothing)

member : ℕ → Table → Maybe ℕ
member x xs = List.foldr go (const (const nothing)) xs x 0
  where
  go : ℕ → (ℕ → ℕ → Maybe ℕ) → ℕ → ℕ → Maybe ℕ
  go zero    ys zero    k = just k
  go zero    ys (suc x) k = ys x (suc k)
  go (suc y) ys zero    _ = nothing
  go (suc y) ys (suc x) k = go y ys x k

fromList : List ℕ → Table
fromList = List.foldr insert []

toList : Table → List ℕ
toList = tail′ ∘ List.map ℕ.pred ∘ List.scanl (λ x y → suc (y ℕ.+ x)) 0
  where
  tail′ : List ℕ → List ℕ
  tail′ [] = []
  tail′ (_ ∷ xs) = xs

private
  open import Relation.Binary.PropositionalEquality
  example₁ : fromList (4 ∷ 3 ∷ 1 ∷ 0 ∷ 2 ∷ []) ≡ (0 ∷ 0 ∷ 0 ∷ 0 ∷ 0 ∷ [])
  example₁ = refl

  example₂ : member 3 (fromList (4 ∷ 3 ∷ 1 ∷ 0 ∷ 2 ∷ [])) ≡ just 3
  example₂ = refl

  example₃ : toList (fromList (4 ∷ 3 ∷ 1 ∷ 0 ∷ 2 ∷ [])) ≡ (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
  example₃ = refl

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


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

module Light.Implementation.Relation.Decidable where

open import Light.Variable.Levels
open import Light.Variable.Sets
open import Light.Library.Relation.Decidable using (Library ; Dependencies)
open import Light.Library.Data.Empty as Empty using (Empty)
open import Light.Library.Data.Unit as Unit using (Unit ; unit)
open import Light.Library.Data.Both as Both using (Both)
import Light.Library.Data.Product as Product
open import Light.Library.Data.These as These using (These)
import Light.Implementation.Data.Empty
import Light.Implementation.Data.Unit
import Light.Implementation.Data.Product
import Light.Implementation.Data.These
import Light.Package

instance dependencies : Dependencies
dependencies = record {}

instance library : Library dependencies
library = record
      {
            Implementation ;
            to‐witness = λ ⦃ a ⦄ → Implementation.to‐witness a ;
            to‐false‐witness = λ ⦃ a ⦄ → Implementation.to‐false‐witness a ;
            from‐witness = λ ⦃ a ⦄ → Implementation.from‐witness a ;
            from‐false‐witness = λ ⦃ a ⦄ → Implementation.from‐false‐witness a
      }
      where
      module Implementation where
            open import Light.Implementation.Relation.Sets using (base) public

            data Decidable (𝕒 : Set ℓ) : Set ℓ where
                  yes : 𝕒 → Decidable 𝕒
                  no : (𝕒 → Empty) → Decidable 𝕒

            module Style where
                  true : Decidable Unit
                  true = yes unit

                  false : Decidable Empty
                  false = no λ a → a

                  ¬_ : Decidable 𝕒 → Decidable (𝕒 → Empty)
                  ¬ yes a = no λ f → f a
                  ¬ no a = yes a

                  _∧_ : ∀ {𝕒 : Set aℓ} {𝕓 : Set bℓ} (a? : Decidable 𝕒) (b? : Decidable 𝕓) → Decidable (Both 𝕒 𝕓)
                  yes a ∧ yes b = yes (Both.both a b)
                  no f ∧ _ = no λ both → f (Both.first both)
                  _ ∧ no f = no λ both → f (Both.second both)

                  _∨_ : ∀ {𝕒 : Set aℓ} {𝕓 : Set bℓ} (a? : Decidable 𝕒) (b? : Decidable 𝕓) → Decidable (These 𝕒 𝕓)
                  no af ∨ no bf = no {!!}
                  yes a ∨ yes b = yes (These.these a b)
                  yes a ∨ no _ = yes (These.this a)
                  no _ ∨ yes b = yes (These.that b)

                  _⇢_ : ∀ {𝕒 : Set aℓ} {𝕓 : Set bℓ} (a? : Decidable 𝕒) (b? : Decidable 𝕓) → Decidable (𝕒 → 𝕓)
                  _ ⇢ yes b = yes λ _ → b
                  no af ⇢ _ = yes λ a → Empty.eliminate (af a)
                  yes a ⇢ no bf = no λ f → bf (f a)

                  True False : Decidable 𝕒 → Set

                  True (yes _) = Unit
                  True (no _) = Empty
                  False a? = True (¬ a?)

            style = record { Style }

            if′_then_else_ : Decidable 𝕒 → 𝕓 → 𝕓 → 𝕓
            if′ yes _ then a else _ = a
            if′ no _ then _ else a = a

            if_then_else_ :
                  ∀ (a : Decidable 𝕒)
                  → (∀ ⦃ witness : 𝕒 ⦄ → 𝕓)
                  → (∀ ⦃ witness : 𝕒 → Empty ⦄ → 𝕓)
                  → 𝕓
            if yes w then a else _ = a ⦃ witness = w ⦄
            if no w then _ else a = a ⦃ witness = w ⦄

            to‐witness : ∀ {a? : Decidable 𝕒} → Style.True a? → 𝕒
            to‐false‐witness : ∀ {a? : Decidable 𝕒} → Style.False a? → 𝕒 → Empty

            from‐witness : ∀ {a? : Decidable 𝕒} → 𝕒 → Style.True a?
            from‐false‐witness : ∀ {a? : Decidable 𝕒} → (𝕒 → Empty) → Style.False a?

            to‐witness {a? = yes a} _ = a
            to‐false‐witness {a? = no f} _ = f

            from‐witness {a? = yes a} _ = _
            from‐witness {a? = no f} w = f w
            from‐false‐witness {a? = no f} _ = _
            from‐false‐witness {a? = yes a} w = w a

ext: agda

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
------------------------------------------------------------------------------
-- Properties of the inequalities of unary numbers
------------------------------------------------------------------------------

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

module FOTC.Data.Nat.UnaryNumbers.Inequalities.PropertiesATP where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.PropertiesATP
open import FOTC.Data.Nat.PropertiesATP
open import FOTC.Data.Nat.UnaryNumbers

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

postulate x<x+1 : ∀ {n} → N n → n < n + 1'
{-# ATP prove x<x+1 x<Sx +-comm #-}

postulate x<x+11 : ∀ {n} → N n → n < n + 11'
{-# ATP prove x<x+11 x<x+Sy #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
data Nat : Set where
  O : Nat
  S : Nat → Nat

syntax S x = suc x

test : Nat → Nat
test _ = suc O

syntax lim (λ n → m) = limit n at m

data lim (f : Nat → Nat) : Set where

syntax foo (λ _ → n) = const-foo n

postulate
  foo : (Nat → Nat) → Nat

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --type-in-type --no-pattern-matching #-}
open import Spire.DarkwingDuck.Primitive
open import Spire.DarkwingDuck.Derived
module Spire.DarkwingDuck.Examples where

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

NatN : String
NatN = "Nat"

NatE : Enum
NatE = "zero" ∷ "suc" ∷ []

NatP : Tel
NatP = Emp

NatI : Indices NatP
NatI = indices NatP Emp

NatC : Constrs NatE NatP NatI
NatC = constrs NatE NatP NatI
  (End tt , Rec tt (End tt) , tt)

Nat : Former NatP NatI
Nat = Form NatN NatE NatP NatI NatC

zero : Inj NatN NatE NatP NatI NatC here
zero = inj NatN NatE NatP NatI NatC here

suc : Inj NatN NatE NatP NatI NatC (there here)
suc = inj NatN NatE NatP NatI NatC (there here)

elimNat : Elim NatN NatE NatP NatI NatC
elimNat = elim NatN NatE NatP NatI NatC

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

VecN : String
VecN = "Vec"

VecE : Enum
VecE = "nil" ∷ "cons" ∷ []

VecP : Tel
VecP = Ext Set λ _ → Emp

VecI : Indices VecP
VecI = indices VecP λ A → Ext Nat λ _ → Emp

VecC : Constrs VecE VecP VecI
VecC = constrs VecE VecP VecI λ A →
    End (zero , tt)
  , Arg Nat (λ n → Arg A λ _ → Rec (n , tt) (End (suc n , tt)))
  , tt

Vec : Former VecP VecI
Vec = Form VecN VecE VecP VecI VecC

nil : Inj VecN VecE VecP VecI VecC here
nil = inj VecN VecE VecP VecI VecC here

cons : Inj VecN VecE VecP VecI VecC (there here)
cons = inj VecN VecE VecP VecI VecC (there here)

elimVec : Elim VecN VecE VecP VecI VecC
elimVec = elim VecN VecE VecP VecI VecC

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

add : Nat → Nat → Nat
add = elimNat
  (λ n → Nat → Nat)
  (λ n → n)
  (λ m ih n → suc (ih n))

mult : Nat → Nat → Nat
mult = elimNat
  (λ n → Nat → Nat)
  (λ n → zero)
  (λ m ih n → add n (ih n))

append : (A : Set) (m n : Nat) (xs : Vec A m) (ys : Vec A n) → Vec A (add m n)
append A m n = elimVec A
  (λ m xs → (ys : Vec A n) → Vec A (add m n))
  (λ ys → ys)
  (λ m' x xs ih ys → cons A (add m' n) x (ih ys))
  m

concat : (A : Set) (m n : Nat) (xss : Vec (Vec A m) n) → Vec A (mult n m)
concat A m n = elimVec (Vec A m)
  (λ n xss → Vec A (mult n m))
  (nil A)
  (λ m' xs xss ih → append A m (mult m' m) xs ih)
  n

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

one : Nat
one = suc zero

two : Nat
two = suc one

three : Nat
three = suc two

[1,2] : Vec Nat two
[1,2] = cons Nat one one (cons Nat zero two (nil Nat))

[3] : Vec Nat one
[3] = cons Nat zero three (nil Nat)

[1,2,3] : Vec Nat three
[1,2,3] = cons Nat two one (cons Nat one two (cons Nat zero three (nil Nat)))

test-append : [1,2,3] ≡ append Nat two one [1,2] [3]
test-append = refl

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

max_stars_repo_name: spire/spire

max_issues_repo_name: spire/spire

max_forks_repo_name: spire/spire


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

module Cubical.Data.FinSet.Binary.Small.Base where

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

open import Cubical.Data.Bool hiding (isSetBool)

data Binary : Type₀
El : Binary → Type₀

data Binary where
  ℕ₂ : Binary
  un : ∀ x y → El x ≃ El y → x ≡ y

El ℕ₂ = Bool
El (un _ _ e i) = ua e i

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:
------------------------------------------------------------------------
-- Examples
------------------------------------------------------------------------

module RecursiveDescent.InductiveWithFix.Examples where

open import Data.List
open import Data.Nat
import Data.Char as C
import Data.String as S
open C using (Char)
open S using (String)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import Utilities
open import RecursiveDescent.Index
open import RecursiveDescent.InductiveWithFix
open import RecursiveDescent.InductiveWithFix.Lib
open Token C.decSetoid

-- A function used to simplify the examples a little.

_∈?_/_ :  forall {nt i r}
       -> String -> Parser Char nt i r -> Grammar Char nt -> List r
s ∈? p / g = parse-complete p g (S.toList s)

module Ex₁ where

  -- e ∷= 0 + e | 0

  data Nonterminal : ParserType₁ where
    e : Nonterminal _ Char

  grammar : Grammar Char Nonterminal
  grammar e = sym '0' ⊛> sym '+' ⊛> ! e
            ∣ sym '0'

  ex₁ : "0+0" ∈? (! e) / grammar ≡ '0' ∷ []
  ex₁ = refl

module Ex₂ where

  -- e ∷= f + e | f
  -- f ∷= 0 | 0 * f | ( e )

  data Nonterminal : ParserType₁ where
    expr   : Nonterminal _ Char
    factor : Nonterminal _ Char

  grammar : Grammar Char Nonterminal
  grammar expr   = ! factor ⊛> sym '+' ⊛> ! expr
                 ∣ ! factor
  grammar factor = sym '0'
                 ∣ sym '0' ⊛> sym '*' ⊛> ! factor
                 ∣ sym '(' ⊛> ! expr <⊛ sym ')'

  ex₁ : "(0*)" ∈? (! expr) / grammar ≡ []
  ex₁ = refl

  ex₂ : "0*(0+0)" ∈? (! expr) / grammar ≡ '0' ∷ []
  ex₂ = refl

{-
module Ex₃ where

  -- This is not allowed:

  -- e ∷= f + e | f
  -- f ∷= 0 | f * 0 | ( e )

  data Nonterminal : ParserType₁ where
    expr   : Nonterminal _ Char
    factor : Nonterminal _ Char

  grammar : Grammar Char Nonterminal
  grammar expr   = ! factor ⊛> sym '+' ⊛> ! expr
                 ∣ ! factor
  grammar factor = sym '0'
                 ∣ ! factor ⊛> sym '*' ⊛> sym '0'
                 ∣ sym '(' ⊛> ! expr <⊛ sym ')'
-}

module Ex₄ where

  -- The language aⁿbⁿcⁿ, which is not context free.

  -- The non-terminal top returns the number of 'a' characters parsed.

  data NT : ParserType₁ where
    top :              NT _ ℕ  -- top     ∷= aⁿbⁿcⁿ
    as  :         ℕ -> NT _ ℕ  -- as n    ∷= aˡ⁺¹bⁿ⁺ˡ⁺¹cⁿ⁺ˡ⁺¹
    bcs : Char -> ℕ -> NT _ ℕ  -- bcs x n ∷= xⁿ⁺¹

  grammar : Grammar Char NT
  grammar top             = return 0 ∣ ! as zero
  grammar (as n)          = suc <$ sym 'a' ⊛
                            ( ! as (suc n)
                            ∣ _+_ <$> ! bcs 'b' n ⊛ ! bcs 'c' n
                            )
  grammar (bcs c zero)    = sym c ⊛> return 0
  grammar (bcs c (suc n)) = sym c ⊛> ! bcs c n

  ex₁ : "aaabbbccc" ∈? (! top) / grammar ≡ 3 ∷ []
  ex₁ = refl

  ex₂ : "aaabbccc" ∈? (! top) / grammar ≡ []
  ex₂ = refl

module Ex₅ where

  -- A grammar making use of a parameterised parser from the library.

  data NT : ParserType₁ where
    a  : NT _ Char
    as : NT _ ℕ

  grammar : Grammar Char NT
  grammar a  = sym 'a'
  grammar as = length <$> ! a ⋆

  ex₁ : "aaaaa" ∈? (! as) / grammar ≡ 5 ∷ []
  ex₁ = refl

module Ex₆ where

  -- A grammar which uses the chain₁ combinator.

  data NT : ParserType₁ where
    op   : NT _ (ℕ -> ℕ -> ℕ)
    expr : Assoc -> NT _ ℕ

  grammar : Grammar Char NT
  grammar op       = _+_ <$ sym '+'
                   ∣ _*_ <$ sym '*'
                   ∣ _∸_ <$ sym '∸'
  grammar (expr a) = chain₁ a number (! op)

  ex₁ : "12345" ∈? number / grammar ≡ 12345 ∷ []
  ex₁ = refl

  ex₂ : "1+5*2∸3" ∈? (! expr left) / grammar ≡ 9 ∷ []
  ex₂ = refl

  ex₃ : "1+5*2∸3" ∈? (! expr right) / grammar ≡ 1 ∷ []
  ex₃ = refl

module Ex₇ where

  -- A proper expression example.

  data NT : ParserType₁ where
    expr   : NT _ ℕ
    term   : NT _ ℕ
    factor : NT _ ℕ
    addOp  : NT _ (ℕ -> ℕ -> ℕ)
    mulOp  : NT _ (ℕ -> ℕ -> ℕ)

  grammar : Grammar Char NT
  grammar expr     = chain₁ left (! term)   (! addOp)
  grammar term     = chain₁ left (! factor) (! mulOp)
  grammar factor   = sym '(' ⊛> ! expr <⊛ sym ')'
                   ∣ number
  grammar addOp    = _+_ <$ sym '+'
                   ∣ _∸_ <$ sym '∸'
  grammar mulOp    = _*_ <$ sym '*'

  ex₁ : "1+5*2∸3" ∈? (! expr) / grammar ≡ 8 ∷ []
  ex₁ = refl

  ex₂ : "1+5*(2∸3)" ∈? (! expr) / grammar ≡ 1 ∷ []
  ex₂ = refl

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module Logic.Leibniz where

-- Leibniz equality
_≡_ : {A : Set} -> A -> A -> Set1
x ≡ y = (P : _ -> Set) -> P x -> P y

≡-refl : {A : Set}(x : A) -> x ≡ x
≡-refl x P px = px

≡-sym : {A : Set}(x y : A) -> x ≡ y -> y ≡ x
≡-sym x y xy P py = xy (\z -> P z -> P x) (\px -> px) py

≡-trans : {A : Set}(x y z : A) -> x ≡ y -> y ≡ z -> x ≡ z
≡-trans x y z xy yz P px = yz P (xy P px)

≡-subst : {A : Set}(P : A -> Set)(x y : A) -> x ≡ y -> P x -> P y
≡-subst P _ _ xy = xy P

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- One form of induction for natural numbers
------------------------------------------------------------------------

-- I want universe polymorphism.

module Induction1.Nat where

open import Data.Nat
import Induction1.WellFounded as WF

------------------------------------------------------------------------
-- Complete induction based on <′

open WF _<′_ using (Acc; acc)

allAcc : ∀ n → Acc n
allAcc n = acc (helper n)
  where
  helper : ∀ n m → m <′ n → Acc m
  helper zero     _ ()
  helper (suc n) .n ≤′-refl        = acc (helper n)
  helper (suc n)  m (≤′-step m<′n) = helper n m m<′n

open WF _<′_ public using () renaming (WfRec to <-Rec)
open WF.All _<′_ allAcc public
  renaming ( wfRec-builder to <-rec-builder
           ; wfRec to <-rec
           )

max_issues_repo_name: larrytheliquid/Lemmachine


text:
-- Checks that UHC FFI calls using non-magic datatypes work
module UHC-FFI where

data Nat : Set where
  Zero : Nat
  Suc : Nat -> Nat
{-# COMPILE UHC Nat = data UHC.Agda.Builtins.Nat (Zero | Suc) #-}

{-# FOREIGN UHC __IMPORT__ Data.Char #-}

open import Common.IO
open import Common.Unit
open import Common.String
open import Common.Char

postulate toLower : Char -> Char
{-# COMPILE UHC toLower = Data.Char.toLower #-}

main : IO Unit
main = putStr (charToStr (toLower 'A'))

max_stars_repo_name: agda/agda-uhc

max_issues_repo_name: agda/agda-uhc

max_forks_repo_name: agda/agda-uhc


text:
-- Andreas, 2014-06-27, issue raised by fsfbugs
-- {-# OPTIONS -v interaction.give:10 -v tc:20 -v tc.conv.sort:30 #-}

open import Common.Level

record R (p r : Level) : Set (lsuc (p ⊔ r)) where
  field
    P   : Set p
    _~_ : P -> P -> Set r
    f   : (p p' : P) -> {!p ~ p'!}  -- Give (p ~ p') here!

-- PROBLEM WAS:
-- When issuing C-c C-SPC, Agda complains
--   Set (r ⊔ p) != Set (suc r ⊔ suc p)
-- even though removing the hole manually (by removing '{!' and '!}')
-- gives a well-typed definition.

-- REASON WAS:
-- Conversion.leqSort produced equality rather than subtyping constraint
-- upon postponement:
--   does (f : (p p' : P) → ?0 p r P _~_ p p') → f
--   of sort Setω
--   fit in Set (lsuc r ⊔ lsuc p) ?
--   adding constraint [0] dLub (Set p)
--                       (λ p → dLub (Set p) (λ p' → Set (_4 p r P _~_ p p')))
--                       == Set (lsuc r ⊔ lsuc p)

-- WORKS NOW


text:
module Unify-revised-correct where

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

open import Prelude.Function

postulate
  Nat : Set
  Term : Nat → Set
  _~>_ : Nat → Nat → Set -- Fin → Term
  _=>_ : Nat → Nat → Set -- Fin → Fin
  ε : ∀ {m n} → m ~> n
  ▹ : ∀ {m n} -> m => n -> m ~> n
  _◃_ : ∀ {m n} → m ~> n → Term m → Term n
  _≐_ : {m n : Nat} → (m ~> n) → (m ~> n) → Set
  ◃ext : ∀ {m n} {f g : m ~> n} → f ≐ g → ∀ t → f ◃ t ≡ g ◃ t
  _◇_ : ∀ {l m n : Nat} → m ~> n → l ~> m → l ~> n
  _◆_ : ∀ {l m n : Nat} → m ~> n → l => m → l ~> n
  ≐-cong : ∀ {m n o} {f : m ~> n} {g} (h : _ ~> o) → f ≐ g → (h ◇ f) ≐ (h ◇ g)
  ≐-sym : ∀ {m n} {f : m ~> n} {g} → f ≐ g → g ≐ f
  subFact1 : ∀ {n} → (t : Term n) → ε ◃ t ≡ t
  subFact2 : ∀ {l m n} → (f : m ~> n) (g : _) (t : Term l) → (f ◇ g) ◃ t ≡ f ◃ (g ◃ t)
  subFact3 : ∀ {l m n} (f : m ~> n) (r : l => m) -> f ◇ ▹ r ≡ f ◆ r

open import Prelude.Equality

◃ext' : ∀ {m n o} {f : m ~> n}{g : m ~> o}{h} -> f ≐ (h ◇ g) -> ∀ t -> f ◃ t ≡ h ◃ (g ◃ t)
◃ext' p t = trans (◃ext p t) (subFact2 _ _ t)


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.HasEquivalence
open import Oscar.Class.Reflexivity
open import Oscar.Class.Symmetry
open import Oscar.Class.Transitivity
open import Oscar.Class.IsEquivalence
open import Oscar.Data.ProductIndexEquivalence
import Oscar.Data.Constraint

module Oscar.Property.Setoid.ProductIndexEquivalence where

module _ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} {ℓ} ⦃ _ : HasEquivalence 𝔒 ℓ ⦄ where

  instance

    𝓡eflexivityExtensionṖropertyEquivalence : Reflexivity.class ProductIndexEquivalence⟦ 𝔒 / 𝔓 ⟧
    𝓡eflexivityExtensionṖropertyEquivalence .⋆ .π₀ = reflexivity

    𝓢ymmetryExtensionṖropertyEquivalence : Symmetry.class ProductIndexEquivalence⟦ 𝔒 / 𝔓 ⟧
    𝓢ymmetryExtensionṖropertyEquivalence .⋆ (∁ P≈Q) .π₀ = symmetry P≈Q

    𝓣ransitivityExtensionṖropertyEquivalence : Transitivity.class ProductIndexEquivalence⟦ 𝔒 / 𝔓 ⟧
    𝓣ransitivityExtensionṖropertyEquivalence .⋆ (∁ P≈Q) (∁ Q≈R) .π₀ = transitivity P≈Q Q≈R

    IsEquivalenceExtensionṖroperty : IsEquivalence ProductIndexEquivalence⟦ 𝔒 / 𝔓 ⟧
    IsEquivalenceExtensionṖroperty = ∁


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 LibraBFT.Impl.Consensus.EpochManagerTypes
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Dijkstra.EitherD
import      LibraBFT.Impl.Properties.Util             as Util
open import LibraBFT.Prelude
open import Optics.All

module LibraBFT.Impl.Handle.InitProperties where

module initHandlerSpec
  (pid : Author)
  (bsi : BootstrapInfo)
  where

  import      LibraBFT.Yasm.Types as LYT

  record ContractOk (rm : RoundManager) (acts : List (LYT.Action NetworkMsg)) : Set where
    constructor mkContractOk
    field
      rmInv   : Util.Invariants.RoundManagerInv rm
      sigs∈bs : ∀ {vs qc}
              → vs              ∈     qcVotes qc
              → qc Util.QCProps.∈RoundManager rm
              → ∈BootstrapInfo-impl bsi (proj₂ vs)
      -- During epoch initialisation, no messages are sent
      -- EXCEPT the leader of Round 1 SENDS a ProposalMsg during initialization.
      -- Rust/Haskell impls do not include signatures in the genesis QC's LIWS.
      -- The initial proposal for (Epoch N) (Round 1) is built on a QC with empty signatures.
      isInitPM : ∀ {m}
               → LYT.send m ∈ acts
               → ∃[ pm ] ( m ≡ P pm
                         × ∀ {vs qc}
                           → vs   ∈ qcVotes qc
                           → qc QC∈NM       m
                           → ⊥)
      sdLVNothing : rm ^∙ rmSafetyRules ∙ srPersistentStorage
                        ∙ pssSafetyData ∙ sdLastVote ≡ nothing

  Contract : Maybe (RoundManager × List (LYT.Action NetworkMsg)) → Set
  Contract nothing            = ⊤
  Contract (just (rm , acts)) = ContractOk rm acts

  import      LibraBFT.Impl.Handle as Handle
  open        Handle.InitHandler

  postulate
    contract : ∀ {x} → initHandler pid bsi ≡ x → Contract x
    -- contract = EitherD-contract {!!} Contract contract'

max_stars_repo_name: oracle/bft-consensus-agda

max_issues_repo_name: oracle/bft-consensus-agda

max_forks_repo_name: oracle/bft-consensus-agda


text:
module Basic where

open import Level
open import Data.Product
open import Relation.Binary
open Setoid renaming (_≈_ to eqSetoid)

module Map where
  record Map {c₀ c₀′ ℓ ℓ′ : Level} (A : Setoid c₀ ℓ) (B : Setoid c₀′ ℓ′) : Set (suc (c₀ ⊔ ℓ ⊔ c₀′ ⊔ ℓ′)) where
    field
      mapping : Carrier A → Carrier B
      preserveEq : {x y : Carrier A} → (eqSetoid A x y) → eqSetoid B (mapping x) (mapping y)

  open Map public

  equality : {c₀ ℓ : Level} {A B : Setoid c₀ ℓ} (f g : Map A B) → Set _
  equality {A = A} {B = B} f g = ∀(x : Carrier A) → eqSetoid B (mapping f x) (mapping g x)

  compose : {c₀ ℓ : Level} {A B C : Setoid c₀ ℓ} (f : Map B C) (g : Map A B) → Map A C
  compose {C = C} f g = record {
    mapping = λ x → mapping f (mapping g x);
    preserveEq = λ x₁ → (preserveEq f (preserveEq g x₁)) }

  identity : {c₀ ℓ : Level} {A : Setoid c₀ ℓ} → Map A A
  identity = record { mapping = λ x → x ; preserveEq = λ x₁ → x₁ }

  subst : ∀{c₀ ℓ} {A B : Setoid c₀ ℓ} {f g : Map A B} (a : Carrier A) → equality f g → eqSetoid B (mapping f a) (mapping g a)
  subst a eq = eq a

LiftSetoid : ∀ {a b ℓ ℓ′} (A : Setoid a ℓ) → Setoid (a ⊔ b) (ℓ ⊔ ℓ′)
LiftSetoid {a} {b} {ℓ} {ℓ′} A = record {
  Carrier = Lift {a} {b} (Carrier A) ;
  _≈_ = λ x x₁ → Lift {ℓ} {ℓ′} (eqSetoid A (lower x) (lower x₁)) ;
  isEquivalence = record {
    refl = lift (refl A) ;
    sym = λ x → lift (sym A (lower x)) ;
    trans = λ x x₁ → lift (trans A (lower x) (lower x₁)) } }

liftMap : {c₀ c₀′ d ℓ ℓ′ ℓ″ : Level} {A : Setoid c₀ ℓ} {B : Setoid c₀′ ℓ′} → (f : Map.Map A B) → Map.Map (LiftSetoid {_} {c₀ ⊔ d} {_} {ℓ ⊔ ℓ″} A) (LiftSetoid {_} {c₀′ ⊔ d} {_} {ℓ′ ⊔ ℓ″} B)
liftMap f = record {
  mapping = λ x → lift (Map.mapping f (lower x)) ;
  preserveEq = λ x≈y → lift (Map.preserveEq f (lower x≈y)) }

lowerMap : {c₀ c₀′ d ℓ ℓ′ ℓ″ : Level} {A : Setoid c₀ ℓ} {B : Setoid c₀′ ℓ′} → (f : Map.Map (LiftSetoid {_} {c₀ ⊔ d} {_} {ℓ ⊔ ℓ″} A) (LiftSetoid {_} {c₀′ ⊔ d} {_} {ℓ′ ⊔ ℓ″} B)) → Map.Map A B
lowerMap f = record {
  mapping = λ x → lower (Map.mapping f (lift x)) ;
  preserveEq = λ x≈y → lower (Map.preserveEq f (lift x≈y)) }

max_stars_repo_name: myuon/agda-cate

max_issues_repo_name: myuon/agda-cate

max_forks_repo_name: myuon/agda-cate


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

open import HoTT
open import cohomology.Theory
open import groups.ExactSequence
open import groups.Exactness
open import groups.HomSequence
open import groups.KernelImageUniqueFactorization
import cw.cohomology.GridPtdMap as GPM

open import cw.CW

module cw.cohomology.HigherCohomologyGroupsOnDiag {i} (OT : OrdinaryTheory i)
  {n} (⊙skel : ⊙Skeleton {i} (S (S n))) (ac : ⊙has-cells-with-choice 0 ⊙skel i) where

private
  n≤SSn : n ≤ S (S n)
  n≤SSn = lteSR lteS

  ⊙skel₋₁ = ⊙cw-init ⊙skel
  ac₋₁ = ⊙init-has-cells-with-choice ⊙skel ac

  ⊙skel₋₂ = ⊙cw-take n≤SSn ⊙skel
  ac₋₂ = ⊙take-has-cells-with-choice n≤SSn ⊙skel ac

open OrdinaryTheory OT
open import cw.cohomology.Descending OT
open import cw.cohomology.WedgeOfCells OT
open import cw.cohomology.HigherCoboundary OT ⊙skel
open import cw.cohomology.HigherCoboundaryGrid OT ⊙skel ac

{-

   Coker ≃ C(X₂/X₀) ≃ C(X)
              ^
              |
              |
           C(X₁/X₀)
             WoC

    WoC := Wedges of Cells
-}

private

  C-apex : Group i
  C-apex = C (ℕ-to-ℤ (S (S n))) (⊙Cofiber (⊙cw-incl-tail n≤SSn ⊙skel))

  open import cohomology.LongExactSequence cohomology-theory
    (ℕ-to-ℤ (S n)) (⊙cw-incl-tail n≤SSn ⊙skel)

  C-apex-iso-C-cw : C-apex ≃ᴳ C (ℕ-to-ℤ (S (S n))) ⊙⟦ ⊙skel ⟧
  C-apex-iso-C-cw = Exact2.G-trivial-and-L-trivial-implies-H-iso-K
    (exact-seq-index 1 C-cofiber-exact-seq)
    (exact-seq-index 2 C-cofiber-exact-seq)
    (C-cw-at-higher ⊙skel₋₂ ltS ac₋₂)
    (C-cw-at-higher ⊙skel₋₂ (ltSR ltS) ac₋₂)

open import groups.KernelImage (cst-hom {H = Lift-group {j = i} Unit-group}) cw-co∂-last
  (CXₙ/Xₙ₋₁-is-abelian ⊙skel (ℕ-to-ℤ (S (S n))))
open import groups.KernelCstImage (Lift-group {j = i} Unit-group) cw-co∂-last
  (CXₙ/Xₙ₋₁-is-abelian ⊙skel (ℕ-to-ℤ (S (S n))))

C-cw-iso-ker/im : C (ℕ-to-ℤ (S (S n))) ⊙⟦ ⊙skel ⟧ ≃ᴳ Ker/Im
C-cw-iso-ker/im = (C-apex-iso-C-cw ∘eᴳ Coker-cw-co∂-last ∘eᴳ Ker-cst-quot-Im) ⁻¹ᴳ

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module BasicIPC.Metatheory.ClosedHilbert-TarskiGluedClosedImplicit where

open import BasicIPC.Syntax.ClosedHilbert public
open import BasicIPC.Semantics.TarskiGluedClosedImplicit public

open ImplicitSyntax (⊢_) public

-- Completeness with respect to a particular model.

module _ {{_ : Model}} where
  reify : ∀ {A} → ⊩ A → ⊢ A
  reify {α P}   s = syn s
  reify {A ▻ B} s = syn s
  reify {A ∧ B} s = pair (reify (π₁ s)) (reify (π₂ s))
  reify {⊤}    s = unit

-- Additional useful equipment.

module _ {{_ : Model}} where
  ⟪K⟫ : ∀ {A B} → ⊩ A → ⊩ B ▻ A
  ⟪K⟫ a = app ck (reify a) ⅋ K a

  ⟪S⟫′ : ∀ {A B C} → ⊩ A ▻ B ▻ C → ⊩ (A ▻ B) ▻ A ▻ C
  ⟪S⟫′ s₁ = app cs (reify s₁) ⅋ λ s₂ →
              app (app cs (reify s₁)) (reify s₂) ⅋ ⟪S⟫ s₁ s₂

  _⟪,⟫′_ : ∀ {A B} → ⊩ A → ⊩ B ▻ A ∧ B
  _⟪,⟫′_ a = app cpair (reify a) ⅋ _,_ a

-- Soundness with respect to all models, or evaluation, for closed terms only.

eval₀ : ∀ {A} → ⊢ A → ⊨ A
eval₀ (app t u) = eval₀ t ⟪$⟫ eval₀ u
eval₀ ci        = ci ⅋ I
eval₀ ck        = ck ⅋ ⟪K⟫
eval₀ cs        = cs ⅋ ⟪S⟫′
eval₀ cpair     = cpair ⅋ _⟪,⟫′_
eval₀ cfst      = cfst ⅋ π₁
eval₀ csnd      = csnd ⅋ π₂
eval₀ unit      = ∙

-- Correctness of evaluation with respect to conversion.

eval₀✓ : ∀ {{_ : Model}} {A} {t t′ : ⊢ A} → t ⋙ t′ → eval₀ t ≡ eval₀ t′
eval₀✓ refl⋙           = refl
eval₀✓ (trans⋙ p q)    = trans (eval₀✓ p) (eval₀✓ q)
eval₀✓ (sym⋙ p)        = sym (eval₀✓ p)
eval₀✓ (congapp⋙ p q)  = cong² _⟪$⟫_ (eval₀✓ p) (eval₀✓ q)
eval₀✓ (congi⋙ p)      = cong I (eval₀✓ p)
eval₀✓ (congk⋙ p q)    = cong² K (eval₀✓ p) (eval₀✓ q)
eval₀✓ (congs⋙ p q r)  = cong³ ⟪S⟫ (eval₀✓ p) (eval₀✓ q) (eval₀✓ r)
eval₀✓ (congpair⋙ p q) = cong² _,_ (eval₀✓ p) (eval₀✓ q)
eval₀✓ (congfst⋙ p)    = cong π₁ (eval₀✓ p)
eval₀✓ (congsnd⋙ p)    = cong π₂ (eval₀✓ p)
eval₀✓ beta▻ₖ⋙         = refl
eval₀✓ beta▻ₛ⋙         = refl
eval₀✓ beta∧₁⋙         = refl
eval₀✓ beta∧₂⋙         = refl
eval₀✓ eta∧⋙           = refl
eval₀✓ eta⊤⋙          = refl

-- The canonical model.

private
  instance
    canon : Model
    canon = record
      { ⊩ᵅ_ = λ P → ⊢ α P
      }

-- Completeness with respect to all models, or quotation, for closed terms only.

quot₀ : ∀ {A} → ⊨ A → ⊢ A
quot₀ s = reify s

-- Normalisation by evaluation, for closed terms only.

norm₀ : ∀ {A} → ⊢ A → ⊢ A
norm₀ = quot₀ ∘ eval₀

-- Correctness of normalisation with respect to conversion.

norm₀✓ : ∀ {{_ : Model}} {A} {t t′ : ⊢ A} → t ⋙ t′ → norm₀ t ≡ norm₀ t′
norm₀✓ p = cong reify (eval₀✓ p)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module resugar where
open import cedille-types
open import general-util
open import syntax-util
open import type-util

{-# TERMINATING #-}
resugar : ∀ {ed} → ⟦ ed ⟧ → ⟦ ed ⟧'
resugar-tk : tpkd → ex-tk

resugar {TERM} (App t t') =
  ExApp (resugar t) ff (resugar t')
resugar {TERM} (AppE t tT) =
  either-else' tT (ExApp (resugar t) tt ∘ resugar) (ExAppTp (resugar t) ∘ resugar)
resugar {TERM} (Beta t t') =
  ExBeta pi-gen (just (PosTm (resugar t) pi-gen)) (just (PosTm (resugar t') pi-gen))
resugar {TERM} (Delta b? T t) =
  ExDelta pi-gen (just (resugar T)) (resugar t)
resugar {TERM} (Hole pi) =
  ExHole pi
resugar {TERM} (IotaPair t₁ t₂ x Tₓ) =
  ExIotaPair pi-gen (resugar t₁) (resugar t₂) (just (ExGuide pi-gen x (resugar Tₓ))) pi-gen
resugar {TERM} (IotaProj t n) =
  ExIotaProj (resugar t) (if n iff ι1 then "1" else "2") pi-gen
resugar {TERM} (Lam me x tk? t) =
  ExLam pi-gen me pi-gen x (maybe-map resugar-tk tk?) (resugar t)
resugar {TERM} (LetTm me x T? t t') =
  ExLet pi-gen me (ExDefTerm pi-gen x (maybe-map resugar T?) (resugar t)) (resugar t')
resugar {TERM} (LetTp x k T t) =
  ExLet pi-gen tt (ExDefType pi-gen x (resugar k) (resugar T)) (resugar t)
resugar {TERM} (Phi t₌ t₁ t₂) =
  ExPhi pi-gen (resugar t₌) (resugar t₁) (resugar t₂) pi-gen
resugar {TERM} (Rho t₌ x Tₓ t) =
  ExRho pi-gen ff nothing (resugar t₌) (just (ExGuide pi-gen x (resugar Tₓ))) (resugar t)
resugar {TERM} (Sigma t) =
  ExSigma pi-gen (resugar t)
resugar {TERM} (Mu μ t Tₘ? f~ ms) =
  ExMu
    pi-gen
    (either-else' μ (λ t → ExIsMu' (resugar <$> t)) (ExIsMu pi-gen))
    (resugar t)
    (maybe-map resugar Tₘ?)
    pi-gen
    (map (λ {(Case x cas t _) → ExCase pi-gen x
      (map (λ {(CaseArg me x tk?) →
        let me' = case (me , tk?) of uncurry λ where
                    ff _ → ExCaseArgTm
                    tt (just (Tkk _)) → ExCaseArgTp
                    tt _ → ExCaseArgEr in
        ExCaseArg me' pi-gen x}) cas) (resugar t)}) ms)
    pi-gen
resugar {TERM} (Var x) =
  ExVar pi-gen x

resugar {TYPE} (TpAbs me x tk T) =
  ExTpAbs pi-gen me pi-gen x (resugar-tk tk) (resugar T)
resugar {TYPE} (TpApp T tT) =
  either-else' tT (ExTpAppt (resugar T) ∘ resugar) (ExTpApp (resugar T) ∘ resugar)
resugar {TYPE} (TpEq t₁ t₂) =
  ExTpEq pi-gen (resugar t₁) (resugar t₂) pi-gen
resugar {TYPE} (TpHole pi) =
  ExTpHole pi
resugar {TYPE} (TpIota x T₁ T₂) =
  ExTpIota pi-gen pi-gen x (resugar T₁) (resugar T₂)
resugar {TYPE} (TpLam x tk T) =
  ExTpLam pi-gen pi-gen x (resugar-tk tk) (resugar T)
resugar {TYPE} (TpVar x) =
  ExTpVar pi-gen x

resugar {KIND} (KdAbs x tk k) =
  ExKdAbs pi-gen pi-gen x (resugar-tk tk) (resugar k)
resugar {KIND} (KdHole pi) =
  ExKdHole pi
resugar {KIND} KdStar =
  ExKdStar pi-gen

resugar-tk = either-else (ExTkt ∘ resugar) (ExTkk ∘ resugar)

max_stars_repo_name: zmthy/cedille

max_issues_repo_name: zmthy/cedille

max_forks_repo_name: zmthy/cedille


text:
open import Prelude

module Implicits.Resolution.GenericFinite.Algorithm.Completeness where

open import Induction.WellFounded
open import Induction.Nat
open import Data.Fin.Substitution
open import Data.Nat.Base using (_<′_)
open import Data.Maybe as Maybe
open import Data.Nat hiding (_<_)
open import Data.Nat.Properties
open import Relation.Binary using (module DecTotalOrder)
open DecTotalOrder decTotalOrder using () renaming (refl to ≤-refl; trans to ≤-trans)
open import Data.Unit

open import Implicits.Syntax
open import Implicits.Syntax.Type.Unification
open import Implicits.Syntax.Type.Unification.Lemmas as mgu hiding (complete)
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas
open import Implicits.Resolution.GenericFinite.Resolution
open import Implicits.Resolution.GenericFinite.Algorithm
open import Implicits.Resolution.GenericFinite.TerminationCondition
open import Implicits.Resolution.Termination

open import Extensions.Bool as Bool

private
  module M = MetaTypeMetaSubst

module ResolutionComplete (cond : TerminationCondition) where

  open TerminationCondition cond
  open ResolutionAlgorithm cond
  open ResolutionRules cond

  open Lemmas

  lemx : ∀ {ν m} {Δ : ICtx ν} {Φ} r c τ (u : M.MetaSub MetaType ν m zero) →
        Δ , Φ ⊢ from-meta (r M./ u M.↑tp) tp[/tp c ] ↓ τ →
        Δ , Φ ⊢ from-meta (open-meta r M./ (to-meta c ∷ u)) ↓ τ
  lemx r c τ u p = {!!}

  mutual
    match'-complete : ∀ {ν m} (Δ : ICtx ν) (Φ : TCtx) τ (r : MetaType m ν) →
                  (Φ↓ : T-Acc Φ) → (m↓ : m<-Acc r) →
                  (∃ λ u → Δ , Φ ⊢ from-meta (r M./ u) ↓ τ) →
                  Is-just (match' Δ Φ τ r Φ↓ m↓)

    match'-complete Δ Φ τ (a ⇒ b) f (acc g) (proj₁ , i-iabs x y b↓τ)
      with match' Δ Φ τ b f (g _ (b-m<-a⇒b a b))
         | match'-complete Δ Φ τ b f (g _ (b-m<-a⇒b a b)) (, b↓τ)
    match'-complete Δ Φ τ (a ⇒ b) f (acc g) (u , i-iabs x y b↓τ) | nothing | ()
    match'-complete Δ Φ τ (a ⇒ b) f (acc g) (u , i-iabs x₁ y b↓τ) | just u' | just px
      with (step Φ Δ (from-meta (a M./ u)) (from-meta (b M./ u)) τ) <? Φ
    match'-complete Δ Φ τ (a ⇒ b) f (acc g) (u , i-iabs x₁ y b↓τ) | just u' | just px | yes p = {!!}
    match'-complete Δ Φ τ (a ⇒ b) f (acc g) (u , i-iabs x₁ y b↓τ) | just u' | just px | no ¬p = {!¬p!}
    -- match'-complete Δ Φ τ (a ⇒ b) (acc f) (acc g) | just u | yes Φ<
      -- with resolve' Δ (step Φ Δ (from-meta (a M./ u)) (from-meta (b M./ u)) τ)
                    -- (from-meta (a M./ u)) (f _ Φ<)
    -- match'-complete Δ Φ τ (a ⇒ b) (acc f) (acc g) | just u | yes Φ< | true = just u
    -- match'-complete Δ Φ τ (a ⇒ b) (acc f) (acc g) | just u | yes Φ< | false = nothing
    -- match'-complete Δ Φ τ (a ⇒ b) (acc f) (acc g) | just u | no φ> = nothing

    match'-complete Δ Φ τ (∀' r) Φ↓ (acc m↓) (u , i-tabs b open-r↓τ)
      with match'          Δ Φ τ (open-meta r) Φ↓ (m↓ _ (open-meta-a-m<-∀'a r))
         | match'-complete Δ Φ τ (open-meta r) Φ↓ (m↓ _ (open-meta-a-m<-∀'a r))
                           (, lemx r b τ u open-r↓τ)
    match'-complete Δ Φ τ (∀' r) Φ↓ (acc m↓) (u , i-tabs b open-r↓τ) | just x | just px = just tt
    match'-complete Δ Φ τ (∀' r) Φ↓ (acc m↓) (u , i-tabs b open-r↓τ) | nothing | ()
    match'-complete Δ Φ .(tvar x) (simpl (tvar x)) Φ↓ m↓ (u , i-simp .(tvar x)) =
      mgu.complete (simpl (tvar x)) (tvar x) u refl
    match'-complete Δ Φ τ (simpl (mvar x)) Φ↓ m↓ (u , proj₂) =
      let (u' , u'-uni) = mvar-unifiable x τ in mgu.complete (simpl (mvar x)) τ u' u'-uni
    match'-complete Δ Φ ._ (simpl (a →' b)) Φ↓ m↓ (u , i-simp ._) =
      mgu.complete (simpl (a →' b)) _ u refl
    match'-complete Δ Φ .(tc x) (simpl (tc x)) Φ↓ m↓ (u , ResolutionRules.i-simp .(tc x)) =
      mgu.complete (simpl (tc x)) _ u refl

    match-complete : ∀ {ν} (Δ : ICtx ν) (Φ : TCtx) → (τ : SimpleType ν) → (r : Type ν) →
                     (Φ↓ : T-Acc Φ) →
                     Δ , Φ ⊢ r ↓ τ →
                     Is-true (match Δ Φ τ r Φ↓)
    match-complete Δ Φ τ r Φ↓ p
      with match'          Δ Φ τ (to-meta {zero} r) Φ↓ (m<-well-founded _)
         | match'-complete Δ Φ τ (to-meta {zero} r) Φ↓ (m<-well-founded _)
                           ([] , subst (λ z → Δ , Φ ⊢ z ↓ τ) (sym $ from-to-meta-/-vanishes) p)
    match-complete Δ Φ τ r Φ↓ p | just x | just px = true tt
    match-complete Δ Φ τ r Φ↓ p | nothing | ()

    match1st-complete : ∀ {ν} (Δ : ICtx ν) (Φ : TCtx) (ρs : ICtx ν) → (τ : SimpleType ν) →
                        (Φ↓ : T-Acc Φ) →
                        (∃ λ r → r List.∈ ρs × Δ , Φ ⊢ r ↓ τ) →
                        Is-true (match1st Δ Φ ρs τ Φ↓)
    match1st-complete Δ Φ List.[] τ Φ↓ (_ , () , _)
    match1st-complete Δ Φ (x List.∷ ρs) τ Φ↓ (.x , here refl , r↓τ)
      with match            Δ Φ τ x Φ↓
         | match-complete   Δ Φ τ x Φ↓ r↓τ
    match1st-complete Δ Φ (x List.∷ ρs) τ Φ↓ (.x , here refl , r↓τ) | true | true _ = true tt
    match1st-complete Δ Φ (x List.∷ ρs) τ Φ↓ (.x , here refl , r↓τ) | false | ()
    match1st-complete Δ Φ (x List.∷ ρs) τ Φ↓ (proj₁ , there p , r↓τ) with match Δ Φ τ x Φ↓
    match1st-complete Δ Φ (x List.∷ ρs) τ Φ↓ (r , there r∈ρs , r↓τ) | true  = true tt
    match1st-complete Δ Φ (x List.∷ ρs) τ Φ↓ (r , there r∈ρs , r↓τ) | false =
      match1st-complete Δ Φ ρs τ Φ↓ (r , r∈ρs , r↓τ)

    complete' : ∀ {ν} (Δ : ICtx ν) Φ {r} → (Φ↓ : T-Acc Φ) → Δ , Φ ⊢ᵣ r → Is-true (resolve' Δ Φ r Φ↓)
    complete' Δ Φ Φ↓ (r-simp x∈Δ x↓τ) = match1st-complete Δ Φ Δ _ Φ↓ (_ , x∈Δ , x↓τ)
    complete' Δ Φ Φ↓ (r-iabs ρ₁ p) = complete' (ρ₁ List.∷ Δ) Φ Φ↓ p
    complete' Δ Φ Φ↓ (r-tabs p) = complete' (ictx-weaken Δ) Φ Φ↓ p

    complete : ∀ {ν} (Δ : ICtx ν) Φ {r} → (Φ↓ : T-Acc Φ) → Δ , Φ ⊢ᵣ r → Is-true (resolve Δ Φ r)
    complete Δ Φ Φ↓ p = complete' Δ Φ (wf-< _) p


text:
------------------------------------------------------------------------
-- A well-typed representation of a dependently typed language
------------------------------------------------------------------------

-- The code is parametrised by an arbitrary (small, unindexed)
-- universe.

import Level
open import Data.Universe

module README.DependentlyTyped.Term
  (Uni₀ : Universe Level.zero Level.zero)
  where

open import Data.Product as Prod renaming (curry to c; uncurry to uc)
open import Data.Unit
open import Data.Universe.Indexed
import deBruijn.Context
open import Function hiding (_∋_) renaming (const to k)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- Wrapper types

-- Used to make El "constructor-headed", which in turn makes Agda
-- infer more types for us.

record U₀ : Set where
  field a : Universe.U Uni₀

record El₀ (a : U₀) : Set where
  field El : Universe.El Uni₀ (U₀.a a)

------------------------------------------------------------------------
-- An indexed universe

-- A type which represents the "spine" of a universe code (or type).

data Spine : Set where
  ⋆ el : Spine
  π    : (sp₁ sp₂ : Spine) → Spine

-- The universe contains the universe above and is closed under
-- Π-types.
--
-- The universe could be defined using induction-recursion, but the
-- following recursive definition has the advantage that more things
-- are definitionally equal. Previously I used induction-recursion,
-- and then I proved π-fst-snd (below) using the assumption of
-- extensionality of functions, and I used a cast in the definition of
-- README.DependentlyTyped.NBE.Value.řeflect.
--
-- TODO: Find out if the use of spines is compatible with large
-- elimination.

mutual

  U : Spine → Set
  U ⋆           = ⊤
  U el          = U₀
  U (π sp₁ sp₂) = Σ (U sp₁) λ a → El a → U sp₂

  El : ∀ {sp} → U sp → Set
  El {⋆}         _       = U₀
  El {el}        a       = El₀ a
  El {π sp₁ sp₂} (a , b) = (x : El a) → El (b x)

Uni : IndexedUniverse _ _ _
Uni = record { I = Spine; U = U; El = El }

-- Some synonyms/specialisations.

U-⋆ : U ⋆
U-⋆ = _

U-el : U₀ → U el
U-el = id

U-π : ∀ {sp₁} {sp₂} (a : U sp₁) → (El a → U sp₂) → U (π sp₁ sp₂)
U-π = _,_

------------------------------------------------------------------------
-- Contexts and variables

-- We get these for free.

open deBruijn.Context Uni public
  renaming (_·_ to _⊙_; ·-cong to ⊙-cong)

-- Some abbreviations.

IType-π : ∀ {Γ} (σ : Type Γ) (τ : Type (Γ ▻ σ)) →
          IType Γ (π (index σ) (index τ))
IType-π σ τ = k U-π ˢ indexed-type σ ˢ c (indexed-type τ)

Type-π : ∀ {Γ} (σ : Type Γ) → Type (Γ ▻ σ) → Type Γ
Type-π σ τ = -, IType-π σ τ

------------------------------------------------------------------------
-- Projections

-- Types with π-spines can be split up into a first and a second part.

ifst : ∀ {Γ sp₁ sp₂} → IType Γ (π sp₁ sp₂) → IType Γ sp₁
ifst σ γ = proj₁ (σ γ)

fst : ∀ {Γ sp₁ sp₂} → IType Γ (π sp₁ sp₂) → Type Γ
fst σ = -, ifst σ

isnd : ∀ {Γ sp₁ sp₂} (σ : IType Γ (π sp₁ sp₂)) →
       IType (Γ ▻ fst σ) sp₂
isnd σ (γ , v) = proj₂ (σ γ) v

snd : ∀ {Γ sp₁ sp₂} (σ : IType Γ (π sp₁ sp₂)) → Type (Γ ▻ fst σ)
snd σ = -, isnd σ

-- The split is correct.

π-fst-snd : ∀ {Γ sp₁ sp₂} (σ : IType Γ (π sp₁ sp₂)) →
            σ ≡ IType-π (fst σ) (snd σ)
π-fst-snd σ = P.refl

------------------------------------------------------------------------
-- Well-typed terms

mutual

  infixl 9 _·_
  infix  3 _⊢_

  -- Terms.

  data _⊢_ (Γ : Ctxt) : Type Γ → Set where
    var : ∀ {σ} (x : Γ ∋ σ) → Γ ⊢ σ
    ƛ   : ∀ {σ τ} (t : Γ ▻ σ ⊢ τ) → Γ ⊢ Type-π σ τ
    _·_ : ∀ {sp₁ sp₂ σ}
          (t₁ : Γ ⊢ π sp₁ sp₂ , σ) (t₂ : Γ ⊢ fst σ) →
          Γ ⊢ snd σ /̂ ŝub ⟦ t₂ ⟧

  -- Semantics of terms.

  ⟦_⟧ : ∀ {Γ σ} → Γ ⊢ σ → Value Γ σ
  ⟦ var x   ⟧ γ = lookup x γ
  ⟦ ƛ t     ⟧ γ = λ v → ⟦ t ⟧ (γ , v)
  ⟦ t₁ · t₂ ⟧ γ = (⟦ t₁ ⟧ γ) (⟦ t₂ ⟧ γ)

-- Terms are "term-like".

Tm : Term-like _
Tm = record { _⊢_ = _⊢_; ⟦_⟧ = ⟦_⟧ }

open Term-like Tm public hiding (_⊢_; ⟦_⟧)

------------------------------------------------------------------------
-- Syntactic contexts and types

-- Syntactic types.

infix 3 _⊢_type

data _⊢_type (Γ : Ctxt) : Type Γ → Set where
  ⋆  : Γ ⊢ -, k U-⋆ type
  el : (t : Γ ⊢ -, k U-⋆) → Γ ⊢ -, k U-el ˢ ⟦ t ⟧ type
  π  : ∀ {sp₁ sp₂ σ τ}
       (σ′ : Γ ⊢ sp₁ , σ type) (τ′ : Γ ▻ (-, σ) ⊢ sp₂ , τ type) →
       Γ ⊢ -, k U-π ˢ σ ˢ c τ type

-- Syntactic contexts.

infixl 5 _▻_
infix  3 _ctxt

data _ctxt : Ctxt → Set where
  ε   : ε ctxt
  _▻_ : ∀ {Γ σ} (Γ′ : Γ ctxt) (σ′ : Γ ⊢ σ type) → Γ ▻ σ ctxt

-- Semantics of types.

⟦_⟧type : ∀ {Γ σ} → Γ ⊢ σ type → Type Γ
⟦_⟧type {σ = σ} _ = σ

-- We can project out the first and second components of a syntactic
-- Π-type.

fst′ : ∀ {Γ sp₁ sp₂} {σ : IType Γ (π sp₁ sp₂)} →
       Γ ⊢ -, σ type → Γ ⊢ fst σ type
fst′ (π σ′ τ′) = σ′

snd′ : ∀ {Γ sp₁ sp₂} {σ : IType Γ (π sp₁ sp₂)} →
       Γ ⊢ -, σ type → Γ ▻ fst σ ⊢ snd σ type
snd′ (π σ′ τ′) = τ′

------------------------------------------------------------------------
-- Examples

-- The polymorphic identity function.

identity : ∀ {Γ} →
           Γ ⊢ ⟦ π ⋆ (π (el (var zero)) (el (var (suc zero)))) ⟧type
identity = ƛ {σ = ⟦ ⋆ ⟧type} (ƛ {σ = ⟦ el (var zero) ⟧type} (var zero))

-- The polymorphic identity function, with the type written in a less
-- compact way.

identity′ : ∀ {Γ} →
            Γ ⊢ -, k U-π ˢ k U-⋆ ˢ
                           c (k U-π ˢ (k U-el ˢ ⟦ var zero ⟧) ˢ
                                      c (k U-el ˢ ⟦ var (suc zero) ⟧))
identity′ = ƛ {σ = ⟦ ⋆ ⟧type} (ƛ {σ = ⟦ el (var zero) ⟧type} (var zero))

-- The polymorphic identity function applied to some variables from
-- the context.

identity· : ∀ {Γ} → Γ ▻ ⟦ ⋆ ⟧type ▻ ⟦ el (var zero) ⟧type ⊢
                    ⟦ el (var (suc zero)) ⟧type
identity· =
  ƛ {σ = ⟦ ⋆ ⟧type} (ƛ {σ = ⟦ el (var zero) ⟧type} (var zero)) ·
  var (suc zero) · var zero

------------------------------------------------------------------------
-- Equality

-- Syntactic type telescopes.

record [type] : Set where
  constructor [_]
  field
    {Γ} : Ctxt
    {σ} : Type Γ
    σ′  : Γ ⊢ σ type

-- Equality of syntactic types.

infix 4 _≅-type_

_≅-type_ : ∀ {Γ₁ σ₁} (σ′₁ : Γ₁ ⊢ σ₁ type)
             {Γ₂ σ₂} (σ′₂ : Γ₂ ⊢ σ₂ type) → Set
σ′₁ ≅-type σ′₂ = _≡_ {A = [type]} [ σ′₁ ] [ σ′₂ ]

-- If the indices are equal, then _≅-type_ coincides with _≡_.

≅-type-⇒-≡ : ∀ {Γ σ} {σ′₁ σ′₂ : Γ ⊢ σ type} →
             σ′₁ ≅-type σ′₂ → σ′₁ ≡ σ′₂
≅-type-⇒-≡ P.refl = P.refl

-- Certain uses of substitutivity can be removed.

drop-subst-⊢-type :
  ∀ {a} {A : Set a} {x₁ x₂ : A} {Γ}
  (f : A → Type Γ) {σ′} (eq : x₁ ≡ x₂) →
  P.subst (λ x → Γ ⊢ f x type) eq σ′ ≅-type σ′
drop-subst-⊢-type f P.refl = P.refl

-- Some congruence lemmas.

IType-π-cong : ∀ {Γ₁ σ₁} {τ₁ : Type (Γ₁ ▻ σ₁)}
                 {Γ₂ σ₂} {τ₂ : Type (Γ₂ ▻ σ₂)} →
               τ₁ ≅-Type τ₂ → IType-π σ₁ τ₁ ≅-IType IType-π σ₂ τ₂
IType-π-cong P.refl = P.refl

Type-π-cong : ∀ {Γ₁ σ₁} {τ₁ : Type (Γ₁ ▻ σ₁)}
                {Γ₂ σ₂} {τ₂ : Type (Γ₂ ▻ σ₂)} →
              τ₁ ≅-Type τ₂ → Type-π σ₁ τ₁ ≅-Type Type-π σ₂ τ₂
Type-π-cong P.refl = P.refl

ifst-cong : ∀ {Γ₁ sp₁₁ sp₂₁} {σ₁ : IType Γ₁ (π sp₁₁ sp₂₁)}
              {Γ₂ sp₁₂ sp₂₂} {σ₂ : IType Γ₂ (π sp₁₂ sp₂₂)} →
            σ₁ ≅-IType σ₂ → ifst σ₁ ≅-IType ifst σ₂
ifst-cong P.refl = P.refl

fst-cong : ∀ {Γ₁ sp₁₁ sp₂₁} {σ₁ : IType Γ₁ (π sp₁₁ sp₂₁)}
             {Γ₂ sp₁₂ sp₂₂} {σ₂ : IType Γ₂ (π sp₁₂ sp₂₂)} →
           σ₁ ≅-IType σ₂ → fst σ₁ ≅-Type fst σ₂
fst-cong P.refl = P.refl

isnd-cong : ∀ {Γ₁ sp₁₁ sp₂₁} {σ₁ : IType Γ₁ (π sp₁₁ sp₂₁)}
              {Γ₂ sp₁₂ sp₂₂} {σ₂ : IType Γ₂ (π sp₁₂ sp₂₂)} →
            σ₁ ≅-IType σ₂ → isnd σ₁ ≅-IType isnd σ₂
isnd-cong P.refl = P.refl

snd-cong : ∀ {Γ₁ sp₁₁ sp₂₁} {σ₁ : IType Γ₁ (π sp₁₁ sp₂₁)}
             {Γ₂ sp₁₂ sp₂₂} {σ₂ : IType Γ₂ (π sp₁₂ sp₂₂)} →
           σ₁ ≅-IType σ₂ → snd σ₁ ≅-Type snd σ₂
snd-cong P.refl = P.refl

-- Note that _ˢ_ and curry are the semantic counterparts of
-- application and abstraction.

ˢ-cong :
  ∀ {Γ₁ sp₁₁ sp₂₁ σ₁} {v₁ : Value Γ₁ (fst σ₁)}
    {f₁ : Value Γ₁ (π sp₁₁ sp₂₁ , σ₁)}
    {Γ₂ sp₁₂ sp₂₂ σ₂} {v₂ : Value Γ₂ (fst σ₂)}
    {f₂ : Value Γ₂ (π sp₁₂ sp₂₂ , σ₂)} →
  f₁ ≅-Value f₂ → v₁ ≅-Value v₂ → f₁ ˢ v₁ ≅-Value f₂ ˢ v₂
ˢ-cong P.refl P.refl = P.refl

curry-cong :
  ∀ {Γ₁ σ₁ τ₁} {v₁ : Value (Γ₁ ▻ σ₁) τ₁}
    {Γ₂ σ₂ τ₂} {v₂ : Value (Γ₂ ▻ σ₂) τ₂} →
  v₁ ≅-Value v₂ → c v₁ ≅-Value c v₂
curry-cong P.refl = P.refl

uncurry-cong :
  ∀ {Γ₁ sp₁₁ sp₂₁ σ₁} {v₁ : Value Γ₁ (π sp₁₁ sp₂₁ , σ₁)}
    {Γ₂ sp₁₂ sp₂₂ σ₂} {v₂ : Value Γ₂ (π sp₁₂ sp₂₂ , σ₂)} →
  v₁ ≅-Value v₂ →
  _≅-Value_ {σ₁ = snd σ₁} (uc v₁) {σ₂ = snd σ₂} (uc v₂)
uncurry-cong P.refl = P.refl

⋆-cong : {Γ₁ Γ₂ : Ctxt} →
         Γ₁ ≅-Ctxt Γ₂ → ⋆ {Γ = Γ₁} ≅-type ⋆ {Γ = Γ₂}
⋆-cong P.refl = P.refl

el-cong : ∀ {Γ₁} {t₁ : Γ₁ ⊢ -, k U-⋆}
            {Γ₂} {t₂ : Γ₂ ⊢ -, k U-⋆} →
          t₁ ≅-⊢ t₂ → el t₁ ≅-type el t₂
el-cong P.refl = P.refl

π-cong : ∀ {Γ₁ σ₁ τ₁} {σ′₁ : Γ₁ ⊢ σ₁ type} {τ′₁ : Γ₁ ▻ σ₁ ⊢ τ₁ type}
           {Γ₂ σ₂ τ₂} {σ′₂ : Γ₂ ⊢ σ₂ type} {τ′₂ : Γ₂ ▻ σ₂ ⊢ τ₂ type} →
         σ′₁ ≅-type σ′₂ → τ′₁ ≅-type τ′₂ → π σ′₁ τ′₁ ≅-type π σ′₂ τ′₂
π-cong P.refl P.refl = P.refl

var-cong : ∀ {Γ₁ σ₁} {x₁ : Γ₁ ∋ σ₁}
             {Γ₂ σ₂} {x₂ : Γ₂ ∋ σ₂} →
           x₁ ≅-∋ x₂ → var x₁ ≅-⊢ var x₂
var-cong P.refl = P.refl

ƛ-cong : ∀ {Γ₁ σ₁ τ₁} {t₁ : Γ₁ ▻ σ₁ ⊢ τ₁}
           {Γ₂ σ₂ τ₂} {t₂ : Γ₂ ▻ σ₂ ⊢ τ₂} →
         t₁ ≅-⊢ t₂ → ƛ t₁ ≅-⊢ ƛ t₂
ƛ-cong P.refl = P.refl

·-cong : ∀ {Γ₁ sp₁₁ sp₂₁ σ₁}
           {t₁₁ : Γ₁ ⊢ π sp₁₁ sp₂₁ , σ₁} {t₂₁ : Γ₁ ⊢ fst σ₁}
           {Γ₂ sp₁₂ sp₂₂ σ₂}
           {t₁₂ : Γ₂ ⊢ π sp₁₂ sp₂₂ , σ₂} {t₂₂ : Γ₂ ⊢ fst σ₂} →
           t₁₁ ≅-⊢ t₁₂ → t₂₁ ≅-⊢ t₂₂ → t₁₁ · t₂₁ ≅-⊢ t₁₂ · t₂₂
·-cong P.refl P.refl = P.refl

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
module Oscar.Data.Proposequality where

open import Agda.Builtin.Equality public using (_≡_) renaming (refl to ∅) public
open import Relation.Binary.PropositionalEquality public using (_≢_) public

open import Oscar.Category.Setoid

open import Relation.Binary.PropositionalEquality using (sym; trans)

open import Oscar.Level
open import Oscar.Relation

instance

  IsSetoidProposequality : ∀ {a} {A : Set a} → IsSetoid (_≡_ {A = A})
  IsSetoid.reflexivity IsSetoidProposequality _ = ∅
  IsSetoid.symmetry IsSetoidProposequality = sym
  IsSetoid.transitivity IsSetoidProposequality = λ ‵ → trans ‵

module _ {a} (A : Set a) where

  setoid : Setoid a a
  setoid = ↑ _≡_ {A = A}

{-
  private

    infixl 7 _∙_
    _∙_ : Transitive (_≡_ {A = A})
    _∙_ = (λ y≡z x≡y → transitivity x≡y y≡z)
-}

  open import Oscar.Category.Morphism
  open import Oscar.Function

  module _ {b} (B : A → A → Set b) where

{-
    private

      infix 4 _≞_
      _≞_ = λ {x} {y} → _≡_ {A = B x y}
-}
    morphism : Morphism a b b
    morphism = -- ↑ λ {x} {y} → _≞_ {x} {y} -- _≡_ {A = B x y}
               ↑ λ {x} {y} → _≡_ {A = B x y}

    open Morphism morphism

    open import Oscar.Category.Semigroupoid

    module _ (_∙_ : Transitive _↦_) (associativity : Associative _∙_ _≞_) where

      instance

        IsSemigroupoidProposequality : IsSemigroupoid morphism _∙_
        IsSemigroupoid.extensionality IsSemigroupoidProposequality ∅ ∅ = ∅
        IsSemigroupoid.associativity IsSemigroupoidProposequality = associativity

-- instance

--   IsSemigroupoidProposequality : ∀ {a} {A : Set a} {b} {B : A → A → Set b}
--     → IsSemigroupoid (morphism B) {!!} -- (transitivity ⦃ setoid A ⦄)
--   IsSemigroupoidProposequality = {!!}

--   IsSemigroupoidProposequality' : ∀ {a} {A : Set a}
--     → IsSemigroupoid (morphism (_≡_ {A = A})) (λ y≡z x≡y → transitivity x≡y y≡z) -- (transitivity ⦃ setoid A ⦄)
--   IsSemigroupoid.extensionality IsSemigroupoidProposequality' = {!!} -- ∅ ∅ = ∅
--   IsSemigroupoid.associativity IsSemigroupoidProposequality' ∅ _ _ = ∅

-- -- semigroupoid : Semigroupoid

-- -- setoid : ∀ {a} (A : Set a) → Setoid a a
-- -- setoid A = ↑ _≡_ {A = A}

-- -- open import Oscar.Category.Morphism
-- -- open import Oscar.Function

-- -- morphism : ∀ {a} {A : Set a} {b} (B : A → A → Set b) → Morphism a b b
-- -- morphism B = ↑ λ {x} {y} → _≡_ {A = B x y}

-- -- open import Oscar.Category.Semigroupoid

-- -- infixl 7 _∙_
-- -- _∙_ : ∀ {y z} → y ↦ z → ∀ {x} → x ↦ y → x ↦ z

-- -- instance

-- --   IsSemigroupoidProposequality : ∀ {a} {A : Set a} {b} {B : A → A → Set b}
-- --     → IsSemigroupoid (morphism B) {!!} -- (transitivity ⦃ setoid A ⦄)
-- --   IsSemigroupoidProposequality = {!!}

-- --   IsSemigroupoidProposequality' : ∀ {a} {A : Set a}
-- --     → IsSemigroupoid (morphism (_≡_ {A = A})) (λ y≡z x≡y → transitivity x≡y y≡z) -- (transitivity ⦃ setoid A ⦄)
-- --   IsSemigroupoid.extensionality IsSemigroupoidProposequality' = {!!} -- ∅ ∅ = ∅
-- --   IsSemigroupoid.associativity IsSemigroupoidProposequality' ∅ _ _ = ∅

-- -- -- semigroupoid : Semigroupoid


text:
-- Andreas, 2017-01-27, issue #2437
-- Polarity checker turns Nonvariant to Unused arg in types,
-- thus, reducing them.
-- However, this should not happen without need.
-- We wish to preserve the types as much as possible.

-- {-# OPTIONS -v 20 #-}
-- {-# OPTIONS -v tc.polarity:30 #-}
-- {-# OPTIONS -v tc.decl:30 #-}
-- {-# OPTIONS -v tc.term:30 #-}
-- {-# OPTIONS -v tc.conv.coerce:20 #-}
-- {-# OPTIONS -v tc.signature:30 #-}
-- {-# OPTIONS -v import.iface:100 #-}

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

plus0 : ∀ x → x + 0 ≡ x
plus0 zero = refl
plus0 (suc x) rewrite plus0 x = refl

Identity : ∀{a} {A : Set a} (f : A → A) → Set a
Identity f = ∀ x → f x ≡ x

plus-0 : Identity (_+ 0)
plus-0 = plus0

-- Test (interactive): C-c C-d plus-0 RET
-- Expected:           Identity (λ section → section + 0)

-- Type should be inferred non-reduced, i.e, not as
-- ∀ x → x + 0 ≡ x


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Macro
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.CommMonoid.Base

private
  variable
    ℓ : Level

module CommMonoidTheory (M' : CommMonoid ℓ) where
 open CommMonoidStr (snd M')
 private M = ⟨ M' ⟩

 commAssocl : (x y z : M) → x · (y · z) ≡ y · (x · z)
 commAssocl x y z = assoc x y z ∙∙ cong (_· z) (comm x y) ∙∙ sym (assoc y x z)

 commAssocr : (x y z : M) → x · y · z ≡ x · z · y
 commAssocr x y z = sym (assoc x y z) ∙∙ cong (x ·_) (comm y z) ∙∙ assoc x z y

 commAssocr2 : (x y z : M) → x · y · z ≡ z · y · x
 commAssocr2 x y z = commAssocr _ _ _ ∙∙ cong (_· y) (comm _ _) ∙∙ commAssocr _ _ _

 commAssocSwap : (x y z w : M) → (x · y) · (z · w) ≡ (x · z) · (y · w)
 commAssocSwap x y z w = assoc (x · y) z w ∙∙ cong (_· w) (commAssocr x y z)
                                               ∙∙ sym (assoc (x · z) y w)

max_stars_repo_name: FernandoLarrain/cubical


text:
------------------------------------------------------------------------
-- The derivative operator does not remove any ambiguity
------------------------------------------------------------------------

module TotalParserCombinators.Derivative.RightInverse where

open import Data.List
open import Data.Maybe
open import Relation.Binary.HeterogeneousEquality as H using (_≅_; refl)
open import Relation.Binary.PropositionalEquality

open import TotalParserCombinators.Derivative.SoundComplete
import TotalParserCombinators.InitialBag as I
open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics hiding (_≅_)

mutual

  sound∘complete : ∀ {Tok R xs x s t} {p : Parser Tok R xs} →
                   (x∈p : x ∈ p · t ∷ s) →
                   sound p (complete x∈p) ≡ x∈p
  sound∘complete x∈p = H.≅-to-≡ (sound∘complete′ x∈p refl)

  sound∘complete′ :
    ∀ {Tok R xs x s′ s t} {p : Parser Tok R xs}
    (x∈p : x ∈ p · s′) (eq : s′ ≡ t ∷ s) →
    sound p (complete′ p x∈p eq) ≅ x∈p
  sound∘complete′ token       refl = refl

  sound∘complete′ (∣-left    x∈p₁) refl rewrite sound∘complete x∈p₁ = refl
  sound∘complete′ (∣-right _ x∈p₂) refl rewrite sound∘complete x∈p₂ = refl

  sound∘complete′ (<$> x∈p)   refl rewrite sound∘complete x∈p  = refl

  sound∘complete′       (_⊛_ {s₁ = _ ∷ _} {fs = nothing} {xs = just _}  f∈p₁ x∈p₂) refl
    rewrite sound∘complete f∈p₁ = refl
  sound∘complete′       (_⊛_ {s₁ = _ ∷ _} {fs = just _}  {xs = just _}  f∈p₁ x∈p₂) refl
    rewrite sound∘complete f∈p₁ = refl
  sound∘complete′ {Tok} (_⊛_ {s₁ = []}    {fs = just _}  {xs = just _}  f∈p₁ x∈p₂) refl
    rewrite Return⋆.sound∘complete {Tok = Tok} (I.complete f∈p₁)
          | I.sound∘complete f∈p₁
          | sound∘complete x∈p₂ = refl

  sound∘complete′       {p = _⊛_ {xs = nothing} _ _}
                        (_⊛_ {s₁ = _ ∷ _} {fs = nothing} {xs = nothing} f∈p₁ x∈p₂) refl
    rewrite sound∘complete f∈p₁ = refl
  sound∘complete′       (_⊛_ {s₁ = _ ∷ _} {fs = just _}  {xs = nothing} f∈p₁ x∈p₂) refl
    rewrite sound∘complete f∈p₁ = refl
  sound∘complete′ {Tok} (_⊛_ {s₁ = []}    {fs = just _}  {xs = nothing} f∈p₁ x∈p₂) refl
    rewrite Return⋆.sound∘complete {Tok = Tok} (I.complete f∈p₁)
          | I.sound∘complete f∈p₁
          | sound∘complete x∈p₂ = refl

  sound∘complete′       (_>>=_ {s₁ = _ ∷ _} {xs = nothing} {f = just _}  x∈p₁ y∈p₂x) refl
    rewrite sound∘complete x∈p₁ = refl
  sound∘complete′       (_>>=_ {s₁ = _ ∷ _} {xs = just _}  {f = just _}  x∈p₁ y∈p₂x) refl
    rewrite sound∘complete x∈p₁ = refl
  sound∘complete′ {Tok} (_>>=_ {s₁ = []}    {xs = just _}  {f = just _}  x∈p₁ y∈p₂x) refl
    rewrite Return⋆.sound∘complete {Tok = Tok} (I.complete x∈p₁)
          | I.sound∘complete x∈p₁
          | sound∘complete y∈p₂x = refl

  sound∘complete′       {p = _>>=_ {xs = nothing} _ _}
                        (_>>=_ {s₁ = _ ∷ _} {xs = nothing} {f = nothing} x∈p₁ y∈p₂x) refl
    rewrite sound∘complete x∈p₁ = refl
  sound∘complete′       (_>>=_ {s₁ = _ ∷ _} {xs = just _}  {f = nothing} x∈p₁ y∈p₂x) refl
    rewrite sound∘complete x∈p₁ = refl
  sound∘complete′ {Tok} (_>>=_ {s₁ = []}    {xs = just _}  {f = nothing} x∈p₁ y∈p₂x) refl
    rewrite Return⋆.sound∘complete {Tok = Tok} (I.complete x∈p₁)
          | I.sound∘complete x∈p₁
          | sound∘complete y∈p₂x = refl

  sound∘complete′ (nonempty x∈p) refl rewrite sound∘complete x∈p = refl

  sound∘complete′ (cast x∈p)     refl rewrite sound∘complete x∈p = refl

  sound∘complete′ (_⊛_   {s₁ = []} {fs = nothing} f∈p₁ _) _ with I.complete f∈p₁
  ... | ()
  sound∘complete′ (_>>=_ {s₁ = []} {xs = nothing} x∈p₁ _) _ with I.complete x∈p₁
  ... | ()

  sound∘complete′ return ()

max_stars_repo_name: nad/parser-combinators


text:
-- Copyright:  (c) 2016 Ertugrul Söylemez
-- License:    BSD3
-- Maintainer: Ertugrul Söylemez <esz@posteo.de>

module Data.Nat.Core where

open import Agda.Builtin.Nat public
  renaming (Nat to ℕ)
  using (suc; zero)
  renaming (_+_ to _+ℕ_; _*_ to _*ℕ_)
open import Classes
open import Core

instance
  ℕ-Number : Number ℕ
  ℕ-Number =
    record {
      Constraint = λ _ → ⊤;
      fromNat = λ n → n
    }

  ℕ-Plus : Plus ℕ
  ℕ-Plus = record { _+_ = _+ℕ_ }

  ℕ-Times : Times ℕ
  ℕ-Times = record { _*_ = _*ℕ_ }

  ℕ,≡ : Equiv ℕ
  ℕ,≡ = PropEq ℕ

  module ℕ,≡ = Equiv ℕ,≡

data _≤_ : ℕ → ℕ → Set where
  instance 0≤s : ∀ {y} → 0 ≤ y
  instance s≤s : ∀ {x y} → x ≤ y → suc x ≤ suc y

infix 4 _≤_

ℕ,≤ : TotalOrder ℕ
ℕ,≤ =
  record {
    partialOrder = record {
      Eq = PropEq ℕ;
      _≤_ = _≤_;
      antisym = antisym;
      refl' = refl';
      trans = trans
    };
    total = total
  }

  where
  antisym : {x y : ℕ} → x ≤ y → y ≤ x → x ≡ y
  antisym 0≤s 0≤s = ≡-refl
  antisym (s≤s p) (s≤s q) = cong suc (antisym p q)

  refl' : {x y : ℕ} → x ≡ y → x ≤ y
  refl' {zero} ≡-refl = 0≤s
  refl' {suc x} ≡-refl = s≤s (refl' ≡-refl)

  trans : {x y z : ℕ} → x ≤ y → y ≤ z → x ≤ z
  trans 0≤s q = 0≤s
  trans (s≤s p) (s≤s q) = s≤s (trans p q)

  total : (x y : ℕ) → Either (x ≤ y) (y ≤ x)
  total zero y = Left 0≤s
  total (suc x) zero = Right 0≤s
  total (suc x) (suc y) with total x y
  total (suc x) (suc y) | Left p = Left (s≤s p)
  total (suc x) (suc y) | Right p = Right (s≤s p)

module ℕ,≤ = TotalOrder ℕ,≤

_≤?_ : ∀ x y → Decision (x ≤ y)
zero ≤? y = yes 0≤s
suc x ≤? zero = no (λ ())
suc x ≤? suc y with x ≤? y
suc x ≤? suc y | yes p = yes (s≤s p)
suc x ≤? suc y | no np = no (λ { (s≤s p) → np p })

_multiple-of_ : ℕ → ℕ → Set
x multiple-of y = ∃ (λ k → k * y ≡ x)

module Props where
  open Equiv (PropEq ℕ)

  private
    _!+!_ : ∀ {x1 x2 y1 y2 : ℕ} → x1 ≡ x2 → y1 ≡ y2 → x1 + y1 ≡ x2 + y2
    _!+!_ = cong2 _+_
    R = λ x → refl {x = x}

    infixl 6 _!+!_

  +-assoc : ∀ x y z → (x + y) + z ≈ x + (y + z)
  +-assoc zero y z = refl
  +-assoc (suc x) y z = cong suc (+-assoc x y z)

  +-left-id : ∀ x → 0 + x ≈ x
  +-left-id _ = refl

  +-right-id : ∀ x → x + 0 ≈ x
  +-right-id zero = refl
  +-right-id (suc x) = cong suc (+-right-id x)

  +-comm : ∀ x y → x + y ≈ y + x
  +-comm zero y = sym (+-right-id y)
  +-comm (suc x) y =
    begin
      suc x + y ≈[ cong suc (+-comm x y) ]
      suc y + x ≈[ sym (one-comm y x) ]
      y + suc x
    qed

    where
    one-comm : ∀ x y → x + suc y ≈ suc x + y
    one-comm zero _ = refl
    one-comm (suc x) y = cong suc (one-comm x y)

  +-suc-assoc : ∀ x y → x + suc y ≈ suc (x + y)
  +-suc-assoc x y =
    begin
      x + suc y   ≈[ sym (+-assoc x 1 y) ]
      (x + 1) + y ≈[ +-comm x 1 !+! R y ]
      suc (x + y)
    qed

  *-+-left-dist : ∀ x a b → x * (a + b) ≈ x * a + x * b
  *-+-left-dist zero a b = refl
  *-+-left-dist (suc x) a b =
    begin
      a + b + x * (a + b)       ≈[ R (a + b) !+! *-+-left-dist x a b ]
      a + b + (x * a + x * b)   ≈[ +-assoc a b _ ]
      a + (b + (x * a + x * b)) ≈[
      cong (a +_) $
        b + (x * a + x * b) ≈[ sym (+-assoc b (x * a) (x * b)) ]
        b + x * a + x * b   ≈[ +-comm b _ !+! R (x * b) ]
        x * a + b + x * b   ≈[ +-assoc (x * a) _ _ ]
        x * a + (b + x * b)
      qed ]
      a + (x * a + (b + x * b)) ≈[ sym (+-assoc a _ _) ]
      a + x * a + (b + x * b)
    qed

  *-+-right-dist : ∀ a b x → (a + b) * x ≈ a * x + b * x
  *-+-right-dist zero b x = refl
  *-+-right-dist (suc a) b x =
    begin
      x + (a + b) * x     ≈[ R x !+! *-+-right-dist a b x ]
      x + (a * x + b * x) ≈[ sym (+-assoc x (a * x) (b * x)) ]
      (x + a * x) + b * x
    qed

  *-assoc : ∀ x y z → (x * y) * z ≈ x * (y * z)
  *-assoc zero y z = refl
  *-assoc (suc x) y z =
    begin
      (y + x * y) * z     ≈[ *-+-right-dist y (x * y) z ]
      y * z + (x * y) * z ≈[ R (y * z) !+! *-assoc x y z ]
      y * z + x * (y * z)
    qed

  *-left-id : ∀ x → 1 * x ≈ x
  *-left-id = +-right-id

  *-right-id : ∀ x → x * 1 ≈ x
  *-right-id zero = refl
  *-right-id (suc x) = cong suc (*-right-id x)

  *-right-zero : ∀ x → x * 0 ≈ 0
  *-right-zero zero = refl
  *-right-zero (suc x) = *-right-zero x

  *-comm : ∀ x y → x * y ≈ y * x
  *-comm zero y = sym (*-right-zero y)
  *-comm (suc x) zero = *-comm x zero
  *-comm (suc x) (suc y) =
    cong suc $
    begin
      y + x * suc y       ≈[ R y !+! (*-+-left-dist x 1 y) ]
      y + (x * 1 + x * y) ≈[ R y !+! (*-right-id x !+! R (x * y)) ]
      y + (x + x * y)     ≈[ sym (+-assoc y x (x * y)) ]
      y + x + x * y       ≈[ +-comm y x !+! *-comm x y ]
      x + y + y * x       ≈[ +-assoc x y (y * x) ]
      x + (y + y * x)     ≈[ R x !+! (sym (*-right-id y) !+! R (y * x)) ]
      x + (y * 1 + y * x) ≈[ R x !+! sym (*-+-left-dist y 1 x) ]
      x + y * suc x
    qed

  suc-inj : ∀ {x y} → suc x ≈ suc y → x ≈ y
  suc-inj ≡-refl = refl

  sum-mult : ∀ {x1 x2 y} → x1 multiple-of y → x2 multiple-of y → (x1 + x2) multiple-of y
  sum-mult {x1} {x2} {y} (k1 , p1) (k2 , p2) =
    k1 + k2
    because:
      (k1 + k2) * y   ≈[ *-+-right-dist k1 k2 y ]
      k1 * y + k2 * y ≈[ p1 !+! p2 ]
      x1 + x2
    qed

max_stars_repo_name: esoeylemez/agda-simple

max_issues_repo_name: esoeylemez/agda-simple

max_forks_repo_name: esoeylemez/agda-simple


text:
------------------------------------------------------------------------
-- Some boring lemmas used by the ring solver
------------------------------------------------------------------------

-- Note that these proofs use all "almost commutative ring" properties
-- except for zero and -‿pres-≈.

open import Algebra
open import Algebra.RingSolver.AlmostCommutativeRing

module Algebra.RingSolver.Lemmas
  (coeff : RawRing)
  (r : AlmostCommutativeRing)
  (morphism : coeff -Raw-AlmostCommutative⟶ r)
  where

private
  module C = RawRing coeff
open AlmostCommutativeRing r
open import Algebra.Morphism
open _-RawRing⟶_ morphism
import Relation.Binary.EqReasoning as EqR; open EqR setoid
open import Data.Function
open import Data.Product

lemma₀ : ∀ x → x + ⟦ C.0# ⟧ ≈ x
lemma₀ x = begin
  x + ⟦ C.0# ⟧  ≈⟨ refl ⟨ +-pres-≈ ⟩ 0-homo ⟩
  x + 0#        ≈⟨ proj₂ +-identity _ ⟩
  x             ∎

lemma₁ : ∀ a b c d x →
         (a + b) * x + (c + d) ≈ (a * x + c) + (b * x + d)
lemma₁ a b c d x = begin
  (a + b) * x + (c + d)      ≈⟨ proj₂ distrib _ _ _ ⟨ +-pres-≈ ⟩ refl ⟩
  (a * x + b * x) + (c + d)  ≈⟨ +-assoc _ _ _ ⟩
  a * x + (b * x + (c + d))  ≈⟨ refl ⟨ +-pres-≈ ⟩ sym (+-assoc _ _ _) ⟩
  a * x + ((b * x + c) + d)  ≈⟨ refl ⟨ +-pres-≈ ⟩ (+-comm _ _ ⟨ +-pres-≈ ⟩ refl) ⟩
  a * x + ((c + b * x) + d)  ≈⟨ refl ⟨ +-pres-≈ ⟩ +-assoc _ _ _ ⟩
  a * x + (c + (b * x + d))  ≈⟨ sym $ +-assoc _ _ _ ⟩
  (a * x + c) + (b * x + d)  ∎

lemma₂ : ∀ x y z → x + (y + z) ≈ y + (x + z)
lemma₂ x y z = begin
  x + (y + z)  ≈⟨ sym $ +-assoc _ _ _ ⟩
  (x + y) + z  ≈⟨ +-comm _ _ ⟨ +-pres-≈ ⟩ refl ⟩
  (y + x) + z  ≈⟨ +-assoc _ _ _ ⟩
  y + (x + z)  ∎

lemma₃ : ∀ a b c x → a * c * x + b * c ≈ (a * x + b) * c
lemma₃ a b c x = begin
  a * c * x + b * c  ≈⟨ lem ⟨ +-pres-≈ ⟩ refl ⟩
  a * x * c + b * c  ≈⟨ sym $ proj₂ distrib _ _ _ ⟩
  (a * x + b) * c    ∎
  where
  lem = begin
    a * c * x    ≈⟨ *-assoc _ _ _ ⟩
    a * (c * x)  ≈⟨ refl ⟨ *-pres-≈ ⟩ *-comm _ _ ⟩
    a * (x * c)  ≈⟨ sym $ *-assoc _ _ _ ⟩
    a * x * c    ∎

lemma₄ : ∀ a b c x → a * b * x + a * c ≈ a * (b * x + c)
lemma₄ a b c x = begin
  a * b * x + a * c    ≈⟨ *-assoc _ _ _ ⟨ +-pres-≈ ⟩ refl ⟩
  a * (b * x) + a * c  ≈⟨ sym $ proj₁ distrib _ _ _ ⟩
  a * (b * x + c)      ∎

lemma₅ : ∀ a b c d x →
         a * c * x * x + ((a * d + b * c) * x + b * d) ≈
         (a * x + b) * (c * x + d)
lemma₅ a b c d x = begin
  a * c * x * x +
  ((a * d + b * c) * x + b * d)          ≈⟨ lem₁ ⟨ +-pres-≈ ⟩
                                            (lem₂ ⟨ +-pres-≈ ⟩ refl) ⟩
  a * x * (c * x) +
  (a * x * d + b * (c * x) + b * d)      ≈⟨ refl ⟨ +-pres-≈ ⟩ +-assoc _ _ _ ⟩
  a * x * (c * x) +
  (a * x * d + (b * (c * x) + b * d))    ≈⟨ sym $ +-assoc _ _ _ ⟩
  a * x * (c * x) + a * x * d +
  (b * (c * x) + b * d)                  ≈⟨ sym $ proj₁ distrib _ _ _
                                                  ⟨ +-pres-≈ ⟩
                                                proj₁ distrib _ _ _ ⟩
  a * x * (c * x + d) + b * (c * x + d)  ≈⟨ sym $ proj₂ distrib _ _ _ ⟩
  (a * x + b) * (c * x + d)              ∎
  where
  lem₁' = begin
    a * c * x    ≈⟨ *-assoc _ _ _ ⟩
    a * (c * x)  ≈⟨ refl ⟨ *-pres-≈ ⟩ *-comm _ _ ⟩
    a * (x * c)  ≈⟨ sym $ *-assoc _ _ _ ⟩
    a * x * c    ∎

  lem₁ = begin
    a * c * x * x    ≈⟨ lem₁' ⟨ *-pres-≈ ⟩ refl ⟩
    a * x * c * x    ≈⟨ *-assoc _ _ _ ⟩
    a * x * (c * x)  ∎

  lem₂ = begin
    (a * d + b * c) * x        ≈⟨ proj₂ distrib _ _ _ ⟩
    a * d * x + b * c * x      ≈⟨ *-assoc _ _ _ ⟨ +-pres-≈ ⟩ *-assoc _ _ _ ⟩
    a * (d * x) + b * (c * x)  ≈⟨ (refl ⟨ *-pres-≈ ⟩ *-comm _ _)
                                    ⟨ +-pres-≈ ⟩ refl ⟩
    a * (x * d) + b * (c * x)  ≈⟨ sym $ *-assoc _ _ _ ⟨ +-pres-≈ ⟩ refl ⟩
    a * x * d + b * (c * x)    ∎

lemma₆ : ∀ a b x → - a * x + - b ≈ - (a * x + b)
lemma₆ a b x = begin
  - a * x + - b    ≈⟨ -‿*-distribˡ _ _ ⟨ +-pres-≈ ⟩ refl ⟩
  - (a * x) + - b  ≈⟨ -‿+-comm _ _ ⟩
  - (a * x + b)    ∎

lemma₇ : ∀ x → ⟦ C.1# ⟧ * x + ⟦ C.0# ⟧ ≈ x
lemma₇ x = begin
  ⟦ C.1# ⟧ * x + ⟦ C.0# ⟧  ≈⟨ (1-homo ⟨ *-pres-≈ ⟩ refl) ⟨ +-pres-≈ ⟩ 0-homo ⟩
  1# * x + 0#              ≈⟨ proj₂ +-identity _ ⟩
  1# * x                   ≈⟨ proj₁ *-identity _ ⟩
  x                        ∎


text:
module Membership-equality where

import Membership-old
open import Relation.Binary.PropositionalEquality as PropEq
open import Data.List
open import Data.List.Any
open import Relation.Binary
import Relation.Binary.InducedPreorders as Ind
open import Function.Related as Related hiding (_∼[_]_)

private
  open module M {a} {A : Set a} = Membership-old (PropEq.setoid A) public
    hiding (lose; ⊆-preorder)

lose : ∀ {a p} {A : Set a} {P : A → Set p} {x xs} →
         x M.∈ xs → P x → Any P xs
lose {P = P} = M.lose (PropEq.subst P)

-- _⊆_ is a preorder.

⊆-preorder : ∀ {a} → Set a → Preorder _ _ _
⊆-preorder A = Ind.InducedPreorder₂ (PropEq.setoid (List A)) _∈_
                                      (PropEq.subst (_∈_ _))

  -- Set and bag equality and related preorders.

open Related public
  using (Kind; Symmetric-kind)
  renaming ( implication         to subset
           ; reverse-implication to superset
           ; equivalence         to set
           ; injection           to subbag
           ; reverse-injection   to superbag
           ; bijection           to bag
           )

[_]-Order : Kind → ∀ {a} → Set a → Preorder _ _ _
[ k ]-Order A = Related.InducedPreorder₂ k (_∈_ {A = A})

[_]-Equality : Symmetric-kind → ∀ {a} → Set a → Setoid _ _
[ k ]-Equality A = Related.InducedEquivalence₂ k (_∈_ {A = A})

infix 4 _∼[_]_

_∼[_]_ : ∀ {a} {A : Set a} → List A → Kind → List A → Set _
_∼[_]_ {A = A} xs k ys = Preorder._∼_ ([ k ]-Order A) xs ys

-- Bag equality implies the other relations.

bag-=⇒ : ∀ {k a} {A : Set a} {xs ys : List A} →
         xs ∼[ bag ] ys → xs ∼[ k ] ys
bag-=⇒ xs≈ys = ↔⇒ xs≈ys

max_stars_repo_name: Zalastax/singly-typed-actors

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
------------------------------------------------------------------------
-- A small definition of a dependently typed language, using the
-- technique from McBride's "Outrageous but Meaningful Coincidences"
------------------------------------------------------------------------

-- The code contains an example, a partial definition of categories,
-- which triggers the use of an enormous amount of memory (with the
-- development version of Agda which is current at the time of
-- writing). I'm not entirely sure if the code is correct: 2.5G heap
-- doesn't seem to suffice to typecheck this code. /NAD

module Language where

------------------------------------------------------------------------
-- Prelude

record ⊤ : Set₁ where

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

open Σ

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

record ↑ (A : Set) : Set₁ where
  constructor lift
  field
    lower : A

------------------------------------------------------------------------
-- Contexts

-- The definition of contexts is parametrised by a universe.

module Context (U : Set₁) (El : U → Set₁) where

  mutual

    -- Contexts.

    data Ctxt : Set₁ where
      ε   : Ctxt
      _▻_ : (Γ : Ctxt) → Ty Γ → Ctxt

    -- Types.

    Ty : Ctxt → Set₁
    Ty Γ = Env Γ → U

    -- Environments.

    Env : Ctxt → Set₁
    Env ε       = ⊤
    Env (Γ ▻ σ) = Σ (Env Γ) λ γ → El (σ γ)

  -- Variables (de Bruijn indices).

  infix 4 _∋_

  data _∋_ : (Γ : Ctxt) → Ty Γ → Set₁ where
    zero : ∀ {Γ σ}               → Γ ▻ σ ∋ λ γ → σ (proj₁ γ)
    suc  : ∀ {Γ σ τ} (x : Γ ∋ τ) → Γ ▻ σ ∋ λ γ → τ (proj₁ γ)

  -- A lookup function.

  lookup : ∀ {Γ σ} → Γ ∋ σ → (γ : Env Γ) → El (σ γ)
  lookup zero    (γ , v) = v
  lookup (suc x) (γ , v) = lookup x γ

------------------------------------------------------------------------
-- A universe

mutual

  data U : Set₁ where
    set : U
    el  : Set → U
    σ π : (a : U) → (El a → U) → U

  El : U → Set₁
  El set     = Set
  El (el A)  = ↑ A
  El (σ a b) = Σ (El a) λ x → El (b x)
  El (π a b) = (x : El a) → El (b x)

open Context U El

-- Abbreviations.

infixr 20 _⊗_
infixr 10 _⇾_

_⇾_ : U → U → U
a ⇾ b = π a λ _ → b

_⊗_ : U → U → U
a ⊗ b = σ a λ _ → b

-- Example.

raw-categoryU : U
raw-categoryU =
  σ set λ obj →
  σ (el obj ⇾ el obj ⇾ set) λ hom →
  (π (el obj) λ x → el (hom x x))
    ⊗
  (π (el obj) λ x → π (el obj) λ y → π (el obj) λ z →
     el (hom x y) ⇾ el (hom y z) ⇾ el (hom x z))

------------------------------------------------------------------------
-- A language

mutual

  infixl 30 _·_
  infix   4 _⊢_

  -- Syntax for types.

  data Type : (Γ : Ctxt) → Ty Γ → Set₁ where
    set : ∀ {Γ} → Type Γ (λ _ → set)
    el  : ∀ {Γ} (x : Γ ⊢ λ _ → set) → Type Γ (λ γ → el (⟦ x ⟧ γ))
    σ   : ∀ {Γ a b} → Type Γ a → Type (Γ ▻ a) b →
          Type Γ (λ γ → σ (a γ) (λ v → b (γ , v)))
    π   : ∀ {Γ a b} → Type Γ a → Type (Γ ▻ a) b →
          Type Γ (λ γ → π (a γ) (λ v → b (γ , v)))

  -- Terms.

  data _⊢_ : (Γ : Ctxt) → Ty Γ → Set₁ where
    var : ∀ {Γ a} → Γ ∋ a → Γ ⊢ a
    ƛ   : ∀ {Γ a b} → Γ ▻ a ⊢ uncurry b →
          Γ ⊢ (λ γ → π (a γ) (λ v → b γ v))
    _·_ : ∀ {Γ a} {b : (γ : Env Γ) → El (a γ) → U} →
          Γ ⊢ (λ γ → π (a γ) (λ v → b γ v)) →
          (t₂ : Γ ⊢ a) → Γ ⊢ (λ γ → b γ (⟦ t₂ ⟧ γ))

  -- The semantics of a term.

  ⟦_⟧ : ∀ {Γ a} → Γ ⊢ a → (γ : Env Γ) → El (a γ)
  ⟦ var x   ⟧ γ = lookup x γ
  ⟦ ƛ t     ⟧ γ = λ v → ⟦ t ⟧ (γ , v)
  ⟦ t₁ · t₂ ⟧ γ = (⟦ t₁ ⟧ γ) (⟦ t₂ ⟧ γ)

-- Example.

raw-category : Type ε (λ _ → raw-categoryU)
raw-category =
     -- Objects.
   σ set
     -- Morphisms.
  (σ (π (el (var zero)) (π (el (var (suc zero))) set))
     -- Identity.
  (σ (π (el (var (suc zero)))
        (el (var (suc zero) · var zero · var zero)))
     -- Composition.
     (π (el (var (suc (suc zero))))                          -- X.
     (π (el (var (suc (suc (suc zero)))))                    -- Y.
     (π (el (var (suc (suc (suc (suc zero))))))              -- Z.
     (π (el (var (suc (suc (suc (suc zero)))) ·
             var (suc (suc zero)) ·
             var (suc zero)))                                -- Hom X Y.
     (π (el (var (suc (suc (suc (suc (suc zero))))) ·
             var (suc (suc zero)) ·
             var (suc zero)))                                -- Hom Y Z.
        (el (var (suc (suc (suc (suc (suc (suc zero)))))) ·
             var (suc (suc (suc (suc zero)))) ·
             var (suc (suc zero)))))                         -- Hom X Z.
  ))))))


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Functor.Properties where

open import Relation.Binary using (_Preserves_⟶_)

open import Categories.Category
open import Categories.Functor
import Categories.Morphisms as Morphisms

module FunctorsAlways {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} (F : Functor C D) where
  open Functor F
  module C = Category C
  module D = Category D

  resp-Iso : ∀ {A B} {f : C [ A , B ]} {g : C [ B , A ]}
           → Morphisms.Iso C f g → Morphisms.Iso D (F₁ f) (F₁ g)
  resp-Iso {f = f} {g} I = record
    { isoˡ = begin
               D [ F₁ g ∘ F₁ f ]
             ↑⟨ homomorphism ⟩
               F₁ (C [ g ∘ f ])
             ↓⟨ F-resp-≡ I.isoˡ ⟩
               F₁ (C.id)
             ↓⟨ identity ⟩
               D.id
             ∎
    ; isoʳ = begin
               D [ F₁ f ∘ F₁ g ]
             ↑⟨ homomorphism ⟩
               F₁ (C [ f ∘ g ])
             ↓⟨ F-resp-≡ I.isoʳ ⟩
               F₁ (C.id)
             ↓⟨ identity ⟩
               D.id
             ∎
    }
    where
    module I = Morphisms.Iso I
    open D.HomReasoning

  resp-≅ : F₀ Preserves Morphisms._≅_ C ⟶ Morphisms._≅_ D
  resp-≅ I = record
    { f = F₁ I.f
    ; g = F₁ I.g
    ; iso = resp-Iso I.iso
    }
    where
    module I = Morphisms._≅_ I

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module LibA where
import LibB

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
-- Andreas, 2014-03-02, issue reported by roly.perera
-- Test case by Nisse

{-# OPTIONS --allow-unsolved-metas #-}

-- To see what is going on:
-- {-# OPTIONS -v tc.meta.assign.proj:25 #-}

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

open Σ public

map : {A B : Set} {P : A → Set} {Q : B → Set} →
      (f : A → B) → (∀ {x} → P x → Q (f x)) →
      Σ A P → Σ B Q
map f g x = t (f (proj₁ x)) (g (proj₂ x))

postulate
  U  : Set
  El : U → Set

mutual

  data C : Set where
    c : (x : C) → (F x → U) → C

  F : C → Set
  F (c x y) = Σ (F x) λ v → El (y v)

f : ∀ x y → F (c x y) → F x
f _ _ = proj₁

postulate
  P : ∀ x y → (F x → F y) → Set
  p : ∀ x y → P (c _ _) (c x y) (map (f _ _) (λ v → v))

-- WAS: internal error in Records.hs
-- NOW: unsolved meta

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda


text:
module PrintNat where

import PreludeShow
open PreludeShow

mainS = showNat 42


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

module Definition.Typed.Consequences.NeTypeEq where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Injectivity
open import Definition.Typed.Consequences.Substitution

open import Tools.Product
import Tools.PropositionalEquality as PE

-- to be moved in Untyped

typelevel-injectivity : ∀ {r r' l l'} → [ r , l ] PE.≡ [ r' , l' ] → r PE.≡ r' × l PE.≡ l'
typelevel-injectivity PE.refl = PE.refl , PE.refl

-- Helper function for the same variable instance of a context have equal types.
varTypeEq′ : ∀ {n R rR T rT Γ} → n ∷ R ^ rR ∈ Γ → n ∷ T ^ rT ∈ Γ → R PE.≡ T × rR PE.≡ rT
varTypeEq′ here here = PE.refl , PE.refl
varTypeEq′ (there n∷R) (there n∷T) with varTypeEq′ n∷R n∷T
... | PE.refl , PE.refl = PE.refl , PE.refl

-- The same variable instance of a context have equal types.
varTypeEq : ∀ {x A B rA rB Γ} → Γ ⊢ A ^ rA → Γ ⊢ B ^ rB
          → x ∷ A ^ rA ∈ Γ
          → x ∷ B ^ rB ∈ Γ
          → Γ ⊢ A ≡ B ^ rA × rA PE.≡ rB
varTypeEq A B x∷A x∷B with varTypeEq′ x∷A x∷B
... | PE.refl , PE.refl = refl A , PE.refl

-- The same neutral term have equal types.
-- to use this with different relevances rA rB we need unicity of relevance for types
neTypeEq : ∀ {t A B rA lA lA' Γ} → Neutral t → Γ ⊢ t ∷ A ^ [ rA , lA ] → Γ ⊢ t ∷ B ^ [ rA , lA' ] →
  lA PE.≡ lA' × Γ ⊢ A ≡ B ^ [ rA , lA ]
neTypeEq (var x) (var x₁ x₂) (var x₃ x₄) =
  let V , e = varTypeEq (syntacticTerm (var x₃ x₂)) (syntacticTerm (var x₃ x₄)) x₂ x₄
      _ , el = typelevel-injectivity e
  in el , V
neTypeEq (∘ₙ neT) (t∷A ∘ⱼ t∷A₁) (t∷B ∘ⱼ t∷B₁) with neTypeEq neT t∷A t∷B
... | e , q = let _ , _ , _ , elG , w = injectivity q
              in PE.cong _ elG , substTypeEq w (genRefl t∷A₁)
neTypeEq (natrecₙ neT) (natrecⱼ x t∷A t∷A₁ t∷A₂) (natrecⱼ x₁ t∷B t∷B₁ t∷B₂) =
  PE.refl , refl (substType x₁ t∷B₂)
neTypeEq Emptyrecₙ (Emptyrecⱼ x t∷A) (Emptyrecⱼ x₁ t∷B) =
  PE.refl , refl x₁
neTypeEq (Idₙ X) (Idⱼ Y Y₁ Y₂) (Idⱼ Z Z₁ Z₂) =
  let e , q = neTypeEq X Y Z
      el = next-inj e
  in e , PE.subst (λ l → _ ⊢ _ ≡ SProp l ^ _) el (refl (Ugenⱼ (wfTerm Y) ) )
neTypeEq (Idℕₙ X) (Idⱼ Y Y₁ Y₂) (Idⱼ Z Z₁ Z₂) =
  let e , q = neTypeEq X Y₁ Z₁
      el = ιinj e
  in PE.cong next el , PE.subst (λ l → _ ⊢ _ ≡ SProp l ^ _) el (refl (Ugenⱼ (wfTerm Y) ) )
neTypeEq (Idℕ0ₙ X) (Idⱼ Y Y₁ Y₂) (Idⱼ Z Z₁ Z₂) =
  let e , q = neTypeEq X Y₂ Z₂
      el = ιinj e
  in PE.cong next el , PE.subst (λ l → _ ⊢ _ ≡ SProp l ^ _) el (refl (Ugenⱼ (wfTerm Y) ) )
neTypeEq (IdℕSₙ X) (Idⱼ Y Y₁ Y₂) (Idⱼ Z Z₁ Z₂) =
  let e , q = neTypeEq X Y₂ Z₂
      el = ιinj e
  in PE.cong next el , PE.subst (λ l → _ ⊢ _ ≡ SProp l ^ _) el (refl (Ugenⱼ (wfTerm Y) ) )
neTypeEq (IdUₙ X) (Idⱼ Y Y₁ Y₂) (Idⱼ Z Z₁ Z₂) =
  let e , q = neTypeEq X Y₁ Z₁
      el = ιinj e
  in PE.cong next el , PE.subst (λ l → _ ⊢ _ ≡ SProp l ^ _) el (refl (Ugenⱼ (wfTerm Y) ) )
neTypeEq (IdUℕₙ X) (Idⱼ Y Y₁ Y₂) (Idⱼ Z Z₁ Z₂) =
  let e , q = neTypeEq X Y₂ Z₂
      el = ιinj e
  in PE.cong next el , PE.subst (λ l → _ ⊢ _ ≡ SProp l ^ _) el (refl (Ugenⱼ (wfTerm Y) ) )
neTypeEq (IdUΠₙ X) (Idⱼ Y Y₁ Y₂) (Idⱼ Z Z₁ Z₂) =
  let e , q = neTypeEq X Y₂ Z₂
      el = ιinj e
  in PE.cong next el , PE.subst (λ l → _ ⊢ _ ≡ SProp l ^ _) el (refl (Ugenⱼ (wfTerm Y) ) )
neTypeEq X (castⱼ Y Y₁ Y₂ Y₃)  (castⱼ Z Z₁ Z₂ Z₃) = PE.refl , refl (univ Y₁)
neTypeEq x (conv t∷A x₁) t∷B =
  let e , q = neTypeEq x t∷A t∷B
  in e , trans (sym x₁) q
neTypeEq x t∷A (conv t∷B x₃) =
  let e , q = neTypeEq x t∷A t∷B
  in e , trans q (PE.subst (λ l → _ ⊢ _ ≡ _ ^ [ _ , l ]) (PE.sym e) x₃)

natTypeEq : ∀ {A rA lA Γ} → Γ ⊢ ℕ ∷ A ^ [ rA , lA ] → rA PE.≡ ! × lA PE.≡ ι ¹ × Γ ⊢ A ≡ U ⁰ ^ [ ! , ι ¹ ]
natTypeEq (ℕⱼ x) = PE.refl , PE.refl , refl (univ (univ 0<1 x))
natTypeEq (conv X x) = let eqrA , eqlA , eqAU = natTypeEq X in eqrA , eqlA ,
  trans (sym (PE.subst (λ l → _ ⊢ _ ≡ _ ^ [ _ , l ] ) eqlA (PE.subst (λ r → _ ⊢ _ ≡ _ ^ [ r , _ ]) eqrA x))) eqAU

emptyTypeEq : ∀ {A rA lA Γ l} → Γ ⊢ Empty l ∷ A ^ [ rA , lA ] →
  rA PE.≡ ! × lA PE.≡ next l × Γ ⊢ A ≡ SProp l ^ [ ! , next l ]
emptyTypeEq (Emptyⱼ x) = PE.refl , PE.refl , refl (Ugenⱼ x)
emptyTypeEq (conv X x) = let eqrA , eqlA , eqAU = emptyTypeEq X in eqrA , eqlA ,
 trans (sym (PE.subst (λ l → _ ⊢ _ ≡ _ ^ [ _ , l ] ) eqlA (PE.subst (λ r → _ ⊢ _ ≡ _ ^ [ r , _ ]) eqrA x))) eqAU

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
module _ where

module M where

open M using () renaming () hiding ()

-- empty lists should not be errors here

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --universe-polymorphism #-}
open import Common.Prelude
open import Common.Level
open import Common.Reflection

module UnquoteSetOmega where

`Level : Term
`Level = def (quote Level) []

-- while building the syntax of ∀ ℓ → Set ℓ (of type Setω) is harmless
`∀ℓ→Setℓ : Term
`∀ℓ→Setℓ = pi (vArg `Level) (abs "_" (sort (set (var 0 []))))

-- unquoting it is harmfull
∀ℓ→Setℓ = unquote (give `∀ℓ→Setℓ)

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
{-

    TBA - Talk 'Bout Agda

    Ulf Norell
    Chalmers

    DTP 2008, Nottingham

-}
module Talk where

-- Normal everyday lists

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

infixr 40 _::_

map : {A B : Set} -> (A -> B) -> List A -> List B
map f []        = []
map f (x :: xs) = f x :: map f xs

-- More boring types: Bool and Maybe

data Bool : Set where
  false : Bool
  true  : Bool

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A -> Maybe A

fmap : forall {A B} -> (A -> B) -> Maybe A -> Maybe B
fmap f nothing  = nothing
fmap f (just x) = just (f x)

-- The intensional equality type

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

-- Sigma types

data Σ {A : Set}(B : A -> Set) : Set where
  _,_ : (x : A) -> B x -> Σ B

fst : {A : Set}{B : A -> Set} -> Σ B -> A
fst (x , y) = x

snd : {A : Set}{B : A -> Set}(p : Σ B) -> B (fst p)
snd (x , y) = y

_×_ : Set -> Set -> Set
A × B = Σ {A} (\_ -> B)

-- A more interesting type

infix 20 _∈_
data _∈_ {A : Set} : A -> List A -> Set where
  first : forall {x xs} -> x ∈ x :: xs
  later : forall {x y xs} -> x ∈ xs -> x ∈ y :: xs

module Map (K V : Set)
           (_=?=_ : (x y : K) -> Maybe (x == y))
    where

  Map : Set
  Map = List (K × V)

  HasKey : K -> Map -> Set
  HasKey k m = k ∈ map fst m

  member : (x : K)(m : Map) -> Maybe (HasKey x m)
  member x [] = nothing
  member x ((y , v) :: m) with x =?= y
  ... | nothing   = fmap later (member x m)
  member x ((.x , v) :: m) | just refl = just first

  lookup : (x : K)(m : Map) -> HasKey x m -> Σ \v -> (x , v) ∈ m
  lookup x []              ()
  lookup x ((.x , u) :: m)  first    = u , first
  lookup x (e        :: m) (later p) with lookup x m p
  ... | v , q = v , later q


text:
open import Agda.Builtin.Equality

record IsGroup (G : Set) : Set where
  field _∙_ : G → G → G

open IsGroup ⦃ ... ⦄

record Group : Set₁ where
  field G       : Set
        ⦃ IsG ⦄ : IsGroup G

open Group using () renaming (G to [_])

variable
  G : Group

postulate
  works : ∀ {G} → (x : [ G ]) → (x ∙ x) ≡ x
  fails : (x : [ G ]) → (x ∙ x) ≡ x
  -- WAS: No instance of type IsGroup [ G ]


text:
module Colist where

open import Size using (Size ; Size<_)

data Colist (i : Size) {a} (A : Set a) : Set a

record ∞Colist (i : Size) {a} (A : Set a) : Set a where
  coinductive
  constructor delay_
  field force : ∀ {j : Size< i} → Colist j A

data Colist (i : Size) {a} (A : Set a) where
  [] : Colist i A
  _∷_ : (x : A) (xs : ∞Colist i A) → Colist i A

max_stars_repo_name: Zalastax/thesis


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Strictness combinators
------------------------------------------------------------------------

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

module Strict where

open import Level
open import Agda.Builtin.Equality

open import Agda.Builtin.Strict
     renaming ( primForce to force
              ; primForceLemma to force-≡) public

-- Derived combinators
module _ {ℓ ℓ′ : Level} {A : Set ℓ} {B : Set ℓ′} where

  force′ : A → (A → B) → B
  force′ = force

  force′-≡ : (a : A) (f : A → B) → force′ a f ≡ f a
  force′-≡ = force-≡

  seq : A → B → B
  seq a b = force a (λ _ → b)

  seq-≡ : (a : A) (b : B) → seq a b ≡ b
  seq-≡ a b = force-≡ a (λ _ → b)


text:
module Common.Predicate where

open import Common public

open import Common.Context public
  using (Cx ; VCx ; ∅ ; _,_)

-- Predicates.

Pred : ∀ {ℓ} → Set ℓ → Set (sucᴸ ℓ)
Pred {ℓ} U = U → Set ℓ

-- Set membership.

module _ {U : Set} where
  infix 3 _∈ᴾ_
  _∈ᴾ_ : U → Pred U → Set
  A ∈ᴾ P = P A

  infix 3 _∉ᴾ_
  _∉ᴾ_ : U → Pred U → Set
  A ∉ᴾ P = Not (A ∈ᴾ P)

-- Empty set.

module _ {U : Set} where
  ∅ᴾ : Pred U
  ∅ᴾ = K 𝟘

  bot∈ᴾ : ∀ {A} → A ∉ᴾ ∅ᴾ
  bot∈ᴾ = elim𝟘

-- Universal set.

module _ {U : Set} where
  Uᴾ : Pred U
  Uᴾ = K 𝟙

  top∈ᴾ : ∀ {A} → A ∈ᴾ Uᴾ
  top∈ᴾ = ∙

-- Set inclusion.

module _ {U : Set} where
  infix 3 _⊆ᴾ_
  _⊆ᴾ_ : Pred U → Pred U → Set
  P ⊆ᴾ Q = ∀ {A : U} → A ∈ᴾ P → A ∈ᴾ Q

  infix 3 _⊈ᴾ_
  _⊈ᴾ_ : Pred U → Pred U → Set
  P ⊈ᴾ Q = Not (P ⊆ᴾ Q)

  refl⊆ᴾ : ∀ {P} → P ⊆ᴾ P
  refl⊆ᴾ = I

  trans⊆ᴾ : ∀ {P Q R} → P ⊆ᴾ Q → Q ⊆ᴾ R → P ⊆ᴾ R
  trans⊆ᴾ η η′ = η′ ∘ η

  bot⊆ᴾ : ∀ {P} → ∅ᴾ ⊆ᴾ P
  bot⊆ᴾ = elim𝟘

  top⊆ᴾ : ∀ {P} → P ⊆ᴾ Uᴾ
  top⊆ᴾ = K ∙

-- Set equality.

module _ {U : Set} where
  infix 3 _⫗ᴾ_
  _⫗ᴾ_ : Pred U → Pred U → Set
  P ⫗ᴾ Q = (P ⊆ᴾ Q) × (Q ⊆ᴾ P)

  refl⫗ᴾ : ∀ {P} → P ⫗ᴾ P
  refl⫗ᴾ {P} = refl⊆ᴾ {P = P} , refl⊆ᴾ {P = P}

  trans⫗ᴾ : ∀ {P Q R} → P ⫗ᴾ Q → Q ⫗ᴾ R → P ⫗ᴾ R
  trans⫗ᴾ {P} (η , μ) (η′ , μ′) = trans⊆ᴾ {P = P} η η′ , trans⊆ᴾ {R = P} μ′ μ

  sym⫗ᴾ : ∀ {P Q} → P ⫗ᴾ Q → Q ⫗ᴾ P
  sym⫗ᴾ (η , μ) = (μ , η)

  antisym⊆ᴾ : ∀ {P Q} → ((P ⊆ᴾ Q) × (Q ⊆ᴾ P)) ≡ (P ⫗ᴾ Q)
  antisym⊆ᴾ = refl

-- Predicate-based necessity.

module _ {U : Set} where
  data All (P : Pred U) : Pred (Cx U) where
    ∅   : All P ∅
    _,_ : ∀ {A Γ} → All P Γ → P A → All P (Γ , A)

  fill : ∀ {Γ P} → (∀ A → P A) → All P Γ
  fill {∅}     f = ∅
  fill {Γ , A} f = fill f , f A

  mapAll : ∀ {P Q} → P ⊆ᴾ Q → All P ⊆ᴾ All Q
  mapAll η ∅       = ∅
  mapAll η (γ , a) = mapAll η γ , η a

  lastAll : ∀ {A Γ P} → All P (Γ , A) → P A
  lastAll (γ , a) = a

  initAll : ∀ {A Γ P} → All P (Γ , A) → All P Γ
  initAll (γ , a) = γ

  all : ∀ {P} → (∀ A → Dec (P A)) → (∀ Γ → Dec (All P Γ))
  all P? ∅       = yes ∅
  all P? (Γ , A) with P? A
  …             | yes a = mapDec (_, a) initAll (all P? Γ)
  …             | no ¬a = no (¬a ∘ lastAll)

-- Predicate-based possibility.

module _ {U : Set} where
  data Any (P : Pred U) : Pred (Cx U) where
    top : ∀ {A Γ} → P A → Any P (Γ , A)
    pop : ∀ {A Γ} → Any P Γ → Any P (Γ , A)

  find : ∀ {Γ P} → Any P Γ → Σ U (λ A → P A)
  find (top {A} a) = A , a
  find (pop i)     = find i

  mapAny : ∀ {P Q} → P ⊆ᴾ Q → Any P ⊆ᴾ Any Q
  mapAny η (top a) = top (η a)
  mapAny η (pop γ) = pop (mapAny η γ)

  initAny : ∀ {A Γ P} → Not (P A) → Any P (Γ , A) → Any P Γ
  initAny ¬a (top a) = a ↯ ¬a
  initAny ¬a (pop γ) = γ

  any : ∀ {P} → (∀ A → Dec (P A)) → (∀ Γ → Dec (Any P Γ))
  any P? ∅       = no λ ()
  any P? (Γ , A) with P? A
  …             | yes a = yes (top a)
  …             | no ¬a = mapDec pop (initAny ¬a) (any P? Γ)


text:
open import Agda.Primitive

variable
  a : Level
  A : Set a
  x : A

postulate
  P : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Set
  p : P x

postulate
  H : ∀ a (A : Set a) (x : A) → Set
  Id : ∀ {a} (A : Set a) → A → A → Set a
  h : (i : H _ _ x) (j : H a _ _) → Id (H _ A _) i j