text:
module DualTail where

open import Data.Nat
open import Data.Fin using (Fin; zero; suc)
open import Data.Product

open import Function using (id; _∘_)

open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import Types.Direction
open import Types.Tail

private
  variable
    n : ℕ

-- instead of unrolling and substituting, we maintain a stack of bodies of recursive types

data Stack : ℕ → Set where
  ε : Stack 0
  ⟪_,_⟫ : Stack n → GType (suc n) → Stack (suc n)

-- the dual of a stack

dual-stack : Stack n → Stack n
dual-stack ε = ε
dual-stack ⟪ σ , g ⟫ = ⟪ dual-stack σ , dualG g ⟫

-- obtain an entry from the stack
-- technically m = n - i, but we don't need to know

get : (i : Fin n) → Stack n → Σ ℕ λ m → Stack m × GType (suc m)
get zero ⟪ σ , x ⟫ = _ , (σ , x)
get (suc i) ⟪ σ , x ⟫ = get i σ

-- relate a stack entry to the corresponding entry on the dual stack

get-dual-stack : (x : Fin n) (σ : Stack n) →
  get x (dual-stack σ) ≡ map id (map dual-stack dualG) (get x σ)
get-dual-stack zero ⟪ σ , x ⟫ = refl
get-dual-stack (suc x) ⟪ σ , x₁ ⟫ = get-dual-stack x σ

-- mapping tail recursive session types to coinductive session types
-- relies on a stack to unfold variables on the fly

import Types.COI as COI

tail2coiT : Type → COI.Type
tail2coiS : Stack n → SType n → COI.SType
tail2coiG : Stack n → GType n → COI.STypeF COI.SType

tail2coiT TUnit = COI.TUnit
tail2coiT TInt = COI.TInt
tail2coiT (TPair t t₁) = COI.TPair (tail2coiT t) (tail2coiT t₁)
tail2coiT (TChan s) = COI.TChan (tail2coiS ε s)

COI.SType.force (tail2coiS σ (gdd g)) = tail2coiG σ g
COI.SType.force (tail2coiS σ (rec g)) = tail2coiG ⟪ σ , g ⟫ g
COI.SType.force (tail2coiS σ (var x))
  with get x σ
... | m , σ' , gxs = tail2coiG ⟪ σ' , gxs ⟫ gxs

tail2coiG σ (transmit d t s) = COI.transmit d (tail2coiT t) (tail2coiS σ s)
tail2coiG σ (choice d m alt) = COI.choice d m (tail2coiS σ ∘ alt)
tail2coiG σ end = COI.end

-- get coinductive bisimulation in scope

_≈_ = COI._≈_
_≈'_ = COI._≈'_

-- main proposition

dual-tailS : (σ : Stack n) (s : SType n) →
  COI.dual (tail2coiS σ s) ≈ tail2coiS (dual-stack σ) (dualS s)
dual-tailG : (σ : Stack n) (g : GType n) →
  COI.dualF (tail2coiG σ g) ≈' tail2coiG (dual-stack σ) (dualG g)

COI.Equiv.force (dual-tailS σ (gdd g)) = dual-tailG σ g
COI.Equiv.force (dual-tailS σ (rec g)) = dual-tailG ⟪ σ , g ⟫ g
COI.Equiv.force (dual-tailS σ (var x))
  rewrite get-dual-stack x σ
  with get x σ
... | m , σ' , g = dual-tailG ⟪ σ' , g ⟫ g

dual-tailG σ (transmit d t s) = COI.eq-transmit (dual-dir d) COI.≈ᵗ-refl (dual-tailS σ s)
dual-tailG σ (choice d m alt) = COI.eq-choice (dual-dir d) (dual-tailS σ ∘ alt)
dual-tailG σ end = COI.eq-end

-- corrolary for SType 0

dual-tail : ∀ s → COI.dual (tail2coiS ε s) ≈ tail2coiS ε (dualS s)
dual-tail = dual-tailS ε

max_stars_repo_name: peterthiemann/dual-session

max_issues_repo_name: peterthiemann/dual-session

max_forks_repo_name: peterthiemann/dual-session


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Terms that operate on changes (Fig. 3).
------------------------------------------------------------------------

import Parametric.Syntax.Type as Type
import Parametric.Syntax.Term as Term
import Parametric.Change.Type as ChangeType

module Parametric.Change.Term
    {Base : Set}
    (Const : Term.Structure Base)
    (ΔBase : ChangeType.Structure Base)
  where

-- Terms that operate on changes

open Type.Structure Base
open Term.Structure Base Const
open ChangeType.Structure Base ΔBase

open import Data.Product

-- Extension point 1: A term for ⊝ on base types.
DiffStructure : Set
DiffStructure = ∀ {ι Γ} → Term Γ (base ι ⇒ base ι ⇒ ΔBase ι)

-- Extension point 2: A term for ⊕ on base types.
ApplyStructure : Set
ApplyStructure = ∀ {ι Γ} → Term Γ (ΔType (base ι) ⇒ base ι ⇒ base ι)

-- Extension point 3: A term for 0 on base types.
NilStructure : Set
NilStructure = ∀ {ι Γ} → Term Γ (base ι ⇒ ΔBase ι)

module Structure
    (apply-base : ApplyStructure)
    (diff-base  : DiffStructure)
    (nil-base   : NilStructure)
  where

  -- g ⊝ f  = λ x . λ Δx . g (x ⊕ Δx) ⊝ f x
  -- f ⊕ Δf = λ x . f x ⊕ Δf x (x ⊝ x)

  -- We provide: terms for ⊕ and ⊝ on arbitrary types.
  apply-term : ∀ {τ Γ} → Term Γ (ΔType τ ⇒ τ ⇒ τ)
  diff-term : ∀ {τ Γ} → Term Γ (τ ⇒ τ ⇒ ΔType τ)
  nil-term : ∀ {τ Γ} → Term Γ (τ ⇒ ΔType τ)

  apply-term {base ι} = apply-base
  apply-term {σ ⇒ τ} =
    let
       _⊕τ_ = λ {Γ} t Δt → app₂ (apply-term {τ} {Γ}) Δt t
       nil-σ = λ {Γ} t → app (nil-term {σ} {Γ}) t
     in
       absV 3 (λ Δh h y → app h y ⊕τ app (app Δh y) (nil-σ y))

  diff-term {base ι} = diff-base
  diff-term {σ ⇒ τ} =
    let
       _⊝τ_ = λ {Γ} s t  → app₂ (diff-term {τ} {Γ}) s t
       _⊕σ_ = λ {Γ} t Δt → app₂ (apply-term {σ} {Γ}) Δt t
     in
       absV 4 (λ g f x Δx → app g (x ⊕σ Δx) ⊝τ app f x)

  nil-term {base ι} = nil-base
  nil-term {σ ⇒ τ} =
    -- What I'd usually write:
    --absV 1 (λ f → app₂ diff-term f f)
    -- What I wrote in fact:
    let
       _⊝τ_ = λ {Γ} s t  → app₂ (diff-term {τ} {Γ}) s t
       _⊕σ_ = λ {Γ} t Δt → app₂ (apply-term {σ} {Γ}) Δt t
     in
       absV 1 (λ ff → app (absV 3 (λ f x Δx → app f (x ⊕σ Δx) ⊝τ app f x)) ff)
    -- This simplified a lot proving meaning-onil by reusing meaning-⊝.
    --
    -- The reason is that the extra lambda-abstraction ensures that f is pushed
    -- twice in the environment.

  apply : ∀ τ {Γ} →
    Term Γ (ΔType τ) → Term Γ τ →
    Term Γ τ
  apply _ = app₂ apply-term

  diff : ∀ τ {Γ} →
    Term Γ τ → Term Γ τ →
    Term Γ (ΔType τ)
  diff _ = app₂ diff-term

  onil₍_₎ : ∀ τ {Γ} →
    Term Γ τ →
    Term Γ (ΔType τ)
  onil₍ _ ₎ = app nil-term

  infixl 6 apply diff

  syntax apply τ x Δx = Δx ⊕₍ τ ₎ x
  syntax diff τ x y = x ⊝₍ τ ₎ y

  infixl 6 _⊕_ _⊝_

  _⊕_ : ∀ {τ Γ} →
    Term Γ (ΔType τ) → Term Γ τ →
    Term Γ τ
  _⊕_ {τ} = apply τ

  _⊝_ : ∀ {τ Γ} →
    Term Γ τ → Term Γ τ →
    Term Γ (ΔType τ)
  _⊝_ {τ} = diff τ

  onil : ∀ {τ Γ} →
    Term Γ τ →
    Term Γ (ΔType τ)
  onil {τ} = onil₍ τ ₎

ext: agda

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

module Data.List.Sugar where

open import Data.List.Base
open import Prelude

[_] : A → List A
[ x ] = x ∷ []

pure : A → List A
pure = [_]

_>>=_ : List A → (A → List B) → List B
_>>=_ = flip concatMap

_>>_ : List A → List B → List B
xs >> ys = xs >>= const ys

_<*>_ : List (A → B) → List A → List B
fs <*> xs = do
  f ← fs
  x ← xs
  [ f x ]

guard : Bool → List ⊤
guard false = []
guard true  = [ tt ]

liftA2 : (A → B → C) → List A → List B → List C
liftA2 {A = A} {B = B} {C = C} f xs ys = go xs
  where
  go′ : A → List A → List B → List C
  go : List A → List C

  go′ x xs [] = go xs
  go′ x xs (y ∷ ys) = f x y ∷ go′ x xs ys

  go [] = []
  go (x ∷ xs) = go′ x xs ys

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module DCBSets where

open import prelude
open import relations

-- The objects:
Obj : Set₁
Obj = Σ[ U ∈ Set ] (Σ[ X ∈ Set ] (Σ[ x ∈ (⊤ → X) ] (Σ[ d ∈ (X × X → X) ](Σ[ α ∈ (U → X → Set) ](
  (∀{u : U}{x₁ x₂ : X} → α u (d (x₁ , x₂)) → ((α u x₁) × (α u x₂))) ×
  ( ∀{Y : Set}{x' : X}{F : Y → X}{y : ⊤ → Y} → d (x' , F (y triv)) ≡ x' ) ×
  ( ∀{Y : Set}{x' : X}{F : Y → X}{y : ⊤ → Y} → d (F (y triv) , x') ≡ x'  ))))))

-- The morphisms:
Hom : Obj → Obj → Set
Hom (U , X , x , d₁ , α , p₁ ) (V , Y , y , d₂ , β , p₂) =
  Σ[ f ∈ (U → V) ]
    (Σ[ F ∈ (U → Y → X) ] ((∀{u : U}{y : Y} → α u (F u y) → β (f u) y)))

-- Composition:
comp : {A B C : Obj} → Hom A B → Hom B C → Hom A C
comp {(U , X , x , d₁ , α , dec₁ , p₁ , p₂)} {(V , Y , y , d₂ , β , dec₂ , p₃ , p₄)} {(W , Z , z , d₃ , γ , dec₃ , p₅ , p₆)} (f , F , q₁) (g , G , q₂) =
  g ∘ f , (((λ u z' → F u (G (f u) z')))  ) , (λ {u} {z'} r → q₂ (q₁ r))

infixl 5 _○_

_○_ = comp

-- The contravariant hom-functor:
Homₐ :  {A' A B B' : Obj} → Hom A' A → Hom B B' → Hom A B → Hom A' B'
Homₐ f h g = comp f (comp g h)

-- The identity function:
id : {A : Obj} → Hom A A
id {(U , V , n , d , α , p)} = (id-set , curry snd , id-set)

-- In this formalization we will only worry about proving that the
-- data of morphisms are equivalent, and not worry about the morphism
-- conditions.  This will make proofs shorter and faster.
--
-- If we have parallel morphisms (f,F) and (g,G) in which we know that
-- f = g and F = G, then the condition for (f,F) will imply the
-- condition of (g,G) and vice versa.  Thus, we can safely ignore it.
infix 4 _≡h_

_≡h_ : {A B : Obj} → (f g : Hom A B) → Set
_≡h_ {(U , X , _ , _ , _ , _ , _ , _)}{(V , Y , _ , β , _ , _ , _ , _)} (f , F , p₁) (g , G , p₂) = f ≡ g × F ≡ G

≡h-refl : {A B : Obj}{f : Hom A B} → f ≡h f
≡h-refl {U , X , _ , α , _ , _ , _ , _}{V , Y , _ , β , _ , _ , _ , _}{f , F , _} = refl , refl

≡h-trans : ∀{A B}{f g h : Hom A B} → f ≡h g → g ≡h h → f ≡h h
≡h-trans {U , X , _ , α , _ , _ , _ , _}{V , Y , _ , β , _ , _ , _ , _}{f , F , _}{g , G , _}{h , H , _} (p₁ , p₂) (p₃ , p₄) rewrite p₁ | p₂ | p₃ | p₄ = refl , refl

≡h-sym : ∀{A B}{f g : Hom A B} → f ≡h g → g ≡h f
≡h-sym {U , X , _ , α , _ , _ , _ , _}{V , Y , _ , β , _ , _ , _ , _}{f , F , _}{g , G , _} (p₁ , p₂) rewrite p₁ | p₂ = refl , refl

≡h-subst-○ : ∀{A B C}{f₁ f₂ : Hom A B}{g₁ g₂ : Hom B C}{j : Hom A C}
  → f₁ ≡h f₂
  → g₁ ≡h g₂
  → f₂ ○ g₂ ≡h j
  → f₁ ○ g₁ ≡h j
≡h-subst-○ {U , X , _ , α , _ , _ , _ , _}
         {V , Y , _ , β , _ , _ , _ , _}
         {W , Z , _ , γ , _ , _ , _ , _}
         {f₁ , F₁ , _}
         {f₂ , F₂ , _}
         {g₁ , G₁ , _}
         {g₂ , G₂ , _}
         {j , J , _}
         (p₅ , p₆) (p₇ , p₈) (p₉ , p₁₀) rewrite p₅ | p₆ | p₇ | p₈ | p₉ | p₁₀ = refl , refl

○-assoc : ∀{A B C D}{f : Hom A B}{g : Hom B C}{h : Hom C D}
  → f ○ (g ○ h) ≡h (f ○ g) ○ h
○-assoc {U , X , _ , α , _ , _ , _ , _}{V , Y , _ , β , _ , _ , _ , _}{W , Z , _ , γ , _ , _ , _ , _}{S , T , _ , ι , _ , _ , _ , _}
        {f , F , _}{g , G , _}{h , H , _} = refl , refl

○-idl : ∀{A B}{f : Hom A B} → id ○ f ≡h f
○-idl {U , X , _ , _ , _ , _ , _ , _}{V , Y , _ , _ , _ , _ , _ , _}{f , F , _} = refl , refl

○-idr : ∀{A B}{f : Hom A B} → f ○ id ≡h f
○-idr {U , X , _ , _ , _ , _ , _ , _}{V , Y , _ , _ , _ , _ , _ , _}{f , F , _} = refl , refl

-- The tensor functor: ⊗
_⊗ᵣ_ : ∀{U X V Y : Set} → (U → X → Set) → (V → Y → Set) → ((U × V) → (X × Y) → Set)
_⊗ᵣ_ α β (u , v) (x , y) = (α u x) × (β v y)

_⊗ₒ_ : (A B : Obj) → Obj
(U , X , n₁ , d₁ , α , pr₁ , q₁ , q₂ ) ⊗ₒ (V , Y , n₂ , d₂ , β , pr₂ , q₃ , q₄) = ((U × V) , (X × Y) , trans-× n₁ n₂ ,  d⊗ , (α ⊗ᵣ β) , pr⊗ , ((λ {Y x' F y} → q₁⊗ {Y} {x'}{F}{y}) , (λ {Y x' F y} → q₂⊗ {Y} {x'}{F}{y})))
 where
   d⊗ : Σ (Σ X (λ x → Y)) (λ x → Σ X (λ x₁ → Y)) → Σ X (λ x → Y)
   d⊗ ((x , y) , (x' , y')) = d₁ (x , x') , d₂ (y , y')

   pr⊗ : {u : Σ U (λ x → V)} {x₁ x₂ : Σ X (λ x → Y)} → (α ⊗ᵣ β) u (d⊗ (x₁ , x₂)) → Σ ((α ⊗ᵣ β) u x₁) (λ x → (α ⊗ᵣ β) u x₂)
   pr⊗ {u , v}{x , y}{x' , y'} (p , p') = (fst (pr₁ p) , fst (pr₂ p')) , snd (pr₁ p) , snd (pr₂ p')

   q₁⊗ : {Y₁ : Set} {x' : Σ X (λ x → Y)} {F : Y₁ → Σ X (λ x → Y)}{y : ⊤ → Y₁} → d⊗ (x' , F (y triv)) ≡ x'
   q₁⊗ {_}{x , y}{F}{p} with q₁ {x' = x}{fst ∘ F}{p} | q₃ {x' = y}{snd ∘ F}{p}
   ... | q'₁ | q'₂ with F (p triv)
   ... | x' , y'  rewrite q'₁ | q'₂ = refl

   q₂⊗ : {Y₁ : Set} {x' : Σ X (λ x → Y)} {F : Y₁ → Σ X (λ x → Y)}{y : ⊤ → Y₁} → d⊗ (F (y triv) , x') ≡ x'
   q₂⊗ {Y}{x , y}{F}{p} with q₂ {_}{x}{fst ∘ F}{p} | q₄ {_}{y}{snd ∘ F}{p}
   ... | q'₁ | q'₂ with F (p triv)
   ... | x' , y' rewrite q'₁ | q'₂ = refl

F⊗ : ∀{Z T V X U Y : Set}{F : U → Z → X}{G : V → T → Y} → (U × V) → (Z × T) → (X × Y)
F⊗ {F = F}{G} (u , v) (z , t) = F u z , G v t

_⊗ₐ_ : {A B C D : Obj} → Hom A C → Hom B D → Hom (A ⊗ₒ B) (C ⊗ₒ D)
_⊗ₐ_ {(U , X , _ , _ , α , _ , _ , _)}{(V , Y , _ , _ , β , _ , _ , _)}{(W , Z , _ , _ , γ , _ , _ , _)}{(S , T , _ , _ , δ , _ , _ , _)} (f , F , p₁) (g , G , p₂) = ⟨ f , g ⟩ , F⊗ {F = F}{G} , p⊗
 where
  p⊗ : {u : Σ U (λ x → V)} {y : Σ Z (λ x → T)} → (α ⊗ᵣ β) u (F⊗ {F = F}{G} u y) → (γ ⊗ᵣ δ) (⟨ f , g ⟩ u) y
  p⊗ {u , v}{z , t} (p₃ , p₄) = p₁  p₃ , p₂ p₄

π₁ : {A B : Obj} → Hom (A ⊗ₒ B) A
π₁ {U , X , n₁ , _ , α , _ , _ , _}{V , Y , n₂ , _ , β , _ , _ , _} = fst , (λ r x → x , n₂ triv) , cond
 where
   cond : {u : Σ U (λ x → V)} {y : X} → (α ⊗ᵣ β) u (y , n₂ triv) → α (fst u) y
   cond {u , v}{x} (p₁ , p₂) = p₁

π₂ : {A B : Obj} → Hom (A ⊗ₒ B) B
π₂ {U , X , n₁ , _ , α , _ , _ , _}{V , Y , n₂ , _ , β , _ , _ , _} = snd , (λ r y → n₁ triv , y) , cond
 where
  cond : {u : Σ U (λ x → V)} {y : Y} → (α ⊗ᵣ β) u (n₁ triv , y) → β (snd u) y
  cond {u , v}{y} (p₁ , p₂) = p₂

cart-ar : {A B C : Obj}
  → (f : Hom C A)
  → (g : Hom C B)
  → Hom C (A ⊗ₒ B)
cart-ar {U , X , x , d₁ , α , pr₁ , q₁ , q₂}{V , Y , y ,  d₂ , β , pr₂ , q₃ , q₄}{W , Z , z , d₃ , γ , pr₃ , q₅ , q₆} (f , F , p₁) (g , G , p₂) = trans-× f g ,  crt , cond
 where
  crt : W → Σ X (λ x₁ → Y) → Z
  crt w (x' , y') = d₃ ((F w x') , (G w y'))

  cond : {u : W} {y₁ : Σ X (λ x₁ → Y)} → γ u (crt u y₁) → (α ⊗ᵣ β) (f u , g u) y₁
  cond {w}{x' , y'} p = p₁ (fst (pr₃ {w}{F w x'}{G w y'} p)) , p₂ (snd (pr₃ {w}{F w x'}{G w y'} p))

cart-diag₁ : ∀{A B C : Obj}
  → {f : Hom C A}
  → {g : Hom C B}
  → (cart-ar f g) ○ π₁ ≡h f
cart-diag₁ {U , X , x , d₁ , α , pr₁ , q₁ , q₂}{V , Y , y , d₂ , β , q₃ , q₄ , q₅}{W , Z , z , d₃ , γ , q₆ , q₇ , q₈}{f , F , p₁}{g , G , p₂} = refl , ext-set (λ {w} → ext-set (λ {x} → q₇ {x' = F w x}{G w}{y}))

cart-diag₂ : ∀{A B C : Obj}
  → {f : Hom C A}
  → {g : Hom C B}
  → (cart-ar f g) ○ π₂ ≡h g
cart-diag₂ {U , X , x , d₁ , α , pr₁ , q₁ , q₂}{V , Y , y , d₂ , β , q₃ , q₄ , q₅}{W , Z , z , d₃ , γ , q₆ , q₇ , q₈}{f , F , p₁}{g , G , p₂} = refl , ext-set (λ {w} → ext-set (λ {y₁} → q₈ {x' = G w y₁}{F w}{x}))

-- The □-comonad:

□ₒ-cond : ∀{U X : Set} → (α : U → X → Set) → U → 𝕃 X → Set
□ₒ-cond {U}{X} α u [] = ⊤
□ₒ-cond {U}{X} α u (x :: xs) = (α u x) × (□ₒ-cond α u xs)

□ₒ-cond-++ : ∀{U X : Set}{α : U → X → Set}{u : U}{l₁ l₂ : 𝕃 X}
  → □ₒ-cond α u (l₁ ++ l₂) ≡ ((□ₒ-cond α u l₁) × (□ₒ-cond α u l₂))
□ₒ-cond-++ {U}{X}{α}{u}{[]}{l₂} = ∧-unit
□ₒ-cond-++ {U}{X}{α}{u}{x :: xs}{l₂} rewrite □ₒ-cond-++ {U}{X}{α}{u}{xs}{l₂} = ∧-assoc

□ₒ : Obj → Obj
□ₒ (U , X , x , d , α , pr , q₁ , q₂) = U ,  X * , (λ t → [ x t ]) , □d , □ₒ-cond {U}{X} α , {!!} , {!!} , {!!}
 where

  □d : (X *) × (X *) → X *
  □d (l₁ , l₂) = l₁ ++ l₂

  -- □pr : {u : U} {x₁ x₂ : 𝕃 X}
  --       → □ₒ-cond α u (□d (x₁ , x₂))
  --       → Σ (□ₒ-cond α u x₁) (λ x₃ → □ₒ-cond α u x₂)
  -- □pr {_}{[]} {[]} x₁ = triv , triv
  -- □pr {u}{x₁ = []} {x₁ :: x₂} (a , b) = triv , snd (pr a) , snd (□pr {u}{[]}{x₂} b)
  -- □pr {u}{x₁ = x₁ :: x₂} {[]} (a , b) = (fst (pr a) , fst (□pr {u}{x₂}{[]} b)) , triv
  -- □pr {_}{x₁ :: x₂} {x₃ :: x₄} (a , b) with pr a
  -- ... | c , e with □pr {x₁ = x₂} b
  -- ... | f , g = (c , f) , (e , g)

  □q₁ : {Y : Set} {x' : 𝕃 X} {F : Y → 𝕃 X} {y : ⊤ → Y} → □d (x' , F (y triv)) ≡ x'
  □q₁ {x' = []}{F}{y} = {!!}
  □q₁ {x' = x₁ :: x'}{F}{y} with F (y triv)
  ... | [] = {!!}
  ... | a :: as = {!!}

{-
□ₐ-s : ∀{U Y X : Set}
  → (U → Y → X)
  → (U → Y * → X *)
□ₐ-s f u l = map (f u) l

□ₐ : {A B : Obj} → Hom A B → Hom (□ₒ A) (□ₒ B)
□ₐ {U , X , α}{V , Y , β} (f , F , p) = f , (□ₐ-s F , aux)
 where
   aux : {u : U} {y : 𝕃 Y} → □ₒ-cond α u (□ₐ-s F u y) → □ₒ-cond β (f u) y
   aux {u}{[]} p₁ = triv
   aux {u}{y :: ys} (p₁ , p₂) = p p₁ , aux p₂

-- Of-course is a comonad:
ε : ∀{A} → Hom (□ₒ A) A
ε {U , X , α} = id-set , (λ u x → [ x ]) , fst

δ-s : {U X : Set} → U → 𝕃 (𝕃 X) → 𝕃 X
δ-s u xs = foldr _++_ [] xs

δ : ∀{A} → Hom (□ₒ A) (□ₒ (□ₒ A))
δ {U , X , α} = id-set , δ-s , cond
 where
   cond : {u : U} {y : 𝕃 (𝕃 X)} → □ₒ-cond α u (foldr _++_ [] y) → □ₒ-cond (□ₒ-cond α) u y
   cond {u}{[]} p = triv
   cond {u}{l :: ls} p with □ₒ-cond-++ {U}{X}{α}{u}{l}{foldr _++_ [] ls}
   ... | p' rewrite p' with p
   ... | p₂ , p₃ = p₂ , cond {u}{ls} p₃

comonand-diag₁ : ∀{A}
  → (δ {A}) ○ (□ₐ (δ {A})) ≡h (δ {A}) ○ (δ { □ₒ A})
comonand-diag₁ {U , X , α} = refl , ext-set (λ {x} → ext-set (λ {l} → aux {x} {l}))
 where
  aux : ∀{x : U}{l : 𝕃 (𝕃 (𝕃 X))}
    → foldr _++_ [] (□ₐ-s (λ u xs
    → foldr _++_ [] xs) x l) ≡ foldr _++_ [] (foldr _++_ [] l)
  aux {u}{[]} = refl
  aux {u}{x :: xs} rewrite aux {u}{xs} = foldr-append {_}{_}{X}{X}{x}{foldr _++_ [] xs}

comonand-diag₂ : ∀{A}
  → (δ {A}) ○ (ε { □ₒ A}) ≡h (δ {A}) ○ (□ₐ (ε {A}))
comonand-diag₂ {U , X , α} =
  refl , ext-set (λ {u} → ext-set (λ {l} → aux {l}))
  where
    aux : ∀{a : 𝕃 X} → a ++ [] ≡ foldr _++_ [] (map (λ x → x :: []) a)
    aux {[]} = refl
    aux {x :: xs} rewrite (++[] xs) | sym (foldr-map {_}{X}{xs}) = refl

-}

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Properties.Semilattice {c ℓ} (L : Semilattice c ℓ) where

open Semilattice L

open import Algebra.Structures
open import Function
open import Data.Product
open import Relation.Binary
open import Relation.Binary.Reasoning.Setoid setoid
import Relation.Binary.Construct.NaturalOrder.Left _≈_ _∧_ as LeftNaturalOrder
open import Relation.Binary.Lattice
import Relation.Binary.Properties.Poset as PosetProperties
open import Relation.Binary.Reasoning.Setoid setoid

------------------------------------------------------------------------
-- Every semilattice can be turned into a poset via the left natural
-- order.

poset : Poset c ℓ ℓ
poset = LeftNaturalOrder.poset isSemilattice

open Poset poset using (_≤_; isPartialOrder)
open PosetProperties poset using (_≥_; ≥-isPartialOrder)

------------------------------------------------------------------------
-- Every algebraic semilattice can be turned into an order-theoretic one.

∧-isOrderTheoreticMeetSemilattice : IsMeetSemilattice _≈_ _≤_ _∧_
∧-isOrderTheoreticMeetSemilattice = record
  { isPartialOrder = isPartialOrder
  ; infimum        = LeftNaturalOrder.infimum isSemilattice
  }

∧-isOrderTheoreticJoinSemilattice : IsJoinSemilattice _≈_ _≥_ _∧_
∧-isOrderTheoreticJoinSemilattice = record
  { isPartialOrder = ≥-isPartialOrder
  ; supremum       = IsMeetSemilattice.infimum
                       ∧-isOrderTheoreticMeetSemilattice
  }

∧-orderTheoreticMeetSemilattice : MeetSemilattice c ℓ ℓ
∧-orderTheoreticMeetSemilattice = record
  { isMeetSemilattice = ∧-isOrderTheoreticMeetSemilattice
  }

∧-orderTheoreticJoinSemilattice : JoinSemilattice c ℓ ℓ
∧-orderTheoreticJoinSemilattice = record
  { isJoinSemilattice = ∧-isOrderTheoreticJoinSemilattice
  }

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.1

isOrderTheoreticMeetSemilattice = ∧-isOrderTheoreticMeetSemilattice
{-# WARNING_ON_USAGE isOrderTheoreticMeetSemilattice
"Warning: isOrderTheoreticMeetSemilattice was deprecated in v1.1.
Please use ∧-isOrderTheoreticMeetSemilattice instead."
#-}
isOrderTheoreticJoinSemilattice = ∧-isOrderTheoreticJoinSemilattice
{-# WARNING_ON_USAGE isOrderTheoreticJoinSemilattice
"Warning: isOrderTheoreticJoinSemilattice was deprecated in v1.1.
Please use ∧-isOrderTheoreticJoinSemilattice instead."
#-}
orderTheoreticMeetSemilattice = ∧-orderTheoreticMeetSemilattice
{-# WARNING_ON_USAGE orderTheoreticMeetSemilattice
"Warning: orderTheoreticMeetSemilattice was deprecated in v1.1.
Please use ∧-orderTheoreticMeetSemilattice instead."
#-}
orderTheoreticJoinSemilattice = ∧-orderTheoreticJoinSemilattice
{-# WARNING_ON_USAGE orderTheoreticJoinSemilattice
"Warning: orderTheoreticJoinSemilattice was deprecated in v1.1.
Please use ∧-orderTheoreticJoinSemilattice instead."
#-}


text:
open import Nat
open import Prelude
open import core
open import contexts
open import preservation

module complete-preservation where
  -- if you substitute a complete term into a complete term, the result is
  -- still complete.
  cp-subst : ∀ {x d1 d2} →
           d1 dcomplete →
           d2 dcomplete →
           ([ d2 / x ] d1) dcomplete
  cp-subst {x = y} (DCVar {x = x}) dc2 with natEQ x y
  cp-subst DCVar dc2 | Inl refl = dc2
  cp-subst DCVar dc2 | Inr x₂ = DCVar
  cp-subst DCConst dc2 = DCConst
  cp-subst {x = x} (DCLam {x = y} dc1 x₂) dc2 with natEQ y x
  cp-subst (DCLam dc1 x₃) dc2 | Inl refl = DCLam dc1 x₃
  cp-subst (DCLam dc1 x₃) dc2 | Inr x₂ = DCLam (cp-subst dc1 dc2) x₃
  cp-subst (DCAp dc1 dc2) dc3 = DCAp (cp-subst dc1 dc3) (cp-subst dc2 dc3)
  cp-subst (DCCast dc1 x₁ x₂) dc2 = DCCast (cp-subst dc1 dc2) x₁ x₂

  -- this just lets me pull the particular x out of a derivation; it's not
  -- bound in any of the constructors explicitly since it's only in the
  -- lambda case; so below i have no idea how else to get a name for it,
  -- instead of leaving it dotted in the context
  lem-proj : {x : Nat} {d : ihexp} { τ : htyp} → (·λ_[_]_ x τ d) dcomplete → Σ[ y ∈ Nat ] (y == x)
  lem-proj {x} (DCLam dc x₁) = x , refl

  -- a complete well typed term steps to a complete term.
  cp-rhs : ∀{d τ d' Δ} →
             d dcomplete →
             Δ , ∅ ⊢ d :: τ →
             d ↦ d' →
             d' dcomplete
  cp-rhs dc TAConst (Step FHOuter () FHOuter)
  cp-rhs dc (TAVar x₁) stp = abort (somenotnone (! x₁))
  cp-rhs dc (TALam _ wt) (Step FHOuter () FHOuter)
  -- this case is a little more complicated than it feels like it ought to
  -- be, just from horsing around with agda implicit variables.
  cp-rhs (DCAp dc dc₁) (TAAp wt wt₁) (Step FHOuter ITLam FHOuter) with lem-proj dc
  cp-rhs (DCAp dc dc₁) (TAAp wt wt₁) (Step FHOuter ITLam FHOuter) | x , refl with cp-subst {x = x} dc dc₁
  ... | qq with natEQ x x
  cp-rhs (DCAp dc dc₁) (TAAp wt wt₁) (Step FHOuter ITLam FHOuter) | x , refl | DCLam qq x₁ | Inl refl = cp-subst qq dc₁
  cp-rhs (DCAp dc dc₁) (TAAp wt wt₁) (Step FHOuter ITLam FHOuter) | x , refl | qq | Inr x₁ = abort (x₁ refl)
  cp-rhs (DCAp (DCCast dc (TCArr x x₁) (TCArr x₂ x₃)) dc₁) (TAAp (TACast wt x₄) wt₁) (Step FHOuter ITApCast FHOuter) = DCCast (DCAp dc (DCCast dc₁ x₂ x)) x₁ x₃
  cp-rhs (DCAp dc dc₁) (TAAp wt wt₁) (Step (FHAp1 x) x₁ (FHAp1 x₂)) = DCAp (cp-rhs dc wt (Step x x₁ x₂)) dc₁
  cp-rhs (DCAp dc dc₁) (TAAp wt wt₁) (Step (FHAp2 x) x₁ (FHAp2 x₂)) = DCAp dc (cp-rhs dc₁ wt₁ (Step x x₁ x₂))
  cp-rhs () (TAEHole x x₁) stp
  cp-rhs () (TANEHole x wt x₁) stp
  cp-rhs (DCCast dc x x₁) (TACast wt x₂) (Step FHOuter ITCastID FHOuter) = dc
  cp-rhs (DCCast dc () x₁) (TACast wt x₂) (Step FHOuter (ITCastSucceed x₃) FHOuter)
  cp-rhs (DCCast dc () x₁) (TACast wt x₂) (Step FHOuter (ITCastFail x₃ x₄ x₅) FHOuter)
  cp-rhs (DCCast dc x ()) (TACast wt x₂) (Step FHOuter (ITGround x₃) FHOuter)
  cp-rhs (DCCast dc () x₁) (TACast wt x₂) (Step FHOuter (ITExpand x₃) FHOuter)
  cp-rhs (DCCast dc x x₁) (TACast wt x₂) (Step (FHCast x₃) x₄ (FHCast x₅)) = DCCast (cp-rhs dc wt (Step x₃ x₄ x₅)) x x₁
  cp-rhs () (TAFailedCast wt x x₁ x₂) stp

  -- this is the main result of this file.
  complete-preservation : ∀{d τ d' Δ} →
             binders-unique d →
             d dcomplete →
             Δ , ∅ ⊢ d :: τ →
             d ↦ d' →
             (Δ , ∅ ⊢ d' :: τ) × (d' dcomplete)
  complete-preservation bd dc wt stp = preservation bd wt stp , cp-rhs dc wt stp

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
module Structure.Sets.Names where

open import Data.Boolean
open import Data.Boolean.Stmt
open import Functional
import      Lvl
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Function
open import Structure.Relator
open import Structure.Setoid using (Equiv) renaming (_≡_ to _≡ₛ_ ; _≢_ to _≢ₛ_)
open import Type
open import Type.Properties.Inhabited

private variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ ℓ₇ ℓ₈ ℓ₉ ℓ₁₀ ℓₑ ℓₑ₁ ℓₑ₂ ℓₑ₃ ℓₑₑ ℓₑₑₗ ℓₑₑᵣ ℓₑᵢ ℓₑₒ ℓₑₛ ℓₗ ℓₗ₁ ℓₗ₂ ℓₗ₃ ℓᵣ ℓₒ ℓᵣₑₗ ℓₛ : Lvl.Level
private variable A B C S S₁ S₂ Sₒ Sᵢ Sₗ Sᵣ E E₁ E₂ Eₗ Eᵣ I O : Type{ℓ}
private variable _∈ₒ_ _∈ᵢ_ : E → S → Stmt{ℓₗ}
private variable _∈ₗ_ : E → Sₗ → Stmt{ℓₗ}
private variable _∈ᵣ_ : E → Sᵣ → Stmt{ℓᵣ}

-- Derivable relation symbols from the subset relation.
module From-[⊆] (_⊆_ : Sₗ → Sᵣ → Stmt{ℓₗ}) where
  -- Superset.
  -- (A ⊇ B) means that every element in the set B is also in the set A (A contains the contents of B).
  _⊇_ = swap(_⊆_)

  -- Non-subset.
  _⊈_ = (¬_) ∘₂ (_⊆_)

  -- Non-superset.
  _⊉_ = (¬_) ∘₂ (_⊇_)

-- Derivable relation symbols from two membership relations.
module From-[∈][∈] (_∈ₗ_ : E → Sₗ → Stmt{ℓₗ}) (_∈ᵣ_ : E → Sᵣ → Stmt{ℓᵣ}) where
  -- Subset.
  -- (A ⊆ B) means that every element in the set A is also in the set B (A is a part of B).
  -- Alternative definition:
  --   A ↦ B ↦ ∀ₗ(x ↦ ((_→ᶠ_) on₂ (x ∈_)) A B)
  _⊆_ = \A B → ∀{x} → (x ∈ₗ A) → (x ∈ᵣ B)

  -- Set equality.
  -- (A ≡ B) means that the sets A and B contains the same elements.
  _≡_ = \A B → ∀{x} → (x ∈ₗ A) ↔ (x ∈ᵣ B)

  open From-[⊆] (_⊆_) public

-- Derivable relation symbols from the membership relation.
module From-[∈] (_∈_ : E → S → Stmt{ℓₗ}) where
  -- Containment.
  -- (a ∋ x) means that the set a contains the element x.
  _∋_ = swap(_∈_)

  -- Not element of.
  _∉_ = (¬_) ∘₂ (_∈_)

  -- Non-containment.
  _∌_ = (¬_) ∘₂ (_∋_)

  open From-[∈][∈] (_∈_)(_∈_) public

module From-[∋] (_∋_ : S → E → Stmt{ℓₗ}) where
  _∈_ = swap(_∋_)

  open From-[∈] (_∈_) hiding (_∋_) public

module Relations (_∈_ : E → S → Stmt{ℓₗ}) where
  -- The property of a set being empty.
  Empty : S → Type
  Empty(s) = ∀ₗ(x ↦ ¬(x ∈ s))

  -- The property of a set being non-empty.
  NonEmpty : S → Type
  NonEmpty(s) = ∃(_∈ s)

  -- The property of a set being the universal set (containing all elements).
  Universal : S → Type
  Universal(s) = ∀ₗ(_∈ s)

  -- The property of two sets being disjoint (not sharing any elements).
  Disjoint : S → S → Type
  Disjoint s₁ s₂ = ∀ₗ(x ↦ ((x ∈ s₁) → (x ∈ s₂) → ⊥))

module One (_∈_ : E → S → Stmt{ℓₗ}) where
  open From-[∈] (_∈_)

  -- The empty set containing no elements.
  -- No elements are in the empty set.
  -- Standard set notation: ∅ = {}.
  EmptyMembership     = \(∅)
                      → ∀{x} → (x ∉ ∅)

  -- The universal set containing all elements.
  -- Every element is in the universal set.
  -- Standard set notation: 𝐔 = {x. ⊤}.
  UniversalMembership = \(𝐔)
                      → ∀{x} → (x ∈ 𝐔)

  module _ {I : Type{ℓ}} ⦃ equiv-I : Equiv{ℓₑᵢ}(I) ⦄ ⦃ equiv-E : Equiv{ℓₑₑ}(E) ⦄ where
  -- The image of a function containing the elements that the function points to.
  -- The elements of the form f(x) for any x.
  -- Standard set notation: ⊶ f = {f(x). (x: I)}.
    ImageMembership = \(⊶ : (f : I → E) → ⦃ func : Function(f) ⦄ → S)
                    → ∀{f} ⦃ func : Function(f) ⦄ → ∀{y} → (y ∈ (⊶ f)) ↔ ∃(x ↦ f(x) ≡ₛ y)

  module _ ⦃ equiv-E : Equiv{ℓₑₑ}(E) ⦄ {O : Type{ℓ}} ⦃ equiv-O : Equiv{ℓₑₒ}(O) ⦄ where
    -- The fiber of a function together with one of its values containing the elements that point to this value.
    -- Standard set notation: fiber f(y) = {x. f(x) ≡ y}
    FiberMembership = \(fiber : (f : E → O) → ⦃ func : Function(f) ⦄ → (O → S))
                    → ∀{f} ⦃ func : Function(f) ⦄ {y}{x} → (x ∈ fiber f(y)) ↔ (f(x) ≡ₛ y)

  module _ ⦃ equiv-E : Equiv{ℓₑₑ}(E) ⦄ where
    -- The singleton set of a single element containing only this element.
    -- Standard set notation: singleton(x) = {x}
    SingletonMembership = \(singleton : E → S)
                        → ∀{y}{x} → (x ∈ singleton(y)) ↔ (x ≡ₛ y)

    -- The pair set of two elements containing only the two elements.
    -- Standard set notation: pair x y = {x,y}
    PairMembership      = \(pair : E → E → S)
                        → ∀{y₁ y₂}{x} → (x ∈ pair y₁ y₂) ↔ ((x ≡ₛ y₁) ∨ (x ≡ₛ y₂))

    module _ {ℓ} where
      -- Set comprehension with a predicate containing all elements that satisfy this predicate.
      -- Also called: Unrestricted set comprehension, set-builder notation.
      -- Standard set notation: comp(P) = {x. P(x)}
      ComprehensionMembership = \(comp : (P : E → Stmt{ℓ}) ⦃ unaryRelator : UnaryRelator(P) ⦄ → S)
                              → ∀{P} ⦃ unaryRelator : UnaryRelator(P) ⦄ {x} → (x ∈ comp(P)) ↔ P(x)
open One public

module Two (_∈ₗ_ : E → Sₗ → Stmt{ℓₗ}) (_∈ᵣ_ : E → Sᵣ → Stmt{ℓᵣ}) where
  private module Def = From-[∈][∈] (_∈ₗ_)(_∈ᵣ_)

  SubsetMembership      = \{ℓᵣₑₗ} (_⊆_ : Sₗ → Sᵣ → Stmt{ℓᵣₑₗ})
                        → ∀{a b} → (a ⊆ b) ↔ (a Def.⊆ b)
  SetEqualityMembership = \{ℓᵣₑₗ} (_≡_ : Sₗ → Sᵣ → Stmt{ℓᵣₑₗ})
                        → ∀{a b} → (a ≡ b) ↔ (a Def.≡ b)
open Two public

module TwoSame (_∈ₗ_ : E → Sₗ → Stmt{ℓₗ}) (_∈ᵣ_ : E → Sᵣ → Stmt{ℓᵣ}) where
  -- The set complement of a set containing all elements not in this set.
  -- Standard set notation: ∁ A =  {x. x ∉ A}
  ComplementMembership  = \(∁ : Sₗ → Sᵣ)
                        → ∀{A}{x} → (x ∈ᵣ (∁ A)) ↔ ¬(x ∈ₗ A)

  module _ ⦃ equiv-E : Equiv{ℓₑₑ}(E) ⦄ where
    AddMembership       = \(add : E → Sₗ → Sᵣ)
                        → ∀{y}{a}{x} → (x ∈ᵣ add y a) ↔ ((x ∈ₗ a) ∨ (x ≡ₛ y))
    RemoveMembership    = \(remove : E → Sₗ → Sᵣ)
                        → ∀{y}{a}{x} → (x ∈ᵣ remove y a) ↔ ((x ∈ₗ a) ∧ (x ≢ₛ y))

    module _ {ℓ} where
      -- The filtering of a set with a predicate containing all elements in the set that satisfy the predicate.
      -- It is the subset where all elements satisfy the predicate.
      -- Standard set notation: filter P(A) =  {(x∊A). P(x)}
      FilterMembership = \(filter : (P : E → Stmt{ℓ}) ⦃ unaryRelator : UnaryRelator(P) ⦄ → (Sₗ → Sᵣ))
                       → ∀{A}{P} ⦃ unaryRelator : UnaryRelator(P) ⦄ {x} → (x ∈ᵣ filter P(A)) ↔ ((x ∈ₗ A) ∧ P(x))
  -- The filtering of a set with a boolean predicate containing all elements in the set that satisfy the predicate.
  -- Standard set notation: boolFilter P(A) =  {(x∊A). P(x) ≡ 𝑇}
  BooleanFilterMembership = \(boolFilter : (E → Bool) → (Sₗ → Sᵣ))
                          → ∀{A}{P}{x} → (x ∈ᵣ boolFilter P(A)) ↔ ((x ∈ₗ A) ∧ IsTrue(P(x)))

  IndexedBigUnionMembership        = \{ℓ}{I : Type{ℓ}} (⋃ᵢ : (I → Sₗ) → Sᵣ)
                                   → ∀{Ai}{x} → (x ∈ᵣ (⋃ᵢ Ai)) ↔ ∃(i ↦ (x ∈ₗ Ai(i)))
  IndexedBigIntersectionMembership = \{ℓ}{I : Type{ℓ}} (⋂ᵢ : (I → Sₗ) → Sᵣ)
                                   → ∀{Ai} → (◊ I) → ∀{x} → (x ∈ᵣ (⋂ᵢ Ai)) ↔ (∀{i} → (x ∈ₗ Ai(i)))
open TwoSame public

module TwoDifferent (_∈ₗ_ : Eₗ → Sₗ → Stmt{ℓₗ}) (_∈ᵣ_ : Eᵣ → Sᵣ → Stmt{ℓᵣ}) where
  module _ ⦃ equiv-Eₗ : Equiv{ℓₑₑₗ}(Eₗ) ⦄ ⦃ equiv-Eᵣ : Equiv{ℓₑₑᵣ}(Eᵣ) ⦄ where
    -- The image of a function and a set containing the elements that the function points to from the set (the domain is restricted to the set).
    -- The elements of the form f(x) for any x in A.
    -- Standard set notation: map f(A) = {f(x). x ∈ A}.
    MapMembership = \(map : (f : Eₗ → Eᵣ) ⦃ func : Function(f) ⦄ → (Sₗ → Sᵣ))
                  → ∀{f} ⦃ func : Function(f) ⦄ {A}{y} → (y ∈ᵣ map f(A)) ↔ ∃(x ↦ (x ∈ₗ A) ∧ (f(x) ≡ₛ y))

    -- The inverse image of a function together with a set containing the elements that point to elements in the set.
    -- Standard set notation: unmap f(A) = {x. f(x) ∈ A}
    UnmapMembership = \(unmap : (f : Eₗ → Eᵣ) ⦃ func : Function(f) ⦄ → (Sᵣ → Sₗ))
                    → ∀{f} ⦃ func : Function(f) ⦄ {A}{x} → (x ∈ₗ unmap f(A)) ↔ (f(x) ∈ᵣ A)
open TwoDifferent public

module Three (_∈ₗ_ : E → Sₗ → Stmt{ℓₗ}) (_∈ᵣ_ : E → Sᵣ → Stmt{ℓᵣ}) (_∈ₒ_ : E → Sₒ → Stmt{ℓₒ}) where
  -- The union of two sets containing the elements that are in at least one of the sets.
  -- Standard set notation: A ∪ B = {x. (x ∈ A) ∨ (x ∈ B)}
  UnionMembership     = \(_∪_ : Sₗ → Sᵣ → Sₒ)
                      → (∀{A B}{x} → (x ∈ₒ (A ∪ B)) ↔ ((x ∈ₗ A) ∨ (x ∈ᵣ B)))

  -- The intersection of two sets containing the elements that are in at both of the sets.
  -- Standard set notation: A ∪ B = {x. (x ∈ A) ∨ (x ∈ B)}
  IntersectMembership = \(_∩_ : Sₗ → Sᵣ → Sₒ)
                      → (∀{A B}{x} → (x ∈ₒ (A ∩ B)) ↔ ((x ∈ₗ A) ∧ (x ∈ᵣ B)))

  -- The relative complement of two sets containing the elements that are in the left set but not in the right.
  -- Standard set notation: A ∖ B = {x. (x ∈ A) ∧ (x ∉ B)}
  WithoutMembership   = \(_∖_ : Sₗ → Sᵣ → Sₒ)
                      → (∀{A B}{x} → (x ∈ₒ (A ∖ B)) ↔ ((x ∈ₗ A) ∧ ¬(x ∈ᵣ B)))
open Three public

module ThreeNestedTwoDifferent (_∈ₒ_ : Sₗ → Sₒ → Stmt{ℓₒ}) where
  module _ (_⊆_ : Sₗ → Sᵣ → Stmt{ℓₛ}) where
    -- The power set of a set containing all subsets of a set.
    -- Standard set notation: ℘(y) = {x. x ⊆ y}
    PowerMembership = \(℘ : Sᵣ → Sₒ)
                    → ∀{y}{x} → (x ∈ₒ ℘(y)) ↔ (x ⊆ y)
open ThreeNestedTwoDifferent public

module ThreeTwoNested (_∈ₗ_ : E → Sₗ → Stmt{ℓₗ}) (_∈ᵣ_ : Sₗ → Sᵣ → Stmt{ℓᵣ}) (_∈ₒ_ : E → Sₒ → Stmt{ℓₒ}) where
  BigUnionMembership      = \(⋃ : Sᵣ → Sₒ)
                          → ∀{A}{x} → (x ∈ₒ (⋃ A)) ↔ ∃(a ↦ (a ∈ᵣ A) ∧ (x ∈ₗ a))
  BigIntersectionMembership = \(⋂ : Sᵣ → Sₒ)
                            → ∀{A} → ∃(_∈ᵣ A) → ∀{x} → (x ∈ₒ (⋂ A)) ↔ (∀{a} → (a ∈ᵣ A) → (x ∈ₗ a))
  BigIntersectionMembershipWithEmpty = \(⋂ : Sᵣ → Sₒ)
                                     → ∀{A}{x} → (x ∈ₒ (⋂ A)) ↔ ∃(a ↦ (a ∈ᵣ A) ∧ (x ∈ₗ a)) ∧ (∀{a} → (a ∈ᵣ A) → (x ∈ₗ a))
  BigIntersectionMembershipWithUniversal = \(⋂ : Sᵣ → Sₒ)
                                         → ∀{A}{x} → (x ∈ₒ (⋂ A)) ↔ (∀{a} → (a ∈ᵣ A) → (x ∈ₗ a))
open ThreeTwoNested 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:
data Nat : Set where
  Zero : Nat
  Suc  : Nat → Nat
{-# COMPILE AGDA2HS Nat #-}

Nat' = Nat
{-# COMPILE AGDA2HS Nat' #-}

myNat : Nat'
myNat = Suc (Suc Zero)
{-# COMPILE AGDA2HS myNat #-}

data List (a : Set) : Set where
  Nil : List a
  Cons : a → List a → List a
{-# COMPILE AGDA2HS List #-}

List' : Set → Set
List' a = List a
{-# COMPILE AGDA2HS List' #-}

NatList = List Nat
{-# COMPILE AGDA2HS NatList #-}

myListFun : List' Nat' → NatList
myListFun Nil = Nil
myListFun (Cons x xs) = Cons x (myListFun xs)
{-# COMPILE AGDA2HS myListFun #-}

ListList : Set → Set
ListList a = List (List a)
{-# COMPILE AGDA2HS ListList #-}

flatten : ∀ {a} → ListList a → List a
flatten Nil = Nil
flatten (Cons Nil xss) = flatten xss
flatten (Cons (Cons x xs) xss) = Cons x (flatten (Cons xs xss))
{-# COMPILE AGDA2HS flatten #-}


text:
open import Data.Empty

open import AEff
open import EffectAnnotations
open import Renamings
open import Types hiding (``)

open import Relation.Binary.PropositionalEquality hiding ([_])

module Substitutions where

-- PARALLEL SUBSTITUTIONS

data Sub : Ctx → Ctx → Set where

  ⟨_,_⟩ : {Γ Γ' : Ctx} {X : VType} →
          Sub Γ Γ' →
          Γ' ⊢V⦂ X →
          --------------------------
          Sub (Γ ∷ X) Γ'

  ε     : {Γ' : Ctx} →
          ------------
          Sub [] Γ'

  π     : {Γ Γ' : Ctx} {X : VType} →
          Sub Γ Γ' →
          --------------------------
          Sub Γ (Γ' ∷ X)

  φ     : {Γ Γ' : Ctx} →
          Sub Γ Γ' →
          ----------------
          Sub (Γ ■) (Γ' ■)

-- RENAMINGS AS SUBSTITUTIONS

sub-of-ren : {Γ Γ' : Ctx} →
             Ren Γ Γ' →
             --------------
             Sub Γ Γ'

sub-of-ren ε =
  ε
sub-of-ren ⟨ f , x ⟩ =
  ⟨ sub-of-ren f , ` x ⟩
sub-of-ren (π f) =
  π (sub-of-ren f)
sub-of-ren (φ f) =
  φ (sub-of-ren f)

-- IDENTITY SUBSTITUTION

sub-id : {Γ : Ctx} →
         -----------
         Sub Γ Γ

sub-id = sub-of-ren ren-id

-- SUBSTITUTION EXTENSION

_[_]s : {Γ Γ' : Ctx} {X : VType} →
        Sub Γ Γ' →
        Γ' ⊢V⦂ X →
        --------------------------
        Sub (Γ ∷ X) Γ'

s [ V ]s = ⟨ s , V ⟩

-- CONGRUENCE OF SUBSTITUTIONS

subst-cong : {Γ Γ' : Ctx} {X : VType} → Sub Γ Γ' → Sub (Γ ∷ X) (Γ' ∷ X)
subst-cong ⟨ s , x ⟩ =
  ⟨ π ⟨ s , x ⟩ , ` Hd ⟩
subst-cong ε =
  ⟨ ε , ` Hd ⟩
subst-cong (π s) =
  ⟨ π (π s) , ` Hd ⟩
subst-cong (φ s) =
  ⟨ π (φ s) , ` Hd ⟩

-- ACTION OF SUBSTITUTION ON WELL-TYPED VALUES AND COMPUTATIONS

val-of-sub : {Γ Γ' : Ctx} {X : VType} → Sub Γ Γ' → X ∈ Γ → Γ' ⊢V⦂ X
val-of-sub ⟨ s , V ⟩ Hd =
  V
val-of-sub ⟨ s , V ⟩ (Tl-v x) =
  val-of-sub s x
val-of-sub (π s) x =
  V-rename ren-wk (val-of-sub s x)
val-of-sub (φ s) (Tl-■ p x) =
  ■-wk p (val-of-sub s x)

mutual

  sub-var : {Γ Γ' : Ctx} {X : VType} →
            X ∈ Γ →
            Sub Γ Γ' →
            --------------------------
            Γ' ⊢V⦂ X

  sub-var Hd ⟨ s , V ⟩ =
    V
  sub-var Hd (π s) =
    V-rename ren-wk (val-of-sub s Hd)
  sub-var (Tl-v x) ⟨ s , V ⟩ =
    sub-var x s
  sub-var (Tl-v x) (π s) =
    V-rename ren-wk (val-of-sub s (Tl-v x))
  sub-var (Tl-■ p x) (π s) =
    V-rename ren-wk (val-of-sub s (Tl-■ p x))
  sub-var (Tl-■ p x) (φ s) =
    ■-wk p (val-of-sub s x)

  sub-comp : {Γ Γ' Γ'' : Ctx} →
             Sub Γ' Γ'' →
             Sub Γ Γ' →
             ------------------
             Sub Γ Γ''

  sub-comp t ⟨ s , V ⟩ =
    ⟨ sub-comp t s , V [ t ]v ⟩
  sub-comp t ε =
    ε
  sub-comp ⟨ t , x ⟩ (π s) =
    sub-comp t s
  sub-comp (π t) (π s) =
    π (sub-comp t (π s))
  sub-comp (π t) (φ s) =
    π (sub-comp t (φ s))
  sub-comp (φ t) (φ s) =
    φ (sub-comp t s)

  _[_]v : {Γ Γ' : Ctx} {X : VType} →
          Γ ⊢V⦂ X →
          Sub Γ Γ' →
          --------------------------
          Γ' ⊢V⦂ X

  (` x) [ s ]v =
    sub-var x s
  (´ c) [ s ]v =
    ´ c
  ⋆ [ s ]v =
    ⋆
  (ƛ M) [ s ]v =
    ƛ (M [ subst-cong s ]c)
  ⟨ V ⟩ [ s ]v =
    ⟨ V [ s ]v ⟩
  (□ V) [ s ]v =
    □ (V [ φ s ]v)

  _[_]c : {Γ Γ' : Ctx} {C : CType} →
          Γ ⊢C⦂ C →
          Sub Γ Γ' →
          --------------------------
          Γ' ⊢C⦂ C

  (return V) [ s ]c =
    return (V [ s ]v)
  (let= M `in N) [ s ]c =
    let= (M [ s ]c) `in (N [ subst-cong s ]c)
  (V · W) [ s ]c =
    (V [ s ]v) · (W [ s ]v)
  (↑ op p V M) [ s ]c =
    ↑ op p (V [ s ]v) (M [ s ]c)
  (↓ op V M) [ s ]c =
    ↓ op (V [ s ]v) (M [ s ]c)
  (promise op ∣ p ↦ M `in N) [ s ]c =
    promise op ∣ p ↦ (M [ subst-cong (subst-cong s) ]c) `in (N [ subst-cong s ]c)
  (await V until M) [ s ]c =
    await (V [ s ]v) until (M [ subst-cong s ]c)
  (unbox V `in M) [ s ]c =
    unbox (V [ s ]v) `in (M [ subst-cong s ]c)
  (spawn M N) [ s ]c =
    spawn (M [ φ s ]c) (N [ s ]c)
  (coerce p q M) [ s ]c =
    coerce p q (M [ s ]c)

  infix 40 _[_]v
  infix 40 _[_]c

-- ACTION OF SUBSTITUTION ON WELL-TYPED PROCESSES

_[_]p : {Γ Γ' : Ctx} {o : O} {PP : PType o} →
        Γ ⊢P⦂ PP →
        Sub Γ Γ' →
        -------------------------------------
        Γ' ⊢P⦂ PP

(run M) [ s ]p =
  run (M [ s ]c)
(P ∥ Q) [ s ]p =
  (P [ s ]p) ∥ (Q [ s ]p)
(↑ op p V P) [ s ]p =
  ↑ op p (V [ s ]v) (P [ s ]p)
(↓ op V P) [ s ]p =
  ↓ op (V [ s ]v) (P [ s ]p)

infix 40 _[_]p

max_stars_repo_name: danelahman/higher-order-aeff-agda

max_issues_repo_name: danelahman/modal-aeff-agda

max_forks_repo_name: danelahman/modal-aeff-agda


text:
-- Andreas, 2014-10-08, issue reported by Andrea Vezzosi

{-# OPTIONS --copatterns #-}

import Common.Level
open import Common.Product

postulate Nat : Set

record Cxt : Set₁ where
  constructor Con  -- essential
  field
    CSet : Set
    CRel : (e0 e1 : CSet) → Set

record Type (Γ : Cxt) : Set₁ where
  open Cxt
  field
    TSet : (e : CSet Γ) → Set
    TRel : (e : CSet Γ) →
           ([e] : CRel Γ e e) →
           (t : TSet e) → Set

open Type

module Works where

  T : (Γ : Cxt) → (a : Type Γ) → Type Γ
  TSet (T Γ a) γ             = Nat × TSet a γ
  TRel (T Γ a) γ [e] (n , b) = TRel a γ [e] b

module Works2 where

  T : (Γ : Cxt) → (a : Type Γ) → Type Γ
  TSet (T Γ a) γ                     = Nat × TSet a γ
  TRel (T (Con S R) a) γ [e] (n , b) = TRel a γ [e] b

module Fails2 where

  T : (Γ : Cxt) → (a : Type Γ) → Type Γ
  TSet (T (Con S R) a) γ     = Nat × TSet a γ
  TRel (T Γ a) γ [e] (n , b) = TRel a γ [e] b

module Fails where

  T : (Γ : Cxt) → (a : Type Γ) → Type Γ
  TSet (T (Con S R) a) γ             = Nat × TSet a γ
  TRel (T (Con S R) a) γ [e] (n , b) = TRel a γ [e] b

-- All version should work!

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Data.Nat
open import Data.Fin
open import Data.List
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.All as All
open import Data.List.All.Properties.Extra
open import Data.Vec hiding (_∷ʳ_ ; _>>=_ ; init)
open import Data.Product
open import Relation.Binary.PropositionalEquality hiding ([_])
open ≡-Reasoning
open import Data.Unit
open import Data.List.Prefix
open import Data.List.Properties.Extra
open import Data.Maybe
open import Common.Weakening

-- This file contains the Agda Scope Graph Library described in
-- Section 4 of the paper.

-- The definitions are parameterized by a scope graph, where a scope
-- graph is a finite map from scope identifiers to scope shape
-- descriptors.
--
-- The scope graph library is also parametric in what the notion of
-- type is for declarations in the scope graph.
--
-- We use modules for this library parameterization.  The `k`
-- parameter of the `ScopesFrames` module represents the number of
-- scope identifiers in the scope graph that all definitions are
-- parameterized over; and the `Ty` parameter is a language-specific
-- notion of type.

module ScopesFrames.ScopesFrames (k : ℕ) (Ty : Set) where

------------------
-- SCOPE GRAPHS --
------------------

-- Type aliases for scope identifiers (`Scope`s) and scope graphs
-- (`Graph`s).
--
-- As described in the paper, scope shapes are given by a list of
-- types corresponding to the declarations of the scope, and a list of
-- scopes, corresponding to the edges of the scope.

Scope = Fin k
Graph = Scope → (List Ty × List Scope)

-- All the following definitions are parameterized by a scope graph
-- `g`.

module UsesGraph (g : Graph) where

  -- Some projection functions:
  declsOf : Scope → List Ty     ;  declsOf s  = proj₁ (g s)
  edgesOf : Scope → List Scope  ;  edgesOf s  = proj₂ (g s)

  -- A resolution path is a witness that we can traverse a sequence of
  -- scope edges (`_⟶_`) in `g` to arrive at a declaration of type
  -- `t`:

  data _⟶_ : Scope → Scope → Set where
    []   :  ∀ {s} → s ⟶ s
    _∷_  :  ∀ {s s' s''} → s' ∈ edgesOf s → s' ⟶ s'' → s ⟶ s''

  -- path concatenation
  concatₚ : ∀ {s s' s''} → s ⟶ s' → s' ⟶ s'' → s ⟶ s''
  concatₚ [] p₂ = p₂
  concatₚ (x ∷ p₁) p₂ = x ∷ (concatₚ p₁ p₂)

  data _↦_ (s : Scope) (t : Ty) : Set where
    path : ∀{s'} → s ⟶ s' → t ∈ declsOf s' → s ↦ t

  prepend : ∀ {s s' t} → s ⟶ s' → s' ↦ t → s ↦ t
  prepend p (path p' d) = path (concatₚ p p') d

  -- The definitions above fully define scope graphs.  The remaining
  -- definitions in this file are intrinsically-typed by this notion
  -- of scope graph.

  ----------------------
  -- FRAMES AND HEAPS --
  ----------------------

  -- Heap types summarize what the scope is for each frame location in
  -- the heap:

  HeapTy = List Scope

  -- A frame pointer `Frame s Σ` is a witness that there is a frame
  -- location scoped by `s` in a heap typed by `Σ`:

  Frame : Scope → (Σ : HeapTy) → Set
  Frame s Σ = s ∈ Σ

  -- Concrete frames and heaps store values that are weakened when the
  -- heap is extended.  The following definitions are parameterized by
  -- a language-specific notion of weakenable value.

  module UsesVal (Val : Ty → HeapTy → Set)
                 (weaken-val : ∀ {t Σ Σ'} → Σ ⊑ Σ' → Val t Σ → Val t Σ') where

    -- Slots are given by a list of values that are in one-to-one
    -- correspondence with a list of declarations (types):

    Slots : (ds : List Ty) → (Σ : HeapTy) → Set
    Slots ds Σ = All (λ t → Val t Σ) ds

    -- Links are given by a list of frame pointers (links) that are in
    -- one-to-one correspondence with a list of edges (scopes):

    Links : (es : List Scope) → (Σ : HeapTy) → Set
    Links es Σ = All (λ s → Frame s Σ) es

    -- A heap frame for a scope `s` is given by a set of slots and
    -- links that are in one-to-one correspondence with the
    -- declarations and edges of the scope:

    HeapFrame : Scope → HeapTy → Set
    HeapFrame s Σ = Slots (declsOf s) Σ × Links (edgesOf s) Σ

    -- A heap typed by `Σ` is given by a list of heap frames such that
    -- each frame location is in the heap is typed by the
    -- corresponding location in `Σ`.

    Heap : (Σ : HeapTy) → Set
    Heap Σ = All (λ s → HeapFrame s Σ) Σ

    ----------------------
    -- FRAME OPERATIONS --
    ----------------------

    -- Frame initialization extends the heap, requiring heap type
    -- weakening.  The `Common.Weakening` module defines a generic
    -- `Weakenable` record, which we instantiate for each entity that
    -- is required to be weakenable.  We use Agda's instance arguments
    -- to automatically resolve the right notion of weakening where
    -- possible.

    -- We add some instances of the Weakenable typeclass
    -- to the instance argument scope:

    instance
      weaken-val' : ∀ {t} → Weakenable (λ Σ → Val t Σ)
      weaken-val' = record { wk = weaken-val }

      weaken-frame : ∀ {s} → Weakenable (Frame s)
      weaken-frame = record { wk = Weakenable.wk any-weakenable }

    -- Frame initialization takes as argument:
    --
    -- * a scope `s`;
    --
    -- * a scope shape witness which asserts that looking up `s` in
    --   the current scope graph `g` yields a scope shape where the
    --   declarations are given by a list of types `ds`, and scope
    --   edges are given by a list of scopes `es`;
    --
    -- * a set of slots typed by `ds`;
    --
    -- * a set of links typed by `es`; and
    --
    -- * a heap typed by the heap type `Σ` which also types the slots
    --   and links.
    --
    -- The operation returns an extended heap (`∷ʳ` appends a single
    -- element to a list, and is defined in `Data.List.Base` in the
    -- Agda Standard Library) and a frame pointer into the extended
    -- heap, i.e., the newly allocated and initialized frame.

    initFrame   :  (s : Scope) → ∀ {Σ ds es}⦃ shape : g s ≡ (ds , es) ⦄ →
                   Slots ds Σ → Links es Σ → Heap Σ → Frame s (Σ ∷ʳ s) × Heap (Σ ∷ʳ s)
    initFrame s {Σ} ⦃ refl ⦄ slots links h =
      let ext = ∷ʳ-⊒ s Σ -- heap extension fact
          f'  = ∈-∷ʳ Σ s -- updated frame pointer witness
          h'  = (wk ext h) all-∷ʳ (wk ext slots , wk ext links) -- extended heap
      in (f' , h')

    -- Frames may be self-referential.  For example, the values stored
    -- in the slots of a frame may contain pointers to the frame
    -- itself.  The `initFrame` function above does not support
    -- initializing such self-referential slots, since the slots are
    -- assumed to be typed under the unextended heap.
    --
    -- The `initFrameι` function we now define takes as argument a
    -- function to be used to initialize possibly-self-referential
    -- frame slots.  The function takes as argument a frame pointer
    -- into a heap extended by the scope that we are currently
    -- initializing, and slots are typed under this extended heap;
    -- hence the slots can have self-references to the frame currently
    -- being initialized.

    initFrameι : (s : Scope) → ∀ {Σ ds es}⦃ shape : g s ≡ (ds , es) ⦄ →
                 (slotsf : Frame s (Σ ∷ʳ s) → Slots ds (Σ ∷ʳ s)) → Links es Σ → Heap Σ →
                 Frame s (Σ ∷ʳ s) × Heap (Σ ∷ʳ s)
    initFrameι s {Σ} ⦃ refl ⦄ slotsf links h =
      let ext = ∷ʳ-⊒ s Σ -- heap extension fact
          f'  = ∈-∷ʳ Σ s -- updated frame pointer witness
          h'  = (wk ext h) all-∷ʳ (slotsf f' , wk ext links) -- extended heap
      in (f' , h')

    -- Given a witness that a declaration typed by `t` is in a scope,
    -- and a frame pointer, we can fetch the well-typed value stored
    -- in the corresponding frame slot:

    getSlot : ∀ {s t Σ} → t ∈ declsOf s → Frame s Σ → Heap Σ → Val t Σ
    getSlot d f h
      with (All.lookup h f)
    ...  | (slots , links) = All.lookup slots d

    -- Given a witness that a declaration typed by `t` is in a scope,
    -- and a frame pointer, we can mutate the corresponding slot in a
    -- type preserving manner:

    setSlot : ∀ {s t Σ} → t ∈ declsOf s → Val t Σ → Frame s Σ → Heap Σ → Heap Σ
    setSlot d v f h
      with (All.lookup h f)
    ...  | (slots , links) = h All.[ f ]≔ (slots All.[ d ]≔ v , links)

    -- ... and similarly for edges:

    getLink : ∀ {s s' Σ} → s' ∈ edgesOf s → Frame s Σ → Heap Σ → Frame s' Σ
    getLink e f h
      with (All.lookup h f)
    ...  | (slots , links) = All.lookup links e

    setLink : ∀ {s s' Σ} → s' ∈ edgesOf s → Frame s' Σ → Frame s Σ → Heap Σ → Heap Σ
    setLink e f' f h
      with (All.lookup h f)
    ...  | (slots , links) = h All.[ f ]≔ (slots , links All.[ e ]≔ f')

    -- Given a witness that there is a path through the scope graph
    -- from scope `s` to scope `s'`, a frame typed by `s`, and a
    -- well-typed heap, we can traverse the path by following the
    -- corresponding frame links in the heap to arrive at a frame
    -- scoped by `s'`:

    getFrame : ∀ {s s' Σ} → (s ⟶ s') → Frame s Σ → Heap Σ → Frame s' Σ
    getFrame []      f h = f
    getFrame (e ∷ p) f h
      with (All.lookup h f)
    ...  | (slots , links) = getFrame p (All.lookup links e) h

    -- Given the definitions above, we can define some shorthand
    -- functions for getting and setting values:

    getVal  :  ∀ {s t} → (s ↦ t) → ∀ {Σ} → Frame s Σ → Heap Σ → Val t Σ
    getVal (path p d) f h = getSlot d (getFrame p f h) h

    setVal  :  ∀ {s t Σ} → (s ↦ t) → Val t Σ → Frame s Σ → Heap Σ → Heap Σ
    setVal (path p d) v f h = setSlot d v (getFrame p f h) h


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

module Cubical.Data.FinSet where

open import Cubical.Data.FinSet.Base public
open import Cubical.Data.FinSet.Properties public

max_stars_repo_name: FernandoLarrain/cubical


text:
module Impure.LFRef.Properties.Decidable where

open import Prelude
open import Relation.Unary
open import Relation.Nullary.Decidable as DecM
open import Data.Fin.Properties as FinP using ()
open import Data.List
open import Data.Vec
open import Data.Vec.Properties
open import Function.Inverse hiding (_∘_; sym)
open import Extensions.List as List↑ using ()
open import Extensions.Vec as Vec↑ using ()
open import Relation.Binary.List.Pointwise using (decidable-≡)
open import Relation.Binary.HeterogeneousEquality as Het using ()

open import Impure.LFRef.Syntax hiding (subst)
open import Impure.LFRef.Welltyped

module DecidableEquality where
  -- termination checker has trouble with mapping
  -- recursively over the arguments of constructors; inlining would prove this terminating
  {-# TERMINATING #-}
  _tm≟_ : ∀ {n} (a b : Term n) → Dec (a ≡ b)
  var x tm≟ var x' with (x FinP.≟ x')
  ... | yes refl = yes refl
  ... | no neq = no (λ{ refl → neq refl })
  var x tm≟ loc x₁ = no (λ ())
  var x tm≟ unit = no (λ ())
  var x tm≟ con fn ts = no (λ ())
  loc x tm≟ var x₁ = no (λ ())
  loc x tm≟ loc x' with x ≟ x'
  ... | yes refl = yes refl
  ... | no neq = no (λ{ refl → neq refl })
  loc x tm≟ unit = no (λ ())
  loc x tm≟ con fn ts = no (λ ())
  unit tm≟ var x = no (λ ())
  unit tm≟ loc x = no (λ ())
  unit tm≟ unit = yes refl
  unit tm≟ con fn ts = no (λ ())
  con fn ts tm≟ var x = no (λ ())
  con fn ts tm≟ loc x = no (λ ())
  con fn ts tm≟ unit = no (λ ())
  con fn ts tm≟ con fn' ts' with fn ≟ fn'
  ... | no neq = no (λ{ refl → neq refl })
  ... | yes refl with decidable-≡ _tm≟_ ts ts'
  ... | no neq = no (λ{ refl → neq refl })
  ... | yes refl = yes refl

  -- decidable type equality
  _ty≟_ : ∀ {n} (a b : Type n) → Dec (a ≡ b)
  (x [ ts ]) ty≟ (x' [ ts' ]) with x ≟ x'
  ... | no neq = no (λ{ refl → neq refl })
  ... | yes refl with decidable-≡ _tm≟_ ts ts'
  ... | yes refl = yes refl
  ... | no neq = no (λ{ refl → neq refl })
  (x [ ts ]) ty≟ Ref b = no (λ ())
  (x [ ts ]) ty≟ Unit = no (λ ())
  Ref a ty≟ (x [ ts ]) = no (λ ())
  Ref a ty≟ Ref b with a ty≟ b
  ... | yes refl = yes refl
  ... | no neq = no (λ{ refl → neq refl })
  Ref a ty≟ Unit = no (λ ())
  Unit ty≟ (x [ ts ]) = no (λ ())
  Unit ty≟ Ref b = no (λ ())
  Unit ty≟ Unit = yes refl

module UniqueTypings where
  unique-tm-type : ∀ {n a b 𝕊 Σ Γ} {t : Term n} → 𝕊 , Σ , Γ ⊢ t ∶ a → 𝕊 , Σ , Γ ⊢ t ∶ b → a ≡ b
  unique-tm-type unit unit = refl
  unique-tm-type (var x) (var x') with Vec↑.[]=-functional _ _ x x'
  ... | refl = refl
  unique-tm-type (loc x) (loc x') with List↑.[]=-functional _ _ x x'
  ... | refl = refl
  unique-tm-type (con c ts refl) (con c' ts' refl)
    with List↑.[]=-functional _ _ c c'
  ... | refl = refl

  unique-type : ∀ {n a b 𝕊 Σ Γ} {e : Exp n} → 𝕊 , Σ , Γ ⊢ₑ e ∶ a → 𝕊 , Σ , Γ ⊢ₑ e ∶ b → a ≡ b
  unique-type (tm x) (tm y) = unique-tm-type x y
  unique-type (fn ·★[ refl ] ts) (fn' ·★[ refl ] ts') with List↑.[]=-functional _ _ fn fn'
  ... | refl = refl
  unique-type (ref p) (ref q) = cong Ref (unique-type p q)
  unique-type (! p) (! q) with unique-type p q
  ... | refl = refl
  unique-type (p ≔ q) (p' ≔ q') = refl

  elim-mistype : ∀ {n a b 𝕊 Σ Γ} {e : Exp n} →
                   𝕊 , Σ , Γ ⊢ₑ e ∶ a → 𝕊 , Σ , Γ ⊢ₑ e ∶ b → ¬ (a ≢ b)
  elim-mistype p q with unique-type p q
  ... | refl = λ neq → neq refl

module DecidableTypability where
  open UniqueTypings
  open DecidableEquality

  mutual
    type-tm : ∀ {n} 𝕊 Σ Γ (t : Term n) → Dec (∃ λ a → 𝕊 , Σ , Γ ⊢ t ∶ a)
    type-tm 𝕊 Σ Γ (var x) =
      yes (, var (proj₂ (Vec↑.strong-lookup _ _)))
    type-tm 𝕊 Σ Γ (loc x) =
      DecM.map′
        (λ{ (_ , p)  → Ref _ , loc p})
        (λ{ (_ , loc p) → _ , p })
        (List↑.dec-lookup x Σ)
    type-tm 𝕊 Σ Γ unit = yes (Unit , unit)
    type-tm 𝕊 Σ Γ (con c ts) with (List↑.dec-lookup c (Sig.constructors 𝕊))
    ... | no ¬p = no (λ{ (._ , con p _ _) → ¬p (, p)})
    ... | yes (p , z) with typecheck-tele 𝕊 Σ Γ ts (weaken+-tele _ (ConType.args p))
    ... | no ¬q = no lem
      where
        lem : ¬ ∃ λ ty → 𝕊 , Σ , Γ ⊢ (con c ts) ∶ ty
        lem (._ , con x q p) with List↑.[]=-functional _ _ z x
        ... | refl = ¬q q
    ... | yes q = yes (, con z q (tele-fit-length q))

    -- deciding whether a term matches a given type follows from
    -- typability with unique type assignments
    typecheck-tm : ∀ {n} 𝕊 Σ Γ (t : Term n) a → Dec (𝕊 , Σ , Γ ⊢ t ∶ a)
    typecheck-tm 𝕊 Σ Γ t a with type-tm 𝕊 Σ Γ t
    ... | no nwt = no (λ wta → nwt (, wta))
    ... | yes (a' , wta') with a ty≟ a'
    ... | yes refl = yes wta'
    ... | no neq = no (λ wta → neq (unique-tm-type wta wta'))

    typecheck-tele : ∀ {n m } 𝕊 Σ Γ (ts : List (Term n)) → (T : Tele n m) → Dec (𝕊 , Σ , Γ ⊢ ts ∶ⁿ T)
    typecheck-tele 𝕊 Σ Γ [] ε = yes ε
    typecheck-tele 𝕊 Σ Γ [] (x ⟶ T) = no (λ ())
    typecheck-tele 𝕊 Σ Γ (x ∷ ts) ε = no (λ ())
    typecheck-tele 𝕊 Σ Γ (x ∷ ts) (ty ⟶ T)
      with typecheck-tm 𝕊 Σ Γ x ty
    ... | no ¬x∶ty = no (λ{ (x∶ty ⟶ _) → ¬x∶ty x∶ty })
    ... | yes x∶ty with typecheck-tele 𝕊 Σ Γ ts (T tele/ (sub x))
    ... | yes ts∶T = yes (x∶ty ⟶ ts∶T)
    ... | no ¬ts∶T = no (λ{ (_ ⟶ ts∶T) → ¬ts∶T ts∶T })

  type : ∀ {n} 𝕊 Σ Γ (e : Exp n) → Dec (∃ λ a → 𝕊 , Σ , Γ ⊢ₑ e ∶ a)
  type 𝕊 Σ Γ (tm t) = DecM.map′
    (λ{ (_ , x ) → , (tm x)})
    (λ{ (_ , tm x) → , x})
    (type-tm 𝕊 Σ Γ t)
  type {n} 𝕊 Σ Γ (fn ·★ ts) with List↑.dec-lookup fn (Sig.funs 𝕊)
  ... | no ¬fn! = no (λ { (_ , (fn! ·★[ q ] _)) → ¬fn! (, fn!) })
  ... | yes (φ , fn!) with typecheck-tele 𝕊 Σ Γ ts (weaken+-tele _ (Fun.args φ))
  ... | no ¬ts∶T = no lem
    where
      lem : ¬ ∃ λ a → 𝕊 , Σ , Γ ⊢ₑ (fn ·★ ts) ∶ a
      lem (_ , (fn!' ·★[ q ] ts∶T)) with List↑.[]=-functional _ _ fn! fn!'
      ... | refl = ¬ts∶T ts∶T
  ... | yes ts∶T = yes (, fn! ·★[ tele-fit-length ts∶T ] ts∶T)
  type 𝕊 Σ Γ (ref e) with (type 𝕊 Σ Γ e)
  ... | no ¬wte = no (λ{ (.(Ref _) , ref wte) → ¬wte (, wte)})
  ... | yes (a , wte) = yes (, ref wte)
  type 𝕊 Σ Γ (! e) with (type 𝕊 Σ Γ e)
  ... | no ¬wte = no ((λ{ (x , (! wte)) → ¬wte (, wte) }))
  type 𝕊 Σ Γ (! e) | yes (x [ ts ] , wte) =
    no λ{ (_ , ! wte') → elim-mistype wte  wte' (λ ()) }
  type 𝕊 Σ Γ (! e) | yes (Unit , wte) =
    no λ{ (_ , ! wte' ) → elim-mistype wte wte' (λ ()) }
  type 𝕊 Σ Γ (! e) | yes (Ref a , wte) = yes (_ , (! wte))
  type 𝕊 Σ Γ (l ≔ r) with type 𝕊 Σ Γ l | type 𝕊 Σ Γ r
  ... | no ¬wtl | _ = no (λ{ (_ , wtl ≔ _ ) → ¬wtl (, wtl) })
  ... | _ | no ¬wtr = no (λ{ (_ , _ ≔ wtr ) → ¬wtr (, wtr) })
  ... | yes (x [ ts ] , wtl) | (yes (b , wtr)) =
    no (λ{ (_ , wtl' ≔ wtr) → elim-mistype wtl wtl' (λ ())})
  ... | yes (Unit , wtl) | (yes (b , wtr)) =
    no (λ{ (_ , wtl' ≔ wtr) → elim-mistype wtl wtl' (λ ())})
  ... | yes (Ref a , wtl) | yes (b , wtr) with a ty≟ b
  ... | yes refl = yes (, wtl ≔ wtr)
  ... | no neq = no lem
    where
      lem : ¬ ∃ λ a → 𝕊 , Σ , Γ ⊢ₑ (l ≔ r) ∶ a
      lem (.Unit , (wtl' ≔ wtr')) with unique-type wtl wtl'
      ... | refl = elim-mistype wtr wtr' (neq ∘ sym)

  typecheck : ∀ {n} 𝕊 Σ Γ (e : Exp n) a → Dec (𝕊 , Σ , Γ ⊢ₑ e ∶ a)
  typecheck 𝕊 Σ Γ e a with type 𝕊 Σ Γ e
  ... | no ¬wte = no (λ wte → ¬wte (, wte))
  ... | yes (a' , wte) with a' ty≟ a
  ... | yes refl = yes wte
  ... | no neq = no (λ{ wte' → elim-mistype wte wte' neq })

  typecheck-seq : ∀ {n} 𝕊 Σ Γ (e : SeqExp n) a → Dec (𝕊 , Σ , Γ ⊢ₛ e ∶ a)
  typecheck-seq 𝕊 Σ Γ (lett e c) a with type 𝕊 Σ Γ e
  ... | no ¬wte = no (λ{ (lett wte _ ) → ¬wte (, wte)})
  ... | yes (b , wte) with typecheck-seq 𝕊 Σ (b :+: Γ) c (weaken₁-tp a)
  ... | yes wtc = yes (lett wte wtc)
  ... | no ¬wtc = no lem
    where
      lem : ¬ 𝕊 , Σ , Γ ⊢ₛ lett e c ∶ a
      lem (lett wte' wtc) with unique-type wte wte'
      ... | refl = ¬wtc wtc
  typecheck-seq 𝕊 Σ Γ (ret e) a = DecM.map′ ret (λ{ (ret wte) → wte }) (typecheck 𝕊 Σ Γ e a)


text:
-- {-# OPTIONS -v tc.term.con:100 #-}
module Issue799 where

data D : Set where
  d : D

x : D
x = d {_} {_} {interesting-argument = _} {_} {_} {_}
  -- should fail

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module STLC.Term where

open import Data.Fin using (Fin)
open import Data.Fin.Substitution
open import Data.Nat using (ℕ; _+_)

open import Relation.Binary.Construct.Closure.ReflexiveTransitive
  using (Star; ε; _◅_)

open import Data.Vec using (Vec; []; _∷_; lookup)

open import Relation.Binary.PropositionalEquality
  using (refl; _≡_; cong₂)

-- --------------------------------------------------------------------
-- Untyped terms and values
-- --------------------------------------------------------------------

infix 7 _·_

data Term (n : ℕ) : Set where
  # : (x : Fin n) -> Term n
  ƛ : Term (1 + n) -> Term n
  _·_ : Term n -> Term n -> Term n

data Value {n : ℕ} : Term n -> Set where
  ƛ :
    ∀ { t }
    -- -----------
    -> Value (ƛ t)

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

module Substitution where

  -- This sub module defines application of the subtitution
  -- TODO: Rename for consistency
  module SubstApplication { T : ℕ -> Set } ( l : Lift T Term ) where
    open Lift l hiding  (var)

    -- Application of substitution to term
    infixl 8 _/_

    _/_ : ∀ { m n : ℕ } -> Term m -> Sub T m n -> Term n
    # x / ρ = lift (lookup ρ x)
    (ƛ t) / ρ = ƛ (t / ρ ↑)
    (t₁ · t₂) / ρ = (t₁ / ρ) · (t₂ / ρ)

    open Application (record { _/_ = _/_ }) using (_/✶_)

  open TermSubst (record { var = #; app = SubstApplication._/_ }) public hiding (var)

  infix 8 _[/_]

  -- Shorthand for single-variable term substitutions
  _[/_] : ∀ { n } → Term (1 + n) → Term n → Term n
  t₁ [/ t₂ ] = t₁ / sub t₂

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

-- TODO: Add additional operators
-- TODO: Add constants w/ delta-rules

max_stars_repo_name: johnyob/agda-types

max_issues_repo_name: johnyob/agda-types

max_forks_repo_name: johnyob/agda-types


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

module sets.empty where

open import level using ()

data ⊥ : Set where

⊥-elim : ∀ {i}{A : Set i} → ⊥ → A
⊥-elim ()

¬_ : ∀ {i} → Set i → Set i
¬ X = X → ⊥
infix 3 ¬_

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


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

module Categories.Functor.Continuous where

open import Level
open import Data.Product using (Σ)

open import Categories.Category
open import Categories.Functor
import Categories.Category.Construction.Cones as Con
import Categories.Diagram.Cone.Properties as Conₚ
import Categories.Diagram.Limit as Lim
import Categories.Morphism as Mor

private
  variable
    o ℓ e : Level
    C D E J : Category o ℓ e

-- G preserves the limit of F.
LimitPreserving : (G : Functor C D) {F : Functor J C} (L : Lim.Limit F) → Set _
LimitPreserving {C = C} {D = D} G {F} L = Σ (Lim.Limit (G ∘F F)) λ L′ → G.F₀ (Lim.Limit.apex L) ≅ Lim.Limit.apex L′
  where module F = Functor F
        module G = Functor G
        open Mor D

-- continuous functors preserves all limits.
Continuous : ∀ o ℓ e (G : Functor C D) → Set _
Continuous {C = C} o ℓ e G = ∀ {J : Category o ℓ e} {F : Functor J C} (L : Lim.Limit F) → LimitPreserving G L

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
{-# OPTIONS --without-K #-}
module UnivalenceFiniteTypes where

open import Data.Empty
open import Data.Unit
open import Data.Unit.Core
open import Data.Nat renaming (_⊔_ to _⊔ℕ_)
open import Data.Sum renaming (map to _⊎→_)
open import Data.Product renaming (map to _×→_)
open import Function renaming (_∘_ to _○_)

open import FT
open import SimpleHoTT
open import Equivalences
open import TypeEquivalences
open import Path2Equiv
open import FT-Nat
open import Inspect
open import LeftCancellation
open import Equiv2Path

-- univalence
{-  This does not typecheck in reasonable time.
univalence₁ : {B₁ B₂ : FT} →
  (e : ⟦ B₁ ⟧ ≃ ⟦ B₂ ⟧) → path2equiv (equiv2path e) ≡ e
univalence₁ {B₁} {B₂} (f , feq) with equiv₂ feq
... | mkqinv g  α  β = {!!}
-}

-- and this can't possibly be true!
-- note that even the "normal form" of equiv2path idequiv (ctrl-C ctrl-N)
-- is an absolutely enormous term.
univalence₂ : {B₁ B₂ : FT} → (p : B₁ ⇛ B₂) → equiv2path (path2equiv p) ≡ p
univalence₂ unite₊⇛ = {!!}
univalence₂ uniti₊⇛ = {!!}
univalence₂ swap₊⇛ = {!!}
univalence₂ assocl₊⇛ = {!!}
univalence₂ assocr₊⇛ = {!!}
univalence₂ unite⋆⇛ = {!!}
univalence₂ uniti⋆⇛ = {!!}
univalence₂ swap⋆⇛ = {!!}
univalence₂ assocl⋆⇛ = {!!}
univalence₂ assocr⋆⇛ = {!!}
univalence₂ distz⇛ = {!!}
univalence₂ factorz⇛ = {!!}
univalence₂ dist⇛ = {!!}
univalence₂ factor⇛ = {!!}
univalence₂ id⇛ = {!!}
univalence₂ (sym⇛ p) = {!!}
univalence₂ (p ◎ q) = {!!}
univalence₂ (p ⊕ q) = {!!}
univalence₂ (p ⊗ q) = {!!}

{-
univalence : {B₁ B₂ : FT} → (B₁ ⇛ B₂) ≃ (⟦ B₁ ⟧ ≃ ⟦ B₂ ⟧)
univalence =
  (path2equiv , equiv₁ (mkqinv equiv2path univalence₁ univalence₂))
-}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module collects the property definitions for left-scaling
-- (LeftDefs), right-scaling (RightDefs), and both (BiDefs).
------------------------------------------------------------------------

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

open import Relation.Binary

module Algebra.Module.Definitions where

  open import Algebra.Core

  import Algebra.Module.Definitions.Left as L
  import Algebra.Module.Definitions.Right as R
  import Algebra.Module.Definitions.Bi as B

  module LeftDefs = L
  module RightDefs = R
  module BiDefs = B


text:
open import Relation.Binary.PropositionalEquality

open import Data.Nat
open import Data.Nat.Properties using (+-suc)

open import Data.Product renaming (_×_ to _∧_)
open import Data.Sum renaming (_⊎_ to _∨_ ; inj₁ to left ; inj₂ to right)

{- 5.1 Extrinsic approach -}

div2 : ℕ → ℕ
div2 zero = zero
div2 (suc zero) = zero
div2 (suc (suc n)) = 1 + div2 n

test5 : ℕ
test5 = div2 (suc (suc (suc (suc (suc zero)))))

suc-≡ : {m n : ℕ} → (m ≡ n) → (suc m ≡ suc n)
suc-≡ refl = refl

div2-correct : (n : ℕ) → (2 * div2 n ≡ n) ∨ (suc (2 * div2 n) ≡ n)
div2-correct zero = left refl
div2-correct (suc zero) = right refl
div2-correct (suc (suc n)) with div2-correct n
div2-correct (suc (suc n)) | left even rewrite +-suc (div2 n) (div2 n + 0) = left (suc-≡ (suc-≡ even))
div2-correct (suc (suc n)) | right odd rewrite +-suc (div2 n) (div2 n + 0) = right (suc-≡ (suc-≡ odd))

{- 5.2 Intrinsic approach -}

{- There might be a more elegant way to rewrite this rather than using trans directly here -}
div2' : (n : ℕ) → Σ ℕ (λ q → (2 * q ≡ n) ∨ (suc (2 * q) ≡ n))
div2' zero = zero , (left refl)
div2' (suc zero) = zero , (right refl)
div2' (suc (suc n)) with proj₂ (div2' n)
...                 | left even =
                            1 + proj₁ (div2' n) ,
                            left ( suc-≡ (trans (+-suc (proj₁ (div2' n)) (proj₁ (div2' n) + 0)) (suc-≡ even) ))
...                 | right odd =
                            1 + proj₁ (div2' n) ,
                            right (suc-≡ (suc-≡ (trans (+-suc (proj₁ (div2' n)) (proj₁ (div2' n) + 0)) odd)))

max_stars_repo_name: erwinkn/program-eq-proof

max_issues_repo_name: erwinkn/program-eq-proof

max_forks_repo_name: erwinkn/program-eq-proof


text:
------------------------------------------------------------------------
-- Some results about various forms of coinductively defined weak
-- bisimilarity for the delay monad
------------------------------------------------------------------------

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

open import Prelude

module Bisimilarity.Weak.Delay-monad {a} {A : Type a} where

open import Delay-monad
open import Delay-monad.Bisimilarity as DB using (force)
import Delay-monad.Bisimilarity.Negative as DN
open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude.Size

open import Function-universe equality-with-J hiding (id; _∘_)
open import Function-universe.Size equality-with-J

import Bisimilarity.Delay-monad as SD
import Bisimilarity.Weak.Alternative.Equational-reasoning-instances
import Bisimilarity.Weak.Equational-reasoning-instances
open import Bisimilarity.Weak.Equivalent
open import Equational-reasoning
import Expansion.Delay-monad as ED
open import Labelled-transition-system.Delay-monad A

open import Bisimilarity delay-monad using ([_]_∼_)
open import Bisimilarity.Weak delay-monad
open import Bisimilarity.Weak.Alternative delay-monad as AW
  using (force)
open import Expansion delay-monad as BE using ([_]_≳_; _≳_)

------------------------------------------------------------------------
-- Several definitions of weak bisimilarity are pointwise logically
-- equivalent

-- Emulations of the constructors DW.later, DW.laterˡ and DW.laterʳ.

later-cong : ∀ {i x y} →
             [ i ] force x ≈′ force y → [ i ] later x ≈ later y
later-cong x≈′y =
  ⟨ (λ { later → _ , ⟶→⇒̂ later , x≈′y })
  , (λ { later → _ , ⟶→⇒̂ later , x≈′y })
  ⟩

laterˡ : ∀ {i x y} → [ i ] force x ≈ y → [ i ] later x ≈ y
laterˡ x≈y =
  ⟨ (λ { later → _ , silent _ done , convert {a = a} x≈y })
  , Σ-map id (Σ-map later⇒̂ id) ∘ right-to-left x≈y
  ⟩

laterʳ : ∀ {i x y} → [ i ] x ≈ force y → [ i ] x ≈ later y
laterʳ x≈y =
  ⟨ Σ-map id (Σ-map later⇒̂ id) ∘ left-to-right x≈y
  , (λ { later → _ , silent _ done , convert {a = a} x≈y })
  ⟩

-- The direct definition of weak bisimilarity is contained in the form
-- of weak bisimilarity obtained from the transition relation.

direct→indirect : ∀ {i x y} →
                  DB.[ i ] x ≈ y → [ i ] x ≈ y
direct→indirect DB.now        = reflexive
direct→indirect (DB.later  p) = later-cong λ { .force →
                                  direct→indirect (force p) }
direct→indirect (DB.laterˡ p) = laterˡ (direct→indirect p)
direct→indirect (DB.laterʳ p) = laterʳ (direct→indirect p)

mutual

  -- The definition of weak bisimilarity obtained from the transition
  -- relation is contained in the direct one.

  indirect→direct : ∀ {i} x y → [ i ] x ≈ y → DB.[ i ] x ≈ y
  indirect→direct {i} (now x) y =
    [ i ] now x ≈ y                                  ↝⟨ (λ p → left-to-right p now) ⟩
    (∃ λ y′ → y [ just x ]⇒̂ y′ × [ i ] now x ≈′ y′)  ↝⟨ DB.≳→ ∘ ED.[just]⇒̂→≳now ∘ proj₁ ∘ proj₂ ⟩
    DB.[ i ] y ≈ now x                               ↝⟨ DB.symmetric ⟩□
    DB.[ i ] now x ≈ y                               □

  indirect→direct {i} x (now y) =
    [ i ] x ≈ now y                                  ↝⟨ (λ p → right-to-left p now) ⟩
    (∃ λ x′ → x [ just y ]⇒̂ x′ × [ i ] x′ ≈′ now y)  ↝⟨ DB.≳→ ∘ ED.[just]⇒̂→≳now ∘ proj₁ ∘ proj₂ ⟩□
    DB.[ i ] x ≈ now y                               □

  indirect→direct (later x) (later y) lx≈ly
    with left-to-right lx≈ly later

  ... | y′ , non-silent contradiction _ , _ =
    ⊥-elim (contradiction _)

  ... | y′ , silent _ (step _ later y⇒y′) , x≈′y′ =
    DB.later λ { .force →
      indirect→direct′ y⇒y′ (force x≈′y′) }

  ... | y′ , silent _ done , x≈′ly
    with right-to-left lx≈ly later

  ...   | x′ , non-silent contradiction _ , _ =
    ⊥-elim (contradiction _)

  ...   | x′ , silent _ (step _ later x⇒x′) , x′≈′y =
    DB.later λ { .force →
      DB.symmetric $
      indirect→direct′ x⇒x′ $
      symmetric (force x′≈′y) }

  ...   | x′ , silent _ done , lx≈′y =
    DB.later λ { .force →
      DB.laterˡʳ⁻¹
        (indirect→direct _ _ (force lx≈′y))
        (indirect→direct _ _ (force x≈′ly)) }

  private

    -- A lemma used by indirect→direct.

    indirect→direct′ : ∀ {i x y y′} →
                       y ⇒ y′ → [ i ] x ≈ y′ → DB.[ i ] x ≈ y
    indirect→direct′ done               p = indirect→direct _ _ p
    indirect→direct′ (step _  later tr) p = DB.laterʳ (indirect→direct′ tr p)
    indirect→direct′ (step () now   _)

-- The direct definition of weak bisimilarity is logically equivalent
-- to the one obtained from the transition relation.
--
-- TODO: Are the two definitions isomorphic?

direct⇔indirect : ∀ {i x y} → DB.[ i ] x ≈ y ⇔ [ i ] x ≈ y
direct⇔indirect = record
  { to   = direct→indirect
  ; from = indirect→direct _ _
  }

-- The direct definition of weak bisimilarity is logically equivalent
-- to the alternative, coinductive form of weak bisimilarity obtained
-- from the transition relation. Note that this proof is not
-- size-preserving.

direct⇔alternative : ∀ {x y} → x DB.≈ y ⇔ x AW.≈ y
direct⇔alternative {x} {y} =
  x DB.≈ y  ↝⟨ direct⇔indirect ⟩
  x ≈ y     ↝⟨ inverse alternative⇔ ⟩□
  x AW.≈ y  □

------------------------------------------------------------------------
-- A non-existence result for the alternative, coinductive indirect
-- definition of weak bisimilarity

private

  -- If A is uninhabited, then AW._≈_ is trivial.

  uninhabited→trivial : ¬ A → ∀ x y → x AW.≈ y
  uninhabited→trivial =
    ¬ A                 ↝⟨ DB.uninhabited→trivial ⟩
    (∀ x y → x DB.≈ y)  ↝⟨ ∀-cong _ (λ _ → ∀-cong _ λ _ → _⇔_.to direct⇔alternative) ⟩
    (∀ x y → x AW.≈ y)  □

-- One can define a size-preserving "later-cong" function iff A is
-- uninhabited.

Later-cong =
  ∀ {i x y} →
  AW.[ i ] force x ≈′ force y → AW.[ i ] later x ≈ later y

size-preserving-later-cong⇔uninhabited : Later-cong ⇔ ¬ A
size-preserving-later-cong⇔uninhabited = record
  { to   = Later-cong                ↝⟨ (λ later-cong → now≈never (λ {i} → later-cong {i})) ⟩
           (∀ x → now x AW.≈ never)  ↝⟨ ∀-cong _ (λ _ → _⇔_.from direct⇔alternative) ⟩
           (∀ x → now x DB.≈ never)  ↝⟨ (λ hyp → DB.now≉never ∘ hyp) ⟩□
           ¬ A                       □
  ; from = ¬ A                 ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x AW.≈ y)  ↝⟨ (λ trivial {_ _ _} _ → trivial _ _) ⟩□
           Later-cong          □
  }
  where

  module _ (later-cong : Later-cong) where

    now≈never : ∀ {i} x → AW.[ i ] now x ≈ never
    now≈never x =
      now x                         ∼⟨ ⇒alternative (laterʳ reflexive) ⟩
      later (λ { .force → now x })  ∼⟨ later-cong (λ { .force → now≈never x }) ⟩■
      never

------------------------------------------------------------------------
-- Some non-existence results for the standard indirect definition of
-- weak bisimilarity

-- There is a transitivity proof that takes weak bisimilarity and
-- expansion to expansion iff A is uninhabited.

Transitivity-≈≳≳ = {x y z : Delay A ∞} → x ≈ y → y ≳ z → x ≳ z
Transitivity-≳≈≳ = {x y z : Delay A ∞} → x ≳ y → y ≈ z → x ≳ z

transitive-≈≳≳⇔uninhabited : Transitivity-≈≳≳ ⇔ ¬ A
transitive-≈≳≳⇔uninhabited =
  Transitivity-≈≳≳     ↝⟨ inverse $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                          →-cong _ direct⇔indirect (→-cong _ ED.direct⇔indirect ED.direct⇔indirect) ⟩
  DN.Transitivity-≈≳≳  ↝⟨ DN.transitive-≈≳≳⇔uninhabited ⟩□
  ¬ A                  □

transitive-≳≈≳⇔uninhabited : Transitivity-≳≈≳ ⇔ ¬ A
transitive-≳≈≳⇔uninhabited =
  Transitivity-≳≈≳     ↝⟨ inverse $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                          →-cong _ ED.direct⇔indirect (→-cong _ direct⇔indirect ED.direct⇔indirect) ⟩
  DN.Transitivity-≳≈≳  ↝⟨ DN.transitive-≳≈≳⇔uninhabited ⟩□
  ¬ A                  □

-- There is a transitivity proof that preserves the size of the second
-- argument iff A is uninhabited.

Transitivityʳ =
  ∀ {i} {x y z : Delay A ∞} →
  x ≈ y → [ i ] y ≈ z → [ i ] x ≈ z

size-preserving-transitivityʳ⇔uninhabited : Transitivityʳ ⇔ ¬ A
size-preserving-transitivityʳ⇔uninhabited =
  Transitivityʳ       ↝⟨ inverse $ implicit-∀-size-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                         →-cong _ direct⇔indirect $ →-cong _ direct⇔indirect direct⇔indirect ⟩
  DN.Transitivity-≈ʳ  ↝⟨ DN.size-preserving-transitivity-≈ʳ⇔uninhabited ⟩□
  ¬ A                 □

-- There is a transitivity proof that preserves the size of the first
-- argument iff A is uninhabited.

Transitivityˡ =
  ∀ {i} {x y z : Delay A ∞} →
  [ i ] x ≈ y → y ≈ z → [ i ] x ≈ z

size-preserving-transitivityˡ⇔uninhabited : Transitivityˡ ⇔ ¬ A
size-preserving-transitivityˡ⇔uninhabited =
  Transitivityˡ       ↝⟨ inverse $ implicit-∀-size-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                         →-cong _ direct⇔indirect $ →-cong _ direct⇔indirect direct⇔indirect ⟩
  DN.Transitivity-≈ˡ  ↝⟨ DN.size-preserving-transitivity-≈ˡ⇔uninhabited ⟩□
  ¬ A                 □

-- There is a transitivity proof that preserves the size of the second
-- argument, a strong bisimilarity, iff A is uninhabited.

Transitivity-≈∼ʳ =
  ∀ {i} {x y z : Delay A ∞} →
  x ≈ y → [ i ] y ∼ z → [ i ] x ≈ z

size-preserving-transitivity-≈∼ʳ⇔uninhabited : Transitivity-≈∼ʳ ⇔ ¬ A
size-preserving-transitivity-≈∼ʳ⇔uninhabited =
  Transitivity-≈∼ʳ     ↝⟨ inverse $ implicit-∀-size-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                          →-cong _ direct⇔indirect $ →-cong _ SD.direct⇔indirect direct⇔indirect ⟩
  DN.Transitivity-≈∼ʳ  ↝⟨ DN.size-preserving-transitivity-≈∼ʳ⇔uninhabited ⟩□
  ¬ A                  □

-- There is a transitivity proof that preserves the size of the first
-- argument, a strong bisimilarity, iff A is uninhabited.

Transitivity-∼≈ˡ =
  ∀ {i} {x y z : Delay A ∞} →
  [ i ] x ∼ y → y ≈ z → [ i ] x ≈ z

size-preserving-transitivity-∼≈ˡ⇔uninhabited : Transitivity-∼≈ˡ ⇔ ¬ A
size-preserving-transitivity-∼≈ˡ⇔uninhabited =
  Transitivity-∼≈ˡ     ↝⟨ inverse $ implicit-∀-size-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                          →-cong _ SD.direct⇔indirect $ →-cong _ direct⇔indirect direct⇔indirect ⟩
  DN.Transitivity-∼≈ˡ  ↝⟨ DN.size-preserving-transitivity-∼≈ˡ⇔uninhabited ⟩□
  ¬ A                  □

-- There is a transitivity-like proof that preserves the size of the
-- first argument, an expansion, iff A is uninhabited.

Transitivity-≳≈ˡ =
  ∀ {i} {x y z : Delay A ∞} →
  [ i ] x ≳ y → y ≈ z → [ i ] x ≈ z

size-preserving-transitivity-≳≈ˡ⇔uninhabited : Transitivity-≳≈ˡ ⇔ ¬ A
size-preserving-transitivity-≳≈ˡ⇔uninhabited =
  Transitivity-≳≈ˡ     ↝⟨ inverse $ implicit-∀-size-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                          →-cong _ ED.direct⇔indirect (→-cong _ direct⇔indirect direct⇔indirect) ⟩
  DN.Transitivity-≳≈ˡ  ↝⟨ DN.size-preserving-transitivity-≳≈ˡ⇔uninhabited ⟩□
  ¬ A                  □

-- There is a transitivity-like proof that takes an expansion as the
-- first argument, and preserves the size of both arguments, iff A is
-- uninhabited.

Transitivity-≳≈ =
  ∀ {i} {x y z : Delay A ∞} →
  [ i ] x ≳ y → [ i ] y ≈ z → [ i ] x ≈ z

size-preserving-transitivity-≳≈⇔uninhabited : Transitivity-≳≈ ⇔ ¬ A
size-preserving-transitivity-≳≈⇔uninhabited =
  Transitivity-≳≈     ↝⟨ inverse $ implicit-∀-size-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                         →-cong _ ED.direct⇔indirect (→-cong _ direct⇔indirect direct⇔indirect) ⟩
  DN.Transitivity-≳≈  ↝⟨ DN.size-preserving-transitivity-≳≈⇔uninhabited ⟩□
  ¬ A                 □

-- There is a transitivity-like proof that preserves the size of the
-- second argument, an expansion (with the arguments swapped), iff A
-- is uninhabited.

Transitivity-≈≲ʳ =
  ∀ {i} {x y z : Delay A ∞} →
  x ≈ y → [ i ] z ≳ y → [ i ] x ≈ z

size-preserving-transitivity-≈≲ʳ⇔uninhabited : Transitivity-≈≲ʳ ⇔ ¬ A
size-preserving-transitivity-≈≲ʳ⇔uninhabited =
  Transitivity-≈≲ʳ     ↝⟨ inverse $ implicit-∀-size-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                          →-cong _ direct⇔indirect (→-cong _ ED.direct⇔indirect direct⇔indirect) ⟩
  DN.Transitivity-≈≲ʳ  ↝⟨ DN.size-preserving-transitivity-≈≲ʳ⇔uninhabited ⟩□
  ¬ A                  □

-- There is a transitivity-like proof that takes an expansion (with
-- the arguments swapped) as the second argument, and preserves the
-- size of both arguments, iff A is uninhabited.

Transitivity-≈≲ =
  ∀ {i} {x y z : Delay A ∞} →
  [ i ] x ≈ y → [ i ] z ≳ y → [ i ] x ≈ z

size-preserving-transitivity-≈≲⇔uninhabited : Transitivity-≈≲ ⇔ ¬ A
size-preserving-transitivity-≈≲⇔uninhabited =
  Transitivity-≈≲     ↝⟨ inverse $ implicit-∀-size-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                         →-cong _ direct⇔indirect (→-cong _ ED.direct⇔indirect direct⇔indirect) ⟩
  DN.Transitivity-≈≲  ↝⟨ DN.size-preserving-transitivity-≈≲⇔uninhabited ⟩□
  ¬ A                 □

-- There is a transitivity-like proof that preserves the size of the
-- first argument, and takes an expansion as the second argument, iff
-- A is uninhabited.

Transitivity-≈≳ˡ =
  ∀ {i} {x y z : Delay A ∞} →
  [ i ] x ≈ y → y ≳ z → [ i ] x ≈ z

size-preserving-transitivity-≈≳ˡ⇔uninhabited : Transitivity-≈≳ˡ ⇔ ¬ A
size-preserving-transitivity-≈≳ˡ⇔uninhabited =
  Transitivity-≈≳ˡ     ↝⟨ inverse $ implicit-∀-size-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                          →-cong _ direct⇔indirect (→-cong _ ED.direct⇔indirect direct⇔indirect) ⟩
  DN.Transitivity-≈≳ˡ  ↝⟨ DN.size-preserving-transitivity-≈≳ˡ⇔uninhabited ⟩□
  ¬ A                  □

------------------------------------------------------------------------
-- A non-existence result for both indirect definitions of weak
-- bisimilarity

-- The function ⇒alternative translating from the standard indirect
-- definition of weak bisimilarity to the alternative, coinductive one
-- can be made size-preserving iff A is uninhabited.

size-preserving-⇒alternative⇔uninhabited :
  (∀ {i p q} → [ i ] p ≈ q → AW.[ i ] p ≈ q) ⇔ ¬ A
size-preserving-⇒alternative⇔uninhabited = record
  { to =
      (∀ {i p q} → [ i ] p ≈ q → AW.[ i ] p ≈ q)  ↝⟨ (λ ⇒alternative x≈y y≈z →
                                                        alternative⇒ (transitive {a = a} (⇒alternative x≈y) (⇒alternative y≈z))) ⟩
      Transitivityʳ                               ↝⟨ _⇔_.to size-preserving-transitivityʳ⇔uninhabited ⟩□
      ¬ A                                         □
  ; from =
      ¬ A                                         ↝⟨ uninhabited→trivial ⟩
      (∀ x y → x AW.≈ y)                          ↝⟨ (λ trivial {_ _ _} _ → trivial _ _) ⟩□
      (∀ {i p q} → [ i ] p ≈ q → AW.[ i ] p ≈ q)  □
  }

------------------------------------------------------------------------
-- More lemmas

-- If x and y both make non-silent transitions of the same kind,
-- then they are weakly bisimilar.

⟶-with-equal-labels→≈ :
  ∀ {x x′ y y′ μ} →
  ¬ Silent μ → x [ μ ]⟶ x′ → y [ μ ]⟶ y′ → x ≈ y
⟶-with-equal-labels→≈ _  now   now = reflexive
⟶-with-equal-labels→≈ ¬s later _   = ⊥-elim (¬s _)

[]⇒-with-equal-labels→≈ :
  ∀ {x x′ y y′ μ} →
  ¬ Silent μ → x [ μ ]⇒ x′ → y [ μ ]⇒ y′ → x ≈ y
[]⇒-with-equal-labels→≈
  {x = x} {y = y} ¬s
  (steps {p′ = x′} x⇒x′ x′⟶x″ x″⇒x‴)
  (steps {p′ = y′} y⇒y′ y′⟶y″ y″⇒y‴) =

  x   ∼⟨ direct→indirect (DB.≳→ (ED.⇒→≳ x⇒x′)) ⟩
  x′  ∼⟨ ⟶-with-equal-labels→≈ ¬s x′⟶x″ y′⟶y″ ⟩
  y′  ∼⟨ symmetric (direct→indirect (DB.≳→ (ED.⇒→≳ y⇒y′))) ⟩■
  y

⇒̂-with-equal-labels→≈ :
  ∀ {x x′ y y′ μ} →
  ¬ Silent μ → x [ μ ]⇒̂ x′ → y [ μ ]⇒̂ y′ → x ≈ y
⇒̂-with-equal-labels→≈ ¬s (non-silent _ x⇒x′) (non-silent _ y⇒y′) =
  []⇒-with-equal-labels→≈ ¬s x⇒x′ y⇒y′
⇒̂-with-equal-labels→≈ ¬s   (silent s _) = ⊥-elim (¬s s)
⇒̂-with-equal-labels→≈ ¬s _ (silent s _) = ⊥-elim (¬s s)

⟶̂-with-equal-labels→≈ :
  ∀ {x x′ y y′ μ} →
  ¬ Silent μ → x [ μ ]⟶̂ x′ → y [ μ ]⟶̂ y′ → x ≈ y
⟶̂-with-equal-labels→≈ ¬s x⟶̂x′ y⟶̂y′ =
  ⇒̂-with-equal-labels→≈ ¬s (⟶̂→⇒̂ x⟶̂x′) (⟶̂→⇒̂ y⟶̂y′)

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
module Signature where

open import Function renaming (const to K)
open import Category.Monad.Predicate
open import Data.Sum
open import Data.Product
open import Data.Container.Indexed hiding (_∈_)
open import Data.Container.Indexed.Combinator
  renaming (_⊎_ to _⊎^C_; _×_ to _×^C_)
open import Data.Container.Indexed.FreeMonad
open import Data.Char
open import Data.String
open import Relation.Unary
open import Relation.Binary.PropositionalEquality

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

data Prompt : Set where
  addFeed search : Prompt

data Mode : Set where
  cmd   : Mode
  input : Prompt → Mode

data Dir : Set where
  up down : Dir

postulate
  Feed : Set

Hårss : Mode ▷ Mode
Hårss =
  {- move    -} ｛ cmd ｝ ∩ K Dir ◃
                U /
                (λ _ _ → cmd) ⊎^C
  {- prompt  -} ｛ cmd ｝ ∩ K Prompt ◃
                U /
                (λ { (_ , p) _ → input p}) ⊎^C
  {- putChar -} (⋃[ p ∶ Prompt ] ｛ input p ｝) ∩ K Char ◃
                U /
                (λ { {._} ((p , refl) , _) _ → input p }) ⊎^C
  {- done    -} ⋃[ p ∶ Prompt ] ｛ input p ｝ ◃
                K (String × Prompt) /
                (λ _ _ → cmd) ⊎^C
  {- fetch   -} ｛ cmd ｝ ◃
                K Feed /
                (λ _ _ → cmd) ⊎^C
  {- searchN -} ｛ input search ｝ ◃
                K String /
                (λ _ _ → input search)

pattern moveP d = inj₁ (refl , d)

move : Dir → cmd ∈ Hårss ⋆ (U ∩ ｛ cmd ｝)
move d = generic (moveP d)

pattern promptP p = inj₂ (inj₁ (refl , p))

prompt : (p : Prompt) → cmd ∈ Hårss ⋆ (U ∩ ｛ input p ｝)
prompt p = generic (promptP p)

pattern putCharP c = inj₂ (inj₂ (inj₁ ((_ , refl) , c)))

putChar : ∀ {p} → Char → input p ∈ Hårss ⋆ (U ∩ ｛ input p ｝)
putChar c = generic (putCharP c)

pattern doneP = inj₂ (inj₂ (inj₂ (inj₁ (_ , refl))))

done : ∀ {p} → input p ∈ Hårss ⋆ (K (String × Prompt) ∩ ｛ cmd ｝)
done = generic doneP

pattern fetchP = inj₂ (inj₂ (inj₂ (inj₂ (inj₁ refl))))

fetch : cmd ∈ Hårss ⋆ (K Feed ∩ ｛ cmd ｝)
fetch = generic fetchP

pattern searchNextP = inj₂ (inj₂ (inj₂ (inj₂ (inj₂ refl))))

searchNext : input search ∈ Hårss ⋆ (K String ∩ ｛ input search ｝)
searchNext = generic searchNextP

prog : cmd ∈ Hårss ⋆ (K (String × Prompt) ∩ ｛ cmd ｝)
prog =
  move down >>
  prompt search >>
  putChar 'a' >>
  putChar 'p' >>
  putChar 'a' >>
  done
  where
  open RawPMonad rawPMonad

max_stars_repo_name: stevana/haarss

max_issues_repo_name: stevana/haarss

max_forks_repo_name: stevana/haarss


text:
module Extensions.Vec where

open import Data.Product hiding (map; zip)
open import Data.Nat
open import Data.Fin
open import Data.Vec
open import Data.Product hiding (map)
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Data.List as L using ()
open import Data.List.Properties
open import Relation.Binary.HeterogeneousEquality as H using ()
open ≡-Reasoning public

private
  module HR = H.≅-Reasoning

[]=-functional : ∀ {a n} {A : Set a} (l : Vec A n) i →
                   ∀ {x y : A} → l [ i ]= x → l [ i ]= y → x ≡ y
[]=-functional .(_ ∷ _) _ here here = refl
[]=-functional .(_ ∷ _) .(suc _) (there p) (there q) = []=-functional _ _ p q

lookup⋆map : ∀ {a b : Set} {n} (v : Vec a n) (f : a → b) x →
             f (lookup x v) ≡ lookup x (map f v)
lookup⋆map [] f ()
lookup⋆map (x ∷ xs) f zero = refl
lookup⋆map (x ∷ xs) f (suc y) = lookup⋆map xs f y

strong-lookup : ∀ {a} {A : Set a} {n} → (v : Vec A n) → (i : Fin n) → ∃ λ x → v [ i ]= x
strong-lookup (x ∷ v) zero = x , here
strong-lookup (x ∷ v) (suc i) with strong-lookup v i
... | y , p = y , there p

∷⋆map : ∀ {a b : Set} {n} (f : a → b) (x : a) (xs : Vec a n) → map f (x ∷ xs) ≡ f x ∷ (map f xs)
∷⋆map f x [] = refl
∷⋆map f x (y ∷ xs) = cong (_∷_ (f x)) (∷⋆map f y xs)

-- TODO replace with []=↔lookup
∈⟶index : ∀ {A : Set} {n} {v : Vec A n} {a : A} → a ∈ v → ∃ λ i → lookup i v ≡ a
∈⟶index here = zero , refl
∈⟶index (there e) with ∈⟶index e
∈⟶index (there e) | i , lookup-i≡a = suc i , lookup-i≡a

∈⋆map : ∀ {A B : Set} {n} {v : Vec A n} {a} → a ∈ v → (f : A → B) → (f a) ∈ (map f v)
∈⋆map here f = here
∈⋆map (there a∈v) f = there (∈⋆map a∈v f)

∷-cong : ∀ {l n n'} {A : Set l} {x : A} {xs : Vec A n} {xs' : Vec A n'} →
         n ≡ n' →
         xs H.≅ xs' →
         x ∷ xs H.≅ x ∷ xs'
∷-cong refl H.refl = H.refl

fromList-map : ∀ {l} {A B : Set l} (f : A → B) (xs : L.List A) →
               (fromList ((L.map f xs))) H.≅ (map f (fromList xs))
fromList-map f L.[] = H.refl
fromList-map f (x L.∷ xs) = ∷-cong (length-map _ xs) (fromList-map f xs)

length-toList : ∀ {A : Set } {n} (v : Vec A n) → L.length (toList v) ≡ n
length-toList [] = refl
length-toList (x ∷ v) = cong suc (length-toList v)

length-map-toList : ∀ {A B : Set} {n} {f : A → B} (v : Vec A n) → L.length (L.map f (toList v)) ≡ n
length-map-toList {n = n} {f} v = begin
  L.length (L.map f (toList v))
    ≡⟨ length-map f (toList v) ⟩
  L.length (toList v)
    ≡⟨ length-toList v ⟩
  n ∎

lookup-≔ : ∀ {n k} {A : Set k} (v : Vec A n) i (a : A) → lookup i (v [ i ]≔ a) ≡ a
lookup-≔ (x ∷ v) zero a = refl
lookup-≔ (x ∷ v) (suc i) a = lookup-≔ v i a

infixl 4 _⊑_
data _⊑_ {a} {A : Set a} : ∀ {n m} → Vec A n -> Vec A m -> Set where
  []  : ∀ {n} {xs : Vec A n} → [] ⊑ xs
  _∷_ : ∀ {n m} x {xs : Vec A n} {ys : Vec A m} -> xs ⊑ ys -> (x ∷ xs) ⊑ (x ∷ ys)

infixl 4 _⊒_
_⊒_ : ∀ {a} {A : Set a} {n m} → Vec A n -> Vec A m -> Set
xs ⊒ ys = ys ⊑ xs

open import Relation.Binary.Core using (Reflexive; Transitive)

⊑-refl : ∀ {a n} {A : Set a} → Reflexive (_⊑_ {A = A} {n = n})
⊑-refl {x = []} = []
⊑-refl {x = x ∷ xs} = x ∷ ⊑-refl

⊑-trans : ∀ {a n m k} {A : Set a} {xs : Vec A n} {ys : Vec A m} {zs : Vec A k} →
          xs ⊑ ys → ys ⊑ zs → xs ⊑ zs
⊑-trans [] [] = []
⊑-trans [] (x ∷ b) = []
⊑-trans (x ∷ xs) (.x ∷ ys) = x ∷ (⊑-trans xs ys)

∷ʳ-⊒ : ∀ {a} {A : Set a} (x : A) {n} (xs : Vec A n) → xs ∷ʳ x ⊒ xs
∷ʳ-⊒ x [] = []
∷ʳ-⊒ x (x₁ ∷ Σ₁) = x₁ ∷ (∷ʳ-⊒ x Σ₁)

xs⊒ys-length : ∀ {a n m} {A : Set a} {xs : Vec A n} {ys : Vec A m} → xs ⊒ ys → n ≥ m
xs⊒ys-length [] = z≤n
xs⊒ys-length (x ∷ p) = s≤s (xs⊒ys-length p)

xs⊒ys[i] : ∀ {a n m} {A : Set a} {xs : Vec A n} {ys : Vec A m} {i y} →
           xs [ i ]= y → (p : ys ⊒ xs) → ys [ inject≤ i (xs⊒ys-length p) ]= y
xs⊒ys[i] here (x ∷ q) = here
xs⊒ys[i] (there p) (x ∷ q) = there (xs⊒ys[i] p q)

∷ʳ[length] : ∀ {a n} {A : Set a} (l : Vec A n) x → ∃ λ i → (l ∷ʳ x) [ i ]= x
∷ʳ[length] [] _ = , here
∷ʳ[length] (x ∷ Σ) y with ∷ʳ[length] Σ y
∷ʳ[length] (x ∷ Σ₁) y | i , p = (suc i) , there p

-- Moar All properties

open import Data.Vec.All

all-lookup' : ∀ {a p} {A : Set a} {P : A → Set p} {k} {xs : Vec A k} {i x} →
              xs [ i ]= x → All P xs → P x
all-lookup' here (px ∷ _) = px
all-lookup' (there p) (_ ∷ xs) = all-lookup' p xs

-- proof matters; update a particular witness of a property
_All[_]≔_ : ∀ {a p} {A : Set a} {P : A → Set p} {k} {xs : Vec A k} {i x} →
            All P xs → xs [ i ]= x → P x → All P xs
[] All[ () ]≔ px
(px ∷ xs) All[ here ]≔ px' = px' ∷ xs
(px ∷ xs) All[ there i ]≔ px' = px ∷ (xs All[ i ]≔ px')

_all-∷ʳ_ : ∀ {a n p} {A : Set a} {l : Vec A n} {x} {P : A → Set p} → All P l → P x → All P (l ∷ʳ x)
_all-∷ʳ_ [] q = q ∷ []
_all-∷ʳ_ (px ∷ p) q = px ∷ (p all-∷ʳ q)


text:
module _ where

open import Agda.Primitive
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

record Category {o h} : Set (lsuc (o ⊔ h)) where
  no-eta-equality
  constructor con

  field
    Obj : Set o
    Hom : Obj → Obj → Set h

  field
    id : ∀ {X : Obj} → Hom X X
    comp : ∀ {X Y Z} → Hom Y Z → Hom X Y → Hom X Z
    id-left : ∀ {X Y} (f : Hom X Y) → comp id f ≡ f

open Category

postulate
  isSet : ∀ {l} → (X : Set l) → Set l

hSets : (o : Level) → Category
hSets o .Obj                 = Σ (Set o) isSet
hSets o .Hom (A , _) (B , _) = A → B
hSets o .id                  = \ x → x
hSets o .comp f g            = \ x → f (g x)
hSets o .id-left f           = refl


text:
-- Andreas, 2015-09-07  Issue reported by identicalsnowflake

data D : Set1 where
  field
    A : Set

-- WAS: Internal error (on master)

-- NOW:
-- Illegal declaration in data type definition
--   field A : Set
-- when scope checking the declaration
--   data D where
--     field A : Set


text:
module Issue175b where

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

data Bool : Set where
  true : Bool
  false : Bool
{-# BUILTIN BOOL Bool #-}
{-# BUILTIN TRUE true #-}
{-# BUILTIN FALSE false #-}

postulate ℝ : Set
{-# BUILTIN FLOAT ℝ #-}

primitive
  -- ℝ functions
  primFloatMinus : ℝ -> ℝ -> ℝ
  primFloatNumericalLess : ℝ -> ℝ -> Bool

_<_ : ℝ -> ℝ -> Bool
a < b = primFloatNumericalLess a b

data _≤_ : ℝ -> ℝ -> Set where
   ≤_ : {x y : ℝ} -> (x < y) ≡ true -> x ≤ y

--absolute value
[|_|] : ℝ -> ℝ
[| a |] with (a < 0.0)
[| a |] | true = primFloatMinus 0.0 a
[| a |] | false = a

--error variable
ε : ℝ
ε = 1.0e-5

-- two floating point numbers can be said to be equal if their
-- difference is less than the given error variable
postulate
  reflℝ : {a b : ℝ} -> [| primFloatMinus a b |] ≤ ε -> a ≡ b

test : 1.0 ≡ 1.0000001
test =  reflℝ (≤ refl)

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
module Nom where

open import Basics
open import Pr

data Nom : Set where
  Ze : Nom
  Su : Nom -> Nom
  Pu : Nom -> Nom

_NomQ_ : Nom -> Nom -> Pr
Ze NomQ Ze = tt
Ze NomQ (Su y) = ff
Ze NomQ (Pu y) = ff
(Su x) NomQ Ze = ff
(Su x) NomQ (Su y) = x eq y
(Su x) NomQ (Pu y) = ff
(Pu x) NomQ Ze = ff
(Pu x) NomQ (Su y) = ff
(Pu x) NomQ (Pu y) = x eq y

nomQ : {x y : Nom} -> [| (x eq y) => (x NomQ y) |]
nomQ {Ze} refl = _
nomQ {Su x} refl = refl
nomQ {Pu x} refl = refl

nomEq : (x y : Nom) -> Decision (x eq y)
nomEq Ze Ze = yes refl
nomEq Ze (Su y) = no nomQ
nomEq Ze (Pu y) = no nomQ
nomEq (Su x) Ze = no nomQ
nomEq (Su x) (Su y) with nomEq x y
nomEq (Su x) (Su .x) | yes refl = yes refl
nomEq (Su x) (Su y) | no p = no (p o nomQ)
nomEq (Su x) (Pu y) = no nomQ
nomEq (Pu x) Ze = no nomQ
nomEq (Pu x) (Su y) = no nomQ
nomEq (Pu x) (Pu y) with nomEq x y
nomEq (Pu x) (Pu .x) | yes refl = yes refl
nomEq (Pu x) (Pu y)  | no p = no (p o nomQ)

data Nat : Set where
  ze : Nat
  su : Nat -> Nat

pfog : Nom -> Nat
pfog Ze = ze
pfog (Su x) = pfog x
pfog (Pu x) = su (pfog x)

NatGE : Nat -> Nat -> Bool
NatGE ze _ = false
NatGE (su _) ze = true
NatGE (su x) (su y) = NatGE x y

_>_ : Nat -> Nat -> Pr
x > y = So (NatGE x y)

_>?_ : (x y : Nat) -> Decision (x > y)
x >? y = so (NatGE x y)

_P>_ : Nom -> Nom -> Pr
x P> y = pfog x > pfog y

_S+_ : Nat -> Nom -> Nom
ze S+ y = y
su x S+ y = Su (x S+ y)

PSlem : (n : Nat)(x : Nom) -> Id (pfog (n S+ x)) (pfog x)
PSlem ze x = refl
PSlem (su n) x = PSlem n x

Plem : (x y : Nom) -> [| x P> y |] -> [| Pu x P> y |]
Plem _ Ze p = _
Plem x (Su y) p = Plem x y p
Plem Ze (Pu y) ()
Plem (Su x) (Pu y) p = Plem x (Pu y) p
Plem (Pu x) (Pu y) p = Plem x y p

asym : (x : Nom) -> [| ∼ (x P> x) |]
asym Ze ()
asym (Su x) p = asym x p
asym (Pu x) p = asym x p

record Nominal (X : Set) : Set1 where
  field
    Everywhere  : Pow Nom -> Pow X
    everywhere  : (P Q : Pow Nom) -> [| P ==> Q |] ->
                  [| Everywhere P ==> Everywhere Q |]

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text: module Issue4954.M (_ : Set₁) where


text:
{-
  Definition of function fixpoint and Kraus' lemma
-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Functions.Fixpoint where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Path

private
  variable
    ℓ : Level
    A : Type ℓ

Fixpoint : (A → A) → Type _
Fixpoint {A = A} f = Σ A (λ x → f x ≡ x)

fixpoint : {f : A → A} → Fixpoint f → A
fixpoint = fst

fixpointPath : {f : A → A} → (p : Fixpoint f) → f (fixpoint p) ≡ fixpoint p
fixpointPath = snd

-- Kraus' lemma
-- a version not using cubical features can be found at
-- https://www.cs.bham.ac.uk/~mhe/GeneralizedHedberg/html/GeneralizedHedberg.html#21576
2-Constant→isPropFixpoint : (f : A → A) → 2-Constant f → isProp (Fixpoint f)
2-Constant→isPropFixpoint f fconst (x , p) (y , q) i = s i , t i where
  noose : ∀ x y → f x ≡ f y
  noose x y = sym (fconst x x) ∙ fconst x y
  -- the main idea is that for any path p, cong f p does not depend on p
  -- but only on its endpoints and the structure of 2-Constant f
  KrausInsight : ∀ {x y} → (p : x ≡ y) → noose x y ≡ cong f p
  KrausInsight {x} = J (λ y p → noose x y ≡ cong f p) (lCancel (fconst x x))
  -- Need to solve for a path s : x ≡ y, such that:
  -- transport (λ i → cong f s i ≡ s i) p ≡ q
  s : x ≡ y
  s = sym p ∙∙ noose x y ∙∙ q
  t' : PathP (λ i → noose x y i ≡ s i) p q
  t' i j = doubleCompPath-filler (sym p) (noose x y) q j i
  t : PathP (λ i → cong f s i ≡ s i) p q
  t = subst (λ kraus → PathP (λ i → kraus i ≡ s i) p q) (KrausInsight s) t'

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
-- Andreas, 2015-08-27 use imported rewrite rule

{-# OPTIONS --rewriting #-}

open import Common.Nat
open import Common.Equality

open import Issue1550

x+0+0+0 : ∀{x} → ((x + 0) + 0) + 0 ≡ x
x+0+0+0 = refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

module Cubical.Data.Fin.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels

open import Cubical.Data.Empty
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Sum

open import Cubical.Relation.Nullary

-- Finite types.
--
-- Currently it is most convenient to define these as a subtype of the
-- natural numbers, because indexed inductive definitions don't behave
-- well with cubical Agda. This definition also has some more general
-- attractive properties, of course, such as easy conversion back to
-- ℕ.
Fin : ℕ → Type₀
Fin n = Σ[ k ∈ ℕ ] k < n

private
  variable
    ℓ : Level
    k : ℕ

fzero : Fin (suc k)
fzero = (0 , suc-≤-suc zero-≤)

-- It is easy, using this representation, to take the successor of a
-- number as a number in the next largest finite type.
fsuc : Fin k → Fin (suc k)
fsuc (k , l) = (suc k , suc-≤-suc l)

-- Conversion back to ℕ is trivial...
toℕ : Fin k → ℕ
toℕ = fst

-- ... and injective.
toℕ-injective : ∀{fj fk : Fin k} → toℕ fj ≡ toℕ fk → fj ≡ fk
toℕ-injective {fj = fj} {fk} = ΣProp≡ (λ _ → m≤n-isProp)

-- A case analysis helper for induction.
fsplit
  : ∀(fj : Fin (suc k))
  → (fzero ≡ fj) ⊎ (Σ[ fk ∈ Fin k ] fsuc fk ≡ fj)
fsplit (0 , k<sn) = inl (toℕ-injective refl)
fsplit (suc k , k<sn) = inr ((k , pred-≤-pred k<sn) , toℕ-injective refl)

-- Fin 0 is empty
¬Fin0 : ¬ Fin 0
¬Fin0 (k , k<0) = ¬-<-zero k<0

-- The full inductive family eliminator for finite types.
finduction
  : ∀(P : ∀{k} → Fin k → Type ℓ)
  → (∀{k} → P {suc k} fzero)
  → (∀{k} {fn : Fin k} → P fn → P (fsuc fn))
  → {k : ℕ} → (fn : Fin k) → P fn
finduction P fz fs {zero} = ⊥-elim ∘ ¬Fin0
finduction P fz fs {suc k} fj
  = case fsplit fj return (λ _ → P fj) of λ
  { (inl p) → subst P p fz
  ; (inr (fk , p)) → subst P p (fs (finduction P fz fs fk))
  }

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical