text:
module API where

open import Algebra
open import Prelude

empty : ∀ {A} -> Graph A
empty = ε

vertex : ∀ {A} -> A -> Graph A
vertex = v

overlay : ∀ {A} -> Graph A -> Graph A -> Graph A
overlay = _+_

connect : ∀ {A} -> Graph A -> Graph A -> Graph A
connect = _*_

edge : ∀ {A} -> A -> A -> Graph A
edge x y = connect (vertex x) (vertex y)

overlays : ∀ {A} -> List (Graph A) -> Graph A
overlays = foldr overlay empty

connects : ∀ {A} -> List (Graph A) -> Graph A
connects = foldr connect empty

vertices : ∀ {A} -> List A -> Graph A
vertices = overlays ∘ map vertex

edges : ∀ {A} -> List (A × A) -> Graph A
edges = overlays ∘ map (uncurry edge)

graph : ∀ {A} -> List A -> List (A × A) -> Graph A
graph vs es = overlay (vertices vs) (edges es)

foldg : ∀ {A} {B : Set} -> B -> (A -> B) -> (B -> B -> B) -> (B -> B -> B) -> Graph A -> B
foldg {A} {B} e w o c = go
  where
    go : Graph A -> B
    go ε       = e
    go (v x)   = w x
    go (x + y) = o (go x) (go y)
    go (x * y) = c (go x) (go y)

path : ∀ {A} -> List A -> Graph A
path []        = empty
path (x :: []) = vertex x
path (x :: xs) = edges (zip (x :: xs) xs)

circuit : ∀ {A} -> List A -> Graph A
circuit []        = empty
circuit (x :: xs) = path ([ x ] ++ xs ++ [ x ])

clique : ∀ {A} -> List A -> Graph A
clique = connects ∘ map vertex

biclique : ∀ {A} -> List A -> List A -> Graph A
biclique xs ys = connect (vertices xs) (vertices ys)

star : ∀ {A} -> A -> List A -> Graph A
star x ys = connect (vertex x) (vertices ys)

max_stars_repo_name: asr/alga

max_issues_repo_name: asr/alga

max_forks_repo_name: asr/alga


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

open import level
open import equality.core
open import sets.list.core

module _ {i}{A : Set i} where
  data all {j}(P : A → Set j) : List A → Set (i ⊔ j) where
    mk-all : ∀ {x xs} → P x → all P xs → all P (x ∷ xs)

  data any {j}(P : A → Set j) : List A → Set (i ⊔ j) where
    hd-any : ∀ {x xs} → P x → any P (x ∷ xs)
    tl-any : ∀ {x xs} → any P xs → any P (x ∷ xs)

  elem : A → List A → Set i
  elem x = any (λ x' → x ≡ x')

ext: agda

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
import SOAS.Syntax.Signature as Sig
open import SOAS.Families.Core

-- Term syntax for a signature
module SOAS.Syntax.Term
  {T : Set}(open Sig T)
  {O : Set}(S : Signature O) where

open import SOAS.Syntax.Arguments {T}
open import SOAS.Metatheory.Syntax {T}

open import SOAS.Common
open import SOAS.Context {T}
open import SOAS.Variable
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive

open import SOAS.Abstract.Hom

open import Categories.Object.Initial

open import Data.List.Base using (List ; [] ; [_] ; _∷_)
open import Data.Unit

open Signature S

private
  variable
    α β τ : T
    Γ Δ Π : Ctx

module _ (𝔛 : Familyₛ) where
  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  -- Grammar of terms for a (⅀,𝔛)-meta-algebra
  data 𝕋 : Familyₛ where
    con  : ⅀ 𝕋 τ Γ → 𝕋 τ Γ
    var  : ℐ τ Γ → 𝕋 τ Γ
    mvar : 𝔛 τ Π → Sub 𝕋 Π Γ → 𝕋 τ Γ

  Tmᵃ : MetaAlg 𝕋
  Tmᵃ = record { 𝑎𝑙𝑔 = con ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 ε → mvar 𝔪 (tabulate ε) }

  -- 𝕋 is the initial meta-algebra
  𝕋:Init : Initial 𝕄etaAlgebras
  𝕋:Init = record
    { ⊥ = 𝕋 ⋉ Tmᵃ
    ; ⊥-is-initial = record
      { ! = λ{ {𝒜 ⋉ 𝒜ᵃ} → (𝕤𝕖𝕞 𝒜ᵃ) ⋉ 𝕤𝕖𝕞ᵃ⇒ 𝒜ᵃ }
      ; !-unique = λ { {𝒜 ⋉ 𝒜ᵃ}(g ⋉ gᵃ⇒) {x = t} →  𝕤𝕖𝕞! 𝒜ᵃ gᵃ⇒ t } } }
    where
    module _ {𝒜 : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜) where
      open MetaAlg 𝒜ᵃ
      𝕤𝕖𝕞 : 𝕋 ⇾̣ 𝒜
      𝔸 : (as : List (Ctx × T)) → Arg as 𝕋 Γ → Arg as 𝒜 Γ
      𝔸 [] tt = tt
      𝔸 (_ ∷ []) t = 𝕤𝕖𝕞 t
      𝔸 (_ ∷ a ∷ as) (t , ts) = (𝕤𝕖𝕞 t , 𝔸 (a ∷ as) ts)
      𝕊 : Sub 𝕋 Π Γ → Π ~[ 𝒜 ]↝ Γ
      𝕊 (t ◂ σ) new = 𝕤𝕖𝕞 t
      𝕊 (t ◂ σ) (old v) = 𝕊 σ v
      𝕤𝕖𝕞 (con (o ⋮ a)) = 𝑎𝑙𝑔 (o ⋮ 𝔸 (Arity o) a)
      𝕤𝕖𝕞 (var v) = 𝑣𝑎𝑟 v
      𝕤𝕖𝕞 (mvar 𝔪 ε) = 𝑚𝑣𝑎𝑟 𝔪 (𝕊 ε)

      𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ Tmᵃ 𝒜ᵃ 𝕤𝕖𝕞
      𝕤𝕖𝕞ᵃ⇒ = record
        { ⟨𝑎𝑙𝑔⟩ = λ{ {t = (o ⋮ a)} → cong (λ - → 𝑎𝑙𝑔 (o ⋮ -)) (𝔸-Arg₁ (Arity o) a) }
        ; ⟨𝑣𝑎𝑟⟩ = refl
        ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{ε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab ε)) }
        }
        where
        𝔸-Arg₁ : (as : List (Ctx × T))(a : Arg as 𝕋 Γ)
            → 𝔸 as a ≡ Arg₁ as 𝕤𝕖𝕞 a
        𝔸-Arg₁ [] tt = refl
        𝔸-Arg₁ (_ ∷ []) t = refl
        𝔸-Arg₁ (_ ∷ a ∷ as) (t , ap) = cong (_ ,_) (𝔸-Arg₁ (a ∷ as) ap)

        𝕊-tab : (ε : Π ~[ 𝕋 ]↝ Γ)(v : ℐ α Π)
              → 𝕊 (tabulate ε) v ≡ 𝕤𝕖𝕞 (ε v)
        𝕊-tab ε new = refl
        𝕊-tab ε (old v) = 𝕊-tab (ε ∘ old) v

      module _ {g : 𝕋 ⇾̣ 𝒜}(gᵃ⇒ : MetaAlg⇒ Tmᵃ 𝒜ᵃ g) where
        open MetaAlg⇒ gᵃ⇒

        𝕤𝕖𝕞! : (t : 𝕋 α Γ) → 𝕤𝕖𝕞 t ≡ g t
        𝕊-ix : (ε : Sub 𝕋 Π Γ)(v : ℐ α Π) → 𝕊 ε v ≡ g (index ε v)
        𝕊-ix (x ◂ ε) new = 𝕤𝕖𝕞! x
        𝕊-ix (x ◂ ε) (old v) = 𝕊-ix ε v
        𝔸-Arg₁ : (as : List (Ctx × T))(ar : Arg as 𝕋 Γ)
              → 𝔸 as ar ≡ Arg₁ as g ar
        𝔸-Arg₁ [] tt = refl
        𝔸-Arg₁ (_ ∷ []) t = 𝕤𝕖𝕞! t
        𝔸-Arg₁ (_ ∷ a ∷ as) (t , ap) = cong₂ _,_ (𝕤𝕖𝕞! t) (𝔸-Arg₁ (a ∷ as) ap)

        𝕤𝕖𝕞! (con (o ⋮ a)) rewrite 𝔸-Arg₁ (Arity o) a = sym ⟨𝑎𝑙𝑔⟩
        𝕤𝕖𝕞! (var v) = sym ⟨𝑣𝑎𝑟⟩
        𝕤𝕖𝕞! (mvar 𝔪 ε) rewrite cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-ix ε)) =
          trans (sym ⟨𝑚𝑣𝑎𝑟⟩) (cong (g ∘ mvar 𝔪) (tab∘ix≈id ε))

-- Syntax instance for a term grammar
𝕋:Syn : Syntax
𝕋:Syn = record
  { ⅀F = ⅀F
  ; ⅀:CS = ⅀:CompatStr
  ; 𝕋:Init = 𝕋:Init
  ; mvarᵢ = mvar }

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module SingleSorted.Example where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Data.Product using (_×_; proj₁; proj₂; <_,_>; ∃; ∃-syntax; _,_)
import Function using (_∘_)
open import SingleSorted.AlgebraicTheory
open import Categories.Category.Instance.Sets
open import Categories.Category.Cartesian
open import Agda.Primitive
open import Categories.Category

module Sets₀ where
  𝒮 : Category (lsuc lzero) lzero lzero
  𝒮 = Sets lzero

open Sets₀
open Category 𝒮

-- Function extensionality
postulate
  funext : ∀ {X : Set} {Y : X → Set} {f g : ∀ (x : X) → (Y x)} → (∀ (x : X) → ((f x) ≡ (g x))) → (f ≡ g)

record singleton : Set where
  constructor ⋆

η-singleton : ∀ (x : singleton) → ⋆ ≡ x
η-singleton ⋆ = refl

prod-elem-structure : ∀ {A B : Set} {x : A × B} → ∃[ a ] ∃[ b ] (a , b) ≡ x
prod-elem-structure {A} {B} {x} = proj₁ x Data.Product., (proj₂ x) , refl

first-factor :  ∀ {X A B : Obj} {f : X ⇒ A} {g : X ⇒ B} → proj₁ ∘ < f , g > ≡ f
first-factor {X} {A} {B} {f} {g} = funext λ x → refl

second-factor : ∀ {X A B : Obj} {f : X ⇒ A} {g : X ⇒ B} → proj₂ ∘ < f , g > ≡ g
second-factor {X} {A} {B} {f} {g} = funext λ{ x → refl}

unique-map-into-product : ∀ {X A B : Set} {h : X → A × B} {f : X → A} {g : X → B}  {x : X}
  → (proj₁ ∘ h) x ≡ f x
  → (proj₂ ∘ h) x ≡ g x
  --------------------
  → < f , g > x ≡ h x
unique-map-into-product {X} {A} {B} {h} {f} {g} {x} eq1 eq2
  rewrite first-factor {X} {A} {B} {f} {g} | second-factor {X} {A} {B} {f} {g}
  = {!!}

cartesian-Sets : Cartesian 𝒮
cartesian-Sets =
  record
    { terminal = record
                 { ⊤ = singleton
                 ; ⊤-is-terminal = record
                                   { ! = λ{ x → ⋆}
                                   ; !-unique = λ{ f {x} → η-singleton (f x)}
                                   }
                 }
    ; products = record
                 { product = λ {A} {B} →
                           record
                           { A×B = A × B
                           ; π₁ = proj₁
                           ; π₂ = proj₂
                           ; ⟨_,_⟩ = <_,_>
                           ; project₁ = λ{ → refl}
                           ; project₂ = λ{ → refl}
                           ; unique = λ{ {X} {h} {f} {g} eq1 eq2 {x} → {!!}}
                           }

                 }
    }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The Maybe type
------------------------------------------------------------------------

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

module Data.Maybe where

open import Data.Empty using (⊥)
open import Data.Unit using (⊤)
open import Data.Bool.Base using (T)
open import Data.Maybe.Relation.Unary.All
open import Data.Maybe.Relation.Unary.Any
open import Level using (Level)

private
  variable
    a : Level
    A : Set a

------------------------------------------------------------------------
-- The base type and some operations

open import Data.Maybe.Base public

------------------------------------------------------------------------
-- Using Any and All to define Is-just and Is-nothing

Is-just : Maybe A → Set _
Is-just = Any (λ _ → ⊤)

Is-nothing : Maybe A → Set _
Is-nothing = All (λ _ → ⊥)

to-witness : ∀ {m : Maybe A} → Is-just m → A
to-witness (just {x = p} _) = p

to-witness-T : ∀ (m : Maybe A) → T (is-just m) → A
to-witness-T (just p) _  = p


text:
data Nat : Set where
  zero : Nat

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

subst : ∀ {A : Set} (P : A → Set) {x y} → x ≡ y → P x → P y
subst P refl px = px

postulate
  Eq : Set → Set
  mkEq : {A : Set} (x y : A) → x ≡ y
  _==_ : {A : Set} {{_ : Eq A}} (x y : A) → x ≡ y

  A : Set
  B : A → Set
  C : ∀ x → B x → Set

case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

id : ∀ {a} (A : Set a) → A → A
id A x = x

eqTriple : {{_ : ∀ {x} {y : B x} → Eq (C x y)}}
           (a : A) (b : B a) (c : C a b)
           (a₁ : A) (b₁ : B a₁) (c : C a₁ b₁) → Nat
eqTriple a b c a₁ b₁ c₁ =
  subst (λ a₂ → ∀ (b₂ : B a₂) (c₂ : _) → Nat) (mkEq a a₁)
        (λ b₂ c₂ → subst (λ b₃ → ∀ c₃ → Nat) (mkEq b b₂)
                           (λ c₃ → case c == c₃ of λ eq → zero) c₂)
        b₁ c₁

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The actual maximum stack size of the compiled program matches the
-- maximum stack size of the instrumented source-level semantics
------------------------------------------------------------------------

open import Prelude

import Lambda.Syntax

module Lambda.Compiler-correctness.Sizes-match
  {Name : Type}
  (open Lambda.Syntax Name)
  (def : Name → Tm 1)
  where

open import Equality.Propositional as E using (refl)
open import Logical-equivalence using (_⇔_)
open import Tactic.By.Propositional using (by)
open import Prelude.Size

open import Colist E.equality-with-J hiding (_++_; length)
import Conat E.equality-with-J as Conat
open import Function-universe E.equality-with-J hiding (id; _∘_)
open import List E.equality-with-J using (_++_; length)
open import Monad E.equality-with-J
open import Nat E.equality-with-J
open import Vec.Data E.equality-with-J

open import Upper-bounds

open import Lambda.Compiler def
open import Lambda.Interpreter.Stack-sizes def as I
open import Lambda.Delay-crash-trace as DCT
  using (Delay-crash-trace)
open import Lambda.Virtual-machine.Instructions Name
open import Lambda.Virtual-machine comp-name as VM

private
  module C = Closure Code
  module T = Closure Tm

open Delay-crash-trace using (tell)

------------------------------------------------------------------------
-- A lemma

-- A rearrangement lemma for ⟦_⟧⁺.

⟦⟧-· :
  ∀ {A n} (t₁ t₂ : Tm n)
    {ρ} tc {k : T.Value → Delay-crash-trace (ℕ → ℕ) A ∞} →
  DCT.[ ∞ ] ⟦ t₁ · t₂ ⟧ ρ tc >>= k ∼
            do v₁ ← ⟦ t₁ ⟧ ρ false
               v₂ ← ⟦ t₂ ⟧ ρ false
               [ pred , pred ] v₁ ∙ v₂ >>= k
⟦⟧-· t₁ t₂ {ρ} tc {k} =
  ⟦ t₁ · t₂ ⟧ ρ tc >>= k                   DCT.∼⟨⟩

  (do v₁ ← ⟦ t₁ ⟧ ρ false
      v₂ ← ⟦ t₂ ⟧ ρ false
      [ pred , pred ] v₁ ∙ v₂) >>= k       DCT.∼⟨ DCT.symmetric (DCT.associativity (⟦ t₁ ⟧ _ _) _ _) ⟩

  (do v₁ ← ⟦ t₁ ⟧ ρ false
      (do v₂ ← ⟦ t₂ ⟧ ρ false
          [ pred , pred ] v₁ ∙ v₂) >>= k)  DCT.∼⟨ ((⟦ t₁ ⟧ _ _ DCT.∎) DCT.>>=-cong λ _ → DCT.symmetric (DCT.associativity (⟦ t₂ ⟧ _ _) _ _)) ⟩

  (do v₁ ← ⟦ t₁ ⟧ ρ false
      v₂ ← ⟦ t₂ ⟧ ρ false
      [ pred , pred ] v₁ ∙ v₂ >>= k)       DCT.∎

------------------------------------------------------------------------
-- Well-formed continuations and stacks

-- A continuation is OK with respect to a certain state if the
-- following property is satisfied.

Cont-OK :
  Size → State → (T.Value → Delay-crash-trace (ℕ → ℕ) C.Value ∞) → Type
Cont-OK i ⟨ c , s , ρ ⟩ k =
  ∀ v → [ i ] VM.stack-sizes ⟨ c , val (comp-val v) ∷ s , ρ ⟩ ≂
              numbers (k v) (1 + length s)

-- A workaround for what might be an Agda bug.

castC :
  ∀ {i} {j : Size< i} {s k} →
  Cont-OK i s k → Cont-OK j s k
castC {s = ⟨ _ , _ , _ ⟩} c-ok = cast-≂ ∘ c-ok

-- If the In-tail-context parameter indicates that we are in a tail
-- context, then the stack must have a certain shape, and it must be
-- related to the continuation in a certain way.

data Stack-OK (i : Size)
              (k : T.Value → Delay-crash-trace (ℕ → ℕ) C.Value ∞) :
              In-tail-context → Stack → Type where
  unrestricted : ∀ {s} → Stack-OK i k false s
  restricted   :
    ∀ {s n} {c : Code n} {ρ : C.Env n} →
    (∀ v → [ i ] 2 + length s ∷′
                 VM.stack-sizes ⟨ c , val (comp-val v) ∷ s , ρ ⟩ ≂
                 numbers (k v) (2 + length s)) →
    Stack-OK i k true (ret c ρ ∷ s)

-- Stacks that are OK in a tail context are OK in any context.

any-OK :
  ∀ {tc i k s} →
  Stack-OK i k true s →
  Stack-OK i k tc   s
any-OK {false} = const unrestricted
any-OK {true}  = id

------------------------------------------------------------------------
-- The stack sizes match

mutual

  -- Some lemmas making up the main part of the correctness result.

  ⟦⟧-correct :
    ∀ {i n} (t : Tm n) (ρ : T.Env n) {tc c s}
      {k : T.Value → Delay-crash-trace (ℕ → ℕ) C.Value ∞} →
    Stack-OK i k tc s →
    Cont-OK i ⟨ c , s , comp-env ρ ⟩ k →
    [ i ] VM.stack-sizes ⟨ comp tc t c , s , comp-env ρ ⟩ ≂
          numbers (⟦ t ⟧ ρ tc >>= k) (length s)

  ⟦⟧-correct (var x) ρ {tc} {c} {s} {k} _ c-ok =
    VM.stack-sizes ⟨ var x ∷ c , s , comp-env ρ ⟩                         ∼⟨ ∷∼∷′ ⟩≂

    (length s ∷′
     VM.stack-sizes ⟨ c , val (index (comp-env ρ) x) ∷ s , comp-env ρ ⟩)  ≡⟨ by (comp-index ρ x) ⟩≂

    (length s ∷′
     VM.stack-sizes ⟨ c , val (comp-val (index ρ x)) ∷ s , comp-env ρ ⟩)  ≂⟨ cons″-≂ (c-ok (index ρ x)) ⟩∼

    (length s ∷′ numbers (k (index ρ x)) (1 + length s))                  ∼⟨ symmetric-∼ ∷∼∷′ ⟩

    numbers (⟦ var x ⟧ ρ tc >>= k) (length s)                             ∎

  ⟦⟧-correct (lam t) ρ {tc} {c} {s} {k} _ c-ok =
    VM.stack-sizes ⟨ clo (comp-body t) ∷ c , s , comp-env ρ ⟩             ∼⟨ ∷∼∷′ ⟩≂

    (length s ∷′
     VM.stack-sizes ⟨ c , val (comp-val (T.lam t ρ)) ∷ s , comp-env ρ ⟩)  ≂⟨ cons″-≂ (c-ok (T.lam t ρ)) ⟩∼

    (length s ∷′ numbers (k (T.lam t ρ)) (1 + length s))                  ∼⟨ symmetric-∼ ∷∼∷′ ⟩

    numbers (⟦ lam t ⟧ ρ tc >>= k) (length s)                             ∎

  ⟦⟧-correct (t₁ · t₂) ρ {tc} {c} {s} {k} _ c-ok =
    VM.stack-sizes ⟨ comp false t₁ (comp false t₂ (app ∷ c))
                   , s
                   , comp-env ρ
                   ⟩                                                ≂⟨ (⟦⟧-correct t₁ _ unrestricted λ v₁ →

      VM.stack-sizes ⟨ comp false t₂ (app ∷ c)
                     , val (comp-val v₁) ∷ s
                     , comp-env ρ
                     ⟩                                                    ≂⟨ (⟦⟧-correct t₂ _ unrestricted λ v₂ →

        VM.stack-sizes ⟨ app ∷ c
                       , val (comp-val v₂) ∷ val (comp-val v₁) ∷ s
                       , comp-env ρ
                       ⟩                                                        ≂⟨ ∙-correct v₁ v₂ c-ok ⟩∼

        numbers ([ pred , pred ] v₁ ∙ v₂ >>= k) (2 + length s)                  ∎) ⟩∼

      numbers (do v₂ ← ⟦ t₂ ⟧ ρ false
                  [ pred , pred ] v₁ ∙ v₂ >>= k)
              (1 + length s)                                              ∎) ⟩∼

    numbers (do v₁ ← ⟦ t₁ ⟧ ρ false
                v₂ ← ⟦ t₂ ⟧ ρ false
                [ pred , pred ] v₁ ∙ v₂ >>= k)
            (length s)                                              ∼⟨ symmetric-∼ (numbers-cong (⟦⟧-· t₁ t₂ tc)) ⟩

    numbers (⟦ t₁ · t₂ ⟧ ρ tc >>= k) (length s)                     ∎

  ⟦⟧-correct (call f t) ρ {false} {c} {s} {k} unrestricted c-ok =
    VM.stack-sizes ⟨ comp false t (cal f ∷ c) , s , comp-env ρ ⟩        ≂⟨ (⟦⟧-correct t _ unrestricted λ v →

      VM.stack-sizes ⟨ cal f ∷ c , val (comp-val v) ∷ s , comp-env ρ ⟩        ∼⟨ ∷∼∷′ ⟩≂

      1 + length s ∷′
      VM.stack-sizes ⟨ comp-name f
                     , ret c (comp-env ρ) ∷ s
                     , comp-val v ∷ []
                     ⟩                                                        ≂⟨ cons′-≂ (_⇔_.from ≂′⇔≂″ λ { .force →
                                                                                body-lemma (def f) [] (castC c-ok) }) ⟩∼
      1 + length s ∷′
      numbers (⟦ def f ⟧ (v ∷ []) true >>= tell pred ∘ return >>= k)
              (1 + length s)                                                  ∼⟨ symmetric-∼ ∷∼∷′ ⟩

      numbers ([ id , pred ] T.lam (def f) [] ∙ v >>= k)
              (1 + length s)                                                  ∎) ⟩∼

    numbers (⟦ t ⟧ ρ false >>= λ v →
             [ id , pred ] T.lam (def f) [] ∙ v >>= k)
            (length s)                                                  ∼⟨ numbers-cong (DCT.associativity (⟦ t ⟧ _ _) _ _) ⟩

    numbers ((⟦ t ⟧ ρ false >>=
              [ id , pred ] T.lam (def f) [] ∙_) >>= k)
            (length s)                                                  ∼⟨⟩

    numbers (⟦ call f t ⟧ ρ false >>= k) (length s)                     ∎

  ⟦⟧-correct {i} (call f t) ρ {true} {c} {ret c′ ρ′ ∷ s} {k}
             s-ok@(restricted c-ok) _ =
    VM.stack-sizes ⟨ comp false t (tcl f ∷ c)
                   , ret c′ ρ′ ∷ s
                   , comp-env ρ
                   ⟩                                                    ≂⟨ (⟦⟧-correct t _ unrestricted λ v →

      VM.stack-sizes ⟨ tcl f ∷ c
                     , val (comp-val v) ∷ ret c′ ρ′ ∷ s
                     , comp-env ρ
                     ⟩                                                        ∼⟨ ∷∼∷′ ⟩≂

      2 + length s ∷′
      VM.stack-sizes ⟨ comp-name f
                     , ret c′ ρ′ ∷ s
                     , comp-val v ∷ []
                     ⟩                                                        ≡⟨⟩≂

      2 + length s ∷′
      VM.stack-sizes ⟨ comp-name f
                     , ret c′ ρ′ ∷ s
                     , comp-env (v ∷ [])
                     ⟩                                                        ≂⟨ cons′-≂ (_⇔_.from ≂′⇔≂″ λ { .force →
                                                                                ⟦⟧-correct (def f) (_ ∷ []) (restricted lemma) (λ v′ →
        VM.stack-sizes ⟨ ret ∷ []
                       , val (comp-val v′) ∷ ret c′ ρ′ ∷ s
                       , comp-env (v ∷ [])
                       ⟩                                                             ∼⟨ ∷∼∷′ ⟩≂

        2 + length s ∷′
        VM.stack-sizes ⟨ c′ , val (comp-val v′) ∷ s , ρ′ ⟩                           ≂⟨ lemma v′ ⟩∼

        numbers (tell id (k v′)) (2 + length s)                                      ∎) }) ⟩∼

      2 + length s ∷′
      numbers (⟦ def f ⟧ (v ∷ []) true >>= tell id ∘ k) (1 + length s)        ∼⟨ (refl ∷ λ { .force →
                                                                                numbers-cong (DCT.associativity (⟦ def f ⟧ _ _) _ _) }) ⟩
      2 + length s ∷′
      numbers (⟦ def f ⟧ (v ∷ []) true >>= tell id ∘ return >>= k)
              (1 + length s)                                                  ∼⟨ symmetric-∼ ∷∼∷′ ⟩

      numbers ([ pred , id ] T.lam (def f) [] ∙ v >>= k)
              (2 + length s)                                                  ∎) ⟩∼

    numbers (⟦ t ⟧ ρ false >>= λ v →
             [ pred , id ] T.lam (def f) [] ∙ v >>= k)
            (1 + length s)                                              ∼⟨ numbers-cong (DCT.associativity (⟦ t ⟧ _ _) _ _) ⟩

    numbers ((⟦ t ⟧ ρ false >>=
              [ pred , id ] T.lam (def f) [] ∙_) >>= k)
            (1 + length s)                                              ∼⟨⟩

    numbers (⟦ call f t ⟧ ρ true >>= k) (1 + length s)                  ∎
    where
    lemma : {j : Size< i} → _
    lemma = λ v′ →
      2 + length s ∷′
      VM.stack-sizes ⟨ c′ , val (comp-val v′) ∷ s , ρ′ ⟩  ≂⟨ consʳ-≂ (inj₁ (here ≤-refl)) (cast-≂ (c-ok v′)) ⟩∼

      2 + length s ∷′
      numbers (k v′) (2 + length s)                       ∼⟨ symmetric-∼ ∷∼∷′ ⟩

      numbers (tell id (k v′)) (2 + length s)             ∎

  ⟦⟧-correct (con b) ρ {tc} {c} {s} {k} _ c-ok =
    VM.stack-sizes ⟨ con b ∷ c , s , comp-env ρ ⟩                       ∼⟨ ∷∼∷′ ⟩≂

    (length s ∷′
     VM.stack-sizes ⟨ c , val (comp-val (T.con b)) ∷ s , comp-env ρ ⟩)  ≂⟨ cons″-≂ (c-ok (T.con b)) ⟩∼

    (length s ∷′ numbers (k (T.con b)) (1 + length s))                  ∼⟨ symmetric-∼ ∷∼∷′ ⟩

    numbers (⟦ con b ⟧ ρ tc >>= k) (length s)                           ∎

  ⟦⟧-correct (if t₁ t₂ t₃) ρ {tc} {c} {s} {k} s-ok c-ok =
    VM.stack-sizes ⟨ comp false t₁
                       (bra (comp tc t₂ []) (comp tc t₃ []) ∷ c)
                   , s
                   , comp-env ρ
                   ⟩                                                ≂⟨ (⟦⟧-correct t₁ _ unrestricted λ v₁ → ⟦if⟧-correct v₁ t₂ t₃ s-ok c-ok) ⟩∼

    numbers (⟦ t₁ ⟧ ρ false >>= λ v₁ → ⟦if⟧ v₁ t₂ t₃ ρ tc >>= k)
            (length s)                                              ∼⟨ numbers-cong (DCT.associativity (⟦ t₁ ⟧ _ _) _ _) ⟩

    numbers ((⟦ t₁ ⟧ ρ false >>= λ v₁ → ⟦if⟧ v₁ t₂ t₃ ρ tc) >>= k)
            (length s)                                              ∎

  body-lemma :
    ∀ {i n n′} (t : Tm (1 + n)) ρ {ρ′ : C.Env n′} {c s v}
      {k : T.Value → Delay-crash-trace (ℕ → ℕ) C.Value ∞} →
    Cont-OK i ⟨ c , s , ρ′ ⟩ k →
    [ i ] VM.stack-sizes ⟨ comp-body t
                         , ret c ρ′ ∷ s
                         , comp-val v ∷ comp-env ρ
                         ⟩ ≂
          numbers (⟦ t ⟧ (v ∷ ρ) true >>= tell pred ∘ return >>= k)
                  (1 + length s)
  body-lemma t ρ {ρ′} {c} {s} {v} {k} c-ok =
    VM.stack-sizes ⟨ comp-body t
                   , ret c ρ′ ∷ s
                   , comp-val v ∷ comp-env ρ
                   ⟩                                               ≡⟨⟩≂

    VM.stack-sizes ⟨ comp-body t
                   , ret c ρ′ ∷ s
                   , comp-env (v ∷ ρ)
                   ⟩                                               ≂⟨ (⟦⟧-correct t (_ ∷ _) (any-OK (restricted lemma)) λ v′ →

      VM.stack-sizes ⟨ ret ∷ []
                     , val (comp-val v′) ∷ ret c ρ′ ∷ s
                     , comp-env (v ∷ ρ)
                     ⟩                                                   ∼⟨ ∷∼∷′ ⟩≂

      2 + length s ∷′
      VM.stack-sizes ⟨ c , val (comp-val v′) ∷ s , ρ′ ⟩                  ≂⟨ lemma v′ ⟩∼

      numbers (tell pred (k v′)) (2 + length s)                          ∎) ⟩∼

    numbers (⟦ t ⟧ (v ∷ ρ) true >>= tell pred ∘ k) (1 + length s)  ∼⟨ numbers-cong (DCT.associativity (⟦ t ⟧ _ _) _ _) ⟩

    numbers (⟦ t ⟧ (v ∷ ρ) true >>= tell pred ∘ return >>= k)
            (1 + length s)                                         ∎
    where
    lemma = λ v′ →
      2 + length s ∷′
      VM.stack-sizes ⟨ c , val (comp-val v′) ∷ s , ρ′ ⟩  ≂⟨ cons″-≂ (c-ok v′) ⟩∼

      2 + length s ∷′ numbers (k v′) (1 + length s)      ∼⟨ symmetric-∼ ∷∼∷′ ⟩

      numbers (tell pred (k v′)) (2 + length s)          ∎

  ∙-correct :
    ∀ {i n} v₁ v₂ {ρ : C.Env n} {c s}
      {k : T.Value → Delay-crash-trace (ℕ → ℕ) C.Value ∞} →
    Cont-OK i ⟨ c , s , ρ ⟩ k →
    [ i ] VM.stack-sizes ⟨ app ∷ c
                         , val (comp-val v₂) ∷ val (comp-val v₁) ∷ s
                         , ρ
                         ⟩ ≂
          numbers ([ pred , pred ] v₁ ∙ v₂ >>= k) (2 + length s)

  ∙-correct (T.lam t₁ ρ₁) v₂ {ρ} {c} {s} {k} c-ok =
    VM.stack-sizes
      ⟨ app ∷ c
      , val (comp-val v₂) ∷ val (comp-val (T.lam t₁ ρ₁)) ∷ s
      , ρ
      ⟩                                                              ∼⟨ ∷∼∷′ ⟩≂

    2 + length s ∷′
    VM.stack-sizes ⟨ comp-body t₁
                   , ret c ρ ∷ s
                   , comp-val v₂ ∷ comp-env ρ₁
                   ⟩                                                 ≂⟨ cons′-≂ (_⇔_.from ≂′⇔≂″ λ { .force → body-lemma t₁ _ (castC c-ok) }) ⟩∼

    2 + length s ∷′
    numbers (⟦ t₁ ⟧ (v₂ ∷ ρ₁) true >>= tell pred ∘ return >>= k)
            (1 + length s)                                           ∼⟨ symmetric-∼ ∷∼∷′ ⟩

    numbers ([ pred , pred ] T.lam t₁ ρ₁ ∙ v₂ >>= k) (2 + length s)  ∎

  ∙-correct (T.con b) v₂ {ρ} {c} {s} {k} _ =
    VM.stack-sizes ⟨ app ∷ c
                   , val (comp-val v₂) ∷ val (C.con b) ∷ s
                   , ρ
                   ⟩                                             ∼⟨ ∷∼∷′ ⟩≂

    2 + length s ∷′ []                                           ∼⟨ symmetric-∼ ∷∼∷′ ⟩≂

    numbers ([ pred , pred ] T.con b ∙ v₂ >>= k) (2 + length s)  □≂

  ⟦if⟧-correct :
    ∀ {i n} v₁ t₂ t₃ {ρ : T.Env n} {tc c s}
      {k : T.Value → Delay-crash-trace (ℕ → ℕ) C.Value ∞} →
    Stack-OK i k tc s →
    Cont-OK i ⟨ c , s , comp-env ρ ⟩ k →
    [ i ] VM.stack-sizes ⟨ bra (comp tc t₂ []) (comp tc t₃ []) ∷ c
                         , val (comp-val v₁) ∷ s
                         , comp-env ρ
                         ⟩ ≂
          numbers (⟦if⟧ v₁ t₂ t₃ ρ tc >>= k) (1 + length s)

  ⟦if⟧-correct (T.lam t₁ ρ₁) t₂ t₃ {ρ} {tc} {c} {s} {k} _ _ =
    VM.stack-sizes ⟨ bra (comp tc t₂ []) (comp tc t₃ []) ∷ c
                   , val (comp-val (T.lam t₁ ρ₁)) ∷ s
                   , comp-env ρ
                   ⟩                                              ∼⟨ ∷∼∷′ ⟩≂

    1 + length s ∷′ []                                            ∼⟨ symmetric-∼ ∷∼∷′ ⟩≂

    numbers (⟦if⟧ (T.lam t₁ ρ₁) t₂ t₃ ρ tc >>= k) (1 + length s)  □≂

  ⟦if⟧-correct (T.con true) t₂ t₃ {ρ} {tc} {c} {s} {k} s-ok c-ok =
    VM.stack-sizes ⟨ bra (comp tc t₂ []) (comp tc t₃ []) ∷ c
                   , val (comp-val (T.con true)) ∷ s
                   , comp-env ρ
                   ⟩                                             ∼⟨ ∷∼∷′ ⟩≂

    1 + length s ∷′
    VM.stack-sizes ⟨ comp tc t₂ [] ++ c , s , comp-env ρ ⟩       ≡⟨ by (comp-++ _ t₂) ⟩≂

    1 + length s ∷′
    VM.stack-sizes ⟨ comp tc t₂ c , s , comp-env ρ ⟩             ≂⟨ cons″-≂ (⟦⟧-correct t₂ _ s-ok c-ok) ⟩∼

    1 + length s ∷′ numbers (⟦ t₂ ⟧ ρ tc >>= k) (length s)       ∼⟨ symmetric-∼ ∷∼∷′ ⟩

    numbers (⟦if⟧ (T.con true) t₂ t₃ ρ tc >>= k) (1 + length s)  ∎

  ⟦if⟧-correct (T.con false) t₂ t₃ {ρ} {tc} {c} {s} {k} s-ok c-ok =
    VM.stack-sizes ⟨ bra (comp tc t₂ []) (comp tc t₃ []) ∷ c
                   , val (comp-val (T.con false)) ∷ s
                   , comp-env ρ
                   ⟩                                              ∼⟨ ∷∼∷′ ⟩≂

    1 + length s ∷′
    VM.stack-sizes ⟨ comp tc t₃ [] ++ c , s , comp-env ρ ⟩        ≡⟨ by (comp-++ _ t₃) ⟩≂

    1 + length s ∷′
    VM.stack-sizes ⟨ comp tc t₃ c , s , comp-env ρ ⟩              ≂⟨ cons″-≂ (⟦⟧-correct t₃ _ s-ok c-ok) ⟩∼

    1 + length s ∷′ numbers (⟦ t₃ ⟧ ρ tc >>= k) (length s)        ∼⟨ symmetric-∼ ∷∼∷′ ⟩

    numbers (⟦if⟧ (T.con false) t₂ t₃ ρ tc >>= k) (1 + length s)  ∎

-- The virtual machine and the interpreter produce related lists of
-- stack sizes.
--
-- (However, the traces are not necessarily bisimilar, see
-- Lambda.Interpreter.Stack-sizes.Counterexample.stack-sizes-not-bisimilar.)

stack-sizes-related :
  (t : Tm 0) →
  [ ∞ ] VM.stack-sizes ⟨ comp₀ t , [] , [] ⟩ ≂ I.stack-sizes t
stack-sizes-related t =
  VM.stack-sizes ⟨ comp false t [] , [] , [] ⟩  ≂⟨ ⟦⟧-correct t [] unrestricted (λ _ → cons″-≂ (_ □≂)) ⟩∼
  numbers (comp-val ⟨$⟩ ⟦ t ⟧ [] false) 0       ∼⟨ scanl-cong (DCT.trace-⟨$⟩ _) ⟩
  numbers (⟦ t ⟧ [] false) 0                    ∼⟨⟩
  I.stack-sizes t                               ∎

-- The maximum stack sizes match.

maximum-stack-sizes-match :
  ∀ (t : Tm 0) {i v} →
  LUB (I.stack-sizes t) i →
  LUB (VM.stack-sizes ⟨ comp₀ t , [] , [] ⟩) v →
  Conat.[ ∞ ] i ∼ v
maximum-stack-sizes-match t {i} {v} i-lub =
  LUB (VM.stack-sizes ⟨ comp₀ t , [] , [] ⟩) v  ↝⟨ LUB-≂ (stack-sizes-related t) ⟩
  LUB (I.stack-sizes t) v                       ↝⟨ lub-unique i-lub ⟩□
  Conat.[ ∞ ] i ∼ v                             □

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


text:
{-# OPTIONS --without-K #-}
open import Equivalence

module PathStructure.Id.Ap {a b} {A : Set a} {B : Set b}
  (f : A → B) (qi : qinv f) where

open import Functoriality
open import GroupoidStructure
open import Homotopy
open import PathOperations
open import Types

private
  g = π₁ qi
  α = π₁ (π₂ qi)
  β = π₂ (π₂ qi)

split-path : {a a′ : A} → a ≡ a′ → f a ≡ f a′
split-path = ap f

merge-path : {a a′ : A} → f a ≡ f a′ → a ≡ a′
merge-path p = β _ ⁻¹ · ap g p · β _

F : (b b′ : B) (p : b ≡ b′) → Set _
F b b′ p =
    ap f (β (g b) ⁻¹ · ap g (ap (f ∘ g) p) · β (g b′))
  ≡ ap (f ∘ g) p

F-lemma : ∀ b → F b b refl
F-lemma b = ap (ap f)
    ( ap (λ y → β (g b) ⁻¹ · y)
       (id·p _)
    · p⁻¹·p (β (g b))
    )

ap-β-lem : ∀ a → ap (g ∘ f) (β a) ≡ β (g (f a))
ap-β-lem a
  = p·id _ ⁻¹
  · ap (λ y → ap (g ∘ f) (β a) · y)
    (p·p⁻¹ (β a) ⁻¹)
  · p·q·r (ap (g ∘ f) (β a)) (β a) (β a ⁻¹)
  · ap (λ y → y · β a ⁻¹)
    (naturality _ _ β (β a) ⁻¹)
  · ap (λ y → (β (g (f a)) · y) · β a ⁻¹)
    (ap-id _)
  · p·q·r (β (g (f a))) (β a) (β a ⁻¹) ⁻¹
  · ap (λ y → β (g (f a)) · y)
    (p·p⁻¹ (β a))
  · p·id _

add-right : ∀ {a} {A : Set a} {a₁ a₂ a₃ : B} (p q : a₁ ≡ a₂) (r : a₂ ≡ a₃) →
  (p ≡ q) ≡ (p · r ≡ q · r)
add-right {a₁ = a₁} p q r = J
  (λ a₂ _ r → (p q : a₁ ≡ a₂) → (p ≡ q) ≡ (p · r ≡ q · r))
  (λ _ p q →
    tr    (λ x → (p ≡ q) ≡ (p · refl ≡ x)) (p·id q ⁻¹)
      (tr (λ x → (p ≡ q) ≡ (x        ≡ q)) (p·id p ⁻¹) refl))
  _ _ r p q

add-left : ∀ {a} {A : Set a} {a₁ a₂ a₃ : B} (p q : a₂ ≡ a₃) (r : a₁ ≡ a₂) →
  (p ≡ q) ≡ (r · p ≡ r · q)
add-left {a₃ = a₃} p q r = J
  (λ _ a₂ r → (p q : a₂ ≡ a₃) → (p ≡ q) ≡ (r · p ≡ r · q))
  (λ _ p q →
    tr    (λ x → (p ≡ q) ≡ (refl · p ≡ x)) (id·p q ⁻¹)
      (tr (λ x → (p ≡ q) ≡ (x        ≡ q)) (id·p p ⁻¹) refl))
  _ _ r p q

F-tr : ∀ a a′ (q : f a ≡ f a′) →
  F (f a) (f a′) q ≡ (ap f (β a ⁻¹ · ap g q · β a′) ≡ q)
F-tr a a′ q =
 ( add-left  {A = A}
   (ap f (β a ⁻¹ · ap g q · β a′)) q (α (f a))
 · add-right {A = A}
   (α (f a) · ap f (β a ⁻¹ · ap g q · β a′)) (α (f a) · q) (α (f a′) ⁻¹)
 · ap (λ x → (α (f a) · ap f (β a ⁻¹ · ap g q · β a′)) · α (f a′) ⁻¹ ≡ x)
   ( ap (λ y → (α (f a) · y) · α (f a′) ⁻¹)
     (ap-id _ ⁻¹)
   · ap (λ y → y · α (f a′) ⁻¹)
     (naturality _ _ α q)
   · p·q·r (ap (f ∘ g) q) (α (f a′)) (α (f a′) ⁻¹) ⁻¹
   · ap (λ y → ap (f ∘ g) q · y)
     (p·p⁻¹ (α (f a′)))
   · p·id _
   )
 · ap (λ x → x ≡ ap (f ∘ g) q)
   ( ap (λ y → (α (f a) · y) · α (f a′) ⁻¹)
     (ap-id _ ⁻¹)
   · ap (λ y → y · α (f a′) ⁻¹)
     (naturality _ _ α (ap f (β a ⁻¹ · ap g q · β a′)))
   · p·q·r (ap (f ∘ g) (ap f (β a ⁻¹ · ap g q · β a′)))
     (α (f a′)) (α (f a′) ⁻¹) ⁻¹
   · ap (λ y → ap (f ∘ g) (ap f (β a ⁻¹ · ap g q · β a′)) · y)
     (p·p⁻¹ (α (f a′)))
   · p·id _
   · ap-∘ f g (ap f (β a ⁻¹ · ap g q · β a′))
   · ap (ap f)
     ( ap-∘ g f (β a ⁻¹ · ap g q · β a′) ⁻¹
     · ap· (g ∘ f) (β a ⁻¹) (ap g q · β a′)
     · ap (λ y → ap (g ∘ f) (β a ⁻¹) · y)
       (ap· (g ∘ f) (ap g q) (β a′))
     · ap (λ y → y · ap (g ∘ f) (ap g q) · ap (g ∘ f) (β a′))
       (ap⁻¹ (g ∘ f) (β a))
     · ap (λ y → y ⁻¹ · ap (g ∘ f) (ap g q) · ap (g ∘ f) (β a′))
       (ap-β-lem a)
     · ap (λ y → β (g (f a)) ⁻¹ · ap (g ∘ f) (ap g q) · y)
       (ap-β-lem a′)
     · ap (λ y → β (g (f a)) ⁻¹ · y · β (g (f a′)))
       ( ap-∘ g f (ap g q)
       · ap (ap g)
         (ap-∘ f g q ⁻¹)
       )
     )
   )
 ) ⁻¹

proof-F : {a a′ : A} → split-path ∘ merge-path {a} {a′} ∼ id
proof-F p = tr id (F-tr _ _ p) (J F F-lemma _ _ p)

-- Copied from HoTT book, theorem 2.11.1.
proof-direct : {a a′ : A} → split-path ∘ merge-path {a} {a′} ∼ id
proof-direct {a} {a′} p
  = ap (ap f)
    (p·q·r (β a ⁻¹) (ap g p) (β a′))
  · id·p _ ⁻¹
  · ap (λ y → y · ap f ((β a ⁻¹ · ap g p) · β a′))
    (p⁻¹·p (α (f a)) ⁻¹)
  · p·q·r (α (f a) ⁻¹) (α (f a)) (ap f ((β a ⁻¹ · ap g p) · β a′)) ⁻¹
  · ap (λ y → α (f a) ⁻¹ · α (f a) · y)
    (ap-id _ ⁻¹)
  · ap (λ y → α (f a) ⁻¹ · y)
    (naturality _ _ α (ap f ((β a ⁻¹ · ap g p) · β a′)))
  · ap (λ y → α (f a) ⁻¹ · y · α (f a′))
    ( ap-∘ f g (ap f ((β a ⁻¹ · ap g p) · β a′))
    · ap (ap f)
      ( ap-∘ g f ((β a ⁻¹ · ap g p) · β a′) ⁻¹
      · p·id _ ⁻¹
      · ap (λ y → ap (g ∘ f) ((β a ⁻¹ · ap g p) · β a′) · y)
        (p·p⁻¹ (β a′) ⁻¹)
      · p·q·r (ap (g ∘ f) ((β a ⁻¹ · ap g p) · β a′)) (β a′) (β a′ ⁻¹)
      · ap (λ y → y · β a′ ⁻¹)
        ( naturality _ _ β ((β a ⁻¹ · ap g p) · β a′) ⁻¹
        · ap (λ y → β a · y)
          (ap-id _)
        )
      · ap (λ y → y · β a′ ⁻¹)
        (p·q·r (β a) (β a ⁻¹ · ap g p) (β a′))
      · p·q·r (β a · β a ⁻¹ · ap g p) (β a′) (β a′ ⁻¹) ⁻¹
      · ap (λ y → (β a · β a ⁻¹ · ap g p) · y)
        (p·p⁻¹ (β a′))
      · p·id _
      · p·q·r (β a) (β a ⁻¹) (ap g p)
      · ap (λ y → y · ap g p)
        (p·p⁻¹ (β a))
      · id·p _
      )
    · ap-∘ f g p ⁻¹
    )
  · ap (λ y → α (f a) ⁻¹ · y)
    (naturality _ _ α p ⁻¹)
  · p·q·r (α (f a) ⁻¹) (α (f a)) (ap id p)
  · ap (λ y → y · ap id p)
    (p⁻¹·p (α (f a)))
  · ap-id _

split-merge-eq : {a a′ : A} → (a ≡ a′) ≃ (f a ≡ f a′)
split-merge-eq
  = split-path
  , (merge-path , proof-F)
  , (merge-path , J
      (λ _ _ p → merge-path (split-path p) ≡ p)
      (λ _ → p⁻¹·p (β _))
      _ _)

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


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

open import Types
open import Paths
open import HLevel
open import Equivalences
open import Univalence

module Funext {i} {A : Set i} where

-- Naive non dependent function extensionality

module FunextNonDep {j} {B : Set j} {f g : A → B} (h : (x : A) → f x ≡ g x)
  where

  private
    equiv-comp : {B C : Set j} (f : B ≃ C)
      → is-equiv (λ (g : A → B) → (λ x → f ☆ (g x)))
    equiv-comp f =
      equiv-induction (λ {B} f → is-equiv (λ (g : A → B) → (λ x → f ☆ (g x))))
                      (λ A' y → id-is-equiv (A → A') y) f

    free-path-space-B : Set j
    free-path-space-B = Σ B (λ x → Σ B (λ y → x ≡ y))

    d : A → free-path-space-B
    d x = (f x , (f x , refl))

    e : A → free-path-space-B
    e x = (f x , (g x , h x))

    abstract
      π₁-is-equiv : is-equiv (λ (y : free-path-space-B) → π₁ y)
      π₁-is-equiv =
        iso-is-eq π₁ (λ z → (z , (z , refl))) (λ _ → refl)
          (λ x' → Σ-eq refl
                    (Σ-eq (π₂ (π₂ x'))
                      (trans-cst≡id (π₂ (π₂ x')) refl)))

      comp-π₁-is-equiv : is-equiv (λ (f : A → free-path-space-B)
                                     → (λ x → π₁ (f x)))
      comp-π₁-is-equiv = equiv-comp ((λ (y : free-path-space-B) → π₁ y),
                                     π₁-is-equiv)

      d≡e : d ≡ e
      d≡e = equiv-is-inj (_ , comp-π₁-is-equiv) _ _ refl

  funext-nondep : f ≡ g
  funext-nondep = ap (λ f' x → π₁ (π₂ (f' x))) d≡e

open FunextNonDep

-- Weak function extensionality (a product of contractible types is
-- contractible)
module WeakFunext {j} {P : A → Set j} (e : (x : A) → is-contr (P x)) where

  P-is-unit : P ≡ (λ x → unit)
  P-is-unit = funext-nondep (λ x → eq-to-path (contr-equiv-unit (e x)))

  abstract
    weak-funext : is-contr (Π A P)
    weak-funext = transport (λ Q → is-contr (Π A Q)) (! P-is-unit)
                            ((λ x → tt) , (λ y → funext-nondep (λ x → refl)))

open WeakFunext

-- Naive dependent function extensionality

module FunextDep {j} {P : A → Set j} {f g : Π A P} (h : (x : A) → f x ≡ g x)
  where

  Q : A → Set j
  Q x = Σ (P x) (λ y → y ≡ f x)

  abstract
    Q-is-contr : (x : A) → is-contr (Q x)
    Q-is-contr x = pathto-is-contr (f x)

    ΠAQ-is-contr : is-contr (Π A Q)
    ΠAQ-is-contr = weak-funext Q-is-contr

  Q-f : Π A Q
  Q-f x = (f x , refl)

  Q-g : Π A Q
  Q-g x = (g x , ! (h x))

  abstract
    Q-f≡Q-g : Q-f ≡ Q-g
    Q-f≡Q-g = contr-has-all-paths ΠAQ-is-contr Q-f Q-g

  funext-p : f ≡ g
  funext-p = ap (λ u x → π₁ (u x)) Q-f≡Q-g

open FunextDep

happly : ∀ {j} {P : A → Set j} {f g : Π A P} (p : f ≡ g) → ((x : A) → f x ≡ g x)
happly p x = ap (λ u → u x) p

-- Strong function extensionality

module StrongFunextDep {j} {P : A → Set j} where

  abstract
    funext-refl : (f : Π A P)
      → funext-p (λ x → refl {a = f x}) ≡ refl
    funext-refl f = ap (ap (λ u x → π₁ (u x)))
      (contr-has-all-paths (≡-is-truncated _
                           (ΠAQ-is-contr (λ x → refl)))
                           (Q-f≡Q-g (λ x → refl)) refl)

  abstract
    funext-happly-p : {f g : Π A P} (p : f ≡ g)
      → funext-p (happly p) ≡ p
    funext-happly-p {f} refl = funext-refl f

  abstract
    happly-path : {f : Π A P} {u v : (x : A) → Q (λ x → refl {a = f x}) x}
      (p : u ≡ v) (x : A)
      → happly (ap (λ u x → π₁ (u x)) p) x ≡ π₂ (u x) ∘ ! (π₂ (v x))
    happly-path {u = u} refl x = ! (opposite-right-inverse (π₂ (u x)))

  abstract
    happly-funext-p : {f g : Π A P} (h : (x : A) → f x ≡ g x)
      → happly (funext-p h) ≡ h
    happly-funext-p h = funext-p (λ x → happly-path (Q-f≡Q-g h) x
                                              ∘ opposite-opposite (h x))

  happly-is-equiv : {f g : Π A P} → is-equiv (happly {f = f} {g = g})
  happly-is-equiv = iso-is-eq _ funext-p happly-funext-p funext-happly-p

  funext-is-equiv-p : {f g : Π A P}
    → is-equiv (funext-p {f = f} {g = g})
  funext-is-equiv-p = iso-is-eq _ happly funext-happly-p happly-funext-p

open StrongFunextDep

-- We only export the following

module _ {j} {P : A → Set j} {f g : Π A P} where

  abstract
    funext : (h : (x : A) → f x ≡ g x) → f ≡ g
    funext = FunextDep.funext-p

    funext-happly : (p : f ≡ g) → funext (happly p) ≡ p
    funext-happly p = funext-happly-p p

    happly-funext : (h : (x : A) → f x ≡ g x)
      → happly (funext h) ≡ h
    happly-funext h = happly-funext-p h

    funext-is-equiv : is-equiv funext
    funext-is-equiv = StrongFunextDep.funext-is-equiv-p

  funext-equiv : ((x : A) → f x ≡ g x) ≃ (f ≡ g)
  funext-equiv = (funext , funext-is-equiv)

  happly-equiv : (f ≡ g) ≃ ((x : A) → f x ≡ g x)
  happly-equiv = (happly , happly-is-equiv)

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

open import equality.core

module _ {i}{A : Set i}
         (_<_ : A → A → Set i) where
  data Ordering (x y : A) : Set i where
    lt : x < y → Ordering x y
    eq : x ≡ y → Ordering x y
    gt : y < x → Ordering x y


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

module Cubical.Categories.Presheaf where

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

open import Cubical.Categories.Presheaf.KanExtension public

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


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

macro

  @0 m : @0 Set → Term → TC ⊤
  m A B =
    bindTC (quoteTC A) λ A →
    unify A B

F : @0 Set → Set
F A = m A


text:
-- Andreas, 2016-10-03, issue #2233
-- Positivity check should return the same result when change
-- all involved definitions from non-abstract to abstract.

abstract
  data Functor : Set where
    Id : Functor

  _·_ : Functor → Set → Set
  Id · A = A

  data ν (F : Functor) : Set where
    inn : F · ν F → ν F

-- Should positivity check ok.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import WarningOnImport.Impo

C = A


text:
module Data.List.Properties.Extra {a}{A : Set a} where

open import Data.Nat
open import Data.Fin hiding (_<_)
open import Data.List
open import Data.Product hiding (map)
open import Data.Fin using (fromℕ≤; zero; suc)
open import Data.List.Relation.Unary.All hiding (map; lookup; _[_]≔_)
open import Data.List.Relation.Unary.Any hiding (map; lookup)
open import Data.List.Membership.Propositional

open import Data.List.Relation.Binary.Pointwise hiding (refl; map)
open import Relation.Binary.PropositionalEquality

∈-∷ʳ : ∀ (l : List A)(x : A) → x ∈ (l ∷ʳ x)
∈-∷ʳ [] x = here refl
∈-∷ʳ (x ∷ l) y = there (∈-∷ʳ l y)

infixl 10 _[_]≔_
_[_]≔_ : (l : List A) → Fin (length l) → A → List A
[] [ () ]≔ x
(x ∷ xs) [ zero ]≔ x' = x' ∷ xs
(x ∷ xs) [ suc i ]≔ y = x ∷ xs [ i ]≔ y

infixl 10 _[_]≔'_
_[_]≔'_ : ∀ {x} → (l : List A) → x ∈ l → A → List A
[] [ () ]≔' y
(x ∷ l) [ here px ]≔' y = y ∷ l
(x ∷ l) [ there px ]≔' y = x ∷ (l [ px ]≔' y)

≔'-[]= :  ∀ {x}{l : List A} (p : x ∈ l) → ∀ {y} → y ∈ (l [ p ]≔' y)
≔'-[]= (here px) = here refl
≔'-[]= (there p) = there (≔'-[]= p)

drop-prefix : ∀ (l m : List A) → drop (length l) (l ++ m) ≡ m
drop-prefix [] m = refl
drop-prefix (x ∷ l) m = drop-prefix l m


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

open import lib.Basics
open import lib.types.Cofiber
open import lib.types.Sigma
open import lib.types.Wedge

module lib.types.Smash {i j} (X : Ptd i) (Y : Ptd j) where

module ∨In× = WedgeRec {X = X} {Y = Y}
  (λ x → (x , pt Y)) (λ y → (pt X , y)) idp

∨-in-× = ∨In×.f

∨-⊙in-× : X ⊙∨ Y ⊙→ X ⊙× Y
∨-⊙in-× = (∨In×.f , idp)

⊙Smash : Ptd (lmax i j)
⊙Smash = ⊙Cofiber ∨-⊙in-×

Smash = de⊙ ⊙Smash

_∧_ = Smash
_⊙∧_ = ⊙Smash

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

open import Level
open import Data.Unit

open import Categories.Support.PropositionalEquality
open import Categories.Category
open import Categories.Globe
open import Categories.Functor
open import Categories.Presheaf
open import Categories.Agda

record GlobularSet (o : Level) : Set (suc o) where
  field
    presheaf : Presheaf Globe (Sets o)

Trivial : GlobularSet zero
Trivial = record
  { presheaf = record
    { F₀ = λ x → ⊤
    ; F₁ = λ x y → y
    ; identity = ≣-refl
    ; homomorphism = ≣-refl
    ; F-resp-≡ = λ x → ≣-refl
    }
  }

zeroCell : ∀ {ℓ} → GlobularSet ℓ → Set ℓ
zeroCell G = Functor.F₀ (GlobularSet.presheaf G) 0

{-
lift : ∀ {ℓ} → (G : GlobularSet ℓ) → (A : Set ℓ) → (f g : zeroCell G → A) → GlobularSet ℓ
lift {ℓ} G A f g = record
  { presheaf = record
    { F₀ = F₀′
    ; F₁ = F₁′
    ; identity = ≣-refl
    ; homomorphism = {!!}
    ; F-resp-≡ = F-resp-≡′
    }
  }
  where
  open GlobularSet G
  open Functor presheaf

  F₀′ : ℕ → Set ℓ
  F₀′ zero = A
  F₀′ (suc n) = F₀ n

  F₁′ : ∀ {A B} → GlobeHom B A → F₀′ A → F₀′ B
  F₁′ I a = a
  F₁′ {suc zero} (σ Z<Sn) a = f a
  F₁′ {suc (suc m)} (σ Z<Sn) a = F₁′ {suc m} (σ Z<Sn) {!!}
  F₁′ (σ (raise< n<m)) a = {!!}
  F₁′ (τ n<m) a = {!!}

  F-resp-≡′ : ∀ {A B} {F G : GlobeHom B A} → F ≣ G → {x : F₀′ A} → F₁′ F x ≣ F₁′ G x
  F-resp-≡′ ≣-refl = ≣-refl

{-
objs : ∀ {ℓ} → (A : Set ℓ) → ℕ → Set ℓ
objs A zero = A
objs A (suc n) = Σ (objs A n) (λ x → Σ (objs A n) (λ y → x ≣ y))

base : ∀ {n} {ℓ} {A : Set ℓ} → objs A n → A
base {zero} o = o
base {suc n} (s , t , s≡t) = base {n} s

homs : ∀ {A B} {ℓ} (Q : Set ℓ) → GlobeHom B A → objs Q A → objs Q B
homs Q I o = o
homs {suc n} Q (σ Z<Sn) (s , t , s≡t) = base {n} s
homs Q (σ (raise< n<m)) (s , .s , ≣-refl) = homs Q (σ n<m) s , homs Q (σ n<m) s , ≣-refl
homs {suc n} Q (τ Z<Sn) (s , t , s≡t) = base {n} t
homs Q (τ (raise< n<m)) (s , .s , ≣-refl) = homs Q (τ n<m) s , homs Q (τ n<m) s , ≣-refl

Equality : ∀ {ℓ} (A : Set ℓ) → GlobularSet ℓ
Equality A = record
  { presheaf = record
    { F₀ = objs A
    ; F₁ = homs A
    ; identity = ≣-refl
    ; homomorphism = λ {_} {_} {_} {f} {g} → homomorphism {f = f} {g}
    ; F-resp-≡ = F-resp-≡
    }
  }
  where
  homomorphism : {X Y Z : ℕ} {f : GlobeHom Y X} {g : GlobeHom Z Y} {x : objs A X} → homs A (f ⊚ g) x ≣ homs A g (homs A f x)
  homomorphism {f = I} = ≣-refl
  homomorphism {f = σ n<m} {I} = ≣-refl
  homomorphism {f = σ n<m} {σ n<m'} = {!!}
  homomorphism {f = σ n<m} {τ n<m'} = {!!}
  homomorphism {f = τ n<m} {I} = ≣-refl
  homomorphism {f = τ n<m} {σ n<m'} = {!!}
  homomorphism {f = τ n<m} {τ n<m'} = {!!}

  F-resp-≡ : {A' B : ℕ} {F G : GlobeHom B A'} → F ≣ G → {x : objs A A'} → _
  F-resp-≡ ≣-refl = ≣-refl
-}
-}

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --warning ShadowingInTelescope #-}

postulate
  _ : (A A : Set) → Set


text:
module BasicIS4.Metatheory.Gentzen-BasicKripkeAlechina where

open import BasicIS4.Syntax.Gentzen public
open import BasicIS4.Semantics.BasicKripkeAlechina public

-- Soundness with respect to all models, or evaluation.

mutual
  eval : ∀ {A Γ} → Γ ⊢ A → Γ ⊨ A
  eval (var i)           γ = lookup i γ
  eval (lam t)           γ = λ ξ a → eval t (mono⊩⋆ ξ γ , a)
  eval (app {A} {B} t u) γ = _⟪$⟫_ {A} {B} (eval t γ) (eval u γ)
  eval (multibox ts u)   γ = λ ξ ζ → eval u (thing ts γ ξ ζ)
  eval (down {A} t)      γ = ⟪↓⟫ {A} (eval t γ)
  eval (pair t u)        γ = eval t γ , eval u γ
  eval (fst t)           γ = π₁ (eval t γ)
  eval (snd t)           γ = π₂ (eval t γ)
  eval unit              γ = ∙

  -- TODO: What is this?
  thing : ∀ {{_ : Model}} {Δ Γ} {w : World}
          → Γ ⊢⋆ □⋆ Δ → w ⊩⋆ Γ → ∀ {w′} → w ≤ w′ → ∀ {v′} → w′ R v′ → v′ ⊩⋆ □⋆ Δ
  thing {∅}     ∙        γ ξ ζ = ∙
  thing {Δ , B} (ts , t) γ ξ ζ = thing ts γ ξ ζ , λ ξ′ ζ′ →
                                 let _ , (ξ″ , ζ″) = R⨾≤→≤⨾R (_ , (ζ , ξ′))
                                 in  eval t γ (trans≤ ξ ξ″) (transR ζ″ ζ′)

eval⋆ : ∀ {Ξ Γ} → Γ ⊢⋆ Ξ → Γ ⊨⋆ Ξ
eval⋆ {∅}     ∙        γ = ∙
eval⋆ {Ξ , A} (ts , t) γ = eval⋆ ts γ , eval t γ

-- TODO: Correctness of evaluation with respect to conversion.

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
------------------------------------------------------------------------
-- Some defined parsers
------------------------------------------------------------------------

-- Note that the fixpoint combinator ensures that _⋆ can be defined
-- without any need for library grammars (c.f.
-- RecursiveDescent.Inductive.Lib). However, use of the fixpoint
-- combinator can lead to code which is hard to understand, and should
-- be kept at a minimum.

-- This module also provides an example of a parser for which the
-- Index cannot be inferred.

module RecursiveDescent.InductiveWithFix.Lib where

open import RecursiveDescent.Index
open import RecursiveDescent.InductiveWithFix
open import Utilities

open import Data.Nat hiding (_≟_)
import Data.Vec  as V;  open V  using (Vec)
import Data.Vec1 as V₁; open V₁ using (Vec₁)
import Data.List as L ; open L  using (List)
open import Relation.Nullary
open import Data.Product.Record
open import Data.Product renaming (_,_ to pair)
open import Data.Bool hiding (_≟_)
open import Data.Function
open import Data.Maybe
open import Data.Unit hiding (_≟_)

------------------------------------------------------------------------
-- Applicative functor parsers

-- We could get these for free with better library support.

infixl 50 _⊛_ _<⊛_ _⊛>_ _<$>_ _<$_

_⊛_ : forall {tok nt i₁ i₂ r₁ r₂} ->
      Parser tok nt i₁ (r₁ -> r₂) ->
      Parser tok nt i₂ r₁ ->
      Parser tok nt _  r₂
p₁ ⊛ p₂ = p₁ >>= \f -> p₂ >>= \x -> return (f x)

_<$>_ : forall {tok nt i r₁ r₂} ->
        (r₁ -> r₂) ->
        Parser tok nt i r₁ ->
        Parser tok nt _ r₂
f <$> x = return f ⊛ x

_<⊛_ : forall {tok nt i₁ i₂ r₁ r₂} ->
       Parser tok nt i₁ r₁ ->
       Parser tok nt i₂ r₂ ->
       Parser tok nt _ r₁
x <⊛ y = const <$> x ⊛ y

_⊛>_ : forall {tok nt i₁ i₂ r₁ r₂} ->
       Parser tok nt i₁ r₁ ->
       Parser tok nt i₂ r₂ ->
       Parser tok nt _ r₂
x ⊛> y = flip const <$> x ⊛ y

_<$_ : forall {tok nt i r₁ r₂} ->
       r₁ ->
       Parser tok nt i r₂ ->
       Parser tok nt _ r₁
x <$ y = const x <$> y

------------------------------------------------------------------------
-- Parsing sequences

infix 55 _⋆ _+

_⋆ : forall {tok nt c r} ->
     Parser tok nt (false , c) r ->
     Parser tok nt _ (List r)
p ⋆ = fix (return L.[] ∣ L._∷_ <$> lift p ⊛ ! fresh)

_+ : forall {tok nt c r} ->
     Parser tok nt (false , c) r ->
     Parser tok nt _ (List r)
p + = L._∷_ <$> p ⊛ p ⋆

chain₁ :  forall {tok nt c₁ i₂ r}
       -> Assoc
       -> Parser tok nt (false , c₁) r
       -> Parser tok nt i₂ (r -> r -> r)
       -> Parser tok nt _ r
chain₁ a p op = chain₁-combine a <$> (pair <$> p ⊛ op) ⋆ ⊛ p

chain :  forall {tok nt c₁ i₂ r}
      -> Assoc
      -> Parser tok nt (false , c₁) r
      -> Parser tok nt i₂ (r -> r -> r)
      -> r
      -> Parser tok nt _ r
chain a p op x = return x ∣ chain₁ a p op

-- Note that the resulting index here cannot be inferred...

private

  exactly'-corners : Corners -> ℕ -> Corners
  exactly'-corners c zero    = _
  exactly'-corners c (suc n) = _

  exactly' : forall {tok nt c r} n ->
             Parser tok nt (false , c) r ->
             Parser tok nt (false , exactly'-corners c n)
                           (Vec r (suc n))
  exactly' zero    p = V.[_] <$> p
  exactly' (suc n) p = V._∷_ <$> p ⊛ exactly' n p

-- ...so we might as well generalise the function a little.
-- exactly n p parses n occurrences of p.

exactly-index : Index -> ℕ -> Index
exactly-index i zero    = _
exactly-index i (suc n) = _

exactly : forall {tok nt i r} n ->
          Parser tok nt i r ->
          Parser tok nt (exactly-index i n) (Vec r n)
exactly zero    p = return V.[]
exactly (suc n) p = V._∷_ <$> p ⊛ exactly n p

-- A function with a similar type:

sequence : forall {tok nt i r n} ->
           Vec₁ (Parser tok nt i r) n ->
           Parser tok nt (exactly-index i n) (Vec r n)
sequence V₁.[]         = return V.[]
sequence (V₁._∷_ p ps) = V._∷_ <$> p ⊛ sequence ps

------------------------------------------------------------------------
-- sat and friends

sat : forall {tok nt r} ->
      (tok -> Maybe r) -> Parser tok nt (0I ·I 1I) r
sat {tok} {nt} {r} p = symbol !>>= \c -> ok (p c)
  where
  okIndex : Maybe r -> Index
  okIndex nothing  = _
  okIndex (just _) = _

  ok : (x : Maybe r) -> Parser tok nt (okIndex x) r
  ok nothing  = fail
  ok (just x) = return x

sat' : forall {tok nt} -> (tok -> Bool) -> Parser tok nt _ ⊤
sat' p = sat (boolToMaybe ∘ p)

any : forall {tok nt} -> Parser tok nt _ tok
any = sat just

------------------------------------------------------------------------
-- Some parsers which require a decidable token equality

open import Relation.Binary

module Token (D : DecSetoid) where

  open DecSetoid D using (_≟_) renaming (carrier to tok)
  open import Data.Vec1

  -- Parsing a given token (or, really, a given equivalence class of
  -- tokens).

  sym : forall {nt} -> tok -> Parser tok nt _ tok
  sym c = sat p
    where
    p : tok -> Maybe tok
    p x with c ≟ x
    ... | yes _ = just x
    ... | no  _ = nothing

  -- Parsing a sequence of tokens.

  string : forall {nt n} -> Vec tok n -> Parser tok nt _ (Vec tok n)
  string cs = sequence (map₀₁ sym cs)

------------------------------------------------------------------------
-- Character parsers

import Data.Char as C
open C using (Char; _==_)
open Token C.decSetoid

digit : forall {nt} -> Parser Char nt _ ℕ
digit = 0 <$ sym '0'
      ∣ 1 <$ sym '1'
      ∣ 2 <$ sym '2'
      ∣ 3 <$ sym '3'
      ∣ 4 <$ sym '4'
      ∣ 5 <$ sym '5'
      ∣ 6 <$ sym '6'
      ∣ 7 <$ sym '7'
      ∣ 8 <$ sym '8'
      ∣ 9 <$ sym '9'

number : forall {nt} -> Parser Char nt _ ℕ
number = toNum <$> digit +
  where toNum = L.foldr (\n x -> 10 * x + n) 0 ∘ L.reverse

-- whitespace recognises an incomplete but useful list of whitespace
-- characters.

whitespace : forall {nt} -> Parser Char nt _ ⊤
whitespace = sat' isSpace
  where
  isSpace = \c -> (c == ' ') ∨ (c == '\t') ∨ (c == '\n') ∨ (c == '\r')

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module RecordConstructors (Parameter : Set) where

-- Note that the fixity declaration has to be given outside of the
-- record definition.

infix 6 _⟨_⟩_

record R (X : Set) (Y : Set) : Set₁ where
  constructor _⟨_⟩_
  field
    {A}       : Set
    f         : A → X
    {B} D {E} : Set
    g         : B → Y → E

postulate A : Set

r : R A A
r = f ⟨ A ⟩ λ (_ : A) → f
  where
  f : A → A
  f x = x

data _≡_ {A : Set₁} (x : A) : A → Set where
  refl : x ≡ x

lemma : r ≡ record {}
lemma = refl

-- Record constructors can be overloaded.

record R′ : Set₁ where
  constructor _⟨_⟩_
  field
    T₁ T₂ T₃ : Set

data D : Set where
  _⟨_⟩_ : D

r′ : R′
r′ = A ⟨ A ⟩ A

d : D
d = _⟨_⟩_


text:
module Relator.Equals.Proofs.Equivalence where

open import Functional
import      Lvl
open import Lang.Instance
open import Logic.Propositional
open import Logic
open import Relator.Equals
open import Structure.Setoid using (Equiv) renaming (_≡_ to _≡ₛ_)
open import Structure.Function
open import Structure.Operator
open import Structure.Relator
open import Structure.Relator.Equivalence
import      Structure.Relator.Names as Names
open import Structure.Relator.Properties
open import Structure.Type.Identity
open import Structure.Type.Identity.Proofs
open import Type

-- TODO: Consider using Structure.Type.Identity instead of these proofs

module One {ℓ} {T : Type{ℓ}} where
  instance
    [≡]-reflexivity : Reflexivity (_≡_ {T = T})
    [≡]-reflexivity = intro [≡]-intro

  instance
    [≡]-identity-eliminator : ∀{ℓₚ} → IdentityEliminator{ℓₚ = ℓₚ}(_≡_ {T = T})
    IdentityEliminator.elim [≡]-identity-eliminator _ proof {x = x}{y = .x} [≡]-intro = proof{x}

  instance
    [≡]-symmetry : Symmetry (_≡_ {T = T})
    [≡]-symmetry = identity-eliminator-to-symmetry

  instance
    [≡]-transitivity : Transitivity (_≡_ {T = T})
    [≡]-transitivity = identity-eliminator-to-transitivity

  instance
    [≡]-equivalence : Equivalence (_≡_ {T = T})
    [≡]-equivalence = intro

  [≡]-to-equivalence : ∀{ℓₗ}{x y : T} → (x ≡ y) → ⦃ equiv-T : Equiv{ℓₗ}(T) ⦄ → (_≡ₛ_ ⦃ equiv-T ⦄ x y)
  [≡]-to-equivalence([≡]-intro) = reflexivity(_≡ₛ_)

  [≡]-equiv : Equiv{ℓ}(T)
  Equiv._≡_ [≡]-equiv = _≡_
  Equiv.equivalence [≡]-equiv = [≡]-equivalence

  -- Equality is a subrelation to every reflexive relation.
  -- One interpretation of this is that identity is the smallest reflexive relation when a relation is interpreted as a set of tuples and size is the cardinality of the set.
  instance
    [≡]-sub-of-reflexive : ∀{ℓₗ}{_▫_ : T → T → Stmt{ℓₗ}} → ⦃ _ : Reflexivity(_▫_) ⦄ → ((_≡_) ⊆₂ (_▫_))
    _⊆₂_.proof [≡]-sub-of-reflexive [≡]-intro = reflexivity(_)

  -- Replaces occurrences of an element in a function
  [≡]-substitutionᵣ : ∀{ℓ₂}{x y} → (x ≡ y) → ∀{f : T → Type{ℓ₂}} → f(x) → f(y)
  [≡]-substitutionᵣ [≡]-intro p = p -- TODO: Express in terms of sub-of-reflexive which is transport so that functors are automatically something

  -- Replaces occurrences of an element in a function
  [≡]-substitutionₗ : ∀{ℓ₂}{x y} → (x ≡ y) → ∀{f : T → Type{ℓ₂}} → f(y) → f(x)
  [≡]-substitutionₗ [≡]-intro p = p

  [≡]-substitution : ∀{ℓ₂}{x y} → (x ≡ y) → ∀{f : T → Type{ℓ₂}} → (f(x) ↔ f(y))
  [≡]-substitution eq = [↔]-intro ([≡]-substitutionₗ eq) ([≡]-substitutionᵣ eq)

  [≡]-unary-relator : ∀{ℓ₂}{P : T → Stmt{ℓ₂}} → UnaryRelator ⦃ [≡]-equiv ⦄ (P)
  UnaryRelator.substitution([≡]-unary-relator {P = P}) xy = [≡]-substitutionᵣ xy {P}

  [≡]-binary-relator : ∀{ℓ₂}{P : T → T → Stmt{ℓ₂}} → BinaryRelator ⦃ [≡]-equiv ⦄ ⦃ [≡]-equiv ⦄ (P)
  BinaryRelator.substitution [≡]-binary-relator [≡]-intro [≡]-intro = id
open One public

module Two {ℓ₁}{A : Type{ℓ₁}} {ℓ₂}{B : Type{ℓ₂}} where
  -- Applies a function to each side of the equality (TODO: Remove this and use Function everywhere instead)
  [≡]-with : (f : A → B) → ∀{x y : A} → (x ≡ y) → (f(x) ≡ f(y))
  [≡]-with f [≡]-intro = [≡]-intro

  [≡]-function : ∀{f} → Function ⦃ [≡]-equiv ⦄ ⦃ [≡]-equiv ⦄ (f)
  Function.congruence([≡]-function {f}) eq = [≡]-with(f) eq

  [≡]-to-function : ∀{ℓₗ} → ⦃ equiv-B : Equiv{ℓₗ}(B) ⦄ → ∀{f : A → B} → Function ⦃ [≡]-equiv ⦄ ⦃ equiv-B ⦄ (f)
  Function.congruence ([≡]-to-function) [≡]-intro = reflexivity(_≡ₛ_)
open Two public

module Three {ℓ₁}{A : Type{ℓ₁}} {ℓ₂}{B : Type{ℓ₂}} {ℓ₃}{C : Type{ℓ₃}} where
  -- Applies an operation to each side of the equality (TODO: Make this an instance of BinaryOperator instead)
  [≡]-with-op : (_▫_ : A → B → C) → {a₁ a₂ : A}{b₁ b₂ : B} → (a₁ ≡ a₂) → (b₁ ≡ b₂) → ((a₁ ▫ b₁) ≡ (a₂ ▫ b₂))
  [≡]-with-op (_▫_) [≡]-intro [≡]-intro = [≡]-intro
  -- [≡]-with-op-[_] (_▫_) {a₁}{a₂} {b₁}{b₂} (a₁≡a₂) (b₁≡b₂) =
  --   [≡]-elimᵣ (b₁≡b₂) {\x → (a₁ ▫ b₁) ≡ (a₂ ▫ x)} ([≡]-with(x ↦ (x ▫ b₁)) (a₁≡a₂))

  [≡]-binary-operator : ∀{_▫_} → BinaryOperator ⦃ [≡]-equiv ⦄ ⦃ [≡]-equiv ⦄ ⦃ [≡]-equiv ⦄ (_▫_)
  BinaryOperator.congruence([≡]-binary-operator {_▫_}) aeq beq = [≡]-with-op(_▫_) aeq beq
open Three public

module Four {ℓ₁}{A : Type{ℓ₁}} {ℓ₂}{B : Type{ℓ₂}} {ℓ₃}{C : Type{ℓ₃}} {ℓ₄}{D : Type{ℓ₄}} where
  [≡]-trinary-operator : ∀{_▫_▫_ : A → B → C → D} → TrinaryOperator ⦃ [≡]-equiv ⦄ ⦃ [≡]-equiv ⦄ ⦃ [≡]-equiv ⦄ ⦃ [≡]-equiv ⦄ (_▫_▫_)
  TrinaryOperator.congruence([≡]-trinary-operator {_▫_▫_}) [≡]-intro [≡]-intro [≡]-intro = [≡]-intro
open Four public

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:
{-# OPTIONS -v tc.lhs:50 #-}
{-# OPTIONS -v tc.coverage:50 #-}

open import Agda.Builtin.String

test : String → String
test x@"foo" = "bar"
test x       = x


text:
{-# OPTIONS --universe-polymorphism #-}
module Issue204 where

open import Issue204.Dependency

postulate
  ℓ : Level
  r : R ℓ
  d : D ℓ

open R r

open M d


text:
-- Andreas, 2014-09-09

mutual
  {-# NON_TERMINATING #-}
  f : Set
  f = g

  {-# TERMINATING #-}
  g : Set
  g = f

-- Expected error:
-- In a mutual block, either all functions must have the same (or no)
-- termination checking pragma.


text:
import Either
open import Boolean

module Logic where

  id : ∀ { A : Set } → A → A
  id x = x

  Rel : Set → Set₁
  Rel X = X → X → Set

  Decidable : ∀ { X } → Rel X → Set
  Decidable R = ∀ x y → Either (R x y) (¬ (R x y))
    where open Either

  modusPonens : { P Q : Set } → ( P → Q ) → P → Q
  modusPonens = id

max_stars_repo_name: cantsin/agda-experiments

max_issues_repo_name: cantsin/agda-experiments

max_forks_repo_name: cantsin/agda-experiments


text:
module Data.Tuple where

import      Lvl
open import Type
open import Syntax.Function

infixr 200 _⨯_ _,_

private variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Lvl.Level
private variable A B C A₁ A₂ B₁ B₂ : Type{ℓ}

-- Definition of a 2-tuple
record _⨯_ (A : Type{ℓ₁}) (B : Type{ℓ₂}) : Type{ℓ₁ Lvl.⊔ ℓ₂} where
  constructor _,_
  field
    left  : A
    right : B
open _⨯_ public

elim : ∀{P : (A ⨯ B) → Type{ℓ}} → ((a : A) → (b : B) → P(a , b)) → ((p : (A ⨯ B)) → P(p))
elim f(a , b) = f a b

map : (A₁ → A₂) → (B₁ → B₂) → (A₁ ⨯ B₁) → (A₂ ⨯ B₂)
map f g (x , y) = (f(x) , g(y))

-- Curries a function taking a 2-tuple, transforming it to a function returning a function instead
curry : ((A ⨯ B) → C) → (A → B → C)
curry f x y = f(x , y)

-- Uncurries a function taking a function, transforming it to a function taking a 2-tuple instead
uncurry : (A → B → C) → ((A ⨯ B) → C)
uncurry = elim

mapLeft : (A₁ → A₂) → (A₁ ⨯ B) → (A₂ ⨯ B)
mapLeft f = map f (x ↦ x)

mapRight : let _ = A in (B₁ → B₂) → (A ⨯ B₁) → (A ⨯ B₂)
mapRight f = map (x ↦ x) f

associateLeft : (A ⨯ (B ⨯ C)) → ((A ⨯ B) ⨯ C)
associateLeft (x , (y , z)) = ((x , y) , z)

associateRight : ((A ⨯ B) ⨯ C) → (A ⨯ (B ⨯ C))
associateRight ((x , y) , z) = (x , (y , z))

-- Swaps the left and right elements of a 2-tuple
swap : (A ⨯ B) → (B ⨯ A)
swap(x , y) = (y , x)

repeat : A → (A ⨯ A)
repeat x = (x , x)


text:
------------------------------------------------------------------------
-- Experiments with Pure Type Systems (PTS)
------------------------------------------------------------------------

-- Author: Sandro Stucki
-- Copyright (c) 2015 EPFL

-- The code in this directory contains a (partial) Agda formalization
-- of Pure Type Systems (PTS).
--
-- The code makes heavy use of the Agda standard library, which is
-- freely available from
--
--   https://github.com/agda/agda-stdlib/
--
-- The code has been tested using Agda 2.5.3 and version 0.14 of the
-- Agda standard library.

module README where

------------------------------------------------------------------------
-- Modules related to pure type systems (PTS)

-- Syntax of (untyped) terms along with support for substitutions.
open import Pts.Syntax

-- Variants of β-reduction/equivalence and properties thereof.
open import Pts.Reduction.Cbv
open import Pts.Reduction.Full
open import Pts.Reduction.Parallel

-- Typing of terms, substitution lemmas and a proofs of type soundess
-- (preservation/subject reduction and progress).
open import Pts.Core
open import Pts.Typing
open import Pts.Typing.Progress

------------------------------------------------------------------------
-- Modules containing generic functionality

-- Extra lemmas that are derivable in the substitution framework of
-- the Agda standard library, as well as support for substitutions
-- lifted to relations and typed substitutions.
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Fin.Substitution.Relation
open import Data.Fin.Substitution.Typed

-- Symmetric and equivalence closures of binary relations.
open import Relation.Binary.SymmetricClosure
open import Relation.Binary.EquivalenceClosure

-- Support for generic reduction relations.
open import Relation.Binary.Reduction

max_stars_repo_name: asr/pts-agda

max_issues_repo_name: asr/pts-agda

max_forks_repo_name: asr/pts-agda


text:
-- {-# OPTIONS -v tc.meta:50 #-}
-- Andreas 2012-03-27, record pattern unification
module Issue376 where

import Common.Level
open import Common.Equality
open import Common.Irrelevance

record Sigma (A : Set)(B : A -> Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst
open Sigma public

record Unit : Set where
  constructor unit

bla1 : (A : Set) (a : A) ->
  let X : Unit -> A
      X = _
  in  X unit ≡ a
bla1 A a = refl

bla2 : (A : Set)(B : A -> Set) ->
  let X : Sigma A B -> Sigma A B
      X = _
  in  (x : A)(y : B x) -> X (x , y) ≡ (x , y)
bla2 A B x y = refl
-- _55 A B (x , y) := (x , y)

-- irrelevant records
bla3 : (A : Set)(B : A -> Set) ->
  let X : .(z : Sigma A B) -> (C : .(Sigma A B) -> Set) -> (.(z : Sigma A B) -> C z) -> C z
      X = _
  in  (x : A)(y : B x)(C : .(Sigma A B) -> Set)(k : .(z : Sigma A B) -> C z) ->
      X (x , y) C k ≡ k (x , y)
bla3 A B x y C k = refl

-- nested irrelevance
bla4 : (A : Set) ->
  let A' = Squash (Squash A) in
  let X : .(z : A') -> (C : .A' -> Set) -> (.(z : A') -> C z) -> C z
      X = _
  in  (a : A)(C : .A' -> Set)(k : .(z : A') -> C z) ->
      X (squash (squash a)) C k ≡ k (squash (squash a))
bla4 A a C k = refl

-- projected bound var
bla5 : (A : Set) (B : A -> Set) ->
  let X : (x : A) (y : B x) -> Sigma A B
      X = _
  in  (z : Sigma A B) -> X (fst z) (snd z) ≡ z
bla5 A B z = refl

-- projected bound var
bla6 : (A : Set) (B : A -> Set) ->
  let X : A -> A
      X = _
  in  (z : Sigma A B) -> X (fst z) ≡ fst z
bla6 A B z = refl

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Structures.Group where

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

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

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

private
  variable
    ℓ ℓ' : Level

raw-group-structure : Type ℓ → Type ℓ
raw-group-structure = raw-semigroup-structure

raw-group-is-SNS : SNS {ℓ} raw-group-structure _
raw-group-is-SNS = raw-semigroup-is-SNS

-- The neutral element and the inverse function will be derived from the
-- axioms, instead of being defined in the raw-group-structure in order
-- to have that isomorphisms between groups are equivalences that preserves
-- multiplication (so we don't have to show that they also preserve inversion
-- and neutral element, although they will preserve them).

group-axioms : (G : Type ℓ) → raw-group-structure G → Type ℓ
group-axioms G _·_ = i × ii

  where
  i = semigroup-axioms G _·_

  ii = Σ[ e ∈ G ] ((x : G) → (x · e ≡ x) × (e · x ≡ x)) ×
                  ((x : G) → Σ[ x' ∈ G ] (x · x' ≡ e) × (x' · x ≡ e))

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

Group : Type (ℓ-suc ℓ)
Group {ℓ} = TypeWithStr ℓ group-structure

-- Extracting components of a group
⟨_⟩ : Group {ℓ} → Type ℓ
⟨ G , _ ⟩ = G

group-operation : (G : Group {ℓ}) → ⟨ G ⟩ → ⟨ G ⟩ → ⟨ G ⟩
group-operation (_ , f , _) = f

module group-operation-syntax where

  group-operation-syntax : (G : Group {ℓ}) → ⟨ G ⟩ → ⟨ G ⟩ → ⟨ G ⟩
  group-operation-syntax = group-operation
  infixr 20 group-operation-syntax
  syntax group-operation-syntax G x y = x ·⟨ G ⟩ y

open group-operation-syntax

group-is-set : (G : Group {ℓ}) → isSet ⟨ G ⟩
group-is-set (_ , _ , (P , _) , _) = P

group-assoc : (G : Group {ℓ})
            → (x y z : ⟨ G ⟩) → (x ·⟨ G ⟩ (y ·⟨ G ⟩ z)) ≡ ((x ·⟨ G ⟩ y) ·⟨ G ⟩ z)
group-assoc (_ , _ , (_ , P) , _) = P

-- Defining identity

group-id : (G : Group {ℓ}) → ⟨ G ⟩
group-id (_ , _ , _ , P) = fst P

group-rid : (G : Group {ℓ})
          → (x : ⟨ G ⟩) → x ·⟨ G ⟩ (group-id G) ≡ x
group-rid (_ , _ , _ , P) x = fst ((fst (snd P)) x)

group-lid : (G : Group {ℓ})
          → (x : ⟨ G ⟩) → (group-id G) ·⟨ G ⟩ x ≡ x
group-lid (_ , _ , _ , P) x = snd ((fst (snd P)) x)

-- Defining the inverse function
group-inv : (G : Group {ℓ}) → ⟨ G ⟩ → ⟨ G ⟩
group-inv (_ , _ , _ , P) x = fst ((snd (snd P)) x)

group-rinv : (G : Group {ℓ})
               → (x : ⟨ G ⟩) → x ·⟨ G ⟩ (group-inv G x) ≡ group-id G
group-rinv (_ , _ , _ , P) x = fst (snd ((snd (snd P)) x))

group-linv : (G : Group {ℓ})
               → (x : ⟨ G ⟩) → (group-inv G x) ·⟨ G ⟩ x ≡ group-id G
group-linv (_ , _ , _ , P) x = snd (snd ((snd (snd P)) x))

-- Iso for groups are those for monoids
group-iso : StrIso group-structure ℓ
group-iso = add-to-iso (nAryFunIso 2) group-axioms

-- Group axioms isProp

group-axioms-isProp : (X : Type ℓ)
                    → (s : raw-group-structure X)
                    → isProp (group-axioms X s)
group-axioms-isProp X s t = η t
  where
  𝒢 : Group
  𝒢 = X , s , t

  is-identity : X → Type _
  is-identity e = (x : X) → (x ·⟨ 𝒢 ⟩ e ≡ x) × (e ·⟨ 𝒢 ⟩ x ≡ x)

  α : (e : X) → isProp (is-identity e)
  α e = isPropΠ (λ _ → isPropΣ (group-is-set 𝒢 _ _) (λ _ → group-is-set 𝒢 _ _))

  β : (e : X) → is-identity e → isProp ((x : X) → Σ[ x' ∈ X ] (x ·⟨ 𝒢 ⟩ x' ≡ e) × (x' ·⟨ 𝒢 ⟩ x ≡ e))
  β e is-identity-e =
   isPropΠ λ { x (x' , _ , P) (x'' , Q , _) → ΣProp≡ (λ _ → isPropΣ (group-is-set 𝒢 _ _) λ _ → group-is-set 𝒢 _ _)
                                                      (inv-lemma ℳ x x' x'' P Q) }
   where
    ℳ : Monoid
    ℳ = ⟨ 𝒢 ⟩ , (e , group-operation 𝒢) ,
        group-is-set 𝒢 ,
        group-assoc 𝒢 ,
        (λ x → fst (is-identity-e x)) ,
        (λ x → snd (is-identity-e x))

  γ : isProp (Σ[ e ∈ X ] ((x : X) → (x ·⟨ 𝒢 ⟩ e ≡ x) × (e ·⟨ 𝒢 ⟩ x ≡ x)) ×
                         ((x : X) → Σ[ x' ∈ X ] (x ·⟨ 𝒢 ⟩ x' ≡ e) × (x' ·⟨ 𝒢 ⟩ x ≡ e)))
  γ (e , P , _) (e' , Q , _) = ΣProp≡ (λ e → isPropΣ (α e) λ is-identity-e → β e is-identity-e)
                                      (e          ≡⟨ sym (fst (Q e)) ⟩
                                      e ·⟨ 𝒢 ⟩ e' ≡⟨ snd (P e') ⟩
                                      e' ∎)

  η : isProp (group-axioms X s)
  η = isPropΣ (semigroup-axiom-isProp X s) λ _ → γ

-- Group paths equivalent to equality
group-is-SNS : SNS {ℓ} group-structure group-iso
group-is-SNS = add-axioms-SNS _ group-axioms-isProp (nAryFunSNS 2)

GroupPath : (M N : Group {ℓ}) → (M ≃[ group-iso ] N) ≃ (M ≡ N)
GroupPath = SIP group-is-SNS

-- Group ·syntax

module group-·syntax (G : Group {ℓ}) where

  infixr 18 _·_

  _·_ : ⟨ G ⟩ → ⟨ G ⟩ → ⟨ G ⟩
  _·_ = group-operation G

  ₁ : ⟨ G ⟩
  ₁ = group-id G

  infix 19 _⁻¹

  _⁻¹ : ⟨ G ⟩ → ⟨ G ⟩
  _⁻¹ = group-inv G