text:
{-
  Copyright 2019 Lisandra Silva

  Licensed under the Apache License, Version 2.0 (the "License");
  you may not use this file except in compliance with the License.
  You may obtain a copy of the License at

      http://www.apache.org/licenses/LICENSE-2.0

  Unless required by applicable law or agreed to in writing, software
  distributed under the License is distributed on an "AS IS" BASIS,
  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  See the License for the specific language governing permissions and
  limitations under the License.
-}

open import Prelude
open import Data.Vec.Bounded renaming ([] to Vec≤[])
open import Data.Vec renaming ( _++_ to _v++_
                              ; [_]  to v[_]
                              ; head to headV
                              ; _∷ʳ_ to _v∷ʳ_
                              ; tail to vTail)
open import Data.List

open import StateMachineModel

module Examples.ProducerConsumer
  {ℓ : Level}
  (Message : Set ℓ) -- Message type
  (Size : ℕ) -- Size of the bounded buffer
  where

  record State : Set (lsuc ℓ) where
    field
     buffer    : Vec≤ Message Size -- The numSpaces ≅ Vec≤.length
     produced  : List Message
     consumed  : List Message
  open State

  data MyEvent : Set ℓ where
    produce : Message → MyEvent
    consume : Message → MyEvent

  data MyEnabled : MyEvent → State → Set ℓ where
    prodEnabled : ∀ {st : State} {msg}
                  → Vec≤.length (buffer st) < Size
                  → MyEnabled (produce msg) st
    consEnabled : ∀ {st : State} {msg}
                  → 0 < Vec≤.length (buffer st)
                  → msg ≡ headV {!!}
                  → MyEnabled (consume msg) st

  MyAction : ∀ {preState : State} {event : MyEvent}
             → MyEnabled event preState
             → State
  MyAction {preSt} {produce m} (prodEnabled x) =
    record preSt
      { buffer    = Vec≤.vec (buffer preSt) v∷ʳ m , x
      ; produced  = produced preSt ++ [ m ]
      }
  MyAction {preSt} {consume m} enabled =
    record preSt
      { buffer    = (vTail (Vec≤.vec {!!})) , {!!}
      ; produced  = consumed preSt ++ [ m ]
      }

  initialState : State
  initialState = record
                   { buffer    = Vec≤[]
                   ; produced  = []
                   ; consumed  = []
                   }

  MyStateMachine : StateMachine State MyEvent
  MyStateMachine = record
                     { initial = λ state → state ≡ initialState
                     ; enabled = MyEnabled
                     ; action  = MyAction
                     }

  MyEventSet : EventSet {Event = MyEvent}
  MyEventSet (produce x) = ⊥
  MyEventSet (consume x) = ⊤

  data MyWeakFairness : EventSet → Set ℓ where
    wf : MyWeakFairness MyEventSet

  MySystem : System State MyEvent
  MySystem = record
             { stateMachine = MyStateMachine
             ; weakFairness = MyWeakFairness
             }

max_stars_repo_name: lisandrasilva/agda-liveness

max_issues_repo_name: lisandrasilva/agda-liveness

max_forks_repo_name: lisandrasilva/agda-liveness


text:
module LecSigma where

open import CS410-Prelude
open import CS410-Nat
open import CS410-Functor

-- look in the Prelude

-- talk about *
-- talk about +

_N>_ : Nat -> Nat -> Set
m N> n = m N>= suc n

Fin : Nat -> Set
Fin n = Sg Nat \ m -> n N> m

foo : Fin 7
foo = 5 , <>

-- command-response systems

_<|_ : (C : Set)(R : C -> Set) -> Set -> Set
(C <| R) X = Sg C (\ c -> R c -> X)

containerFunctor : (C : Set)(R : C -> Set) -> Functor (C <| R)
containerFunctor C R = record
  { map = \ {f (c , k) -> c , (f o k)}
  ; mapid = \ _ -> refl
  ; mapcomp = \ _ _ _ -> refl
  }

IC : Set -> Set
IC = One <| \ c -> One

LC : Set -> Set
LC = Nat <| Fin

nil : {X : Set} -> LC X
nil = 0 , (\ { (m , ()) })

cons : {X : Set} -> X -> LC X -> LC X
cons x (n , k) = (suc n) , (\
     { (zero , p) -> x
     ; (suc m , p) -> k (m , p)
     })

{-
look : {X : Set} -> IC X -> Zero
look (<> , snd) = {!!}
-}

postulate goAway : {X : Set} -> X

-- the free monad on a command-response system

module FREEMONAD (C : Set)(R : C -> Set) where

  data Free (X : Set) : Set where
    ret : X -> Free X
    do : (C <| R) (Free X) -> Free X

  graft : {X Y : Set} -> Free X -> (X -> Free Y) -> Free Y
  graft (ret x) k = k x
  graft (do (c , rx)) k = do (c , (\ r -> graft (rx r) k))

  graftLawHelp : {X : Set}(c : C)(rx : R c -> Free X)(r : R c) ->
    graft (rx r) ret == rx r
  graftLaw2 : {X : Set}(t : Free X) -> graft t ret == t
  graftLaw2 (ret x) = refl
  graftLaw2 (do (c , rx)) rewrite (ext (graftLawHelp c rx)) = refl
  graftLawHelp c rx r = graftLaw2 (rx r)

  freeMonad : Monad Free
  freeMonad = record
    {  return  = ret
    ;  _>>=_   = graft
    ;  law1 = \ _ _ -> refl
    ;  law2 = graftLaw2
    ;  law3 = goAway
    }

-- tree-like data

-- shapes and positions

ext: agda


text:
open import Oscar.Class.Similarity
open import Oscar.Class.Reflexivity
open import Oscar.Class.Surjection
open import Oscar.Class.Leftunit
open import Oscar.Class.Smap
open import Oscar.Class.Symmetrical
open import Oscar.Class.Unit
open import Oscar.Data.Surjcollation
open import Oscar.Prelude

module Oscar.Class.Smapoid where

module _
  {𝔵₁} {𝔛₁ : Ø 𝔵₁}
  {𝔵₂} {𝔛₂ : Ø 𝔵₂}
  {𝔯} (ℜ : 𝔛₁ → 𝔛₁ → Ø 𝔯)
  {𝔭₁} (𝔓₁ : 𝔛₂ → Ø 𝔭₁)
  {𝔭₂} (𝔓₂ : 𝔛₂ → Ø 𝔭₂)
  {𝔯̇} (ℜ̇ : ∀ {x y} → ℜ x y → ℜ x y → Ø 𝔯̇)
  {𝔭̇₁₁} (𝔓̇₁₁ : ∀ {x} → 𝔓₁ x → 𝔓₁ x → Ø 𝔭̇₁₁)
  {𝔭̇₂₂} (𝔓̇₂₂ : ∀ {x} → 𝔓₂ x → 𝔓₂ x → Ø 𝔭̇₂₂)
  {𝔭̇₁₂} (𝔓̇₁₂ : ∀ {x} → 𝔓₁ x → 𝔓₂ x → Ø 𝔭̇₁₂)
  where
  record IsSmapoid : Ø 𝔵₁ ∙̂ 𝔵₂ ∙̂ 𝔯 ∙̂ 𝔯̇ ∙̂ 𝔭₁ ∙̂ 𝔭₂ ∙̂ 𝔭̇₁₁ ∙̂ 𝔭̇₂₂ ∙̂ 𝔭̇₁₂ where
    constructor ∁
    field

      ⦃ `Surjection ⦄ : Surjection.class 𝔛₁ 𝔛₂

      -- ℜ 𝓂 𝓃 → 𝔓₁ (surjection 𝓂) → 𝔓₂ (surjection 𝓃)
      ⦃ `Smaparrow ⦄ : Smaparrow.class ℜ 𝔓₁ 𝔓₂ surjection surjection -- epfs, Smap

      -- 𝒫 ₁≈₁ 𝒬 → 𝒻 ◃ 𝒫 ₂≈₂ 𝒻 ◃ 𝒬
      ⦃ `leftSim ⦄ : Similarity,smaparrow!.class ℜ 𝔓₁ 𝔓₂ 𝔓̇₁₁ 𝔓̇₂₂ -- fact5, Similarity, Smaparrowleftsimilarity

      ⦃ `𝓡eflexivity ⦄ : Reflexivity.class ℜ

      -- 𝒫 ₁≈₂ 𝒖 ◃ 𝒫
      ⦃ `leftyunit ⦄ : ∀ {x} {p : 𝔓₁ (surjection x)}
                     → Leftunit.class (flip (𝔓̇₁₂ {surjection x})) ε smap p

module _
  {𝔵₁} {𝔛₁ : Ø 𝔵₁}
  {𝔵₂} {𝔛₂ : Ø 𝔵₂}
  {𝔯} (ℜ : 𝔛₁ → 𝔛₁ → Ø 𝔯)
  {𝔭₁} (𝔓₁ : 𝔛₂ → Ø 𝔭₁)
  {𝔭₂} (𝔓₂ : 𝔛₂ → Ø 𝔭₂)
  {𝔯̇} (ℜ̇ : ∀ {x y} → ℜ x y → ℜ x y → Ø 𝔯̇)
  {𝔭̇₁₁} (𝔓̇₁₁ : ∀ {x} → 𝔓₁ x → 𝔓₁ x → Ø 𝔭̇₁₁)
  {𝔭̇₂₂} (𝔓̇₂₂ : ∀ {x} → 𝔓₂ x → 𝔓₂ x → Ø 𝔭̇₂₂)
  {𝔭̇₁₂} (𝔓̇₁₂ : ∀ {x} → 𝔓₁ x → 𝔓₂ x → Ø 𝔭̇₁₂)
  where
  record IsSmapoidR : Ø 𝔵₁ ∙̂ 𝔵₂ ∙̂ 𝔯 ∙̂ 𝔯̇ ∙̂ 𝔭₁ ∙̂ 𝔭₂ ∙̂ 𝔭̇₁₁ ∙̂ 𝔭̇₂₂ ∙̂ 𝔭̇₁₂ where
    constructor ∁
    field

      ⦃ `IsSmapoid ⦄ : IsSmapoid ℜ 𝔓₁ 𝔓₂ ℜ̇ 𝔓̇₁₁ 𝔓̇₂₂ 𝔓̇₁₂

      -- 𝒻 ᵣ≈ᵣ ℊ → 𝒻 ◃ 𝒫 ₂≈₂ ℊ ◃ 𝒫
      ⦃ `rightSim ⦄ : Similarity,cosmaparrow!.class ℜ 𝔓₁ 𝔓₂ ℜ̇ 𝔓̇₂₂ -- fact6, Similarity, Smaparrowrightsimilarity

-- TODO add these somewhere?
-- fact4 needs Propergroup's Nothing -- ⦃ `Leftstar ⦄ : Leftstar.class
-- left-identity-∧ needs Propergroup
-- fact1 -- ⦃ `Symmetrical ⦄ : ∀ {m} → Symmetrical (surjcollation[ 𝔓 ]⟦ ℜ / 𝔓̇ ⟧ {m}) (λ { (∁ f) (∁ g) → {!f {m}!}})
-- Properties-fact1


text:
module list-test where

open import bool
open import list
open import nat
open import list-to-string
open import bool-to-string
open import eq

test1 : 𝕃 𝔹
test1 = tt :: tt :: tt :: []

test2 : 𝕃 𝔹
test2 = ff :: ff :: []

test3 = test1 ++ test2

test-lem : test3 ≡ tt :: tt :: tt :: ff :: ff :: []
test-lem = refl

test-lem2 : reverse test3 ≡ ff :: ff :: tt :: tt :: tt :: []
test-lem2 = refl

test3-string = 𝕃-to-string 𝔹-to-string ", " test3

test4-even = filter is-even (1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: [])

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


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

open import lib.Basics

module lib.types.Bool where

{-
data Bool : Type₀ where
  true : Bool
  false : Bool

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

Bool = ⊤ ⊔ ⊤

pattern true = inl unit
pattern false = inr unit

⊙Bool : Ptd₀
⊙Bool = ⊙[ Bool , true ]

Bool-elim : ∀ {i} {P : Bool → Type i} → P true → P false → Π Bool P
Bool-elim true* false* true = true*
Bool-elim true* false* false = false*

Bool-rec : ∀ {i} {A : Type i} → A → A → (Bool → A)
Bool-rec {A = A} = Bool-elim {P = λ _ → A}

private
  Bool-true≠false-type : Bool → Type₀
  Bool-true≠false-type true  = Unit
  Bool-true≠false-type false = Empty

abstract
  Bool-true≠false : true ≠ false
  Bool-true≠false p = transport Bool-true≠false-type p unit

  Bool-false≠true : false ≠ true
  Bool-false≠true p = transport Bool-true≠false-type (! p) unit

  Bool-has-dec-eq : has-dec-eq Bool
  Bool-has-dec-eq true true = inl idp
  Bool-has-dec-eq true false = inr Bool-true≠false
  Bool-has-dec-eq false true = inr Bool-false≠true
  Bool-has-dec-eq false false = inl idp

  Bool-is-set : is-set Bool
  Bool-is-set = dec-eq-is-set Bool-has-dec-eq

instance
  Bool-level : {n : ℕ₋₂} → has-level (S (S n)) Bool
  Bool-level = set-has-level-SS Bool-is-set

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
open import Coinduction using ( ∞ ; ♯_ ; ♭ )
open import Data.Product using ( _×_ ; _,_ ; proj₁ )
open import FRP.LTL.Time.Bound using
  ( Time∞ ; _≼_ ; _≺_ ; fin ; +∞ ; +∞-top
  ; ≼-refl ; _≼-trans_ ; ≡-impl-≽ ; ≺-impl-≼ ; ≺-impl-⋡ ; t≺+∞
  ; _≼-case_ ; lt ; eq ; gt )
open import FRP.LTL.Time.Interval using ( [_⟩ ; _⊑_ ; _~_ ; _⌢_∵_ )
open import FRP.LTL.ISet.Causal using ( _⊵_ ; _∙_⊸_∙_ ; done ; inp ; out ; _/_/_ )
open import FRP.LTL.ISet.Core using ( ISet ; [_] ; _,_ ; ⟦_⟧ ; M⟦_⟧ ; splitM⟦_⟧ ; subsumM⟦_⟧ )
open import FRP.LTL.ISet.Stateless using ( _⇒_ )
open import FRP.LTL.Util using ( ⊥-elim ; ≡-relevant )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )

module FRP.LTL.ISet.Product where

_∧_ : ISet → ISet → ISet
A ∧ B = [ (λ i → M⟦ A ⟧ i × M⟦ B ⟧ i) , split , subsum ] where

  split : ∀ i j i~j →
    (M⟦ A ⟧ (i ⌢ j ∵ i~j) × M⟦ B ⟧ (i ⌢ j ∵ i~j)) →
      ((M⟦ A ⟧ i × M⟦ B ⟧ i) × (M⟦ A ⟧ j × M⟦ B ⟧ j))
  split i j i~j (σ , τ) with splitM⟦ A ⟧ i j i~j σ | splitM⟦ B ⟧ i j i~j τ
  split i j i~j (σ , τ) | (σ₁ , σ₂) | (τ₁ , τ₂) = ((σ₁ , τ₁) , (σ₂ , τ₂))

  subsum : ∀ i j → (i ⊑ j) → (M⟦ A ⟧ j × M⟦ B ⟧ j) → (M⟦ A ⟧ i × M⟦ B ⟧ i)
  subsum i j i⊑j (σ , τ) = (subsumM⟦ A ⟧ i j i⊑j σ , subsumM⟦ B ⟧ i j i⊑j τ)

-- We could define fst and snd in terms of arr, but we define them explictly for efficiency.

π₁ : ∀ {A B} t → ((A ∧ B) ∙ t ⊸ A ∙ t)
π₁ {A} {B} +∞      = done refl
π₁ {A} {B} (fin t) = inp ≼-refl t≺+∞ P where

  P : ∀ {u} .(t≺u : fin t ≺ u) → M⟦ A ∧ B ⟧ [ t≺u ⟩ → ∞ ((A ∧ B) ∙ u ⊸ A ∙ fin t)
  P {u} t≺u [ σ , τ ] = ♯ out t≺u σ (♯ π₁ u)

fst : ∀ {A B} → ⟦ A ∧ B ⊵ A ⟧
fst = [ (λ t t∈i → π₁ (fin t)) ]

π₂ : ∀ {A B} t → ((A ∧ B) ∙ t ⊸ B ∙ t)
π₂ {A} {B} +∞      = done refl
π₂ {A} {B} (fin t) = inp ≼-refl t≺+∞ Q where

  Q : ∀ {u} .(t≺u : fin t ≺ u) → M⟦ A ∧ B ⟧ [ t≺u ⟩ → ∞ ((A ∧ B) ∙ u ⊸ B ∙ fin t)
  Q {u} t≺u [ σ , τ ] = ♯ out t≺u τ (♯ π₂ u)

snd : ∀ {A B} → ⟦ A ∧ B ⊵ B ⟧
snd = [ (λ t t∈i → π₂ (fin t)) ]

-- Mediating morphism

_&&_ : ∀ {A B C s t} → (A ∙ s ⊸ B ∙ t) → (A ∙ s ⊸ C ∙ t) → (A ∙ s ⊸ (B ∧ C) ∙ t)
inp s≼t t≺∞ P   && Q               = inp s≼t t≺∞ (λ s≺u σ → ♯ (♭ (P s≺u σ)   && (Q / s≺u / σ)))
P               && inp s≼t t≺∞ Q   = inp s≼t t≺∞ (λ s≺u σ → ♯ ((P / s≺u / σ) && ♭ (Q s≺u σ)))
P               && done t≡∞        = done t≡∞
done t≡∞        && Q               = done t≡∞
out {u} t≺u σ P && out {v} t≺v τ Q with u ≼-case v
out t≺u σ P     && out t≺v τ Q | lt u≺v with splitM⟦ _ ⟧ [ t≺u ⟩ [ u≺v ⟩ refl τ
out t≺u σ P     && out t≺v τ Q | lt u≺v | (τ₁ , τ₂) = out t≺u [ σ , τ₁ ] (♯ (♭ P && out u≺v τ₂ Q))
out t≺u σ P     && out t≺v τ Q | eq u≡v with ≡-relevant u≡v
out t≺u σ P     && out t≺v τ Q | eq u≡v | refl      = out t≺u [ σ , τ ] (♯ (♭ P && ♭ Q))
out t≺u σ P     && out t≺v τ Q | gt v≺u with splitM⟦ _ ⟧ [ t≺v ⟩ [ v≺u ⟩ refl σ
out t≺u σ P     && out t≺v τ Q | gt v≺u | (σ₁ , σ₂) = out t≺v [ σ₁ , τ ] (♯ (out v≺u σ₂ P && ♭ Q))

_&&&_ : ∀ {A B C} → ⟦ (A ⊵ B) ⇒ (A ⊵ C) ⇒ (A ⊵ (B ∧ C)) ⟧
[ [ f ] ] &&& [ [ g ] ] = [ (λ t t∈i → f t t∈i && g t t∈i) ]

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
module UselessAbstractPrimitive where

postulate Int : Set

{-# BUILTIN INTEGER Int #-}

abstract
  primitive
    primIntegerPlus : Int -> Int -> Int

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

-- This library is licensed under 0BSD. You can read more about it at its GitHub repository: https://github.com/Zambonifofex/lightlib

module index where

-- The `Light.Libary` file exports modules referencing interface files and other miscellaneous files in the library.
import Light.Library

-- The `Light.Implementation` file exports modules referencing files that provide an implementation for the interfaces above.
import Light.Implementation

-- The `Light` file can be used conveniently to use the given implementation for their appropriate interfaces.
import Light

-- The `Light.Implementation.Standard` file provides an implementation that uses definitions from the standard library: https://github.com/agda/agda-stdlib
import Light.Implementation.Standard

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
open import Everything

module Test.Test7 where

  𝓅rop-id : ∀
    {𝔵} {𝔛 : Ø 𝔵}
    {𝔞} {𝔄 : 𝔛 → Ø 𝔞}
    {𝔟} {𝔅 : 𝔛 → Ø 𝔟}
    (let _∼_ = Arrow 𝔄 𝔅)
    {ℓ̇} {_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ̇}
    ⦃ _ : Transitivity.class _∼_ ⦄
    ⦃ _ : Reflexivity.class _∼_ ⦄
    ⦃ _ : Transleftidentity!.class _∼_ _∼̇_ ⦄
    ⦃ _ : ∀ {x y} → Symmetry.class (_∼̇_ {x} {y}) ⦄
    {m n}
    {ℓ} {f : m ∼ n} (P : ExtensionṖroperty ℓ (Arrow 𝔄 𝔅 m) _∼̇_) (let P₀ = π₀ (π₀ P))
    → P₀ f
    → P₀ (ε ∙ f)

  𝓅rop-id P Pf = hmap _ P Pf


text:
{-

          Types Summer School 2007

                 Bertinoro
             Aug 19 - 31, 2007

                   Agda

                Ulf Norell

-}

-- Now we're getting somewhere! Inductive families of datatypes.

module Families where

-- You can import modules defined in other files.
-- More details later...
-- open import Nat

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

_+_ : Nat -> Nat -> Nat
zero + m = m
suc n + m = suc (n + m)

-- Think of an inductive family...

data Vec (A : Set) : Nat -> Set where
  []   : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

infixr 40 _::_

-- Some simple functions
head : {A : Set}{n : Nat} -> Vec A (suc n) -> A
head (x :: _) = x  -- no need for a [] case

-- Does the definition look familiar?
map : {A B : Set}{n : Nat} -> (A -> B) -> Vec A n -> Vec B n
map f []        = []
map f (x :: xs) = f x :: map f xs

infixr 40 _++_

_++_ : {A : Set}{n m : Nat} -> Vec A n -> Vec A m -> Vec A (n + m)
[]        ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

-- Why does this type check? Let's walk through it slowly.
-- When pattern matching on the first vector, n is instantiated.

-- What happens if we make the lengths explicit?

cat : {A : Set}(n m : Nat) -> Vec A n -> Vec A m -> Vec A (n + m)
cat .zero    m []              ys = ys
cat .(suc n) m (_::_ {n} x xs) ys = x :: (cat n m xs ys)

-- Patterns which get instantiated by pattern matching on other stuff
-- get tagged by a dot. If you erase all the dotted things you get a
-- well-formed linear first-order pattern.

-- Inside the dot we could have arbitrary terms. For instance,

data Image_∋_ {A B : Set}(f : A -> B) : B -> Set where
  im : (x : A) -> Image f ∋ f x

inv : {A B : Set}(f : A -> B)(y : B) -> Image f ∋ y -> A
inv f .(f x) (im x) = x

-- Let's do some other interesting families.

-- The identity type.
data _==_ {A : Set} : A -> A -> Set where
  refl : (x : A) -> x == x

subst : {A : Set}(C : A -> Set)(x y : A) -> x == y -> C x -> C y
subst C .x .x (refl x) cx = cx

-- Finite sets

{-

Fin zero        -
Fin (suc zero)  fzero
Fin 2           fzero, fsuc fzero

-}

data Fin : Nat -> Set where
  fzero : {n : Nat} -> Fin (suc n)
  fsuc  : {n : Nat} -> Fin n -> Fin (suc n)

_!_ : {A : Set}{n : Nat} -> Vec A n -> Fin n -> A
[]        ! ()
(x :: xs) ! fzero  = x
(x :: xs) ! fsuc i = xs ! i

{-

  What's next?

-}

-- Actually, inductive families are sufficiently fun that
-- you'll never get bored, but there's even more fun to be had.

-- Move on to: Filter.agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS -Wall #-}

module noinfixdecl where

-- warning acts on data constructors
data #2 : Set where
  one  : #2
  two  : #2
  neg_ : #2 → #2

-- warning acts on definitions
infixl 3 _⊓_
_⊔_ : #2 → #2 → #2
_⊓_ : #2 → #2 → #2

one     ⊔ n = n
two     ⊔ n = two
(neg v) ⊔ n = neg (v ⊓ neg n)

one     ⊓ n = one
two     ⊓ n = n
(neg m) ⊓ n = neg (m ⊔ (neg n))

-- warning acts on postulates
postulate _≤_ : #2 → #2 → Set

-- warning does not act on 'closed' mixfix definitions
postulate [_] : #2 → Set


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

open import lib.Basics
open import lib.NType2
open import lib.types.Nat
open import lib.types.TLevel
open import lib.types.Empty
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Truncation
open import lib.types.Pointed
open import lib.types.Group
open import lib.types.LoopSpace
open import lib.groups.TruncationGroup
open import lib.groups.GroupProduct
open import lib.groups.Homomorphisms
open import lib.groups.Unit

module lib.groups.HomotopyGroup where

{- Higher homotopy groups -}
module _ {i} where

  πS : (n : ℕ) (X : Ptd i) → Group i
  πS n X = Trunc-group (Ω^S-group-structure n X)

  fundamental-group : (X : Ptd i) → Group i
  fundamental-group X = πS 0 X

{- π_(n+1) of a space is π_n of its loop space -}
abstract
  πS-inner-iso : ∀ {i} (n : ℕ) (X : Ptd i)
    → πS (S n) X == πS n (⊙Ω X)
  πS-inner-iso n X = group-ua
    (record {
       f = Trunc-fmap (Ω^-inner-out (S n) X);
       pres-comp =
         Trunc-elim (λ _ → Π-level (λ _ → =-preserves-level _ Trunc-level))
           (λ p → Trunc-elim (λ _ → =-preserves-level _ Trunc-level)
              (λ q → ap [_] (Ω^S-inner-out-conc^S n X p q)))} ,
     is-equiv-Trunc 0 (Ω^-inner-out (S n) X) (Ω^-inner-is-equiv (S n) X))

{- We can shift the truncation inside the loop in the definition of π -}
module _ {i} where

  private
    record Ω^STs-PreIso (m : ℕ₋₂) (n : ℕ) (k : ℕ₋₂) (X : Ptd i)
      : Type i where
      field
        F : fst (⊙Ω^ (S n) (⊙Trunc k X) ⊙→ ⊙Trunc m (⊙Ω^ (S n) X))
        pres-comp : ∀ (p q : Ω^ (S n) (⊙Trunc k X))
          → fst F (conc^S n p q) == Trunc-fmap2 (conc^S n) (fst F p) (fst F q)
        e : is-equiv (fst F)

    Ω^S-Trunc-shift-preiso : (n : ℕ) (m : ℕ₋₂) (X : Ptd i)
      → Ω^STs-PreIso m n (⟨ S n ⟩₋₂ +2+ m) X
    Ω^S-Trunc-shift-preiso O m X =
      record { F = (–> (Trunc=-equiv [ snd X ] [ snd X ]) , idp);
               pres-comp = Trunc=-∙-comm;
               e = snd (Trunc=-equiv [ snd X ] [ snd X ]) }
    Ω^S-Trunc-shift-preiso (S n) m X =
      let
        r : Ω^STs-PreIso (S m) n (⟨ S n ⟩₋₂ +2+ S m) X
        r = Ω^S-Trunc-shift-preiso n (S m) X

        H = (–> (Trunc=-equiv [ idp^ (S n) ] [ idp^ (S n) ]) , idp)
        G = ap^ 1 (Ω^STs-PreIso.F r)
      in
      transport (λ k → Ω^STs-PreIso m (S n) k X)
        (+2+-βr ⟨ S n ⟩₋₂ m)
        (record {
           F = H ⊙∘ G;
           pres-comp = λ p q →
             ap (fst H) (ap^S-conc^S 0 (Ω^STs-PreIso.F r) p q)
             ∙ (Trunc=-∙-comm (fst G p) (fst G q));
           e = snd (Trunc=-equiv [ idp^ (S n) ] [ idp^ (S n) ]
                    ∘e equiv-ap^ 1 (Ω^STs-PreIso.F r) (Ω^STs-PreIso.e r))})

  πS-Trunc-shift-iso : (n : ℕ) (X : Ptd i)
    → Ω^S-group n (⊙Trunc ⟨ S n ⟩ X) Trunc-level == πS n X
  πS-Trunc-shift-iso n X = group-ua (group-hom (fst F) pres-comp , e)
    where
    n-eq : ∀ (n : ℕ) → ⟨ n ⟩₋₂ +2+ 0 == ⟨ n ⟩
    n-eq O = idp
    n-eq (S n) = ap S (n-eq n)

    r = transport (λ k → Ω^STs-PreIso 0 n k X)
                  (n-eq (S n)) (Ω^S-Trunc-shift-preiso n 0 X)
    open Ω^STs-PreIso r

abstract
  πS-below-trunc : ∀ {i} (n : ℕ) (m : ℕ₋₂) (X : Ptd i)
    → (⟨ S n ⟩ ≤T m) → πS n (⊙Trunc m X) == πS n X
  πS-below-trunc n m X lte =
    πS n (⊙Trunc m X)
      =⟨ ! (πS-Trunc-shift-iso n (⊙Trunc m X)) ⟩
    Ω^S-group n (⊙Trunc ⟨ S n ⟩ (⊙Trunc m X)) Trunc-level
      =⟨ lemma ⟩
    Ω^S-group n (⊙Trunc ⟨ S n ⟩ X) Trunc-level
      =⟨ πS-Trunc-shift-iso n X ⟩
    πS n X ∎
    where
    lemma : Ω^S-group n (⊙Trunc ⟨ S n ⟩ (⊙Trunc m X)) Trunc-level
         ==  Ω^S-group n (⊙Trunc ⟨ S n ⟩ X) Trunc-level
    lemma = ap (uncurry $ Ω^S-group n) $
      pair=
        (⊙ua (⊙≃-in (fuse-Trunc (fst X) ⟨ S n ⟩ m) idp) ∙
         ap (λ k → ⊙Trunc k X) (minT-out-l lte))
        (prop-has-all-paths-↓ has-level-is-prop)

  πS-above-trunc : ∀ {i} (n : ℕ) (m : ℕ₋₂) (X : Ptd i)
    → (m <T ⟨ S n ⟩) → πS n (⊙Trunc m X) == 0ᴳ
  πS-above-trunc n m X lt =
    πS n (⊙Trunc m X)
      =⟨ ! (πS-Trunc-shift-iso n (⊙Trunc m X)) ⟩
    Ω^S-group n (⊙Trunc ⟨ S n ⟩ (⊙Trunc m X)) Trunc-level
      =⟨ contr-is-0ᴳ _ $ inhab-prop-is-contr
           (Group.ident (Ω^S-group n (⊙Trunc ⟨ S n ⟩ (⊙Trunc m X)) Trunc-level))
           (Ω^-level-in -1 (S n) _ $ Trunc-preserves-level ⟨ S n ⟩ $
             raise-level-≤T
               (transport (λ k → m ≤T k) (+2+-comm -1 ⟨ S n ⟩₋₂) (<T-to-≤T lt))
               (Trunc-level {n = m})) ⟩
    0ᴳ ∎

  πS-above-level : ∀ {i} (n : ℕ) (m : ℕ₋₂) (X : Ptd i)
    → (m <T ⟨ S n ⟩) → has-level m (fst X)
    → πS n X == 0ᴳ
  πS-above-level n m X lt pX =
    ap (πS n) (! (⊙ua (⊙≃-in (unTrunc-equiv _ pX) idp)))
    ∙ πS-above-trunc n m X lt

{- πₙ(X × Y) == πₙ(X) × πₙ(Y) -}
module _ {i j} (n : ℕ) (X : Ptd i) (Y : Ptd  j) where

  πS-× : πS n (X ⊙× Y) == πS n X ×ᴳ πS n Y
  πS-× =
    group-ua (Trunc-group-iso f pres-comp (is-eq f g f-g g-f))
    ∙ Trunc-group-× _ _
    where
    f : Ω^ (S n) (X ⊙× Y) → Ω^ (S n) X × Ω^ (S n) Y
    f r = (fst (ap^ (S n) ⊙fst) r , fst (ap^ (S n) ⊙snd) r)

    g : Ω^ (S n) X × Ω^ (S n) Y → Ω^ (S n) (X ⊙× Y)
    g = fst (ap2^ (S n) (⊙idf _))

    f-g : (s : Ω^ (S n) X × Ω^ (S n) Y) → f (g s) == s
    f-g (p , q) = pair×=
      (app= (ap fst (ap^-ap2^ (S n) ⊙fst (⊙idf _) ∙ ap2^-fst (S n))) (p , q))
      (app= (ap fst (ap^-ap2^ (S n) ⊙snd (⊙idf _) ∙ ap2^-snd (S n))) (p , q))

    g-f : (r : Ω^ (S n) (X ⊙× Y)) → g (f r) == r
    g-f = app= $ ap fst $
      ap (λ h → h ⊙∘ ⊙diag) (ap2^-ap^ (S n) (⊙idf _) ⊙fst ⊙snd)
      ∙ ap2^-diag (S n) (⊙idf _ ⊙∘ pair⊙→ ⊙fst ⊙snd)
      ∙ ap^-idf (S n)

    pres-comp : (p q : Ω^ (S n) (X ⊙× Y))
      → f (conc^S n p q) == (conc^S n (fst (f p)) (fst (f q)) ,
                             conc^S n (snd (f p)) (snd (f q)))
    pres-comp p q = pair×= (ap^S-conc^S n ⊙fst p q) (ap^S-conc^S n ⊙snd p q)

module _ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j} (f : fst (X ⊙→ Y)) where

  πS-fmap : πS n X →ᴳ πS n Y
  πS-fmap = Trunc-group-hom (fst (ap^ (S n) f)) (ap^S-conc^S n f)

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
module Human.Test where

open import Human.Humanity

-- sum 7
-- 0 + 1 + 2 + 3 + 4 + 5 + 6

-- function sum(x) {
  -- var result = 0;
  -- for (var i = 0; i < 10; ++i) {
    -- result = result + i;
  -- }
  -- return result;
-- }

sum : Nat → Nat
sum i =
  init 0
  for i from 0 to 10 do:
    λ result → result + 1

max_stars_repo_name: MaisaMilena/JuiceMaker

max_issues_repo_name: MaisaMilena/JuiceMaker

max_forks_repo_name: MaisaMilena/JuiceMaker


text:
------------------------------------------------------------------------
-- A small library of derived parser combinators
------------------------------------------------------------------------

module TotalParserCombinators.Lib where

open import Category.Monad
open import Codata.Musical.Notation
open import Function.Base
open import Function.Equality using (_⟶_; _⟨$⟩_)
open import Function.Injection using (Injection; Injective)
open import Function.Inverse using (_↔_; module Inverse)
open import Data.Bool hiding (_≤?_)
open import Data.Char as Char using (Char; _==_)
open import Data.List as List
import Data.List.Categorical
open import Data.List.Membership.Propositional
import Data.List.Membership.Propositional.Properties as ∈
open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
open import Data.List.Relation.Unary.Any
open import Data.Maybe hiding (_>>=_)
open import Data.Nat hiding (_^_)
open import Data.Product as Prod
open import Data.Unit using (⊤)
open import Data.Vec as Vec using (Vec; []; _∷_)
import Level
open import Relation.Binary
open import Relation.Binary.HeterogeneousEquality as H using (_≅_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
import Relation.Binary.PropositionalEquality.WithK as P
open import Relation.Nullary
open import Relation.Nullary.Decidable

private
  open module ListMonad =
         RawMonad {f = Level.zero} Data.List.Categorical.monad
         using ()
         renaming (_<$>_ to _<$>′_; _⊛_ to _⊛′_; _>>=_ to _>>=′_)

import TotalParserCombinators.InitialBag as I
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics as S
  hiding (_≅_; return; token)

------------------------------------------------------------------------
-- Kleene star

-- The intended semantics of the Kleene star.

infixr 5 _∷_
infix  4 _∈[_]⋆·_

data _∈[_]⋆·_ {Tok R xs} :
              List R → Parser Tok R xs → List Tok → Set₁ where
  []  : ∀ {p} → [] ∈[ p ]⋆· []
  _∷_ : ∀ {x xs s₁ s₂ p} →
        (x∈p : x ∈ p · s₁) (xs∈p⋆ : xs ∈[ p ]⋆· s₂) →
        x ∷ xs ∈[ p ]⋆· s₁ ++ s₂

-- An implementation which requires that the argument parser is not
-- nullable.

infix 55 _⋆ _+

mutual

  _⋆ : ∀ {Tok R} →
       Parser Tok R        [] →
       Parser Tok (List R) [ [] ]
  p ⋆ = return [] ∣ p +

  _+ : ∀ {Tok R} →
       Parser Tok R        [] →
       Parser Tok (List R) []
  p + = _∷_ <$> p ⊛ ♯ (p ⋆)

module KleeneStar where

  -- The implementation is correct.

  sound : ∀ {Tok R xs s} {p : Parser Tok R []} →
          xs ∈ p ⋆ · s → xs ∈[ p ]⋆· s
  sound (∣-left S.return)              = []
  sound (∣-right ._ (<$> x∈p ⊛ xs∈p⋆)) = x∈p ∷ sound xs∈p⋆

  complete : ∀ {Tok R xs s} {p : Parser Tok R []} →
             xs ∈[ p ]⋆· s → xs ∈ p ⋆ · s
  complete []                           = ∣-left S.return
  complete (_∷_ {s₁ = []}    x∈p xs∈p⋆) with I.complete x∈p
  ... | ()
  complete (_∷_ {s₁ = _ ∷ _} x∈p xs∈p⋆) =
    ∣-right [ [] ] ([ ○ - ◌ ] <$> x∈p ⊛ complete xs∈p⋆)

  complete∘sound :
    ∀ {Tok R xs s} {p : Parser Tok R []} (xs∈ : xs ∈ p ⋆ · s) →
    complete (sound xs∈) ≡ xs∈
  complete∘sound (∣-left S.return) = P.refl
  complete∘sound (∣-right ._ (_⊛_ {s₁ = _ ∷ _} (<$> x∈p) xs∈p⋆))
    rewrite complete∘sound xs∈p⋆ = P.refl
  complete∘sound (∣-right ._ (_⊛_ {s₁ = []}    (<$> x∈p) xs∈p⋆))
    with I.complete x∈p
  ... | ()

  sound∘complete : ∀ {Tok R xs s} {p : Parser Tok R []}
                   (xs∈ : xs ∈[ p ]⋆· s) →
                   sound (complete xs∈) ≡ xs∈
  sound∘complete []                           = P.refl
  sound∘complete (_∷_ {s₁ = []}    x∈p xs∈p⋆) with I.complete x∈p
  ... | ()
  sound∘complete (_∷_ {s₁ = _ ∷ _} x∈p xs∈p⋆) =
    P.cong (_∷_ x∈p) $ sound∘complete xs∈p⋆

  correct : ∀ {Tok R xs s} {p : Parser Tok R []} →
            xs ∈ p ⋆ · s ↔ xs ∈[ p ]⋆· s
  correct = record
    { to         = P.→-to-⟶ sound
    ; from       = P.→-to-⟶ complete
    ; inverse-of = record
      { left-inverse-of  = complete∘sound
      ; right-inverse-of = sound∘complete
      }
    }

  -- The definition of _⋆ is restricted to non-nullable parsers. This
  -- restriction cannot be removed: an unrestricted Kleene star
  -- operator would be incomplete because, in the present framework, a
  -- parser can only return a finite number of results.

  unrestricted-incomplete :
    ∀ {R Tok} →
    R →
    (f : ∀ {xs} → Parser Tok R xs → List (List R)) →
    (_⋆′ : ∀ {xs} (p : Parser Tok R xs) → Parser Tok (List R) (f p)) →
    ¬ (∀ {xs ys s} {p : Parser Tok R ys} →
         xs ∈[ p ]⋆· s → xs ∈ p ⋆′ · s)
  unrestricted-incomplete {R} x f _⋆′ complete =
    ∈.finite (record { to = to; injective = injective })
             (f (return x)) (I.complete ∘ complete ∘ lemma)
    where
    to : P.setoid ℕ ⟶ P.setoid (List R)
    to = P.→-to-⟶ (flip replicate x)

    helper : ∀ {xs ys} → _≡_ {A = List R} (x ∷ xs) (x ∷ ys) → xs ≡ ys
    helper P.refl = P.refl

    injective : Injective to
    injective {zero}  {zero}  _  = P.refl
    injective {suc m} {suc n} eq = P.cong suc $
                                     injective $ helper eq
    injective {zero}  {suc n} ()
    injective {suc m} {zero}  ()

    lemma : ∀ i → replicate i x ∈[ return x ]⋆· []
    lemma zero    = []
    lemma (suc i) = S.return ∷ lemma i

------------------------------------------------------------------------
-- A combinator for recognising a string a fixed number of times

infixl 55 _^_ _↑_

^-initial : ∀ {R} → List R → (n : ℕ) → List (Vec R n)
^-initial xs zero    = [ [] ]
^-initial xs (suc n) = List.map _∷_ xs ⊛′ ^-initial xs n

_^_ : ∀ {Tok R xs} →
      Parser Tok R xs → (n : ℕ) → Parser Tok (Vec R n) (^-initial xs n)
p ^ 0     = return []
p ^ suc n = _∷_ <$> p ⊛ p ^ n

mutual

  -- A variant.

  -- The two functions below are not actually mutually recursive, but
  -- are placed in a mutual block to ensure that the constraints
  -- generated by the second function can be used to instantiate the
  -- underscores in the body of the first.

  ↑-initial : ∀ {R} → List R → ℕ → List (List R)
  ↑-initial _ _ = _

  _↑_ : ∀ {Tok R xs} →
        Parser Tok R xs → (n : ℕ) → Parser Tok (List R) (↑-initial xs n)
  p ↑ n = Vec.toList <$> p ^ n

-- Some lemmas relating _↑_ to _⋆.

module Exactly where

  ↑≲⋆ : ∀ {Tok R} {p : Parser Tok R []} n → p ↑ n ≲ p ⋆
  ↑≲⋆ {R = R} {p} n (<$> ∈pⁿ) = KleeneStar.complete $ helper n ∈pⁿ
    where
    helper : ∀ n {xs s} → xs ∈ p ^ n · s → Vec.toList xs ∈[ p ]⋆· s
    helper zero    S.return       = []
    helper (suc n) (<$> ∈p ⊛ ∈pⁿ) = ∈p ∷ helper n ∈pⁿ

  ⋆≲∃↑ : ∀ {Tok R} {p : Parser Tok R []} {xs s} →
         xs ∈ p ⋆ · s → ∃ λ i → xs ∈ p ↑ i · s
  ⋆≲∃↑ {R = R} {p} ∈p⋆ with helper $ KleeneStar.sound ∈p⋆
    where
    helper : ∀ {xs s} → xs ∈[ p ]⋆· s →
             ∃₂ λ i (ys : Vec R i) →
                  xs ≡ Vec.toList ys × ys ∈ p ^ i · s
    helper []         = (0 , [] , P.refl , S.return)
    helper (∈p ∷ ∈p⋆) =
      Prod.map suc (λ {i} →
        Prod.map (_∷_ _) (
          Prod.map (P.cong (_∷_ _))
                   (λ ∈pⁱ → [ ○ - ○ ] <$> ∈p ⊛ ∈pⁱ)))
       (helper ∈p⋆)
  ... | (i , ys , P.refl , ∈pⁱ) = (i , <$> ∈pⁱ)

------------------------------------------------------------------------
-- A parser which returns any element in a given list

return⋆ : ∀ {Tok R} (xs : List R) → Parser Tok R xs
return⋆ []       = fail
return⋆ (x ∷ xs) = return x ∣ return⋆ xs

module Return⋆ where

  sound : ∀ {Tok R x} {s : List Tok}
          (xs : List R) → x ∈ return⋆ xs · s → s ≡ [] × x ∈ xs
  sound []       ()
  sound (y ∷ ys) (∣-left S.return)       = (P.refl , here P.refl)
  sound (y ∷ ys) (∣-right .([ y ]) x∈ys) =
    Prod.map id there $ sound ys x∈ys

  complete : ∀ {Tok R x} {xs : List R} →
             x ∈ xs → x ∈ return⋆ {Tok} xs · []
  complete (here P.refl) = ∣-left S.return
  complete (there x∈xs)  =
    ∣-right [ _ ] (complete x∈xs)

  complete∘sound : ∀ {Tok R x} {s : List Tok}
                   (xs : List R) (x∈xs : x ∈ return⋆ xs · s) →
                   complete {Tok = Tok} (proj₂ $ sound xs x∈xs) ≅ x∈xs
  complete∘sound []       ()
  complete∘sound (y ∷ ys) (∣-left S.return)       = H.refl
  complete∘sound (y ∷ ys) (∣-right .([ y ]) x∈ys)
    with sound ys x∈ys | complete∘sound ys x∈ys
  complete∘sound (y ∷ ys) (∣-right .([ y ]) .(complete p))
    | (P.refl , p) | H.refl = H.refl

  sound∘complete : ∀ {Tok R x} {xs : List R} (x∈xs : x ∈ xs) →
                   sound {Tok = Tok} {s = []} xs (complete x∈xs) ≡
                   (P.refl , x∈xs)
  sound∘complete       (here P.refl)          = P.refl
  sound∘complete {Tok} (there {xs = xs} x∈xs)
    with sound {Tok = Tok} xs (complete x∈xs)
       | sound∘complete {Tok} {xs = xs} x∈xs
  sound∘complete (there x∈xs) | .(P.refl , x∈xs) | P.refl = P.refl

  correct : ∀ {Tok R} {xs : List R} {x s} →
            (s ≡ [] × x ∈ xs) ↔ x ∈ return⋆ {Tok} xs · s
  correct {xs = xs} {x} = record
    { to         = P.→-to-⟶ complete′
    ; from       = P.→-to-⟶ $ sound xs
    ; inverse-of = record
      { left-inverse-of  = sound∘complete′
      ; right-inverse-of = complete′∘sound xs
      }
    }
    where
    complete′ : ∀ {Tok R x} {xs : List R} {s : List Tok} →
                s ≡ [] × x ∈ xs → x ∈ return⋆ xs · s
    complete′ (P.refl , x∈xs) = complete x∈xs

    sound∘complete′ : ∀ {Tok R x} {xs : List R} {s : List Tok}
                      (p : s ≡ [] × x ∈ xs) → sound xs (complete′ p) ≡ p
    sound∘complete′ (P.refl , x∈xs) = sound∘complete x∈xs

    complete′∘sound : ∀ {Tok R x} {s : List Tok}
                      (xs : List R) (x∈xs : x ∈ return⋆ xs · s) →
                      complete′ (sound xs x∈xs) ≡ x∈xs
    complete′∘sound xs x∈ with sound xs x∈ | complete∘sound xs x∈
    complete′∘sound xs .(complete x∈xs) | (P.refl , x∈xs) | H.refl =
      P.refl

------------------------------------------------------------------------
-- The sat parser

module Sat where

  -- Helper functions for sat.

  mutual

    ok-bag : {R : Set} → Maybe R → List R
    ok-bag nothing  = _
    ok-bag (just _) = _

    ok : {Tok R : Set} → (x : Maybe R) → Parser Tok R (ok-bag x)
    ok nothing  = fail
    ok (just x) = return x

  ok-correct : ∀ {Tok R x s} (m : Maybe R) →
               (s ≡ [] × m ≡ just x) ↔ x ∈ ok {Tok} m · s
  ok-correct {Tok} {x = x} m = record
    { to         = P.→-to-⟶ (to m)
    ; from       = P.→-to-⟶ (from m)
    ; inverse-of = record
      { left-inverse-of  = from∘to m
      ; right-inverse-of = to∘from m
      }
    }
    where
    to : ∀ {s} m → (s ≡ [] × m ≡ just x) → x ∈ ok {Tok} m · s
    to (just .x) (P.refl , P.refl) = S.return
    to nothing   (P.refl , ())

    from : ∀ {s} m → x ∈ ok {Tok} m · s → s ≡ [] × m ≡ just x
    from (just .x) S.return = (P.refl , P.refl)
    from nothing   ()

    from∘to : ∀ {s} m (eqs : s ≡ [] × m ≡ just x) →
              from m (to m eqs) ≡ eqs
    from∘to (just .x) (P.refl , P.refl) = P.refl
    from∘to nothing   (P.refl , ())

    to∘from : ∀ {s} m (x∈ : x ∈ ok {Tok} m · s) →
              to m (from m x∈) ≡ x∈
    to∘from (just .x) S.return = P.refl
    to∘from nothing   ()

  -- sat p accepts a single token t iff p t ≡ just x for some x. The
  -- returned value is x.

  sat : ∀ {Tok R} → (Tok → Maybe R) → Parser Tok R _
  sat p = token >>= (ok ∘ p)

  correct : ∀ {Tok R x s} (p : Tok → Maybe R) →
            (∃ λ t → s ≡ [ t ] × p t ≡ just x) ↔ x ∈ sat p · s
  correct {x = x} p = record
    { to         = P.→-to-⟶ to
    ; from       = P.→-to-⟶ from
    ; inverse-of = record
      { left-inverse-of  = from∘to
      ; right-inverse-of = to∘from
      }
    }
    where
    to : ∀ {s} → (∃ λ t → s ≡ [ t ] × p t ≡ just x) → x ∈ sat p · s
    to (t , P.refl , p-t≡just-x) =
      [ ○ - ○ ] S.token >>=
                (Inverse.to (ok-correct (p t)) ⟨$⟩ (P.refl , p-t≡just-x))

    from : ∀ {s} → x ∈ sat p · s → ∃ λ t → s ≡ [ t ] × p t ≡ just x
    from (S.token {x = t} >>= x∈ok-p-t) =
      (t , Prod.map (P.cong (_∷_ t)) id
             (Inverse.from (ok-correct (p t)) ⟨$⟩ x∈ok-p-t))

    from∘to : ∀ {s} (eqs : ∃ λ t → s ≡ [ t ] × p t ≡ just x) →
              from (to eqs) ≡ eqs
    from∘to (t , P.refl , p-t≡just-x) =
      P.cong₂ (λ eq₁ eq₂ → (t , eq₁ , eq₂))
              (P.≡-irrelevant _ _)
              (P.≡-irrelevant _ _)

    to∘from : ∀ {s} (x∈ : x ∈ sat p · s) → to (from x∈) ≡ x∈
    to∘from (S.token {x = t} >>= x∈ok-p-t)
      with Inverse.from (ok-correct (p t)) ⟨$⟩ x∈ok-p-t
         | Inverse.right-inverse-of (ok-correct (p t)) x∈ok-p-t
    to∘from (S.token {x = t} >>= .(Inverse.to (ok-correct (p t)) ⟨$⟩
                                     (P.refl , p-t≡just-x)))
      | (P.refl , p-t≡just-x) | P.refl = P.refl

open Sat public using (sat)

-- A simplified variant of sat. Does not return anything interesting.

sat′ : ∀ {Tok} → (Tok → Bool) → Parser Tok ⊤ _
sat′ p = sat (boolToMaybe ∘ p)

-- Accepts a single whitespace character (from a limited set of such
-- characters).

whitespace : Parser Char ⊤ _
whitespace = sat′ isSpace
  where
  isSpace = λ c →
    (c == ' ') ∨ (c == '\t') ∨ (c == '\n') ∨ (c == '\r')

------------------------------------------------------------------------
-- A parser for a given token

module Token
         (Tok : Set)
         (_≟_ : Decidable (_≡_ {A = Tok}))
         where

  private
    p : Tok → Tok → Maybe Tok
    p t t′ = if ⌊ t ≟ t′ ⌋ then just t′ else nothing

  tok : Tok → Parser Tok Tok []
  tok t = sat (p t)

  sound : ∀ t {t′ s} →
          t′ ∈ tok t · s → t ≡ t′ × s ≡ [ t′ ]
  sound t t′∈ with Inverse.from (Sat.correct (p t)) ⟨$⟩ t′∈
  sound t t′∈ | (t″ , P.refl , p-t-t″≡just-t′) with t ≟ t″
  sound t t∈  | (.t , P.refl , P.refl) | yes P.refl = (P.refl , P.refl)
  sound t t′∈ | (t″ , P.refl , ())     | no  _

  private
    p-lemma : ∀ t → p t t ≡ just t
    p-lemma t with t ≟ t
    ... | yes P.refl = P.refl
    ... | no  t≢t    with t≢t P.refl
    ...   | ()

  complete : ∀ {t} → t ∈ tok t · [ t ]
  complete {t} =
    Inverse.to (Sat.correct (p t)) ⟨$⟩ (t , P.refl , p-lemma t)

  η : ∀ {t} (t∈ : t ∈ tok t · [ t ]) → t∈ ≡ complete {t = t}
  η {t = t} t∈ = H.≅-to-≡ $ helper t∈ P.refl
    where
    helper₂ : (t∈ : t ∈ Sat.ok {Tok = Tok} (p t t) · []) →
              t∈ ≡ Inverse.to (Sat.ok-correct (p t t)) ⟨$⟩
                     (P.refl , p-lemma t)
    helper₂ t∈       with t ≟ t
    helper₂ S.return | yes P.refl = P.refl
    helper₂ t∈       | no  t≢t  with t≢t P.refl
    helper₂ t∈       | no  t≢t  | ()

    helper : ∀ {s} (t∈ : t ∈ tok t · s) → s ≡ [ t ] →
             t∈ ≅ complete {t = t}
    helper (S.token >>= t∈) P.refl rewrite helper₂ t∈ = H.refl

------------------------------------------------------------------------
-- Map then choice

-- y ∈ ⋁ f xs · s  iff  ∃ x ∈ xs. y ∈ f x · s.

⋁ : ∀ {Tok R₁ R₂} {f : R₁ → List R₂} →
    ((x : R₁) → Parser Tok R₂ (f x)) → (xs : List R₁) →
    Parser Tok R₂ (xs >>=′ f)
⋁ f xs = return⋆ xs >>= f

module ⋁ where

  sound : ∀ {Tok R₁ R₂ y s} {i : R₁ → List R₂} →
          (f : (x : R₁) → Parser Tok R₂ (i x)) (xs : List R₁) →
          y ∈ ⋁ f xs · s → ∃ λ x → (x ∈ xs) × (y ∈ f x · s)
  sound f xs (∈ret⋆ >>= y∈fx) with Return⋆.sound xs ∈ret⋆
  ...   | (P.refl , x∈xs) = (_ , x∈xs , y∈fx)

  complete : ∀ {Tok R₁ R₂ x y s} {i : R₁ → List R₂} →
             (f : (x : R₁) → Parser Tok R₂ (i x)) {xs : List R₁} →
             x ∈ xs → y ∈ f x · s → y ∈ ⋁ f xs · s
  complete f x∈xs y∈fx =
    [ ○ - ○ ] Return⋆.complete x∈xs >>= y∈fx

  complete∘sound : ∀ {Tok R₁ R₂ y s} {i : R₁ → List R₂} →
                   (f : (x : R₁) → Parser Tok R₂ (i x)) (xs : List R₁)
                   (y∈⋁fxs : y ∈ ⋁ f xs · s) →
                   let p = proj₂ $ sound f xs y∈⋁fxs in
                   complete f (proj₁ p) (proj₂ p) ≡ y∈⋁fxs
  complete∘sound f xs (∈ret⋆ >>= y∈fx)
    with Return⋆.sound xs ∈ret⋆
       | Inverse.right-inverse-of Return⋆.correct ∈ret⋆
  complete∘sound f xs (.(Return⋆.complete x∈xs) >>= y∈fx)
    | (P.refl , x∈xs) | P.refl = P.refl

  sound∘complete :
    ∀ {Tok R₁ R₂ x y s} {i : R₁ → List R₂} →
    (f : (x : R₁) → Parser Tok R₂ (i x)) {xs : List R₁} →
    (x∈xs : x ∈ xs) (y∈fx : y ∈ f x · s) →
    sound f xs (complete f x∈xs y∈fx) ≡ (x , x∈xs , y∈fx)
  sound∘complete {Tok} f {xs} x∈xs y∈fx
    with Return⋆.sound {Tok = Tok} xs (Return⋆.complete x∈xs)
       | Inverse.left-inverse-of (Return⋆.correct {Tok = Tok})
                                 (P.refl , x∈xs)
  ... | (P.refl , .x∈xs) | P.refl = P.refl

------------------------------------------------------------------------
-- Digits and numbers

-- Digits.

digit = sat (λ t → if in-range t then just (to-number t) else nothing)
  where
  in-range : Char → Bool
  in-range t = ⌊ Char.toℕ '0' ≤? Char.toℕ  t  ⌋ ∧
               ⌊ Char.toℕ  t  ≤? Char.toℕ '9' ⌋

  to-number : Char → ℕ
  to-number t = Char.toℕ t ∸ Char.toℕ '0'

-- Numbers.

number : Parser Char ℕ _
number = digit + >>= (return ∘ foldl (λ n d → 10 * n + d) 0)

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
{-
  Definition of various kinds of categories.

  This library follows the UniMath terminology, that is:

  Concept              Ob C   Hom C  Univalence

  Precategory          Type   Type   No
  Category             Type   Set    No
  Univalent Category   Type   Set    Yes

  The most useful notion is Category and the library is hence based on
  them. If one needs precategories then they can be found in
  Cubical.Categories.Category.Precategory

-}
{-# OPTIONS --safe #-}
module Cubical.Categories.Category where

open import Cubical.Categories.Category.Base public
open import Cubical.Categories.Category.Properties public

max_stars_repo_name: FernandoLarrain/cubical


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

open import Algebra
open import Relation.Unary
open import Relation.Binary hiding (Decidable)

module Data.FingerTree.Split.StoredPredicate
  {r m}
  (ℳ : Monoid r m)
  {s}
  {ℙ : Pred (Monoid.Carrier ℳ) s}
  (ℙ-resp : ℙ Respects (Monoid._≈_ ℳ))
  (ℙ? : Decidable ℙ)
  where

open Monoid ℳ renaming (Carrier to 𝓡)
open import Level using (_⊔_)
open import Relation.Nullary

infixl 2 _≈ℙ_[_]
record ⟪ℙ⟫ (x : 𝓡) : Set (s ⊔ r ⊔ m) where
  constructor _≈ℙ_[_]
  field
    result : Dec (ℙ x)
    stored : 𝓡
    equiv  : stored ≈ x
open ⟪ℙ⟫ public

⟪ℙ?⟫ : ∀ x → ⟪ℙ⟫ x
result (⟪ℙ?⟫ x) = ℙ? x
stored (⟪ℙ?⟫ x) = x
equiv  (⟪ℙ?⟫ x) = refl

max_stars_repo_name: oisdk/agda-indexed-fingertree

max_issues_repo_name: oisdk/agda-indexed-fingertree

max_forks_repo_name: oisdk/agda-indexed-fingertree


text:
------------------------------------------------------------------------
-- Commutative semirings with some additional structure ("almost"
-- commutative rings), used by the ring solver
------------------------------------------------------------------------

module Algebra.RingSolver.AlmostCommutativeRing where

open import Relation.Binary
open import Algebra
open import Algebra.Structures
open import Algebra.FunctionProperties
open import Algebra.Morphism
open import Data.Function

------------------------------------------------------------------------
-- Definitions

record IsAlmostCommutativeRing {A} (_≈_ : Rel A)
         (_+_ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set where
  field
    isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1#
    -‿pres-≈              : -_ Preserves _≈_ ⟶ _≈_
    -‿*-distribˡ          : ∀ x y → ((- x) * y)     ≈ (- (x * y))
    -‿+-comm              : ∀ x y → ((- x) + (- y)) ≈ (- (x + y))

  open IsCommutativeSemiring isCommutativeSemiring public

record AlmostCommutativeRing : Set₁ where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    carrier                 : Set
    _≈_                     : Rel carrier
    _+_                     : Op₂ carrier
    _*_                     : Op₂ carrier
    -_                      : Op₁ carrier
    0#                      : carrier
    1#                      : carrier
    isAlmostCommutativeRing :
      IsAlmostCommutativeRing _≈_ _+_ _*_ -_ 0# 1#

  open IsAlmostCommutativeRing isAlmostCommutativeRing public

  commutativeSemiring : CommutativeSemiring
  commutativeSemiring =
    record { isCommutativeSemiring = isCommutativeSemiring }

  open CommutativeSemiring commutativeSemiring public
         using ( setoid
               ; +-semigroup; +-monoid; +-commutativeMonoid
               ; *-semigroup; *-monoid; *-commutativeMonoid
               ; semiring
               )

  rawRing : RawRing
  rawRing = record
    { _≈_ = _≈_
    ; _+_ = _+_
    ; _*_ = _*_
    ; -_  = -_
    ; 0#  = 0#
    ; 1#  = 1#
    }

------------------------------------------------------------------------
-- Homomorphisms

_-Raw-AlmostCommutative⟶_ : RawRing → AlmostCommutativeRing → Set
from -Raw-AlmostCommutative⟶ to = from -RawRing⟶ rawRing to
  where open AlmostCommutativeRing

-raw-almostCommutative⟶
  : ∀ r →
    AlmostCommutativeRing.rawRing r -Raw-AlmostCommutative⟶ r
-raw-almostCommutative⟶ r = record
  { ⟦_⟧    = id
  ; +-homo = λ _ _ → refl
  ; *-homo = λ _ _ → refl
  ; -‿homo = λ _ → refl
  ; 0-homo = refl
  ; 1-homo = refl
  }
  where open AlmostCommutativeRing r

------------------------------------------------------------------------
-- Conversions

-- Commutative rings are almost commutative rings.

fromCommutativeRing : CommutativeRing → AlmostCommutativeRing
fromCommutativeRing cr = record
  { isAlmostCommutativeRing = record
      { isCommutativeSemiring = isCommutativeSemiring
      ; -‿pres-≈              = -‿pres-≈
      ; -‿*-distribˡ          = -‿*-distribˡ
      ; -‿+-comm              = -‿∙-comm
      }
  }
  where
  open CommutativeRing cr
  import Algebra.Props.Ring as R; open R ring
  import Algebra.Props.AbelianGroup as AG; open AG +-abelianGroup

-- Commutative semirings can be viewed as almost commutative rings by
-- using identity as the "almost negation".

fromCommutativeSemiring : CommutativeSemiring → AlmostCommutativeRing
fromCommutativeSemiring cs = record
  { -_                      = id
  ; isAlmostCommutativeRing = record
      { isCommutativeSemiring = isCommutativeSemiring
      ; -‿pres-≈              = id
      ; -‿*-distribˡ          = λ _ _ → refl
      ; -‿+-comm              = λ _ _ → refl
      }
  }
  where open CommutativeSemiring cs

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module Prelude.Nat.Properties where

open import Prelude.Bool
open import Prelude.Nat.Core
open import Prelude.Equality
open import Prelude.Semiring

suc-inj : ∀ {n m} → suc n ≡ suc m → n ≡ m
suc-inj refl = refl

--- Addition ---

add-zero-r : (n : Nat) → n + 0 ≡ n
add-zero-r zero    = refl
add-zero-r (suc n) = suc $≡ add-zero-r n

add-suc-r : (n m : Nat) → n + suc m ≡ suc (n + m)
add-suc-r zero    m = refl
add-suc-r (suc n) m = suc $≡ add-suc-r n m

add-commute : (a b : Nat) → a + b ≡ b + a
add-commute zero    b = sym (add-zero-r _)
add-commute (suc a) b = suc $≡ add-commute a b ⟨≡⟩ʳ add-suc-r b _

add-assoc : (a b c : Nat) → a + (b + c) ≡ a + b + c
add-assoc zero    b c = refl
add-assoc (suc a) b c = suc $≡ add-assoc a b c

add-inj₂ : (a b c : Nat) → a + b ≡ a + c → b ≡ c
add-inj₂ zero    b c eq = eq
add-inj₂ (suc a) b c eq = add-inj₂ a b c (suc-inj eq)

add-inj₁ : (a b c : Nat) → a + c ≡ b + c → a ≡ b
add-inj₁ a b c eq = add-inj₂ c a b (add-commute c a ⟨≡⟩ eq ⟨≡⟩ add-commute b c)

--- Subtraction ---

--- Multiplication ---

mul-one-r : (x : Nat) → x * 1 ≡ x
mul-one-r zero    = refl
mul-one-r (suc x) = suc $≡ mul-one-r x

mul-zero-r : (x : Nat) → x * 0 ≡ 0
mul-zero-r zero    = refl
mul-zero-r (suc x) = mul-zero-r x

mul-distr-r : (x y z : Nat) → (x + y) * z ≡ x * z + y * z
mul-distr-r zero    y z = refl
mul-distr-r (suc x) y z = z +_ $≡ mul-distr-r x y z ⟨≡⟩ add-assoc z _ _

private
  shuffle : (a b c d : Nat) → a + b + (c + d) ≡ a + c + (b + d)
  shuffle a b c d = add-assoc a _ _ ʳ⟨≡⟩
                    a +_ $≡ (add-assoc b c d ⟨≡⟩ _+ d $≡ add-commute b c ⟨≡⟩ʳ add-assoc c b d) ⟨≡⟩
                    add-assoc a _ _

mul-distr-l : (x y z : Nat) → x * (y + z) ≡ x * y + x * z
mul-distr-l zero    y z = refl
mul-distr-l (suc x) y z = y + z +_ $≡ mul-distr-l x y z ⟨≡⟩ shuffle y z (x * y) (x * z)

mul-assoc : (x y z : Nat) → x * (y * z) ≡ x * y * z
mul-assoc zero    y z = refl
mul-assoc (suc x) y z = y * z +_ $≡ mul-assoc x y z ⟨≡⟩ʳ mul-distr-r y (x * y) z

mul-commute : (x y : Nat) → x * y ≡ y * x
mul-commute x zero    = mul-zero-r x
mul-commute x (suc y) = mul-distr-l x 1 y ⟨≡⟩ _+ x * y $≡ mul-one-r x ⟨≡⟩ x +_ $≡ mul-commute x y

mul-inj₁ : (x y z : Nat) {{_ : NonZero z}} → x * z ≡ y * z → x ≡ y
mul-inj₁ x        y      zero {{}}
mul-inj₁ zero     zero   (suc z) eq = refl
mul-inj₁ zero    (suc y) (suc z) ()
mul-inj₁ (suc x) zero    (suc z) ()
mul-inj₁ (suc x) (suc y) (suc z) eq = suc $≡ mul-inj₁ x y (suc z) (add-inj₂ z _ _ (suc-inj eq))

mul-inj₂ : (x y z : Nat) {{_ : NonZero x}} → x * y ≡ x * z → y ≡ z
mul-inj₂ x y z eq = mul-inj₁ y z x (mul-commute y x ⟨≡⟩ eq ⟨≡⟩ mul-commute x z)

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Keys for AVL trees -- the original key type extended with a new
-- minimum and maximum.
-----------------------------------------------------------------------

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

open import Relation.Binary

module Data.AVL.Key
  {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
  where

open import Level
open import Data.Empty
open import Data.Unit
open import Data.Product
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
open import Relation.Nullary.Construct.Add.Extrema
  as AddExtremaToSet using (_±)
open import Relation.Binary.Construct.Add.Extrema.Strict
  as AddExtremaToOrder using ()

open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)

-----------------------------------------------------------------------
-- Keys are augmented with new extrema (i.e. an artificial minimum and
-- maximum)

Key⁺ : Set a
Key⁺ = Key ±

open AddExtremaToSet public
  using ([_]; [_]-injective)
  renaming
  ( ⊥± to ⊥⁺
  ; ⊤± to ⊤⁺
  )

-----------------------------------------------------------------------
-- The order is extended in a corresponding manner

open AddExtremaToOrder _<_ public
  using () renaming
  (_<±_    to _<⁺_
  ; [_]    to [_]ᴿ
  ; ⊥±<⊤±  to ⊥⁺<⊤⁺
  ; [_]<⊤± to [_]<⊤⁺
  ; ⊥±<[_] to ⊥⁺<[_]
  )

-- A pair of ordering constraints.

infix 4 _<_<_

_<_<_ : Key⁺ → Key → Key⁺ → Set (a ⊔ ℓ₂)
l < x < u = l <⁺ [ x ] × [ x ] <⁺ u

-- Properties

⊥⁺<[_]<⊤⁺ : ∀ k → ⊥⁺ < k < ⊤⁺
⊥⁺<[ k ]<⊤⁺ = ⊥⁺<[ k ] , [ k ]<⊤⁺

trans⁺ : ∀ l {m u} → l <⁺ m → m <⁺ u → l <⁺ u
trans⁺ l = AddExtremaToOrder.<±-trans _<_ trans


text:
open import Data.Nat

ten : ℕ
ten = 10

max_stars_repo_name: supeterlau/bedev

max_issues_repo_name: supeterlau/bedev

max_forks_repo_name: supeterlau/bedev


text:
module Data.Collection.Inclusion where

open import Data.Collection.Equivalence
open import Data.Collection.Core

open import Function using (id; _∘_)
open import Function.Equivalence using (equivalence)
open import Level using (Level; suc; zero)
open import Relation.Unary hiding (_⇒_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

≋⇒⊆ : _≋_ ⇒ _⊆_
≋⇒⊆ P≋Q ∈P = nach P≋Q ∈P

⊆-Transitive : ∀ {a ℓ} {A : Set a} → Transitive {_} {_} {Pred A ℓ} _⊆_
⊆-Transitive P⊆Q Q⊆R = Q⊆R ∘ P⊆Q

⊆-IsPreorder : IsPreorder _≋_ _⊆_
⊆-IsPreorder = record
    { isEquivalence = ≋-IsEquivalence
    ; reflexive = ≋⇒⊆
    ; trans = ⊆-Transitive
    }

⊆-Preorder : Preorder _ _ _
⊆-Preorder = record
    { Carrier = Pred String zero
    ; _≈_ = _≋_
    ; _∼_ = _⊆_
    ; isPreorder = ⊆-IsPreorder
    }

⊆-Antisymmetric : Antisymmetric _≋_ _⊆_
⊆-Antisymmetric P⊆Q Q⊆P = equivalence P⊆Q Q⊆P

⊆-IsPartialOrder : IsPartialOrder _≋_ _⊆_
⊆-IsPartialOrder = record
    { isPreorder = ⊆-IsPreorder
    ; antisym = ⊆-Antisymmetric
    }

⊆-Poset : Poset _ _ _
⊆-Poset = record
    { Carrier = Pred String zero
    ; _≈_ = _≋_
    ; _≤_ = _⊆_
    ; isPartialOrder = ⊆-IsPartialOrder
    }

--------------------------------------------------------------------------------
--  Conditional Inclusion
--------------------------------------------------------------------------------

_⊆[_]_ : ∀ {a ℓ₀ ℓ₁ ℓ₂} {A : Set a} → Pred A ℓ₀ → Pred A ℓ₁ → Pred A ℓ₂ → Set _
A ⊆[ P ] B = ∀ {x} → x ∈ P → x ∈ A → x ∈ B

_⊈[_]_ : ∀ {a ℓ₀ ℓ₁ ℓ₂} {A : Set a} → Pred A ℓ₀ → Pred A ℓ₁ → Pred A ℓ₂ → Set _
A ⊈[ P ] B = ∀ {x} → x ∈ P → x ∉ A → x ∉ B

-- prefix version of _⊆[_]_, with the predicate being the first argument
[_]⊆ : ∀ {a ℓ₀ ℓ₁ ℓ₂} {A : Set a} → Pred A ℓ₁ → Pred A ℓ₀ → Pred A ℓ₂ → Set _
[ P ]⊆ A B = A ⊆[ P ] B

≋[]⇒⊆[] : ∀ {a} {P : Pred Element a} → [ P ]≋ ⇒ [ P ]⊆
≋[]⇒⊆[] A≋B = nach ∘ A≋B

⊆[]-Transitive : ∀ {a ℓ} {P : Pred Element a} → Transitive {_} {_} {Pred String ℓ} [ P ]⊆
⊆[]-Transitive A⊆B B⊆C ∈P = B⊆C ∈P ∘ A⊆B ∈P

⊆[]-IsPreorder : ∀ {a} {P : Pred Element a} → IsPreorder [ P ]≋ [ P ]⊆
⊆[]-IsPreorder = record
    { isEquivalence = ≋[]-IsEquivalence
    ; reflexive = ≋[]⇒⊆[]
    ; trans = ⊆[]-Transitive
    }

⊆[]-Preorder : ∀ {a} {P : Pred Element a} → Preorder _ _ _
⊆[]-Preorder {_} {P} = record
    { Carrier = Pred String zero
    ; _≈_ = [ P ]≋
    ; _∼_ = [ P ]⊆
    ; isPreorder = ⊆[]-IsPreorder
    }

⊆[]-Antisymmetric : ∀ {a} {P : Pred Element a} → Antisymmetric [ P ]≋ [ P ]⊆
⊆[]-Antisymmetric P⊆Q Q⊆P ∈P = equivalence (P⊆Q ∈P) (Q⊆P ∈P)

⊆[]-IsPartialOrder : ∀ {a} {P : Pred Element a} → IsPartialOrder [ P ]≋ [ P ]⊆
⊆[]-IsPartialOrder = record
    { isPreorder = ⊆[]-IsPreorder
    ; antisym = ⊆[]-Antisymmetric
    }

⊆[]-Poset : ∀ {a} {P : Pred Element a} → Poset _ _ _
⊆[]-Poset {_} {P} = record
    { Carrier = Pred String zero
    ; _≈_ = [ P ]≋
    ; _≤_ = [ P ]⊆
    ; isPartialOrder = ⊆[]-IsPartialOrder
    }

max_stars_repo_name: banacorn/lambda-calculus

max_issues_repo_name: banacorn/lambda-calculus

max_forks_repo_name: banacorn/lambda-calculus


text:
{-# OPTIONS --without-K #-}
module well-typed-syntax-pre-interpreter where
open import common public
open import well-typed-syntax
open import well-typed-syntax-helpers

max-level : Level
max-level = lsuc lzero

module inner
  (context-pick-if' : ∀ ℓ (P : Context → Set ℓ)
                          (Γ : Context)
                          (dummy : P (ε ▻ ‘Σ’ ‘Context’ ‘Typ’))
                          (val : P Γ) →
                        P (ε ▻ ‘Σ’ ‘Context’ ‘Typ’))
  (context-pick-if-refl' : ∀ ℓ P dummy val →
                            context-pick-if' ℓ P (ε ▻ ‘Σ’ ‘Context’ ‘Typ’) dummy val ≡ val)
  where

  context-pick-if : ∀ {ℓ} {P : Context → Set ℓ}
                          {Γ : Context}
                          (dummy : P (ε ▻ ‘Σ’ ‘Context’ ‘Typ’))
                          (val : P Γ) →
                        P (ε ▻ ‘Σ’ ‘Context’ ‘Typ’)
  context-pick-if {P = P} dummy val = context-pick-if' _ P _ dummy val
  context-pick-if-refl : ∀ {ℓ P dummy val} →
                            context-pick-if {ℓ} {P} {ε ▻ ‘Σ’ ‘Context’ ‘Typ’} dummy val ≡ val
  context-pick-if-refl {P = P} = context-pick-if-refl' _ P _ _

  private
    dummy : Typ ε
    dummy = ‘Context’

  cast-helper : ∀ {X T A} {x : Term X} → A ≡ T → Term {ε} (T ‘’ x ‘→'’ A ‘’ x)
  cast-helper refl = ‘λ∙’ ‘VAR₀’

  cast'-proof : ∀ {T} → Term {ε} (context-pick-if {P = Typ} (W dummy) T ‘’ ‘existT’ ⌜ ε ▻ ‘Σ’ ‘Context’ ‘Typ’ ⌝c ⌜ T ⌝T
                ‘→'’ T ‘’ ‘existT’ ⌜ ε ▻ ‘Σ’ ‘Context’ ‘Typ’ ⌝c ⌜ T ⌝T)
  cast'-proof {T} = cast-helper {‘Σ’ ‘Context’ ‘Typ’}
                      {context-pick-if {P = Typ} {ε ▻ ‘Σ’ ‘Context’ ‘Typ’} (W dummy) T}
                      {T} (sym (context-pick-if-refl {P = Typ} {dummy = W dummy}))

  cast-proof : ∀ {T} → Term {ε} (T ‘’ ‘existT’ ⌜ ε ▻ ‘Σ’ ‘Context’ ‘Typ’ ⌝c ⌜ T ⌝T
                ‘→'’ context-pick-if {P = Typ} (W dummy) T ‘’ ‘existT’ ⌜ ε ▻ ‘Σ’ ‘Context’ ‘Typ’ ⌝c ⌜ T ⌝T)
  cast-proof {T} = cast-helper {‘Σ’ ‘Context’ ‘Typ’} {T}
                      {context-pick-if {P = Typ} {ε ▻ ‘Σ’ ‘Context’ ‘Typ’} (W dummy) T}
                      (context-pick-if-refl {P = Typ} {dummy = W dummy})

  ‘idfun’ : ∀ {T} → Term {ε} (T ‘→'’ T)
  ‘idfun’ = ‘λ∙’ ‘VAR₀’

  mutual
    Context⇓ : (Γ : Context) → Set (lsuc max-level)
    Typ⇓ : {Γ : Context} → Typ Γ → Context⇓ Γ → Set max-level

    Context⇓ ε = ⊤
    Context⇓ (Γ ▻ T) = Σ (Context⇓ Γ) (λ Γ' → Typ⇓ T Γ')

    Typ⇓ (T₁ ‘’ x) Γ⇓ = Typ⇓ T₁ (Γ⇓ , Term⇓ x Γ⇓)
    Typ⇓ (T₂ ‘’₁ a) (Γ⇓ , A⇓) = Typ⇓ T₂ ((Γ⇓ , Term⇓ a Γ⇓) , A⇓)
    Typ⇓ (T₃ ‘’₂ a) ((Γ⇓ , A⇓) , B⇓) = Typ⇓ T₃ (((Γ⇓ , Term⇓ a Γ⇓) , A⇓) , B⇓)
    Typ⇓ (T₃ ‘’₃ a) (((Γ⇓ , A⇓) , B⇓) , C⇓) = Typ⇓ T₃ ((((Γ⇓ , Term⇓ a Γ⇓) , A⇓) , B⇓) , C⇓)
    Typ⇓ (W T₁) (Γ⇓ , _) = Typ⇓ T₁ Γ⇓
    Typ⇓ (W1 T₂) ((Γ⇓ , A⇓) , B⇓) = Typ⇓ T₂ (Γ⇓ , B⇓)
    Typ⇓ (W2 T₃) (((Γ⇓ , A⇓) , B⇓) , C⇓) = Typ⇓ T₃ ((Γ⇓ , B⇓) , C⇓)
    Typ⇓ (T ‘→’ T₁) Γ⇓ = (T⇓ : Typ⇓ T Γ⇓) → Typ⇓ T₁ (Γ⇓ , T⇓)
    Typ⇓ ‘Context’ Γ⇓ = Lifted Context
    Typ⇓ ‘Typ’ (Γ⇓ , T⇓) = Lifted (Typ (lower T⇓))
    Typ⇓ ‘Term’ (Γ⇓ , T⇓ , t⇓) = Lifted (Term (lower t⇓))
    Typ⇓ (‘Σ’ T T₁) Γ⇓ = Σ (Typ⇓ T Γ⇓) (λ T⇓ → Typ⇓ T₁ (Γ⇓ , T⇓))

    Term⇓ : ∀ {Γ : Context} {T : Typ Γ} → Term T → (Γ⇓ : Context⇓ Γ) → Typ⇓ T Γ⇓
    Term⇓ (w t) (Γ⇓ , A⇓) = Term⇓ t Γ⇓
    Term⇓ (‘λ∙’ t) Γ⇓ T⇓ = Term⇓ t (Γ⇓ , T⇓)
    Term⇓ (t ‘’ₐ t₁) Γ⇓ = Term⇓ t Γ⇓ (Term⇓ t₁ Γ⇓)
    Term⇓ ‘VAR₀’ (Γ⇓ , A⇓) = A⇓
    Term⇓ (⌜ Γ ⌝c) Γ⇓ = lift Γ
    Term⇓ (⌜ T ⌝T) Γ⇓ = lift T
    Term⇓ (⌜ t ⌝t) Γ⇓ = lift t
    Term⇓ ‘quote-term’ Γ⇓ (lift T⇓) = lift ⌜ T⇓ ⌝t
    Term⇓ (‘quote-sigma’ {Γ₀} {Γ₁}) Γ⇓ (lift Γ , lift T) = lift (‘existT’ {Γ₁} ⌜ Γ ⌝c ⌜ T ⌝T)
    Term⇓ ‘cast’ Γ⇓ T⇓ = lift (context-pick-if
                              {P = Typ}
                              {lower (Σ.proj₁ T⇓)}
                              (W dummy)
                              (lower (Σ.proj₂ T⇓)))
    Term⇓ (SW t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (weakenTyp-substTyp-tProd t) Γ⇓ T⇓ = Term⇓ t Γ⇓ T⇓
    Term⇓ (substTyp-weakenTyp1-VAR₀ t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (weakenTyp-tProd t) Γ⇓ T⇓ = Term⇓ t Γ⇓ T⇓
    Term⇓ (weakenTyp-tProd-inv t) Γ⇓ T⇓ = Term⇓ t Γ⇓ T⇓
    Term⇓ (weakenTyp-weakenTyp-tProd t) Γ⇓ T⇓ = Term⇓ t Γ⇓ T⇓
    Term⇓ (substTyp1-tProd t) Γ⇓ T⇓ = Term⇓ t Γ⇓ T⇓
    Term⇓ (weakenTyp1-tProd t) Γ⇓ T⇓ = Term⇓ t Γ⇓ T⇓
    Term⇓ (substTyp2-tProd t) Γ⇓ T⇓ = Term⇓ t Γ⇓ T⇓
    Term⇓ (substTyp1-substTyp-weakenTyp-inv t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (substTyp1-substTyp-weakenTyp t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (weakenTyp-weakenTyp-substTyp1-substTyp-weakenTyp t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (weakenTyp-substTyp2-substTyp1-substTyp-weakenTyp-inv t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (substTyp2-substTyp1-substTyp-weakenTyp t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (weakenTyp-substTyp2-substTyp1-substTyp-tProd t) Γ⇓ T⇓ = Term⇓ t Γ⇓ T⇓
    Term⇓ (weakenTyp2-weakenTyp1 t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (weakenTyp1-weakenTyp t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (weakenTyp1-weakenTyp-inv t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (weakenTyp1-weakenTyp1-weakenTyp t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (substTyp1-weakenTyp1 t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (weakenTyp1-substTyp-weakenTyp1-inv t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (weakenTyp1-substTyp-weakenTyp1 t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (weakenTyp-substTyp-substTyp-weakenTyp1 t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (weakenTyp-substTyp-substTyp-weakenTyp1-inv t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (substTyp-weakenTyp1-weakenTyp t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (substTyp3-substTyp2-substTyp1-substTyp-weakenTyp t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (weakenTyp-substTyp2-substTyp1-substTyp-weakenTyp1 t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (substTyp1-substTyp-tProd t) Γ⇓ T⇓ = Term⇓ t Γ⇓ T⇓
    Term⇓ (substTyp2-substTyp-substTyp-weakenTyp1-weakenTyp-weakenTyp t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (substTyp1-substTyp-weakenTyp2-weakenTyp t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (weakenTyp-weakenTyp1-weakenTyp t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ (beta-under-subst t) Γ⇓ = Term⇓ t Γ⇓
    Term⇓ ‘proj₁'’ Γ⇓ (x , p) = x
    Term⇓ ‘proj₂'’ (Γ⇓ , (x , p)) = p
    Term⇓ (‘existT’ x p) Γ⇓ = Term⇓ x Γ⇓ , Term⇓ p Γ⇓
    Term⇓ (f ‘‘’’ x) Γ⇓ = lift (lower (Term⇓ f Γ⇓) ‘’ lower (Term⇓ x Γ⇓))
    Term⇓ (f w‘‘’’ x) Γ⇓ = lift (lower (Term⇓ f Γ⇓) ‘’ lower (Term⇓ x Γ⇓))
    Term⇓ (f ‘‘→'’’ x) Γ⇓ = lift (lower (Term⇓ f Γ⇓) ‘→'’ lower (Term⇓ x Γ⇓))
    Term⇓ (f w‘‘→'’’ x) Γ⇓ = lift (lower (Term⇓ f Γ⇓) ‘→'’ lower (Term⇓ x Γ⇓))
    Term⇓ (w→ x) Γ⇓ A⇓ = Term⇓ x (Σ.proj₁ Γ⇓) A⇓
    Term⇓ w‘‘→'’’→‘‘→'’’ Γ⇓ T⇓ = T⇓
    Term⇓ ‘‘→'’’→w‘‘→'’’ Γ⇓ T⇓ = T⇓
    Term⇓ ‘tApp-nd’ Γ⇓ f⇓ x⇓ = lift (SW (lower f⇓ ‘’ₐ lower x⇓))
    Term⇓ ⌜←'⌝ Γ⇓ T⇓ = T⇓
    Term⇓ ⌜→'⌝ Γ⇓ T⇓ = T⇓
    Term⇓ (‘‘fcomp-nd’’ {A} {B} {C}) Γ⇓ g⇓ f⇓ = lift (_‘∘’_ {ε} (lower g⇓) (lower f⇓))
    Term⇓ (⌜‘’⌝ {B} {A} {b}) Γ⇓ = lift (‘λ∙’ {ε} (‘VAR₀’ {ε} {_‘’_ {ε} A b}))
    Term⇓ (⌜‘’⌝' {B} {A} {b}) Γ⇓ = lift (‘λ∙’ {ε} (‘VAR₀’ {ε} {_‘’_ {ε} A b}))
    Term⇓ (‘cast-refl’ {T}) Γ⇓ = lift (cast-proof {T})
    Term⇓ (‘cast-refl'’ {T}) Γ⇓ = lift (cast'-proof {T})
    Term⇓ (‘s→→’ {T} {B} {b} {c} {v}) Γ⇓ = lift (‘idfun’ {_‘’_ {ε} (lower (Term⇓ b tt (Term⇓ v Γ⇓))) (lower (Term⇓ c tt (Term⇓ v Γ⇓)))})
    Term⇓ (‘s←←’ {T} {B} {b} {c} {v}) Γ⇓ = lift (‘idfun’ {_‘’_ {ε} (lower (Term⇓ b tt (Term⇓ v Γ⇓))) (lower (Term⇓ c tt (Term⇓ v Γ⇓)))})

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob


text:
-- Andreas, 2016-06-20
-- Issue #191, reported 2009-12-02 by Nisse

data T (A : Set) : Set → Set1 where
  c₁ : {B : Set} → T A B
  c₂ :             T A A

foo : {A B C : Set} → T A (B → C) → T A B → Set₁
foo c₁ y = Set
foo x  y = {!y!}

-- WAS:
-- Perform the indicated case split. Agda will happily replace the
-- last clause with two separate clauses, one for each constructor
-- of T, but the resulting file is not type correct:

-- Bug.agda:8,1-10,13
-- Cannot split on the constructor c₂
-- when checking the definition of foo

-- In this case Agda should not modify the source file, it is
-- preferable to just give an error indicating that the split cannot
-- be performed.

-- NOW (Agda-2.5.2):
-- I'm not sure if there should be a case for the constructor c₂,
-- because I get stuck when trying to solve the following unification
-- problems (inferred index ≟ expected index):
--   A ≟ A → C
-- when checking that the expression ? has type Set₁

-- Current behavior (not splitting) is correct.

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- Equivalence relations
------------------------------------------------------------------------

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

open import Equality

module Equivalence-relation
  {e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where

open Derived-definitions-and-properties eq

open import Prelude

open import H-level eq
open import H-level.Closure eq

private
  variable
    a r r₁ r₂         : Level
    A A₁ A₂ B B₁ B₂ C : Type a
    R R₁ R₂           : A → B → Type r

------------------------------------------------------------------------
-- The definition

-- The definition of "equivalence relation".

record Is-equivalence-relation
         {A : Type a} (R : A → A → Type r) : Type (a ⊔ r) where
  field
    reflexive  : ∀ {x} → R x x
    symmetric  : ∀ {x y} → R x y → R y x
    transitive : ∀ {x y z} → R x y → R y z → R x z

------------------------------------------------------------------------
-- Some examples of equivalence relations/equivalence relation
-- transformers

-- A trivial binary relation.

Trivial : A → B → Type r
Trivial _ _ = ↑ _ ⊤

-- Homogeneous instances of Trivial are equivalence relations.

Trivial-is-equivalence-relation :
  Is-equivalence-relation (Trivial {A = A} {r = r})
Trivial-is-equivalence-relation = _

-- Trivial is propositional.

Trivial-is-propositional :
  {x y : A} → Is-proposition (Trivial {r = r} x y)
Trivial-is-propositional = ↑-closure 1 (mono₁ 0 ⊤-contractible)

-- The superscript P used in the names of the definitions in this
-- section stands for "pointwise".

-- Lifts binary relations from B to A → B.

infix 0 _→ᴾ_

_→ᴾ_ :
  (A : Type a) →
  (B → C → Type r) →
  ((A → B) → (A → C) → Type (a ⊔ r))
(_ →ᴾ R) f g = ∀ x → R (f x) (g x)

-- _→ᴾ_ preserves equivalence relations.

→ᴾ-preserves-Is-equivalence-relation :
  Is-equivalence-relation R →
  Is-equivalence-relation (A →ᴾ R)
→ᴾ-preserves-Is-equivalence-relation R-equiv = record
  { reflexive  = λ _ → reflexive
  ; symmetric  = λ f∼g x → symmetric (f∼g x)
  ; transitive = λ f∼g g∼h x → transitive (f∼g x) (g∼h x)
  }
  where
  open Is-equivalence-relation R-equiv

-- _→ᴾ_ preserves Is-proposition (assuming extensionality).

→ᴾ-preserves-Is-proposition :
  {A : Type a} (R : B → C → Type r) →
  Extensionality a r →
  (∀ {x y} → Is-proposition (R x y)) →
  ∀ {f g} → Is-proposition ((A →ᴾ R) f g)
→ᴾ-preserves-Is-proposition _ ext R-prop =
  Π-closure ext 1 λ _ →
  R-prop

-- Lifts binary relations from A and B to A ⊎ B.

infixr 1 _⊎ᴾ_

_⊎ᴾ_ :
  (A₁ → A₂ → Type r) →
  (B₁ → B₂ → Type r) →
  (A₁ ⊎ B₁ → A₂ ⊎ B₂ → Type r)
(P ⊎ᴾ Q) (inj₁ x) (inj₁ y) = P x y
(P ⊎ᴾ Q) (inj₂ x) (inj₂ y) = Q x y
(P ⊎ᴾ Q) _        _        = ⊥

-- _⊎ᴾ_ preserves Is-equivalence-relation.

⊎ᴾ-preserves-Is-equivalence-relation :
  Is-equivalence-relation R₁ →
  Is-equivalence-relation R₂ →
  Is-equivalence-relation (R₁ ⊎ᴾ R₂)
⊎ᴾ-preserves-Is-equivalence-relation R₁-equiv R₂-equiv = record
  { reflexive  = λ { {x = inj₁ _} → reflexive R₁-equiv
                   ; {x = inj₂ _} → reflexive R₂-equiv
                   }
  ; symmetric  = λ { {x = inj₁ _} {y = inj₁ _} → symmetric R₁-equiv
                   ; {x = inj₂ _} {y = inj₂ _} → symmetric R₂-equiv
                   ; {x = inj₁ _} {y = inj₂ _} ()
                   ; {x = inj₂ _} {y = inj₁ _} ()
                   }
  ; transitive = λ
     { {x = inj₁ _} {y = inj₁ _} {z = inj₁ _} → transitive R₁-equiv
     ; {x = inj₂ _} {y = inj₂ _} {z = inj₂ _} → transitive R₂-equiv

     ; {x = inj₁ _} {y = inj₂ _} ()
     ; {x = inj₂ _} {y = inj₁ _} ()
     ; {y = inj₁ _} {z = inj₂ _} _ ()
     ; {y = inj₂ _} {z = inj₁ _} _ ()
     }
  }
  where
  open Is-equivalence-relation

-- _⊎ᴾ_ preserves Is-proposition.

⊎ᴾ-preserves-Is-proposition :
  (∀ {x y} → Is-proposition (R₁ x y)) →
  (∀ {x y} → Is-proposition (R₂ x y)) →
  ∀ {x y} → Is-proposition ((R₁ ⊎ᴾ R₂) x y)
⊎ᴾ-preserves-Is-proposition = λ where
  R₁-prop R₂-prop {inj₁ _} {inj₁ _} → R₁-prop
  R₁-prop R₂-prop {inj₁ _} {inj₂ _} → ⊥-propositional
  R₁-prop R₂-prop {inj₂ _} {inj₁ _} → ⊥-propositional
  R₁-prop R₂-prop {inj₂ _} {inj₂ _} → R₂-prop

-- Lifts a binary relation from A to Maybe A.

Maybeᴾ :
  (A → B → Type r) →
  (Maybe A → Maybe B → Type r)
Maybeᴾ R = Trivial ⊎ᴾ R

-- Maybeᴾ preserves Is-equivalence-relation.

Maybeᴾ-preserves-Is-equivalence-relation :
  Is-equivalence-relation R →
  Is-equivalence-relation (Maybeᴾ R)
Maybeᴾ-preserves-Is-equivalence-relation =
  ⊎ᴾ-preserves-Is-equivalence-relation Trivial-is-equivalence-relation

-- Maybeᴾ preserves Is-proposition.

Maybeᴾ-preserves-Is-proposition :
  (∀ {x y} → Is-proposition (R x y)) →
  ∀ {x y} → Is-proposition (Maybeᴾ R x y)
Maybeᴾ-preserves-Is-proposition =
  ⊎ᴾ-preserves-Is-proposition λ {x} →
  Trivial-is-propositional {x = x}

-- Lifts binary relations from A and B to A × B.

infixr 2 _×ᴾ_

_×ᴾ_ :
  (A₁ → B₁ → Type r₁) →
  (A₂ → B₂ → Type r₂) →
  (A₁ × A₂ → B₁ × B₂ → Type (r₁ ⊔ r₂))
(P ×ᴾ Q) (x₁ , x₂) (y₁ , y₂) = P x₁ y₁ × Q x₂ y₂

-- _×ᴾ_ preserves Is-equivalence-relation.

×ᴾ-preserves-Is-equivalence-relation :
  Is-equivalence-relation R₁ →
  Is-equivalence-relation R₂ →
  Is-equivalence-relation (R₁ ×ᴾ R₂)
×ᴾ-preserves-Is-equivalence-relation R₁-equiv R₂-equiv = λ where
    .Is-equivalence-relation.reflexive →
      E₁.reflexive , E₂.reflexive
    .Is-equivalence-relation.symmetric →
      Σ-map E₁.symmetric E₂.symmetric
    .Is-equivalence-relation.transitive →
      Σ-zip E₁.transitive E₂.transitive
  where
  module E₁ = Is-equivalence-relation R₁-equiv
  module E₂ = Is-equivalence-relation R₂-equiv

-- _×ᴾ_ preserves Is-proposition.

×ᴾ-preserves-Is-proposition :
  (∀ {x y} → Is-proposition (R₁ x y)) →
  (∀ {x y} → Is-proposition (R₂ x y)) →
  ∀ {x y} → Is-proposition ((R₁ ×ᴾ R₂) x y)
×ᴾ-preserves-Is-proposition R₁-prop R₂-prop =
  ×-closure 1 R₁-prop R₂-prop

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Types4Crib where

open import Basics public

_<=_ : Nat -> Nat -> Set
ze <= y = One
su x <= ze = Zero
su x <= su y = x <= y

cmp : (x y : Nat) -> (x <= y) + (y <= x)
cmp ze y = inl <>
cmp (su x) ze = inr <>
cmp (su x) (su y) = cmp x y

data Bnd : Set where
  bot : Bnd
  # : Nat -> Bnd
  top : Bnd

_<B=_ : Bnd -> Bnd -> Set
bot <B= _ = One
# x <B= # y = x <= y
_ <B= top = One
_ <B= _ = Zero

data T23 (l u : Bnd) : Nat -> Set where
  leaf : (lu : l <B= u) -> T23 l u ze
  node2 : forall {h} x
    (tlx : T23 l (# x) h)(txu : T23 (# x) u h) ->
    T23 l u (su h)
  node3 : forall {h} x y
    (tlx : T23 l (# x) h)(txy : T23 (# x) (# y) h)(tyu : T23 (# y) u h) ->
    T23 l u (su h)

data Intv (l u : Bnd) : Set where
  intv : (x : Nat)(lx : l <B= # x)(xu : # x <B= u) -> Intv l u

TooBig : Bnd -> Bnd -> Nat -> Set
TooBig l u h = Sg Nat \ x -> T23 l (# x) h * T23 (# x) u h

insert : forall {h l u} -> Intv l u -> T23 l u h ->
          TooBig l u h + T23 l u h
insert (intv x lx xu) (leaf lu) = inl (x , (leaf lx , leaf xu))
insert (intv x lx xu) (node2 y tly tyu) with cmp x y
insert (intv x lx xu) (node2 y tly tyu) | inl xy with insert (intv x lx xy) tly
insert (intv x lx xu) (node2 y tly tyu) | inl xy | inl (z , tlz , tzu)
  = inr (node3 z y tlz tzu tyu)
insert (intv x lx xu) (node2 y tly tyu) | inl xy | inr tly'
  = inr (node2 y tly' tyu)
insert (intv x lx xu) (node2 y tly tyu) | inr yx with insert (intv x yx xu) tyu
insert (intv x lx xu) (node2 y tly tyu) | inr yx | inl (v , tyv , tvu) = inr (node3 y v tly tyv tvu)
insert (intv x lx xu) (node2 y tly tyu) | inr yx | inr tyv' = inr (node2 y tly tyv')
insert (intv x lx xu) (node3 y z tly tyz tzu) with cmp x y
insert (intv x lx xu) (node3 y z tly tyz tzu) | inl xy with insert (intv x lx xy) tly
insert (intv x lx xu) (node3 y z tly tyz tzu) | inl xy | inl (v , tlv , tvy) = inl (y , node2 v tlv tvy , node2 z tyz tzu)
insert (intv x lx xu) (node3 y z tly tyz tzu) | inl xy | inr tly' = inr (node3 y z tly' tyz tzu)
insert (intv x lx xu) (node3 y z tly tyz tzu) | inr yx with cmp x z
insert (intv x lx xu) (node3 y z tly tyz tzu) | inr yx | inl xz with insert (intv x yx xz) tyz
insert (intv x lx xu) (node3 y z tly tyz tzu) | inr yx | inl xz | inl (v , tyv , tvz)
  = inl (v , node2 y tly tyv , node2 z tvz tzu)
insert (intv x lx xu) (node3 y z tly tyz tzu) | inr yx | inl xz | inr tyz'
  = inr (node3 y z tly tyz' tzu)
insert (intv x lx xu) (node3 y z tly tyz tzu) | inr yx | inr zx with insert (intv x zx xu) tzu
insert (intv x lx xu) (node3 y z tly tyz tzu) | inr yx | inr zx | inl (v , tzv , tvu) = inl (z , node2 y tly tyz , node2 v tzv tvu)
insert (intv x lx xu) (node3 y z tly tyz tzu) | inr yx | inr zx | inr tzu' = inr (node3 y z tly tyz tzu')


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.AbGroup.Instances.Direct-Sum where

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.AbGroup

open import Cubical.Algebra.Direct-Sum.Base
open import Cubical.Algebra.Direct-Sum.Properties

open import Cubical.Algebra.Polynomials.Multivariate.Base

private variable
  ℓ ℓ' : Level

module _ (Idx : Type ℓ) (P : Idx → Type ℓ') (AGP : (r : Idx) → AbGroupStr (P r)) where

  open AbGroupStr

  ⊕-AbGr : AbGroup (ℓ-max ℓ ℓ')
  fst ⊕-AbGr = ⊕ Idx P AGP
  0g (snd ⊕-AbGr) = neutral
  _+_ (snd ⊕-AbGr) = _add_
  - snd ⊕-AbGr = inv Idx P AGP
  isAbGroup (snd ⊕-AbGr) = makeIsAbGroup trunc addAssoc addRid (rinv Idx P AGP) addComm

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
-- Testing the version option when used without type-check the file.
--
-- N.B. It is necessary to change the Issue1244b.out file when using
-- different versions of Agda.


text:
-- Andreas, 2019-04-30, issue #3731
-- Compiler backend: Do not look for a main function if not the main module.

open import Agda.Builtin.Nat

module Issue3731 where
module M where
  module main where

  record R : Set where
    field
      main : Nat

  data Main : Set where
    main : Main

module N where
  data main : Set where

module O where
  record main : Set where

module P where
  postulate
    main : Nat

module Q where
  abstract
    main : Nat
    main = 1

main : Nat
main = 0

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda


text:
module Function.Multi.Functions where

open import Data
import      Data.Option.Functions as Option
open import Data.Tuple renaming (curry to curry₁ ; uncurry to uncurry₁) using (_⨯_ ; _,_)
open import Data.Tuple.Raise
import      Data.Tuple.Raiseᵣ.Functions as Raise
open import Data.Tuple.RaiseTypeᵣ
open import Data.Tuple.RaiseTypeᵣ.Functions
open import Function.Multi
open import Functional using (_→ᶠ_ ; id ; _∘_ ; _∘ᵢₙₛₜ_ ; _⦗_⦘_) renaming (const to const₁ ; apply to apply₁ ; swap to swap₁ ; _$_ to _$₁_)
open import Logic
import      Lvl
import      Lvl.MultiFunctions as Lvl
open import Numeral.Finite
open import Numeral.Finite.Bound
open import Numeral.Natural
open import Syntax.Function
open import Syntax.Number
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓ₃ : Lvl.Level
private variable n n₁ n₂ : ℕ
private variable ℓ𝓈 ℓ𝓈₁ ℓ𝓈₂ : Lvl.Level ^ n
private variable A B C : Type{ℓ}
private variable As Bs Cs : Types{n}(ℓ𝓈)

-- TODO: Make all n, n₁, n₂ explicit. Find a way to do this while having generalized variables
-- TODO: Some of these functions can be generalised to arbitrary categories instead of using the function type (_→_). This makes it possible to skip the specialized variants for different parameter types (e.g. compose and composeᵢₙₛₜ)

-- A constant function of many variables.
-- Lifts a value to being a number of nested functions.
-- Examples:
--   const(x) _ _ _ ... = x
--   const(x)
--   = (const₁ ∘ const₁ ∘ const₁ ∘ ...)(x)
--   = (_ ↦ (_ ↦ (_ ↦ x)))
--   = (_ ↦ _ ↦ _ ↦ x)
const : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)}{ℓ}{B : Type{ℓ}} → B → (As ⇉ B)
const(0)       = id
const(1)       = const₁
const(𝐒(𝐒(n))) = const₁ ∘ const(𝐒(n))

-- A projection function of many variables.
-- Returns one of the specified arguments.
-- Examples:
--   proj(2)(0) x y = x
--   proj(2)(1) x y = y
--   proj(3)(0) x y z = x
--   proj(3)(1) x y z = y
--   proj(3)(2) x y z = z
--   proj(4)(0) x y z w = x
--   proj(4)(1) x y z w = y
--   proj(4)(2) x y z w = z
--   proj(4)(3) x y z w = w
proj : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)} → (i : 𝕟(n)) → (As ⇉ index i As)
proj(1)       𝟎      x = x
proj(𝐒(𝐒(n))) 𝟎      x = const(𝐒(n)) x
proj(𝐒(𝐒(n))) (𝐒(i)) _ = proj(𝐒(n)) i

-- Applies a function on the return value of a multivariate function.
-- Composes the first argument and the last function of the second argument.
-- Can also be seen as lifting the function type to the structure of (As ⇉_).
-- Examples:
--   f ∘ᵣ g = (((f ∘_) ∘_) ∘_) ..
--   ((((f ∘ᵣ g) x₁) x₂) x₃) .. = f((((g x₁) x₂) x₃) ..)
--   (f ∘ᵣ g) x₁ x₂ x₃ .. = f(g x₁ x₂ x₃ ..)
-- Note: This can be used to specify the `map` function of a functor (As ⇉_).
compose : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)}{ℓ₁}{B : Type{ℓ₁}}{ℓ₂}{C : Type{ℓ₂}} → (B → C) → (As ⇉ B) → (As ⇉ C)
compose(0)         = id
compose(1)         = _∘_
compose(𝐒(𝐒(n))) f = compose(𝐒(n)) f ∘_
_∘ᵣ_ : ∀{As : Types{n}(ℓ𝓈)}{B : Type{ℓ₁}}{C : Type{ℓ₂}} → (B → C) → (As ⇉ B) → (As ⇉ C)
_∘ᵣ_ {n = n} = compose(n)

composeᵢₙₛₜ : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)}{ℓ₁}{B : Type{ℓ₁}}{ℓ₂}{C : Type{ℓ₂}} → (B → C) → (As ⇉ᵢₙₛₜ B) → (As ⇉ᵢₙₛₜ C)
composeᵢₙₛₜ(0)           = id
composeᵢₙₛₜ(1)       f g = f(g)
composeᵢₙₛₜ(𝐒(𝐒(n))) f g = composeᵢₙₛₜ(𝐒(n)) f g

-- Puts the second function on every argument of the first function.
-- Example:
--   (f on g) x₁ x₂ x₃ .. = f (g x₁) (g x₂) (g x₃) ..
composeOnEvery : (n : ℕ) → ∀{ℓ₁}{A : Type{ℓ₁}}{ℓ₂}{B : Type{ℓ₂}}{ℓ₃}{C : Type{ℓ₃}} → (repeat n B ⇉ C) → (A → B) → (repeat n A ⇉ C)
composeOnEvery 0               = const₁
composeOnEvery 1               = _∘_
composeOnEvery (𝐒(𝐒(n))) f g x = composeOnEvery(𝐒(n)) (f(g(x))) g
_on_ : ∀{A : Type{ℓ₁}}{B : Type{ℓ₂}}{C : Type{ℓ₃}} → (repeat n B ⇉ C) → (A → B) → (repeat n A ⇉ C)
_on_ {n = n} = composeOnEvery(n)

applyTwice : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)}{ℓ}{B : Type{ℓ}} → (As ⇉ As ⇉ B) → (As ⇉ B)
applyTwice(0)            = id
applyTwice(1)       f(x) = f(x)(x)
applyTwice(𝐒(𝐒(n))) f(x) = applyTwice(𝐒(n)) ((_$₁ x) ∘ᵣ (f(x)))

swap : (n₁ n₂ : ℕ) → ∀{ℓ𝓈₁}{As : Types{n₁}(ℓ𝓈₁)}{ℓ𝓈₂}{Bs : Types{n₂}(ℓ𝓈₂)}{ℓ}{C : Type{ℓ}} → (As ⇉ Bs ⇉ C) → (Bs ⇉ As ⇉ C)
swap(n₁)(0)            = id
swap(n₁)(1)        f b = (_$₁ b) ∘ᵣ f
swap(n₁)(𝐒(𝐒(n₂))) f b = swap(n₁)(𝐒(n₂)) ((_$₁ b) ∘ᵣ f)

-- Lifts a function/operator pointwise.
-- A generalized variant of `(_∘ᵣ_)` that allows the left function to have multiple arguments.
-- Example:
--   (f ∘ₗ g₁ g₂ g₃ ...) x₁ x₂ x₃ ... = f (g₁ x₁ x₂ x₃ ...) (g₂ x₁ x₂ x₃ ...) (g₃ x₁ x₂ x₃ ...) ...
--   (f ∘ₗ g) x₁ x₂ x₃ ... = (f ∘ᵣ g) x₁ x₂ x₃ ...
--   pointwise(1)(2) (_+_) = (f ↦ g ↦ x ↦ f(x) + g(x))
pointwise : (n₁ n₂ : ℕ) → ∀{ℓ𝓈₁}{As : Types{n₁}(ℓ𝓈₁)}{ℓ𝓈₂}{Bs : Types{n₂}(ℓ𝓈₂)}{ℓ}{C : Type{ℓ}} → (Bs ⇉ C) → (map (As ⇉_) Bs) ⇉ (As ⇉ C)
pointwise(n₁)(0)            = const(n₁)
pointwise(n₁)(1)            = compose(n₁)
pointwise(n₁)(𝐒(𝐒(n₂))) {As = As}{Bs = B , Bs}{C = C} f g = p{n = 𝐒(n₂)} (pointwise(n₁)(𝐒(n₂))) (f ∘ᵣ g) where
  p : ∀{Ts : Types{n}(ℓ𝓈)} → ((Bs ⇉ C) → (Ts ⇉ As ⇉ C)) → ((As ⇉ Bs ⇉ C) → (Ts ⇉ As ⇉ C)) -- TODO: Is it possible to simplify this helper function?
  p{n = n}{Ts = Ts} f g = compose(n) (applyTwice(n₁)) (swap(n₁)(n) (compose(n₁) f g))
_∘ₗ : ∀{As : Types{n₁}(ℓ𝓈₁)}{Bs : Types{n₂}(ℓ𝓈₂)}{C : Type{ℓ}} → (Bs ⇉ C) → (map (As ⇉_) Bs) ⇉ (As ⇉ C)
_∘ₗ {n₁ = n₁}{n₂ = n₂} = pointwise(n₁)(n₂)

-- Converts a function using a tuple to represent its arguments to a curried function (nested function types).
-- Example:
--   curry((x,y,z,...) ↦ φ) = (x ↦ y ↦ z ↦ ... ↦ φ)
--   curry(0) = id                       : (A₁                  → B) → (A₁                → B)
--   curry(1) = curry₁                   : ((A₁ ⨯ A₂)           → B) → (A₁ → A₂           → B)
--   curry(2) = curry₁ ∘ curry₁          : ((A₁ ⨯ A₂ ⨯ A₃)      → B) → (A₁ → A₂ → A₃      → B)
--   curry(3) = curry₁ ∘ curry₁ ∘ curry₁ : ((A₁ ⨯ A₂ ⨯ A₃ ⨯ A₄) → B) → (A₁ → A₂ → A₃ → A₄ → B)
-- Note: If there is a nested uncurry and curry, one can often use (_∘ᵣ_) instead (I think?).
curry : (n : ℕ) → ∀{ℓ𝓈}{As : Types{𝐒(n)}(ℓ𝓈)}{ℓ}{B : Type{ℓ}} → (reduceᵣ(_⨯_) As → B) → (As ⇉ B)
curry(𝟎)        = id
curry(𝐒(n)) f x = curry(n) (f ∘ (x ,_))

-- Converts a curried function (nested function types) to a function using a tuple to represent its arguments.
-- Example:
--   uncurry(x ↦ y ↦ z ↦ ... ↦ φ) = ((x,y,z,...) ↦ φ)
uncurry : (n : ℕ) → ∀{ℓ𝓈}{As : Types{𝐒(n)}(ℓ𝓈)}{ℓ}{B : Type{ℓ}} → (As ⇉ B) → (reduceᵣ(_⨯_) As → B)
uncurry(𝟎)               = id
uncurry(𝐒(n)) f (x , xs) = uncurry(n) (f(x)) xs

-- Applies a tuple as arguments to a multivariate function.
-- Example:
--   apply(x,y,z,...) (x ↦ y ↦ z ↦ ... ↦ φ) = φ
applyTuple : (n : ℕ) → ∀{ℓ𝓈}{As : Types{𝐒(n)}(ℓ𝓈)}{ℓ}{B : Type{ℓ}} → (reduceᵣ(_⨯_) As) → (As ⇉ B) → B
applyTuple(n) = swap₁(uncurry(n))

-- Applies an argument to a specific position in the arguments of an argument list of a multivariate function.
-- Examples:
--   applyAt 0 (x ↦ y ↦ ... ↦ f(x,y)) a = (y ↦ ... ↦ f(a,y))
--   applyAt 1 (x ↦ y ↦ ... ↦ f(x,y)) b = (x ↦ ... ↦ f(x,b))
--   applyAt 0 (x ↦ y ↦ z ↦ ... ↦ f(x,y,z)) a = (y ↦ z ↦ ... ↦ f(a,y,z))
--   applyAt 1 (x ↦ y ↦ z ↦ ... ↦ f(x,y,z)) b = (x ↦ z ↦ ... ↦ f(x,b,z))
--   applyAt 2 (x ↦ y ↦ z ↦ ... ↦ f(x,y,z)) c = (x ↦ y ↦ ... ↦ f(x,y,c))
applyAt : (n : ℕ) → ∀{ℓ𝓈}{As : Types{𝐒(n)}(ℓ𝓈)}{ℓ}{B : Type{ℓ}} → (i : 𝕟(𝐒(n))) → (index i As) → (As ⇉ B) → (without i As ⇉ B)
applyAt(0)       𝟎      xi f    = f xi
applyAt(1)       𝟎      xi f x  = f xi x
applyAt(1)       (𝐒(𝟎)) xi f x  = f x xi
applyAt(𝐒(𝐒(n))) 𝟎      xi f xs = f xi xs
applyAt(𝐒(𝐒(n))) (𝐒(i)) xi f x  = applyAt(𝐒(n)) i xi (f(x))

-- Puts the second and each succeeding functions on the respective arguments of the first function.
-- Applies each argument `xₙ` on the inner function `gₙ`, and then apply the value of these as the arguments to an outer function `f`.
-- This is similiar to (_on_) but uses different functions for every argument and each argument is applied to its respective function instead.
-- Example:
--   (onMany(n) f g₁ g₂ g₃ ...) x₁ x₂ x₃ ... = f (g₁ x₁) (g₂ x₂) (g₃ x₃) ...
-- TODO: Try to get rid of the curry/uncurry by using (_∘ᵣ_)
onEach : (n : ℕ) → ∀{ℓ𝓈₁}{As : Types{n}(ℓ𝓈₁)}{ℓ𝓈₂}{Bs : Types{n}(ℓ𝓈₂)}{C : Type{ℓ}} → (Bs ⇉ C) → (As ⦗ map₂(_→ᶠ_) ⦘ Bs) ⇉ (As ⇉ C)
onEach(0)           = id
onEach(1)           = _∘_
onEach(𝐒(𝐒(n))) f g = curry(n) (gs ↦ x ↦ uncurry(n) (onEach(𝐒(n)) (f(g(x)))) gs)

-- Note: One of the parts of being an "applicative functor". The other being `const`
liftedApply : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)}{ℓ₁}{B : Type{ℓ₁}}{ℓ₂}{C : Type{ℓ₂}} → (As ⇉ (B → C)) → ((As ⇉ B) → (As ⇉ C))
liftedApply(0)             = id
liftedApply(1)       f g x = f x (g x)
liftedApply(𝐒(𝐒(n))) f g x = liftedApply(𝐒(n)) (f(x)) (g(x))

lifted-[,] : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)}{ℓ₁}{B : Type{ℓ₁}}{ℓ₂}{C : Type{ℓ₂}} → (As ⇉ B) → (As ⇉ C) → (As ⇉ (B ⨯ C))
lifted-[,](n) f g = liftedApply(n) ((swap₁ _,_) ∘ᵣ g) f

-- TODO: How to implement something like this
--(F(x) ▫ F(y)) ▫ F(x . y)
--_aryᵣFromBinaryOperator_ : (n : ℕ) → ∀{X : Type{ℓ₁}}{Y : Type{ℓ₂}} → (_▫_ : X → Y → X) →
-- _aryᵣFromBinaryOperator_ : (n : ℕ) → ∀{F}{_○_} → (_▫_ : ∀{x y} → F(x) → F(y) → F(x ○ y)) →
-- _aryᵣFromBinaryOperator_ : (n : ℕ) → ∀{F} → (_▫_ : ∀{x y z} → F(x)(y) → F(y)(z) → F(x)(z)) →
-- CategoricalOperator₊ : ℕ → {Obj : Type{ℓ₁}} → (Obj → Obj → Type{ℓ₂}) → Type
-- CategoricalOperator₊(0)       F = ∀{x₁ x₂} → F(x₁)(x₂) → F(x₁)(x₂)
-- CategoricalOperator₊(1)       F = ∀{x₁ x₂ x₃} → F(x₂)(x₃) → F(x₁)(x₂) → F(x₁)(x₃)
-- CategoricalOperator₊(𝐒(𝐒(n))) F = {!!}

-- Nested binary type relations that associate to the right.
-- Used to define n-ary binary relations that accepts any types.
-- Example:
--   binaryTypeRelator₊(4)(_▫_) A B C D = A ▫ (B ▫ (C ▫ D))
-- TODO: It is possible to generalize the levels
binaryTypeRelator₊ : (n : ℕ) → (∀{ℓ₁ ℓ₂} → Type{ℓ₁} → Type{ℓ₂} → Type{ℓ₁ Lvl.⊔ ℓ₂}) → (∀{ℓ} → Type{ℓ}) → ∀{ℓ𝓈} → TypesOfTypes{n}(ℓ𝓈) ⇉ Type{Lvl.⨆(ℓ𝓈)}
binaryTypeRelator₊(0)       (_▫_) id   = id
binaryTypeRelator₊(1)       (_▫_) _  A = A
binaryTypeRelator₊(𝐒(𝐒(n))) (_▫_) id A = compose(𝐒(n)) (A ▫_) (binaryTypeRelator₊(𝐒(n)) (_▫_) id)

-- Nested quantifiers over multiple values.
-- Used to define nested universal and existential quantifications.
-- Example:
--   quantifier₊(3) □(P) = □(x ↦ □(y ↦ □(z ↦ P(x)(y)(z))))
quantifier₊ : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)} → (∀{ℓ₁ ℓ₂}{T : Type{ℓ₁}} → (T → Stmt{ℓ₂}) → Stmt{ℓ₁ Lvl.⊔ ℓ₂}) → (As ⇉ Stmt{ℓ}) → Stmt{ℓ Lvl.⊔ (Lvl.⨆(ℓ𝓈))}
quantifier₊(0)       □(P) = P
quantifier₊(1)       □(P) = □(P)
quantifier₊(𝐒(𝐒(n))) □(P) = □(x ↦ quantifier₊(𝐒(n)) □(P(x)))

quantifier₊ᵢₘₚₗ : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)} → (∀{ℓ₁ ℓ₂}{T : Type{ℓ₁}} → (T → Stmt{ℓ₂}) → Stmt{ℓ₁ Lvl.⊔ ℓ₂}) → (As ⇉ᵢₘₚₗ Stmt{ℓ}) → Stmt{ℓ Lvl.⊔ (Lvl.⨆(ℓ𝓈))}
quantifier₊ᵢₘₚₗ(0)       □(P) = P
quantifier₊ᵢₘₚₗ(1)       □(P) = □(x ↦ P{x})
quantifier₊ᵢₘₚₗ(𝐒(𝐒(n))) □(P) = □(x ↦ quantifier₊ᵢₘₚₗ(𝐒(n)) □(P{x}))

quantifier₊ᵢₙₛₜ : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)} → (∀{ℓ₁ ℓ₂}{T : Type{ℓ₁}} → (T → Stmt{ℓ₂}) → Stmt{ℓ₁ Lvl.⊔ ℓ₂}) → (As ⇉ᵢₙₛₜ Stmt{ℓ}) → Stmt{ℓ Lvl.⊔ (Lvl.⨆(ℓ𝓈))}
quantifier₊ᵢₙₛₜ(0)       □(P) = P
quantifier₊ᵢₙₛₜ(1)       □(P) = □(x ↦ P ⦃ x ⦄)
quantifier₊ᵢₙₛₜ(𝐒(𝐒(n))) □(P) = □(x ↦ quantifier₊ᵢₙₛₜ(𝐒(n)) □(P ⦃ x ⦄))

quantify : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)} → (As ⇉ Stmt{ℓ}) → Stmt{ℓ Lvl.⊔ (Lvl.⨆(ℓ𝓈))}
quantify(n) P = quantifier₊(n) (Pred ↦ (∀(x) → Pred(x))) P

quantifyᵢₘₚₗ : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)} → (As ⇉ᵢₘₚₗ Stmt{ℓ}) → Stmt{ℓ Lvl.⊔ (Lvl.⨆(ℓ𝓈))}
quantifyᵢₘₚₗ(n) P = quantifier₊ᵢₘₚₗ(n) (Pred ↦ (∀{x} → Pred(x))) P

quantifyᵢₙₛₜ : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)} → (As ⇉ᵢₙₛₜ Stmt{ℓ}) → Stmt{ℓ Lvl.⊔ (Lvl.⨆(ℓ𝓈))}
quantifyᵢₙₛₜ(n) P = quantifier₊ᵢₙₛₜ(n) (Pred ↦ (∀ ⦃ x ⦄ → Pred(x))) P

quantifierSpecific : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)} → (∀{i} → (index i As → Stmt{ℓ}) → Stmt{ℓ}) → (As ⇉ Stmt{ℓ}) → Stmt{ℓ}
quantifierSpecific(0)       □(P) = P
quantifierSpecific(1)       □(P) = □{𝟎}(P)
quantifierSpecific(𝐒(𝐒(n))) □(P) = □{𝟎}(x ↦ quantifierSpecific(𝐒(n)) (\{i} → □{𝐒(i)})(P(x)))

{- TODO: MOre general levels
quantifierSpecific : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)} → (∀{i} → (index i As → Stmt{Raise.index i ℓ𝓈}) → Stmt{ℓ}) → (As ⇉ Stmt{Lvl.⨆(ℓ𝓈)}) → Stmt{(Raise.head₀ ℓ𝓈) Option.or ℓ}
quantifierSpecific(0)       □(P) = {!!}
quantifierSpecific(1)       □(P) = □{𝟎}(P)
quantifierSpecific(𝐒(𝐒(n))) □(P) = □{𝟎}(x ↦ {!quantifierSpecific(𝐒(n)) (\{i} → □{𝐒(i)})(P(x))!})
-}

expl-to-impl : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)}{ℓ}{B : Type{ℓ}} → (As ⇉ B) → (As ⇉ᵢₘₚₗ B)
expl-to-impl 0         f = f
expl-to-impl 1         f{x} = f(x)
expl-to-impl (𝐒(𝐒(n))) f{x} = expl-to-impl(𝐒(n)) (f(x))

expl-to-inst : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)}{ℓ}{B : Type{ℓ}} → (As ⇉ B) → (As ⇉ᵢₙₛₜ B)
expl-to-inst 0         f = f
expl-to-inst 1         f ⦃ x ⦄ = f(x)
expl-to-inst (𝐒(𝐒(n))) f ⦃ x ⦄ = expl-to-inst(𝐒(n)) (f(x))

impl-to-expl : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)}{ℓ}{B : Type{ℓ}} → (As ⇉ᵢₘₚₗ B) → (As ⇉ B)
impl-to-expl 0         f = f
impl-to-expl 1         f(x) = f{x}
impl-to-expl (𝐒(𝐒(n))) f(x) = impl-to-expl(𝐒(n)) (f{x})

inst-to-expl : (n : ℕ) → ∀{ℓ𝓈}{As : Types{n}(ℓ𝓈)}{ℓ}{B : Type{ℓ}} → (As ⇉ᵢₙₛₜ B) → (As ⇉ B)
inst-to-expl 0         f = f
inst-to-expl 1         f(x) = f ⦃ x ⦄
inst-to-expl (𝐒(𝐒(n))) f(x) = inst-to-expl(𝐒(n)) (f ⦃ x ⦄)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
open import Mockingbird.Forest using (Forest)

-- Gödel's Forest
module Mockingbird.Problems.Chapter17 {b ℓ} (forest : Forest {b} {ℓ}) where

open import Data.Empty using (⊥-elim)
open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃-syntax)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_$_; _⇔_; Equivalence; mk⇔)
open import Function.Equivalence.Reasoning renaming (begin_ to ⇔-begin_; _∎ to _⇔-∎)
open import Level using (_⊔_)
open import Relation.Binary using (_Respects_)
open import Relation.Nullary using (¬_)
open import Relation.Unary using (Pred; _∈_)

open Forest forest
open import Mockingbird.Problems.Chapter15 forest using (⇔-¬; ⇔-↯)

record HasMate {s} (Sings : Pred Bird s) : Set (s ⊔ b) where
  field
    _′ : Bird → Bird
    isMate : ∀ {x} y → Sings (x ′ ∙ y) ⇔ (¬ Sings (x ∙ y))

open HasMate ⦃ ... ⦄

record HasAssociate {s} (Sings : Pred Bird s) : Set (s ⊔ b) where
  field
    _* : Bird → Bird
    isAssociate : ∀ {x} y → Sings (x * ∙ y) ⇔ Sings (x ∙ (y ∙ y))

open HasAssociate ⦃ ... ⦄

weakLEM : ∀ {a} (A : Set a) → ¬ ¬ (A ⊎ ¬ A)
weakLEM A ¬[A⊎¬A] =
  let ¬A : ¬ A
      ¬A a = ¬[A⊎¬A] (inj₁ a)

      A⊎¬A : A ⊎ ¬ A
      A⊎¬A = inj₂ ¬A
  in ¬[A⊎¬A] A⊎¬A

module _ {n s} (IsNightingale : Pred Bird n) (Sings : Pred Bird s) (𝒩 : Bird)
         (respects : Sings Respects _≈_)
         (LEM : ∀ x → Sings x ⊎ (¬ Sings x))
         (C₁ : ∀ {x} → IsNightingale x → Sings x)
         ⦃ C₂ : HasMate Sings ⦄
         ⦃ C₃ : HasAssociate Sings ⦄
         (C₄ : ∀ x → Sings (𝒩 ∙ x) ⇔ IsNightingale x) where

  private
    doubleNegation : ∀ x → ¬ ¬ Sings x → Sings x
    doubleNegation x ¬¬x-sings with LEM x
    ... | inj₁ x-sings = x-sings
    ... | inj₂ ¬x-sings = ⊥-elim $ ¬¬x-sings ¬x-sings

    doubleNegation-⇔ : ∀ x → (¬ ¬ Sings x) ⇔ Sings x
    doubleNegation-⇔ x = mk⇔ (doubleNegation x) (λ x-sings ¬x-sings → ¬x-sings x-sings)

  problem₁ : ∃[ 𝒢 ] (Sings 𝒢 × ¬ IsNightingale 𝒢)
  problem₁ = (𝒢 , conclusion)
    where
      𝒩′ = 𝒩 ′
      𝒩′* = 𝒩′ *
      𝒢 = 𝒩′* ∙ 𝒩′*

      𝒢-sings⇔¬𝒩𝒢-sings : Sings 𝒢 ⇔ (¬ Sings (𝒩 ∙ 𝒢))
      𝒢-sings⇔¬𝒩𝒢-sings = ⇔-begin
        Sings 𝒢                   ⇔⟨⟩
        Sings (𝒩′* ∙ 𝒩′*)         ⇔⟨ isAssociate 𝒩′* ⟩
        Sings (𝒩′ ∙ (𝒩′* ∙ 𝒩′*))  ⇔⟨⟩
        Sings (𝒩′ ∙ 𝒢)            ⇔⟨ isMate 𝒢 ⟩
        (¬ Sings (𝒩 ∙ 𝒢))         ⇔-∎

      ¬𝒢-sings⇔𝒢-isNightingale : (¬ Sings 𝒢) ⇔ IsNightingale 𝒢
      ¬𝒢-sings⇔𝒢-isNightingale = ⇔-begin
        ¬ Sings 𝒢          ⇔⟨ ⇔-¬ 𝒢-sings⇔¬𝒩𝒢-sings ⟩
        ¬ ¬ Sings (𝒩 ∙ 𝒢)  ⇔⟨ doubleNegation-⇔ $ 𝒩 ∙ 𝒢 ⟩
        Sings (𝒩 ∙ 𝒢)      ⇔⟨ C₄ 𝒢 ⟩
        IsNightingale 𝒢    ⇔-∎

      𝒢-sings⇔¬𝒢-isNightingale : Sings 𝒢 ⇔ (¬ IsNightingale 𝒢)
      𝒢-sings⇔¬𝒢-isNightingale = ⇔-begin
        Sings 𝒢              ⇔˘⟨ doubleNegation-⇔ 𝒢 ⟩
        ¬ ¬ Sings 𝒢          ⇔⟨ ⇔-¬ ¬𝒢-sings⇔𝒢-isNightingale ⟩
        (¬ IsNightingale 𝒢)  ⇔-∎

      conclusion : Sings 𝒢 × ¬ IsNightingale 𝒢
      conclusion with LEM 𝒢
      ... | inj₁ 𝒢-sings = (𝒢-sings , Equivalence.f 𝒢-sings⇔¬𝒢-isNightingale 𝒢-sings)
      ... | inj₂ ¬𝒢-sings = ⊥-elim $ ¬𝒢-sings $ C₁ $ Equivalence.f ¬𝒢-sings⇔𝒢-isNightingale ¬𝒢-sings

  problem₂ : ∃[ 𝒢 ] (Sings 𝒢 × ¬ IsNightingale 𝒢)
  problem₂ = (𝒢 , conclusion)
    where
      𝒩* = 𝒩 *
      𝒩*′ = 𝒩* ′
      𝒢 = 𝒩*′ ∙ 𝒩*′

      -- Note: this proof (and the definition of 𝒢) is the only difference to
      -- the proof of problem 1.
      𝒢-sings⇔¬𝒩𝒢-sings : Sings 𝒢 ⇔ (¬ Sings (𝒩 ∙ 𝒢))
      𝒢-sings⇔¬𝒩𝒢-sings = ⇔-begin
        Sings 𝒢 ⇔⟨⟩
        Sings (𝒩*′ ∙ 𝒩*′)          ⇔⟨ isMate 𝒩*′ ⟩
        ¬ Sings (𝒩* ∙ 𝒩*′)         ⇔⟨ ⇔-¬ $ isAssociate 𝒩*′ ⟩
        ¬ Sings (𝒩 ∙ (𝒩*′ ∙ 𝒩*′))  ⇔⟨⟩
        (¬ Sings (𝒩 ∙ 𝒢))          ⇔-∎

      ¬𝒢-sings⇔𝒢-isNightingale : (¬ Sings 𝒢) ⇔ IsNightingale 𝒢
      ¬𝒢-sings⇔𝒢-isNightingale = ⇔-begin
        ¬ Sings 𝒢          ⇔⟨ ⇔-¬ 𝒢-sings⇔¬𝒩𝒢-sings ⟩
        ¬ ¬ Sings (𝒩 ∙ 𝒢)  ⇔⟨ doubleNegation-⇔ $ 𝒩 ∙ 𝒢 ⟩
        Sings (𝒩 ∙ 𝒢)      ⇔⟨ C₄ 𝒢 ⟩
        IsNightingale 𝒢    ⇔-∎

      𝒢-sings⇔¬𝒢-isNightingale : Sings 𝒢 ⇔ (¬ IsNightingale 𝒢)
      𝒢-sings⇔¬𝒢-isNightingale = ⇔-begin
        Sings 𝒢              ⇔˘⟨ doubleNegation-⇔ 𝒢 ⟩
        ¬ ¬ Sings 𝒢          ⇔⟨ ⇔-¬ ¬𝒢-sings⇔𝒢-isNightingale ⟩
        (¬ IsNightingale 𝒢)  ⇔-∎

      conclusion : Sings 𝒢 × ¬ IsNightingale 𝒢
      conclusion with LEM 𝒢
      ... | inj₁ 𝒢-sings = (𝒢-sings , Equivalence.f 𝒢-sings⇔¬𝒢-isNightingale 𝒢-sings)
      ... | inj₂ ¬𝒢-sings = ⊥-elim $ ¬𝒢-sings $ C₁ $ Equivalence.f ¬𝒢-sings⇔𝒢-isNightingale ¬𝒢-sings

  _Represents_ : ∀ {r} → (A : Bird) → (𝒮 : Pred Bird r) → Set (b ⊔ s ⊔ r)
  A Represents 𝒮 = ∀ x → Sings (A ∙ x) ⇔ x ∈ 𝒮

  IsSociety : ∀ {r} → (𝒮 : Pred Bird r) → Set (b ⊔ s ⊔ r)
  IsSociety 𝒮 = ∃[ A ] A Represents 𝒮

  _ : IsSociety IsNightingale
  _ = (𝒩 , C₄)

  problem₃ : ¬ IsSociety Sings
  problem₃ 𝒮@(A , A-represents) =
    let A′ = A ′
        A′* = A′ *

        𝒮ᶜ : IsSociety λ x → ¬ Sings x
        𝒮ᶜ =
          ( A′
          , λ x → ⇔-begin
              Sings (A′ ∙ x)   ⇔⟨ isMate x ⟩
              ¬ Sings (A ∙ x)  ⇔⟨ ⇔-¬ $ A-represents x ⟩
              (¬ Sings x)      ⇔-∎
          )

        A′*A′*-sings⇔¬A′*A′*-sings : Sings (A′* ∙ A′*) ⇔ (¬ Sings (A′* ∙ A′*))
        A′*A′*-sings⇔¬A′*A′*-sings = ⇔-begin
          Sings (A′* ∙ A′*)         ⇔⟨ isAssociate A′* ⟩
          Sings (A′ ∙ (A′* ∙ A′*))  ⇔⟨ proj₂ 𝒮ᶜ (A′* ∙ A′*) ⟩
          (¬ Sings (A′* ∙ A′*))     ⇔-∎

    in ⇔-↯ A′*A′*-sings⇔¬A′*A′*-sings

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
------------------------------------------------------------------------
-- A definitional interpreter
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

module Lambda.Delay-monad.Interpreter where

open import Equality.Propositional
open import Prelude
open import Prelude.Size

open import Maybe equality-with-J
open import Monad equality-with-J
open import Vec.Function equality-with-J

open import Delay-monad
open import Delay-monad.Bisimilarity
open import Delay-monad.Monad

open import Lambda.Syntax hiding ([_])

open Closure Tm

------------------------------------------------------------------------
-- An interpreter monad

-- The interpreter monad.

M : ∀ {ℓ} → Size → Type ℓ → Type ℓ
M i = MaybeT (λ A → Delay A i)

-- A variant of the interpreter monad.

M′ : ∀ {ℓ} → Size → Type ℓ → Type ℓ
M′ i = MaybeT (λ A → Delay′ A i)

-- A lifted variant of later.

laterM : ∀ {i a} {A : Type a} → M′ i A → M i A
run (laterM x) = later (run x)

-- A lifted variant of weak bisimilarity.

infix 4 _≈M_

_≈M_ : ∀ {a} {A : Type a} → M ∞ A → M ∞ A → Type a
x ≈M y = run x ≈ run y

------------------------------------------------------------------------
-- The interpreter

infix 10 _∙_

mutual

  ⟦_⟧ : ∀ {i n} → Tm n → Env n → M i Value
  ⟦ con i ⟧   ρ = return (con i)
  ⟦ var x ⟧   ρ = return (ρ x)
  ⟦ ƛ t ⟧     ρ = return (ƛ t ρ)
  ⟦ t₁ · t₂ ⟧ ρ = ⟦ t₁ ⟧ ρ >>= λ v₁ →
                  ⟦ t₂ ⟧ ρ >>= λ v₂ →
                  v₁ ∙ v₂

  _∙_ : ∀ {i} → Value → Value → M i Value
  con i  ∙ v₂ = fail
  ƛ t₁ ρ ∙ v₂ = laterM (⟦ t₁ ⟧′ (cons v₂ ρ))

  ⟦_⟧′ : ∀ {i n} → Tm n → Env n → M′ i Value
  force (run (⟦ t ⟧′ ρ)) = run (⟦ t ⟧ ρ)

------------------------------------------------------------------------
-- An example

-- The semantics of Ω is the non-terminating computation never.

Ω-loops : ∀ {i} → [ i ] run (⟦ Ω ⟧ nil) ∼ never
Ω-loops = later λ { .force → Ω-loops }

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad