text:
{-# OPTIONS --type-in-type #-}

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

Pair : Set → Set → Set;Pair
  = λ A B → (P : Set) → (A → B → P) → P

dup : ∀ {A : Set} → A → Pair A A;dup
  = λ a P p → p a a

Nat : Set;Nat
 = (n : Set) → (n → n) → n → n

zero : Nat;zero
 = λ n s z → z

suc : Nat → Nat;suc
 = λ a n s z → s (a n s z)

Vec : Set → Nat → Set;Vec
 = λ A n → (V : Nat → Set) → (∀{n} → A → V n → V (suc n)) → V zero → V n

nil : ∀ {A : Set} → Vec A zero;nil
 = λ V c n → n

cons : ∀ {A : Set}{n : Nat} → A → Vec A n → Vec A (suc n);cons
 = λ a as V c n → c a (as V c n)

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

-- Fails
-- idTest : ∀ {A} → A → A;idTest
--   = id id id id id id id id id id id id id id id id id id id id
--     id id id id id id id id id id id id id id id id id id id id

-- Fails
-- pairTest =
--   let x0  = dup Set
--       x1  = dup x0
--       x2  = dup x1
--       x3  = dup x2
--       x4  = dup x3
--       x5  = dup x4
--       x6  = dup x5
--       x7  = dup x6
--       x8  = dup x7
--       x9  = dup x8
--       x10 = dup x9
--       x11 = dup x10
--       x12 = dup x11
--       x13 = dup x12
--       x14 = dup x13
--       x15 = dup x14
--       x16 = dup x15
--       x17 = dup x16
--       x18 = dup x17
--       x19 = dup x18
--       x20 = dup x19
--   in x20

vecTest
 =
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set
   (cons Set (cons Set (cons Set (cons Set (cons Set (cons Set

   nil

   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))
   ))))))))))))))))))))))))))))))

max_stars_repo_name: int-index/smalltt

max_issues_repo_name: int-index/smalltt

max_forks_repo_name: int-index/smalltt


text:
module MLib.Prelude.TransitiveProver.Test where

open import MLib.Prelude.FromStdlib

open import Data.Nat
open import Data.Nat.Properties

open import MLib.Prelude.TransitiveProver _≤_ ≤-trans

open Search <-isStrictTotalOrder

1≤3 : 1 ≤ 3
1≤3 = s≤s z≤n

3≤5 : 3 ≤ 5
3≤5 = s≤s (s≤s (s≤s z≤n))

5≤9 : 5 ≤ 9
5≤9 = s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))

3≤6 : 3 ≤ 6
3≤6 = s≤s (s≤s (s≤s z≤n))

9≤13 : 9 ≤ 13
9≤13 = s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))))))

5≤13 : 5 ≤ 13
5≤13 = s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))

3≤3 : 3 ≤ 3
3≤3 = s≤s (s≤s (s≤s z≤n))

db : Database
db
  = (_ , _ , 1≤3)
  ∷ (_ , _ , 3≤3)
  ∷ (_ , _ , 3≤6)
  ∷ (_ , _ , 9≤13)
  ∷ (_ , _ , 3≤5)
  ∷ (_ , _ , 3≤5)
  ∷ (_ , _ , 5≤13)
  ∷ (_ , _ , 5≤9)
  ∷ []

res : 3 ≤ 9
res = s≤s (s≤s (s≤s z≤n))

test1 : tryProve db 3 9 ≡ just res
test1 = ≡.refl

test2 = findTransTargets db 1

ext: agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A categorical view of Vec
------------------------------------------------------------------------

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

module Data.Vec.Categorical {a n} where

open import Category.Applicative using (RawApplicative)
open import Category.Applicative.Indexed using (Morphism)
open import Category.Functor as Fun using (RawFunctor)
import Function.Identity.Categorical as Id
open import Category.Monad using (RawMonad)
open import Data.Fin.Base using (Fin)
open import Data.Vec.Base as Vec hiding (_⊛_)
open import Data.Vec.Properties
open import Function

------------------------------------------------------------------------
-- Functor and applicative

functor : RawFunctor (λ (A : Set a) → Vec A n)
functor = record
  { _<$>_ = map
  }

applicative : RawApplicative (λ (A : Set a) → Vec A n)
applicative = record
  { pure = replicate
  ; _⊛_  = Vec._⊛_
  }

------------------------------------------------------------------------
-- Get access to other monadic functions

module TraversableA {f F} (App : RawApplicative {f} F) where

  open RawApplicative App

  sequenceA : ∀ {A n} → Vec (F A) n → F (Vec A n)
  sequenceA []       = pure []
  sequenceA (x ∷ xs) = _∷_ <$> x ⊛ sequenceA xs

  mapA : ∀ {a} {A : Set a} {B n} → (A → F B) → Vec A n → F (Vec B n)
  mapA f = sequenceA ∘ map f

  forA : ∀ {a} {A : Set a} {B n} → Vec A n → (A → F B) → F (Vec B n)
  forA = flip mapA

module TraversableM {m M} (Mon : RawMonad {m} M) where

  open RawMonad Mon

  open TraversableA rawIApplicative public
    renaming
    ( sequenceA to sequenceM
    ; mapA      to mapM
    ; forA      to forM
    )

------------------------------------------------------------------------
-- Other

-- lookup is a functor morphism from Vec to Identity.

lookup-functor-morphism : (i : Fin n) → Fun.Morphism functor Id.functor
lookup-functor-morphism i = record
  { op     = flip lookup i
  ; op-<$> = lookup-map i
  }

-- lookup is an applicative functor morphism.

lookup-morphism : (i : Fin n) → Morphism applicative Id.applicative
lookup-morphism i = record
  { op      = flip lookup i
  ; op-pure = lookup-replicate i
  ; op-⊛    = lookup-⊛ i
  }


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax Monad | M

type
  T : 1-ary

term
  ret  : α  ->  T α
  bind : T α  α.(T β)  ->  T β | _>>=_ r10

theory
  (LU) a : α   b : α.(T β) |> bind (ret(a), x. b[x]) =  b[a]
  (RU) t : T α |> bind (t, x. ret(x)) = t
  (AS) t : T α  b : α.(T β)  c : β.(T γ) |> bind (bind (t, x.b[x]), y.c[y]) = bind (t, x. bind (b[x], y.c[y]))
-}

module Monad.Signature where

open import SOAS.Context

-- Type declaration
data MT : Set where
  T : MT → MT

open import SOAS.Syntax.Signature MT public
open import SOAS.Syntax.Build MT public

-- Operator symbols
data Mₒ : Set where
  retₒ : {α : MT} → Mₒ
  bindₒ : {α β : MT} → Mₒ

-- Term signature
M:Sig : Signature Mₒ
M:Sig = sig λ
  { (retₒ  {α})    → (⊢₀ α) ⟼₁ T α
  ; (bindₒ {α}{β}) → (⊢₀ T α) , (α ⊢₁ T β) ⟼₂ T β
  }

open Signature M:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
-- Andreas, 2016-12-31, issue #1976 raised by nad
-- Check for correct parameters in projection pattern

-- {-# OPTIONS -v tc.lhs.split:40 #-}

postulate
  A B : Set

module M (_ : Set) where

  record R : Set₂ where
    field
      F : Set₁

  open R public

open M A

wrong : M.R B
F wrong = Set

-- Expected error:
-- A != B of type Set
-- when checking that the clause F wrong = Set has type M.R B

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Agda.Builtin.Nat

data Tick : Nat → Set where
  tick : ∀ {n} → Tick (suc n)

data Tensor : ∀ n → Tick n → Set where
  ss : ∀ {n} → Tensor (1 + n) tick

tensor→a : ∀ {n s} → Tensor n s → Set
tensor→a x = {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of sums (disjoint unions)
------------------------------------------------------------------------

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

module Data.Sum.Properties where

open import Data.Sum
open import Function
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (yes; no)

module _ {a b} {A : Set a} {B : Set b} where

  inj₁-injective : ∀ {x y} → (A ⊎ B ∋ inj₁ x) ≡ inj₁ y → x ≡ y
  inj₁-injective refl = refl

  inj₂-injective : ∀ {x y} → (A ⊎ B ∋ inj₂ x) ≡ inj₂ y → x ≡ y
  inj₂-injective refl = refl

  ≡-dec : Decidable _≡_ → Decidable _≡_ → Decidable {A = A ⊎ B} _≡_
  ≡-dec dec₁ dec₂ (inj₁ x) (inj₁ y) with dec₁ x y
  ... | yes refl = yes refl
  ... | no  x≢y  = no (x≢y ∘ inj₁-injective)
  ≡-dec dec₁ dec₂ (inj₁ x) (inj₂ y) = no λ()
  ≡-dec dec₁ dec₂ (inj₂ x) (inj₁ y) = no λ()
  ≡-dec dec₁ dec₂ (inj₂ x) (inj₂ y) with dec₂ x y
  ... | yes refl = yes refl
  ... | no  x≢y  = no (x≢y ∘ inj₂-injective)

  swap-involutive : swap {A = A} {B} ∘ swap ≗ id
  swap-involutive = [ (λ _ → refl) , (λ _ → refl) ]


text:
------------------------------------------------------------------------
-- The universe used to define breadth-first manipulations of trees
------------------------------------------------------------------------

module BreadthFirst.Universe where

open import Codata.Musical.Colist using (Colist; []; _∷_)
open import Codata.Musical.Notation
open import Data.Product using (_×_; _,_)
open import Relation.Binary.PropositionalEquality using (_≡_)

open import Stream using (Stream; _≺_)
open import Tree using (Tree; node; leaf)

infixr 5 _≺_ _∷_
infixr 4 _,_
infixr 2 _⊗_

data U : Set₁ where
  tree   : (a : U) → U
  stream : (a : U) → U
  colist : (a : U) → U
  _⊗_    : (a b : U) → U
  ⌈_⌉    : (A : Set) → U

El : U → Set
El (tree a)   = Tree.Tree (El a)
El (stream a) = Stream (El a)
El (colist a) = Colist (El a)
El (a ⊗ b)    = El a × El b
El ⌈ A ⌉      = A

-- Equality.

data Eq : ∀ a → El a → El a → Set₁ where
  leaf : ∀ {a} → Eq (tree a) leaf leaf
  node : ∀ {a x x′ l l′ r r′}
         (l≈l′ : ∞ (Eq (tree a) (♭ l) (♭ l′)))
         (x≈x′ :    Eq a        x     x′     )
         (r≈r′ : ∞ (Eq (tree a) (♭ r) (♭ r′))) →
         Eq (tree a) (node l x r) (node l′ x′ r′)
  _≺_  : ∀ {a x x′ xs xs′}
         (x≈x′   :    Eq a              x      x′  )
         (xs≈xs′ : ∞ (Eq (stream a) (♭ xs) (♭ xs′))) →
         Eq (stream a) (x ≺ xs) (x′ ≺ xs′)
  []   : ∀ {a} → Eq (colist a) [] []
  _∷_  : ∀ {a x x′ xs xs′}
         (x≈x′   :    Eq a              x      x′  )
         (xs≈xs′ : ∞ (Eq (colist a) (♭ xs) (♭ xs′))) →
         Eq (colist a) (x ∷ xs) (x′ ∷ xs′)
  _,_  : ∀ {a b x x′ y y′}
         (x≈x′ : Eq a x x′) (y≈y′ : Eq b y y′) →
         Eq (a ⊗ b) (x , y) (x′ , y′)
  ⌈_⌉  : ∀ {A} {x x′} (x≡x′ : x ≡ x′) → Eq ⌈ A ⌉ x x′

-- PrefixOf a xs ys is inhabited iff xs is a prefix of ys.

data PrefixOf (a : U) : Colist (El a) → Stream (El a) → Set₁ where
  []  : ∀ {ys} → PrefixOf a [] ys
  _∷_ : ∀ {x y xs ys}
        (x≈y : Eq a x y) (p : ∞ (PrefixOf a (♭ xs) (♭ ys))) →
        PrefixOf a (x ∷ xs) (y ≺ ys)

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
module StateSizedIO.GUI.VariableList where

open import Data.Product hiding (map)
open import Data.List

open import NativeIO
open import StateSizedIO.GUI.WxBindingsFFI

data VarList : Set₁ where
  []     : VarList
  addVar : (A : Set) → Var A → VarList → VarList

addVar' : {A : Set} → Var A → VarList → VarList
addVar' {A} = addVar A

[_]var : ∀ {A : Set} → Var A → VarList
[_]var{A} x = addVar A x []

prod : VarList → Set
prod [] = Unit
prod (addVar A v []) = A
prod (addVar A v l)  = A × prod l

varListProj₁ : (l : VarList){A : Set}{v : Var A}(p : prod (addVar A v l)) → A
varListProj₁ [] {A} {v} a = a
varListProj₁ (addVar A₁ x l) {A} {v} (a , rest) = a

varListUpdateProj₁ : (l : VarList){A : Set}{v : Var A}(a : A)
                     (p : prod (addVar A v l))
                     → prod (addVar A v l)
varListUpdateProj₁ [] {A} {v} a p = a
varListUpdateProj₁ (addVar A₁ x l) {A} {v} a' (a , rest)  = ( a' , rest )

takeVar : (l : VarList) → NativeIO (prod l)
takeVar [] = nativeReturn _
takeVar (addVar A v []) = nativeTakeVar {A} v  native>>= λ a →
                         nativeReturn a
takeVar (addVar A v (addVar B v' l))  = nativeTakeVar {A} v        native>>= λ a →
                                       takeVar (addVar B v' l)    native>>= λ rest →
                                       nativeReturn ( a , rest )

putVar : (l : VarList) → prod l → NativeIO Unit
putVar  [] _ = nativeReturn _
putVar  (addVar A v []) a         = nativePutVar {A} v a
putVar  (addVar A v (addVar B v' l)) (a , rest)
                                  = nativePutVar {A} v a         native>>= λ _ →
                                    putVar (addVar B v' l)  rest native>>=
                                    nativeReturn

dispatch : (l : VarList) → (prod l → NativeIO (prod l)) → NativeIO Unit
dispatch l f = takeVar l     native>>= λ a →
               f a          native>>= λ a₁ →
               putVar l a₁

dispatchList : (l : VarList) → List (prod l → NativeIO (prod l)) → NativeIO Unit
dispatchList l []         = nativeReturn _
dispatchList l (p ∷ rest) = dispatch l p native>>= λ _ →
                            dispatchList l rest

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
module Measure where

import Data.Nat              as ℕ
import Data.Nat.Coprimality  as Coprimality
import Data.Nat.GCD          as GCD
import Data.Nat.Show         as ℕshow
import Data.Nat.Divisibility as Divisibility

open ℕ            using (ℕ; suc; zero)
open Coprimality  using (Coprime)
open Divisibility using (divides)

open import Relation.Nullary.Decidable using (True; False; toWitness; fromWitness)
open import Data.Product using (_,_; ∃; proj₁; proj₂)
open import Data.String as String using (String)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≢_; cong; sym; refl)

open import Data.Empty as ⊥ using (⊥)

record ℙ : Set where
  field
    numerator     : ℕ
    denominator-1 : ℕ
    .coprime      : Coprime numerator (suc denominator-1)

  denominator : ℕ
  denominator = suc denominator-1
open ℙ

infixl 7 _÷₌_
_÷₌_ : (n : ℕ) → (d : ℕ) → .{coprime : Coprime n d} → .{≢0 : False (d ℕ.≟ 0)} → ∃ (λ p → denominator p ≡ d)
numerator     (proj₁ (n ÷₌ _))                 = n
denominator-1 (proj₁ ((_ ÷₌ zero) {≢0 = ()}))
denominator-1 (proj₁ (_ ÷₌ suc d))             = d
coprime       (proj₁ ((_ ÷₌ zero) {≢0 = ()}))
coprime       (proj₁ ((_ ÷₌ suc d) {coprime})) = coprime
proj₂ ((n ÷₌ zero) {≢0 = ()})
proj₂ (n ÷₌ suc d) = refl

infixl 7 _÷_
_÷_ : (n d : ℕ) → .{coprime : Coprime n d} → .{≢0 : False (d ℕ.≟ 0)} → ℙ
numerator (n ÷ d) = n
denominator-1 ((n ÷ zero) {≢0 = ()})
denominator-1 (n ÷ suc d-1) = d-1
coprime ((n ÷ zero) {≢0 = ()})
coprime ((n ÷ suc d-1) {coprime}) = coprime

fromNat : ℕ → ℙ
numerator (fromNat n) = n
denominator-1 (fromNat _) = 0
coprime (fromNat n) = Coprimality.sym (Coprimality.1-coprimeTo n)

private  1+≢*0 : ∀ x y → suc x ≢ y ℕ.* 0
         1+≢*0 x zero ()
         1+≢*0 x (suc y) = 1+≢*0 x y

infixl 7 _?÷₌_
_?÷₌_ : ∀ x y → .{≢0 : False (y ℕ.≟ 0)} → ∃ (λ p → x ℕ.* denominator p ≡ numerator p ℕ.* y)
_?÷₌_ x zero {≢0 = ()}
_?÷₌_ x (suc y-1) with GCD.Bézout.lemma x (suc y-1)
_?÷₌_ x (suc y-1) | GCD.Bézout.result 0 (GCD.GCD.is (_ , divides y′ y-eq) _) _ = ⊥.⊥-elim (1+≢*0 y-1 y′ y-eq)
_?÷₌_ x (suc y-1) | GCD.Bézout.result (suc d-1) (GCD.GCD.is (divides x′ x-eq , divides y′ y-eq) _) bézout = proj₁ frac , eq-prf
  where
    open import Data.Nat using (_*_)

    y = suc y-1
    d = suc d-1

    bézout′ : GCD.Bézout.Identity d (x′ * d) (y′ * d)
    bézout′ = ≡.subst₂ (GCD.Bézout.Identity d) x-eq y-eq bézout

    coprime-prf : Coprime x′ y′
    coprime-prf = Coprimality.Bézout-coprime bézout′

    open ≡.≡-Reasoning
    open import Data.Nat.Properties.Simple

    y′≢0 : False (y′ ℕ.≟ 0)
    y′≢0 = Relation.Nullary.Decidable.fromWitnessFalse wtns
      where
      suc-≢0 : {n : ℕ} → (suc n ≡ 0) → ⊥
      suc-≢0 {n} ()

      open import Relation.Nullary using (¬_)
      wtns : ¬ (y′ ≡ 0)
      wtns refl = suc-≢0 {y-1} y-eq

    frac : ∃ (λ p → denominator p ≡ y′)
    frac = (x′ ÷₌ y′) {coprime = coprime-prf} {≢0 = y′≢0}

    eq-prf : x * denominator (proj₁ frac) ≡ numerator (proj₁ frac) * suc y-1
    eq-prf = begin
      x * denominator (proj₁ frac) ≡⟨ cong (λ z → x * z) (proj₂ frac) ⟩
      x * y′         ≡⟨ cong (λ z → z * y′) x-eq ⟩
      x′ * d * y′    ≡⟨ *-assoc x′ d y′ ⟩
      x′ * (d * y′)  ≡⟨ sym (cong (_*_ x′) (*-comm y′ d)) ⟩
      x′ * (y′ * d)  ≡⟨ sym (cong (_*_ x′) y-eq)  ⟩
      x′ * y ∎

infixl 7 _?÷_
_?÷_ : (x y : ℕ) → .{≢0 : False (y ℕ.≟ 0)} → ℙ
(x ?÷ zero) {≢0 = ()}
x ?÷ suc y-1 with GCD.Bézout.lemma x (suc y-1)
(n ?÷ suc y-1) | GCD.Bézout.result 0 (GCD.GCD.is (_ , divides y′ y-eq) _) _ = ⊥.⊥-elim (1+≢*0 y-1 y′ y-eq)
(n ?÷ suc y-1) | GCD.Bézout.result (suc d-1) (GCD.GCD.is (divides x′ x-eq , divides y′ y-eq) _) bézout = (x′ ÷ y′) {coprime = coprime-prf} {≢0 = y′≢0}
  where
  open import Data.Nat using (_*_)

  y = suc y-1
  d = suc d-1

  bézout′ : GCD.Bézout.Identity d (x′ * d) (y′ * d)
  bézout′ = ≡.subst₂ (GCD.Bézout.Identity d) x-eq y-eq bézout

  coprime-prf : Coprime x′ y′
  coprime-prf = Coprimality.Bézout-coprime bézout′

  y′≢0 : False (y′ ℕ.≟ 0)
  y′≢0 = Relation.Nullary.Decidable.fromWitnessFalse wtns
    where
    suc-≢0 : {n : ℕ} → (suc n ≡ 0) → ⊥
    suc-≢0 {n} ()

    open import Relation.Nullary using (¬_)
    wtns : ¬ (y′ ≡ 0)
    wtns refl = suc-≢0 {y-1} y-eq

_+_ : ℙ → ℙ → ℙ
x + y = ((numerator x ℕ.* denominator y) ℕ.+ (numerator y ℕ.* denominator x)) ?÷ (denominator x ℕ.* denominator y)

_*_ : ℙ → ℙ → ℙ
x * y = (numerator x ℕ.* numerator y) ?÷ (denominator x ℕ.* denominator y)

show : ℙ → String
show p = ℕshow (numerator p) ++ "÷" ++ ℕshow (denominator p)
  where
  open String using (_++_)
  open import Data.Nat.Show renaming (show to ℕshow)

max_stars_repo_name: oisdk/prob-presentation

max_issues_repo_name: oisdk/prob-presentation

max_forks_repo_name: oisdk/prob-presentation


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Sets.EquivalenceRelations
open import Setoids.Setoids

module Setoids.Product {m n o p : _} {A : Set m} {B : Set n} (R : Setoid {m} {o} A) (S : Setoid {n} {p} B) where

open Setoid

productSetoid : Setoid (A && B)
_∼_ (productSetoid) (a ,, b) (c ,, d) = (Setoid._∼_ R a c) && (Setoid._∼_ S b d)
Equivalence.reflexive (eq (productSetoid)) {(a ,, b)} = Equivalence.reflexive (Setoid.eq R) ,, Equivalence.reflexive (Setoid.eq S)
Equivalence.symmetric (eq (productSetoid)) {(a ,, b)} {(c ,, d)} (fst ,, snd) = Equivalence.symmetric (Setoid.eq R) fst ,, Equivalence.symmetric (Setoid.eq S) snd
Equivalence.transitive (eq (productSetoid)) {a ,, b} {c ,, d} {e ,, f} (fst1 ,, snd1) (fst2 ,, snd2) = Equivalence.transitive (Setoid.eq R) fst1 fst2 ,, Equivalence.transitive (Setoid.eq S) snd1 snd2

productLift : {r s : A} {t u : B} → (Setoid._∼_ R r s) → (Setoid._∼_ S t u) → Setoid._∼_ productSetoid (r ,, t) (s ,, u)
_&&_.fst (productLift r=s t=u) = r=s
_&&_.snd (productLift r=s t=u) = t=u


text:
module Issue4435-1 where

record ⊤ : Set where

-- Declarations.
data Foo (a : Set) : Set
Bar : {a : Set} → Foo a → Set

-- Definitions.
data Foo a : Set where
  c1 : Foo a
  c2 : (x : Foo a) (y : Bar x → Foo a) → Foo a

Bar c1 = ⊤
Bar (c2 a b) = (x : Bar a) → Bar (b x)


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

module Equality where

open import Cubical.Core.Everything         using (_≡_; Level; Type; Σ; _,_; fst; snd; _≃_; ~_)
open import Cubical.Foundations.Prelude     using (refl; sym; cong; transport; subst; funExt; transp; I; i0; i1)
open import Cubical.Foundations.Function    using (_∘_)
open import Cubical.Foundations.Univalence  using (ua)
open import Cubical.Foundations.Isomorphism using (iso; Iso; isoToPath; section; retract)

open import Data.Bool.Base      using (Bool; true; false; _∧_)
open import Data.Nat.Base       using (ℕ; zero; suc; _+_)
open import Data.Fin            using (Fin; toℕ; fromℕ; #_; opposite) renaming (zero to fz; suc to fs)
open import Data.Product        using (_×_; proj₁; proj₂)

-- mutual recursion
data Γ : ℕ → Type
data U : {n : ℕ} → Γ n → Type

-- context (snoc list of dependent types)
data Γ where
  ε   : Γ 0
  _∙_ : {n : ℕ} → (γ : Γ n) → U γ → Γ (suc n)

tail : {n : ℕ} → Γ (suc n) → Γ n
tail (γ ∙ _) = γ

drop : {n : ℕ} → (k : ℕ) → Γ (k + n) → Γ n
drop zero    γ       = γ
drop (suc k) (γ ∙ x) = drop k γ

head : {n : ℕ} → (γ : Γ (suc n)) → U (tail γ)
head (_ ∙ A) = A

-- lookup a type in a context at position k
lookup : {n : ℕ} → (k : ℕ) → (γ : Γ (k + suc n)) → U (tail (drop k γ))
lookup k γ = head (drop k γ)

-- type universe
data U where
  nat : {n : ℕ} → {γ : Γ n} → U γ
  pi  : {n : ℕ} → {γ : Γ n} → (A : U γ) → U (γ ∙ A) → U γ

data Term : {n : ℕ} → (γ : Γ n) → U γ → Type where
--  v  : {n : ℕ} → (k : ℕ) → {γ : Γ (k + suc n)} → {A : U (tail (drop k γ))} → Term (tail (drop k γ)) A
  v  : {n : ℕ} → (k : ℕ) → {γ : Γ (k + suc n)} → {A : U (tail (drop k γ))} → Term (tail (drop k γ)) A
  tz : {n : ℕ} → {γ : Γ n} → Term γ nat -- zero
  ts : {n : ℕ} → {γ : Γ n} → Term γ nat → Term γ nat -- suc
--  tn : (P : Term nat → U) → Term (P tz) → ((n : Term nat) → Term (P n) → Term (P (ts n))) → (n : Term nat) → Term (P n) -- natrec
  tλ : {n : ℕ} → {γ : Γ n} → {A : U γ} → {B : U (γ ∙ A)} → Term (γ ∙ A) B → Term γ (pi A B)
  ta : {n : ℕ} → {γ : Γ n} → {A : U γ} → {B : U (γ ∙ A)} → Term γ (pi A B) → Term γ A → Term (γ ∙ A) B

--+1 : Term ε (pi nat nat)
--+1 = tλ {!!} --(v {n = 0} 0)

data Eq : Type where
  eq : Eq -- equal
  ne : Eq -- not equal

data Maybe (a : Type) : Type where
  nothing : Maybe a
  just    : a → Maybe a

ℕeq : ℕ → ℕ → Eq
ℕeq zero zero       = eq
ℕeq zero (suc n)    = ne
ℕeq (suc m) zero    = ne
ℕeq (suc m) (suc n) = ℕeq m n

natrec : (P : ℕ → Type) → P 0 → ((n : ℕ) → P n → P (suc n)) → (n : ℕ) → P n
natrec P z s zero    = z
natrec P z s (suc n) = s n (natrec P z s n)

_+'_ : ℕ → ℕ → ℕ
_+'_ = λ m → λ n → natrec (λ _ → ℕ) n (λ _ → suc) m

0=0 : 0 ≡ 0
0=0 = refl

suc=suc : (m n : ℕ) → m ≡ n → suc m ≡ suc n
suc=suc m n e = cong suc e

0+n=n : (n : ℕ) → 0 + n ≡ n
0+n=n = natrec (λ k → 0 + k ≡ k) 0=0 (λ n e → suc=suc n n e)

n=0+n : (n : ℕ) → n + 0 ≡ n
n=0+n = natrec (λ k → k + 0 ≡ k) 0=0 λ n e → suc=suc (n + 0) n e

max_stars_repo_name: halfaya/Alae

max_issues_repo_name: halfaya/Alae

max_forks_repo_name: halfaya/Alae


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Setoids.Setoids
open import Functions
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Numbers.Naturals.Naturals
open import Sets.FinSet
open import Groups.Definition
open import Groups.Lemmas
open import Groups.Groups
open import Groups.Actions.Definition
open import Groups.Actions.Stabiliser
open import Groups.Groups2
open import Sets.EquivalenceRelations

module Groups.Actions.OrbitStabiliser where

orbitStabiliserEquivRel1 : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) → Rel A
orbitStabiliserEquivRel1 {T = T} action x g1 g2 = Setoid._∼_ T (GroupAction.action action g1 x) (GroupAction.action action g2 x)

orbitStabiliserEquivRel2 : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) → Rel A
orbitStabiliserEquivRel2 {T = T} {_+_ = _+_} {G = G} action x g1 g2 = Setoid._∼_ T (GroupAction.action action ((Group.inverse G g2) + g1) x) x

osEquivRel1Equiv : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) → Equivalence (orbitStabiliserEquivRel1 action x)
Equivalence.reflexive (osEquivRel1Equiv {T = T} action x) {a} = Equivalence.reflexive (Setoid.eq T)
Equivalence.symmetric (osEquivRel1Equiv {T = T} action x) {a} {b} = Equivalence.symmetric (Setoid.eq T)
Equivalence.transitive (osEquivRel1Equiv {T = T} action x) {a} {b} {c} = Equivalence.transitive (Setoid.eq T)

osEquivRel2Equiv : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) → Equivalence (orbitStabiliserEquivRel2 action x)
Equivalence.reflexive (osEquivRel2Equiv {T = T} {G = G} action x) = transitive (GroupAction.actionWellDefined1 action (Group.invLeft G)) (GroupAction.identityAction action)
  where
    open Equivalence (Setoid.eq T)
Equivalence.symmetric (osEquivRel2Equiv {S = S} {T = T} {_+_ = _+_} {G = G} gAction x) {b} {c} b=c = need
  where
    open Equivalence (Setoid.eq T)
    open Equivalence (Setoid.eq S) renaming (symmetric to symmetricS ; transitive to transitiveS ; reflexive to reflexiveS)
    open Setoid T
    open GroupAction gAction
    open Group G
    have : action ((inverse c) + b) x ∼ x
    have = b=c
    p : action (inverse (inverse b + c)) x ∼ x
    p = transitive (actionWellDefined1 (transitiveS (invContravariant G) (Group.+WellDefined G reflexiveS (invInv G)))) have
    q : action ((inverse b) + c) (action (inverse (inverse b + c)) x) ∼ action ((inverse b) + c) x
    q = actionWellDefined2 p
    r : action (((inverse b) + c) + (inverse (inverse b + c))) x ∼ action ((inverse b) + c) x
    r = transitive associativeAction q
    s : action identity x ∼ action ((inverse b) + c) x
    s = transitive (actionWellDefined1 (symmetricS invRight)) r
    need : action ((inverse b) + c) x ∼ x
    need = symmetric (transitive (symmetric identityAction) s)
Equivalence.transitive (osEquivRel2Equiv {S = S} {T = T} {_+_ = _+_} {G = G} gAction x) {a} {b} {c} a=b b=c = need
  where
    open Equivalence (Setoid.eq T)
    open Equivalence (Setoid.eq S) renaming (symmetric to symmetricS ; reflexive to reflexiveS ; transitive to transitiveS)
    open Setoid T
    open GroupAction gAction
    open Group G
    have1 : action ((inverse c) + b) x ∼ x
    have1 = b=c
    have2 : action ((inverse b) + a) x ∼ x
    have2 = a=b
    p : action ((inverse c) + b) (action (inverse b + a) x) ∼ x
    p = transitive (actionWellDefined2 have2) have1
    q : action ((inverse c + b) + (inverse b + a)) x ∼ x
    q = transitive associativeAction p
    need : action ((inverse c) + a) x ∼ x
    need = transitive (actionWellDefined1 (transitiveS (+WellDefined reflexiveS (transitiveS (symmetricS identLeft) (+WellDefined (symmetricS invRight) reflexiveS))) (fourWayAssoc G))) q

osEquivRelsEqual' : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) {g h : A} → (orbitStabiliserEquivRel2 action x) g h → (orbitStabiliserEquivRel1 action x) g h
osEquivRelsEqual' {S = S} {T = T} {_+_ = _+_} {G = G} action x {g} {h} g=h = need
  where
    open Setoid T
    open Group G
    open Equivalence eq
    open Equivalence (Setoid.eq S) renaming (symmetric to symmetricS ; transitive to transitiveS)
    have : (GroupAction.action action ((inverse h) + g) x) ∼ x
    have = g=h
    p : (GroupAction.action action (inverse h) (GroupAction.action action g x)) ∼ x
    p = transitive (symmetric (GroupAction.associativeAction action)) have
    q : (GroupAction.action action h (GroupAction.action action (inverse h) (GroupAction.action action g x))) ∼ GroupAction.action action h x
    q = GroupAction.actionWellDefined2 action p
    r : (GroupAction.action action (h + inverse h) (GroupAction.action action g x)) ∼ GroupAction.action action h x
    r = transitive (GroupAction.associativeAction action) q
    s : (GroupAction.action action identity (GroupAction.action action g x)) ∼ GroupAction.action action h x
    s = transitive (GroupAction.actionWellDefined1 action (symmetricS (Group.invRight G))) r
    need : (GroupAction.action action g x) ∼ (GroupAction.action action h x)
    need = transitive (symmetric (GroupAction.identityAction action)) s

osEquivRelsEqual : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) {g h : A} → (orbitStabiliserEquivRel1 action x) g h → (orbitStabiliserEquivRel2 action x) g h
osEquivRelsEqual {T = T} {_+_ = _+_} {G = G} action x {g} {h} g=h = need
  where
    open Setoid T
    open Group G
    open Equivalence eq
    have : (GroupAction.action action g x) ∼ (GroupAction.action action h x)
    have = g=h
    p : GroupAction.action action (inverse h) (GroupAction.action action g x) ∼ GroupAction.action action (inverse h) (GroupAction.action action h x)
    p = GroupAction.actionWellDefined2 action have
    need : (GroupAction.action action ((inverse h) + g) x) ∼ x
    need = transitive (GroupAction.associativeAction action) (transitive p (transitive (symmetric (GroupAction.associativeAction action)) (transitive (GroupAction.actionWellDefined1 action (Group.invLeft G)) (GroupAction.identityAction action))))

orbitStabiliserBijection : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) → A → ((Stabiliser action x) && Orbit action x)
orbitStabiliserBijection action x g = stab {!GroupAction.action action ? ?!} {!!} ,, orbitElt g
  where

osBijWellDefined : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) → {r s : A} → (Setoid._∼_ S r s) → Setoid._∼_ (directSumSetoid (stabiliserSetoid action x) (orbitSetoid action x)) (orbitStabiliserBijection action x r) (orbitStabiliserBijection action x s)
_&&_.fst (osBijWellDefined action x r~s) = {!!}
_&&_.snd (osBijWellDefined action x r~s) = GroupAction.actionWellDefined1 action r~s

orbitStabiliserTheorem : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) → SetoidBijection S (directSumSetoid (stabiliserSetoid action x) (orbitSetoid action x)) (orbitStabiliserBijection action x)
SetoidInjection.+WellDefined (SetoidBijection.inj (orbitStabiliserTheorem {S = S} action x)) = osBijWellDefined action x
SetoidInjection.injective (SetoidBijection.inj (orbitStabiliserTheorem {S = S} action x)) {g} {h} (fst ,, gx=hx) = {!!}
SetoidSurjection.+WellDefined (SetoidBijection.surj (orbitStabiliserTheorem action x)) = osBijWellDefined action x
SetoidSurjection.surjective (SetoidBijection.surj (orbitStabiliserTheorem action x)) {stab g gx=x ,, orbitElt h} = h , ({!!} ,, {!!})


text:
open import Data.Nat using ( ℕ ; fold ) renaming ( zero to zero' ; suc to suc' )
open import Data.String using ( String )

module Data.Natural.Primitive where

infixl 6 _+_

postulate
  Natural : Set
  zero : Natural
  suc : Natural → Natural
  _+_ : Natural → Natural → Natural
  show : Natural → String
  foldl : {A : Set} → (A → A) → A → Natural → A
  foldl' : {A : Set} → (A → A) → A → Natural → A
  foldr : {A : Set} → (A → A) → A → Natural → A
{-# IMPORT Data.Natural.AgdaFFI #-}
{-# COMPILED_TYPE Natural Data.Natural.AgdaFFI.Natural #-}
{-# COMPILED zero 0 #-}
{-# COMPILED suc succ #-}
{-# COMPILED _+_ (+) #-}
{-# COMPILED show show #-}
{-# COMPILED foldl (\ _ -> Data.Natural.AgdaFFI.nfoldl) #-}
{-# COMPILED foldl' (\ _ -> Data.Natural.AgdaFFI.nfoldl') #-}
{-# COMPILED foldr (\ _ -> Data.Natural.AgdaFFI.nfoldr) #-}

private
  postulate
    # : ∀ {l} {A : Set l} → A → Natural
{-# COMPILED # (\ _ -> Data.Natural.AgdaFFI.convert MAlonzo.Data.Nat.mazNatToInteger) #-}

fromℕ : ℕ → Natural
fromℕ = #

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
------------------------------------------------------------------------
-- Unary relations (variant for Set₁)
------------------------------------------------------------------------

-- I want universe polymorphism.

module Relation.Unary1 where

------------------------------------------------------------------------
-- Unary relations

Pred : Set → Set₂
Pred a = a → Set₁

------------------------------------------------------------------------
-- Unary relations can be seen as sets

-- I.e., they can be seen as subsets of the universe of discourse.

private
 module Dummy {a : Set} -- The universe of discourse.
          where

  -- Set membership.

  infix 4 _∈_

  _∈_ : a → Pred a → Set₁
  x ∈ P = P x

  -- The property of being universal.

  Universal : Pred a → Set₁
  Universal P = ∀ x → x ∈ P

  -- P ⊆ Q means that P is a subset of Q. _⊆′_ is a variant of _⊆_.

  infix 4 _⊆_ _⊇_ _⊆′_ _⊇′_

  _⊆_ : Pred a → Pred a → Set₁
  P ⊆ Q = ∀ {x} → x ∈ P → x ∈ Q

  _⊆′_ : Pred a → Pred a → Set₁
  P ⊆′ Q = ∀ x → x ∈ P → x ∈ Q

  _⊇_ : Pred a → Pred a → Set₁
  Q ⊇ P = P ⊆ Q

  _⊇′_ : Pred a → Pred a → Set₁
  Q ⊇′ P = P ⊆′ Q

open Dummy public

max_issues_repo_name: larrytheliquid/Lemmachine


text:
-- Andreas, 2012-02-25 reported by edgmnt on behalf of xplat.
module Issue574 where

open import Common.Level

wah : ∀ o a → Set (lsuc lzero ⊔ (lsuc a ⊔ o)) → Set ((lsuc lzero ⊔ lsuc a) ⊔ o)
wah o a x = x -- should succeed

-- Error message was:
-- Set (suc zero ⊔ (suc a ⊔ o)) != Set (suc a ⊔ o)
-- when checking that the expression x has type Set (suc a ⊔ o)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Data.Either.Setoid where

import      Lvl
open import Data.Either as Either
open import Data.Either.Equiv
open import Logic
open import Logic.Propositional
open import Structure.Function.Domain
open import Structure.Function
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Setoid
open import Type

private variable ℓ ℓₑ ℓₑ₁ ℓₑ₂ : Lvl.Level
private variable A B : Type{ℓ}

module _ ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄ ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ where
  data EitherEquality : (A ‖ B) → (A ‖ B) → Stmt{Lvl.of(A) Lvl.⊔ Lvl.of(B) Lvl.⊔ ℓₑ₁ Lvl.⊔ ℓₑ₂} where
    Left  : ∀{x y} → (x ≡ y) → EitherEquality(Left  x)(Left  y)
    Right : ∀{x y} → (x ≡ y) → EitherEquality(Right x)(Right y)

  EitherEquality-elim : ∀{ℓ}{P : ∀{ab₁ ab₂ : (A ‖ B)} → EitherEquality ab₁ ab₂ → Type{ℓ}} → (∀{x y : A} → (xy : (x ≡ y)) → P(Left xy)) → (∀{x y : B} → (xy : (x ≡ y)) → P(Right xy)) → ∀{ab₁ ab₂ : (A ‖ B)} → (eq : EitherEquality ab₁ ab₂) → P(eq)
  EitherEquality-elim l r (Left  p) = l p
  EitherEquality-elim l r (Right p) = r p

  EitherEquality-not-Left-Right : ∀{a : A}{b : B} → ¬(EitherEquality (Left a) (Right b))
  EitherEquality-not-Left-Right ()

  instance
    Either-equiv : Equiv(A ‖ B)
    Equiv._≡_ Either-equiv = EitherEquality
    Reflexivity.proof (Equivalence.reflexivity (Equiv.equivalence Either-equiv)) {Left  _} = Left (reflexivity(_≡_))
    Reflexivity.proof (Equivalence.reflexivity (Equiv.equivalence Either-equiv)) {Right _} = Right (reflexivity(_≡_))
    Symmetry.proof (Equivalence.symmetry (Equiv.equivalence Either-equiv)) {.(Left _)} {.(Left _)} (Left p) = Left (symmetry(_≡_) p)
    Symmetry.proof (Equivalence.symmetry (Equiv.equivalence Either-equiv)) {.(Right _)} {.(Right _)} (Right p) = Right (symmetry(_≡_) p)
    Transitivity.proof (Equivalence.transitivity (Equiv.equivalence Either-equiv)) {.(Left _)} {.(Left _)} {.(Left _)} (Left xy) (Left yz) = Left (transitivity(_≡_) xy yz)
    Transitivity.proof (Equivalence.transitivity (Equiv.equivalence Either-equiv)) {.(Right _)} {.(Right _)} {.(Right _)} (Right xy) (Right yz) = Right (transitivity(_≡_) xy yz)

  instance
    Left-function : Function ⦃ equiv-A ⦄ ⦃ Either-equiv ⦄ (Left)
    Function.congruence Left-function = Left

  instance
    Right-function : Function ⦃ equiv-B ⦄ ⦃ Either-equiv ⦄ (Right)
    Function.congruence Right-function = Right

  instance
    Left-injectivity : Injective(Left {A = A}{B = B})
    Injective.proof Left-injectivity (Left p) = p

  instance
    Right-injectivity : Injective(Right {A = A}{B = B})
    Injective.proof Right-injectivity (Right p) = p

  instance
    EitherEquality-extensionality : Extensionality(Either-equiv)
    Extensionality.Left-Right-inequality EitherEquality-extensionality ()

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:
------------------------------------------------------------------------
-- Functional semantics for a non-deterministic untyped λ-calculus
-- with constants
------------------------------------------------------------------------

module Lambda.Closure.Functional.Non-deterministic where

open import Category.Monad.Partiality as Pa using (_⊥; now; later)
open import Codata.Musical.Notation
open import Data.Fin using (Fin; zero; suc; #_)
open import Data.List hiding (lookup)
open import Data.Maybe hiding (_>>=_)
open import Data.Nat
open import Data.Vec using ([]; _∷_; lookup)
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Relation.Nullary.Decidable

open import Lambda.Syntax using (Ty; Ctxt)
open Lambda.Syntax.Closure using (con; ƛ)
open Lambda.Syntax.Ty
open import Lambda.VirtualMachine
  hiding (comp; comp-val; comp-env; lookup-hom)
open Functional
private
  module VM = Lambda.Syntax.Closure Code

------------------------------------------------------------------------
-- A monad with partiality, failure and non-determinism

module D where

  -- This is basically the maybe monad transformer applied to the
  -- partiality monad transformer applied to the non-determinism monad
  -- N A = μX. A ⊎ X × X. Unfortunately it is somewhat awkward to
  -- implement the partiality monad transformer in Agda: the
  -- definition
  --
  --   data Partiality′ (M : Set → Set) (A : Set) : Set where
  --     now-or-later : M (A ⊎ Partiality′ M A) → Partiality′ M A
  --
  -- is rejected, because M might use its argument negatively.

  infixr 6 _∣_

  data D (A : Set) : Set where
    fail   : D A
    return : (x : A) → D A
    _∣_    : (x y : D A) → D A
    later  : (x : ∞ (D A)) → D A

  -- The function force n removes (up to) n layers of later
  -- constructors.

  force : {A : Set} → ℕ → D A → D A
  force (suc n) (later x) = force n (♭ x)
  force n       (x₁ ∣ x₂) = force n x₁ ∣ force n x₂
  force _       x         = x

  -- Bind.

  infixl 5 _>>=_

  _>>=_ : {A B : Set} → D A → (A → D B) → D B
  fail      >>= f = fail
  return x  >>= f = f x
  (x₁ ∣ x₂) >>= f = (x₁ >>= f) ∣ (x₂ >>= f)
  later x   >>= f = later (♯ (♭ x >>= f))

  -- A deterministic non-terminating computation.

  never : {A : Set} → D A
  never = later (♯ never)

  -- Strong bisimilarity.

  infix 4 _≅_

  data _≅_ {A : Set} : D A → D A → Set where
    fail   : fail ≅ fail
    return : ∀ {x} → return x ≅ return x
    _∣_    : ∀ {x₁ x₂ y₁ y₂}
             (x₁≅y₁ : x₁ ≅ y₁) (x₂≅y₂ : x₂ ≅ y₂) → x₁ ∣ x₂ ≅ y₁ ∣ y₂
    later  : ∀ {x y} (x≅y : ∞ (♭ x ≅ ♭ y)) → later x ≅ later y

  -- Strong bisimilarity is reflexive.

  infixr 3 _∎

  _∎ : {A : Set} (x : D A) → x ≅ x
  fail     ∎ = fail
  return x ∎ = return
  x₁ ∣ x₂  ∎ = (x₁ ∎) ∣ (x₂ ∎)
  later x  ∎ = later (♯ (♭ x ∎))

  -- Strong bisimilarity is symmetric.

  sym : {A : Set} {x y : D A} → x ≅ y → y ≅ x
  sym fail            = fail
  sym return          = return
  sym (x₁≅y₁ ∣ x₂≅y₂) = sym x₁≅y₁ ∣ sym x₂≅y₂
  sym (later x≅y)     = later (♯ sym (♭ x≅y))

  -- Strong bisimilarity is transitive.

  infixr 2 _≅⟨_⟩_

  _≅⟨_⟩_ : ∀ {A : Set} (x : D A) {y z} → x ≅ y → y ≅ z → x ≅ z
  ._ ≅⟨ fail          ⟩ fail          = fail
  ._ ≅⟨ return        ⟩ return        = return
  ._ ≅⟨ x₁≅y₁ ∣ x₂≅y₂ ⟩ y₁≅z₁ ∣ y₂≅z₂ = (_ ≅⟨ x₁≅y₁ ⟩ y₁≅z₁) ∣ (_ ≅⟨ x₂≅y₂ ⟩ y₂≅z₂)
  ._ ≅⟨ later x≅y     ⟩ later y≅z     = later (♯ (_ ≅⟨ ♭ x≅y ⟩ ♭ y≅z))

  -- The monad laws hold up to strong bisimilarity.

  left-identity : {A B : Set} {x : A} {f : A → D B} →
                  return x >>= f ≅ f x
  left-identity {x = x} {f} = f x ∎

  right-identity : {A : Set} (x : D A) → x >>= return ≅ x
  right-identity fail       = fail
  right-identity (return x) = return
  right-identity (x₁ ∣ x₂)  = right-identity x₁ ∣ right-identity x₂
  right-identity (later x)  = later (♯ right-identity (♭ x))

  associative : {A B C : Set} (x : D A) {f : A → D B} {g : B → D C} →
                x >>= f >>= g ≅ x >>= λ y → f y >>= g
  associative fail               = fail
  associative (return x) {f} {g} = f x >>= g ∎
  associative (x₁ ∣ x₂)          = associative x₁ ∣ associative x₂
  associative (later x)          = later (♯ associative (♭ x))

  -- Bind respects strong bisimilarity.

  infixl 5 _>>=-cong_

  _>>=-cong_ : {A B : Set} {x₁ x₂ : D A} {f₁ f₂ : A → D B} →
               x₁ ≅ x₂ → (∀ y → f₁ y ≅ f₂ y) → x₁ >>= f₁ ≅ x₂ >>= f₂
  fail          >>=-cong f₁≅f₂ = fail
  return        >>=-cong f₁≅f₂ = f₁≅f₂ _
  later x≅y     >>=-cong f₁≅f₂ = later (♯ (♭ x≅y >>=-cong f₁≅f₂))
  x₁≅x₂ ∣ y₁≅y₂ >>=-cong f₁≅f₂ =
    (x₁≅x₂ >>=-cong f₁≅f₂) ∣ (y₁≅y₂ >>=-cong f₁≅f₂)

  -- More laws.

  never-left-zero : {A B : Set} {f : A → D B} → never >>= f ≅ never
  never-left-zero = later (♯ never-left-zero)

  fail-left-zero : {A B : Set} {f : A → D B} → fail >>= f ≅ fail
  fail-left-zero = fail ∎

open D using (D; _≅_; _≅⟨_⟩_; _∎; _>>=-cong_) hiding (module D)
open D.D
open D._≅_

------------------------------------------------------------------------
-- Syntax

infixl 9 _·_
infixr 6 _∣_

data Tm (n : ℕ) : Set where
  con : (i : ℕ) → Tm n
  var : (x : Fin n) → Tm n
  ƛ   : (t : Tm (suc n)) → Tm n
  _·_ : (t₁ t₂ : Tm n) → Tm n
  _∣_ : (t₁ t₂ : Tm n) → Tm n

-- Convenient helper.

vr : ∀ m {n} {m<n : True (suc m ≤? n)} → Tm n
vr _ {m<n = m<n} = var (#_ _ {m<n = m<n})

open Lambda.Syntax.Closure Tm hiding (con; ƛ)

------------------------------------------------------------------------
-- A workaround for the limitations of guardedness

module Workaround where

  infixr 6 _∣_
  infixl 5 _>>=_

  data DP : Set → Set₁ where
    fail   : ∀ {A} → DP A
    return : ∀ {A} (x : A) → DP A
    _∣_    : ∀ {A} (x y : DP A) → DP A
    later  : ∀ {A} (x : ∞ (DP A)) → DP A
    _>>=_  : ∀ {A B} (x : DP A) (f : A → DP B) → DP B

  private

    data DW : Set → Set₁ where
      fail   : ∀ {A} → DW A
      return : ∀ {A} (x : A) → DW A
      _∣_    : ∀ {A} (x y : DW A) → DW A
      later  : ∀ {A} (x : DP A) → DW A

    mutual

      _>>=W_ : ∀ {A B} → DW A → (A → DP B) → DW B
      fail     >>=W f = fail
      return x >>=W f = whnf (f x)
      (x ∣ y)  >>=W f = (x >>=W f) ∣ (y >>=W f)
      later x  >>=W f = later (x >>= f)

      whnf : ∀ {A} → DP A → DW A
      whnf fail       = fail
      whnf (return x) = return x
      whnf (later x)  = later (♭ x)
      whnf (x ∣ y)    = whnf x ∣ whnf y
      whnf (x >>= f)  = whnf x >>=W f

  mutual

    private

      ⟪_⟫W : ∀ {A} → DW A → D A
      ⟪ fail     ⟫W = fail
      ⟪ return x ⟫W = return x
      ⟪ x ∣ y    ⟫W = ⟪ x ⟫W ∣ ⟪ y ⟫W
      ⟪ later x  ⟫W = later (♯ ⟪ x ⟫P)

    ⟪_⟫P : ∀ {A} → DP A → D A
    ⟪ p ⟫P = ⟪ whnf p ⟫W

  -- The definitions above make sense. ⟪_⟫P is homomorphic with respect
  -- to fail, return, _∣_, later and _>>=_.

  fail-hom : ∀ {A} → ⟪ fail {A = A} ⟫P ≅ fail
  fail-hom = fail ∎

  return-hom : ∀ {A} (x : A) → ⟪ return x ⟫P ≅ return x
  return-hom x = return x ∎

  ∣-hom : ∀ {A} (x y : DP A) → ⟪ x ∣ y ⟫P ≅ ⟪ x ⟫P ∣ ⟪ y ⟫P
  ∣-hom x y = ⟪ x ⟫P ∣ ⟪ y ⟫P ∎

  later-hom : ∀ {A} (x : ∞ (DP A)) → ⟪ later x ⟫P ≅ later (♯ ⟪ ♭ x ⟫P)
  later-hom x = later (♯ (⟪ ♭ x ⟫P ∎))

  mutual

    private

      >>=-homW : ∀ {A B} (x : DW A) (f : A → DP B) →
                 ⟪ x >>=W f ⟫W ≅ D._>>=_ ⟪ x ⟫W (λ y → ⟪ f y ⟫P)
      >>=-homW fail       f = fail ∎
      >>=-homW (return x) f = ⟪ f x ⟫P ∎
      >>=-homW (x ∣ y)    f = >>=-homW x f ∣ >>=-homW y f
      >>=-homW (later x)  f = later (♯ >>=-hom x f)

    >>=-hom : ∀ {A B} (x : DP A) (f : A → DP B) →
              ⟪ x >>= f ⟫P ≅ D._>>=_ ⟪ x ⟫P (λ y → ⟪ f y ⟫P)
    >>=-hom x f = >>=-homW (whnf x) f

open Workaround hiding (_>>=_)

------------------------------------------------------------------------
-- Semantics

infix 9 _∙_

mutual

  ⟦_⟧′ : ∀ {n} → Tm n → Env n → DP Value
  ⟦ con i ⟧′   ρ = return (con i)
  ⟦ var x ⟧′   ρ = return (lookup ρ x)
  ⟦ ƛ t ⟧′     ρ = return (ƛ t ρ)
  ⟦ t₁ · t₂ ⟧′ ρ = ⟦ t₁ ⟧′ ρ >>= λ v₁ →
                   ⟦ t₂ ⟧′ ρ >>= λ v₂ →
                   v₁ ∙ v₂
                   where open Workaround
  ⟦ t₁ ∣ t₂ ⟧′ ρ = ⟦ t₁ ⟧′ ρ ∣ ⟦ t₂ ⟧′ ρ

  _∙_ : Value → Value → DP Value
  con i  ∙ v₂ = fail
  ƛ t₁ ρ ∙ v₂ = later (♯ (⟦ t₁ ⟧′ (v₂ ∷ ρ)))

⟦_⟧ : ∀ {n} → Tm n → Env n → D Value
⟦ t ⟧ ρ = ⟪ ⟦ t ⟧′ ρ ⟫P

-- An abbreviation.

infix 9 _⟦·⟧_

_⟦·⟧_ : D Value → D Value → D Value
v₁ ⟦·⟧ v₂ = v₁ >>= λ v₁ → v₂ >>= λ v₂ → ⟪ v₁ ∙ v₂ ⟫P
  where open D

-- The semantics of application is compositional (with respect to the
-- syntactic equality which is used).

·-comp : ∀ {n} (t₁ t₂ : Tm n) {ρ} →
         ⟦ t₁ · t₂ ⟧ ρ ≅ ⟦ t₁ ⟧ ρ ⟦·⟧ ⟦ t₂ ⟧ ρ
·-comp t₁ t₂ {ρ} =
  ⟦ t₁ · t₂ ⟧ ρ                                   ≅⟨ >>=-hom (⟦ t₁ ⟧′ ρ) _ ⟩

  D._>>=_ (⟦ t₁ ⟧ ρ) (λ v₁ →
          ⟪ Workaround._>>=_ (⟦ t₂ ⟧′ ρ) (λ v₂ →
            v₁ ∙ v₂) ⟫P)                          ≅⟨ ((⟦ t₁ ⟧ ρ ∎) >>=-cong λ _ →
                                                      >>=-hom (⟦ t₂ ⟧′ ρ) _) ⟩
  ⟦ t₁ ⟧ ρ ⟦·⟧ ⟦ t₂ ⟧ ρ                           ∎

open D

------------------------------------------------------------------------
-- Compiler

-- The compiler takes a code continuation.
--
-- Non-determinism is resolved by always picking the left choice.

comp : ∀ {n} → Tm n → Code n → Code n
comp (con i)   c = con i ∷ c
comp (var x)   c = var x ∷ c
comp (ƛ t)     c = clo (comp t [ ret ]) ∷ c
comp (t₁ · t₂) c = comp t₁ (comp t₂ (app ∷ c))
comp (t₁ ∣ t₂) c = comp t₁ c

-- Environments and values can also be compiled.

mutual

  comp-env : ∀ {n} → Env n → VM.Env n
  comp-env []      = []
  comp-env (v ∷ ρ) = comp-val v ∷ comp-env ρ

  comp-val : Value → VM.Value
  comp-val (con i) = con i
  comp-val (ƛ t ρ) = ƛ (comp t [ ret ]) (comp-env ρ)

-- lookup x is homomorphic with respect to comp-env/comp-val.

lookup-hom : ∀ {n} (x : Fin n) ρ →
             lookup (comp-env ρ) x ≡ comp-val (lookup ρ x)
lookup-hom zero    (v ∷ ρ) = P.refl
lookup-hom (suc x) (v ∷ ρ) = lookup-hom x ρ

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

-- A non-terminating term.

Ω : Tm 0
Ω = ω · ω
  where ω = ƛ (vr 0 · vr 0)

Ω-loops : ⟦ Ω ⟧ [] ≅ never
Ω-loops = later (♯ Ω-loops)

-- A call-by-value fix-point combinator.

Z : {n : ℕ} → Tm n
Z = ƛ (t · t)
  where t = ƛ (vr 1 · ƛ (vr 1 · vr 1 · vr 0))

-- A non-deterministically non-terminating term.

! : Tm 0
! = Z · ƛ (ƛ (vr 1 · vr 0 ∣ vr 1 · vr 0)) · con 0

-- Its semantics.

!-sem : D Value
!-sem = later (♯ later (♯ later (♯ later (♯ (!-sem ∣ !-sem)))))

⟦!⟧≅!-sem : ⟦ ! ⟧ [] ≅ !-sem
⟦!⟧≅!-sem = later (♯ lem)
  where
  lem : force 1 (⟦ ! ⟧ []) ≅ force 1 !-sem
  lem = later (♯ later (♯ later (♯ (later (♯ lem) ∣ later (♯ lem)))))

-- How did I come up with this proof term? Through a manual
-- calculation...
--
-- Let us first define some abbreviations:
--
--   t₀ = vr 1 · vr 1 · vr 0
--   t₁ = ƛ t₀
--   t₂ = vr 1 · t₁
--   t₃ = ƛ t₂
--
--   u₀ = vr 1 · vr 0
--   u₁ = u₀ ∣ u₀
--   u₂ = ƛ u₁
--   u₃ = ƛ u₂
--
--   c₀ = ƛ u₂ []
--   c₁ = ƛ t₂ (c₀ ∷ [])
--   c₂ = ƛ t₀ (c₁ ∷ c₀ ∷ [])
--
-- Now we can calculate as follows (ignoring ♯):
--
--   ⟦ Z · u₃ · con 0 ⟧ []
-- = ⟦ Z · u₃ ⟧ [] ⟦·⟧ return (con 0)
-- = ƛ (t₃ · t₃) [] ∙ c₀ ⟦·⟧ return (con 0)
-- = later (⟦ t₃ · t₃ ⟧ (c₀ ∷ []) ⟦·⟧ return (con 0))
-- = later (c₁ ∙ c₁ ⟦·⟧ return (con 0))
--
-- = c₁ ∙ c₁ ⟦·⟧ return (con 0)
-- = later (⟦ t₂ ⟧ (c₁ ∷ c₀ ∷ []) ⟦·⟧ return (con 0))
-- = later (c₀ ∙ c₂ ⟦·⟧ return (con 0))
-- = later (later (⟦ u₂ ⟧ (c₂ ∷ []) ⟦·⟧ return (con 0)))
-- = later (later (ƛ u₁ (c₂ ∷ []) ∙ con 0))
-- = later (later (later (⟦ u₁ ⟧ (con 0 ∷ c₂ ∷ []))))
-- = later (later (later (⟦ u₀ ⟧ (con 0 ∷ c₂ ∷ []) ∣
--                        ⟦ u₀ ⟧ (con 0 ∷ c₂ ∷ []))))
-- = later (later (later (c₂ ∙ con 0 ∣ c₂ ∙ con 0)))
-- = later (later (later (⟦ t₀ ⟧ (con 0 ∷ c₁ ∷ c₀ ∷ []) ∣
--                        ⟦ t₀ ⟧ (con 0 ∷ c₁ ∷ c₀ ∷ []))))
-- = later (later (later (later (c₁ ∙ c₁ ⟦·⟧ return (con 0)) ∣
--                        later (c₁ ∙ c₁ ⟦·⟧ return (con 0)))))

------------------------------------------------------------------------
-- A relation relating deterministic and non-deterministic
-- computations

-- x ≈∈ y means that x implements /one/ possible semantics of y (up to
-- weak bisimilarity).

infix 4 _≈∈_

data _≈∈_ {A : Set} : Maybe A ⊥ → D A → Set where
  fail   : now nothing ≈∈ fail

  return : ∀ {x} → now (just x) ≈∈ return x

  ∣ˡ     : ∀ {x y₁ y₂} (x≈∈y₁ : x ≈∈ y₁) → x ≈∈ y₁ ∣ y₂
  ∣ʳ     : ∀ {x y₁ y₂} (x≈∈y₂ : x ≈∈ y₂) → x ≈∈ y₁ ∣ y₂

  later  : ∀ {x y} (x≈∈y : ∞ (♭ x ≈∈ ♭ y)) → later x ≈∈ later y
  laterˡ : ∀ {x y} (x≈∈y :    ♭ x ≈∈   y ) → later x ≈∈       y
  laterʳ : ∀ {x y} (x≈∈y :      x ≈∈ ♭ y ) →       x ≈∈ later y

-- A transitivity-like result for _≡_ and _≈∈_.

infixr 2 _≡⟨_⟩_

_≡⟨_⟩_ : ∀ {A : Set} (x : Maybe A ⊥) {y z} → x ≡ y → y ≈∈ z → x ≈∈ z
_ ≡⟨ P.refl ⟩ y≈z = y≈z

-- A transitivity-like result for _≈∈_ and _≅_.

infixr 2 _≈∈⟨_⟩_

_≈∈⟨_⟩_ : ∀ {A : Set} (x : Maybe A ⊥) {y z} → x ≈∈ y → y ≅ z → x ≈∈ z
._ ≈∈⟨ fail        ⟩ fail          = fail
._ ≈∈⟨ return      ⟩ return        = return
_  ≈∈⟨ ∣ˡ x₁≈∈y₁   ⟩ y₁≅z₁ ∣ y₂≅z₂ = ∣ˡ (_ ≈∈⟨ x₁≈∈y₁ ⟩ y₁≅z₁)
_  ≈∈⟨ ∣ʳ x₂≈∈y₂   ⟩ y₁≅z₁ ∣ y₂≅z₂ = ∣ʳ (_ ≈∈⟨ x₂≈∈y₂ ⟩ y₂≅z₂)
._ ≈∈⟨ later  x≈∈y ⟩ later y≅z     = later (♯ (_ ≈∈⟨ ♭ x≈∈y ⟩ ♭ y≅z))
._ ≈∈⟨ laterˡ x≈∈y ⟩       y≅z     = laterˡ   (_ ≈∈⟨   x≈∈y ⟩   y≅z)
_  ≈∈⟨ laterʳ x≈∈y ⟩ later y≅z     = laterʳ   (_ ≈∈⟨   x≈∈y ⟩ ♭ y≅z)

-- An example.

lemma : Pa.never ≈∈ !-sem
lemma = later (♯ later (♯ later (♯ later (♯ ∣ˡ lemma))))

------------------------------------------------------------------------
-- Compiler correctness

module Correctness where

  infix  4 _≈∈P_ _≈∈W_
  infixr 2 _≡⟨_⟩W_ _≈∈⟨_⟩P_ _≈∈⟨_⟩W_

  mutual

    data _≈∈P_ : Maybe VM.Value ⊥ → D VM.Value → Set where
      _≈∈⟨_⟩P_ : ∀ x {y z} (x≈y : x ≈∈P y) (y≅z : y ≅ z) → x ≈∈P z
      correct :
        ∀ {n} t {ρ : Env n} {c s} {k : Value → D VM.Value} →
        (hyp : ∀ v → exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩
                       ≈∈W k v) →
        exec ⟨ comp t c , s , comp-env ρ ⟩ ≈∈P (⟦ t ⟧ ρ >>= k)

    data _≈∈W_ : Maybe VM.Value ⊥ → D VM.Value → Set where
      ⌈_⌉    : ∀ {x y} (x≈y : x ≈∈ y) → x ≈∈W y
      ∣ˡ     : ∀ {x y₁ y₂} (x≈y₁ : x ≈∈W y₁) → x ≈∈W y₁ ∣ y₂
      later  : ∀ {x y} (x≈y : ♭ x ≈∈P ♭ y) → later x ≈∈W later y
      laterˡ : ∀ {x y} (x≈y : ♭ x ≈∈W   y) → later x ≈∈W       y

  _≡⟨_⟩W_ : ∀ x {y z} → x ≡ y → y ≈∈W z → x ≈∈W z
  _ ≡⟨ P.refl ⟩W y≈z = y≈z

  _≈∈⟨_⟩W_ : ∀ x {y z} → x ≈∈W y → y ≅ z → x ≈∈W z
  _  ≈∈⟨ ⌈ x≈y ⌉    ⟩W       y≅z     = ⌈ _ ≈∈⟨ x≈y ⟩ y≅z ⌉
  _  ≈∈⟨ ∣ˡ x≈y₁    ⟩W y₁≅z₁ ∣ y₂≅z₂ = ∣ˡ (_ ≈∈⟨ x≈y₁ ⟩W y₁≅z₁)
  ._ ≈∈⟨ later  x≈y ⟩W later y≅z     = later  (_ ≈∈⟨ x≈y ⟩P ♭ y≅z)
  ._ ≈∈⟨ laterˡ x≈y ⟩W       y≅z     = laterˡ (_ ≈∈⟨ x≈y ⟩W   y≅z)

  mutual

    correctW :
      ∀ {n} t {ρ : Env n} {c s} {k : Value → D VM.Value} →
      (∀ v → exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≈∈W k v) →
      exec ⟨ comp t c , s , comp-env ρ ⟩ ≈∈W (⟦ t ⟧ ρ >>= k)
    correctW (con i) {ρ} {c} {s} {k} hyp = laterˡ (
      exec ⟨ c , val (con i) ∷ s , comp-env ρ ⟩  ≈∈⟨ hyp (con i) ⟩W
      k (con i)                                  ∎)
    correctW (var x) {ρ} {c} {s} {k} hyp = laterˡ (
      exec ⟨ c , val (lookup (comp-env ρ) x) ∷ s , comp-env ρ ⟩  ≡⟨ P.cong (λ v → exec ⟨ c , val v ∷ s , comp-env ρ ⟩) (lookup-hom x ρ) ⟩W
      exec ⟨ c , val (comp-val (lookup ρ x)) ∷ s , comp-env ρ ⟩  ≈∈⟨ hyp (lookup ρ x) ⟩W
      k (lookup ρ x)                                             ∎)
    correctW (ƛ t) {ρ} {c} {s} {k} hyp = laterˡ (
      exec ⟨ c , val (comp-val (ƛ t ρ)) ∷ s , comp-env ρ ⟩  ≈∈⟨ hyp (ƛ t ρ) ⟩W
      k (ƛ t ρ)                                             ∎)
    correctW (t₁ · t₂) {ρ} {c} {s} {k} hyp =
      exec ⟨ comp t₁ (comp t₂ (app ∷ c)) , s , comp-env ρ ⟩           ≈∈⟨ correctW t₁ (λ v₁ → correctW t₂ (λ v₂ →
                                                                            ∙-correctW v₁ v₂ hyp)) ⟩W
      (⟦ t₁ ⟧ ρ >>= λ v₁ →  ⟦ t₂ ⟧ ρ >>= λ v₂ → ⟪ v₁ ∙ v₂ ⟫P  >>= k)  ≅⟨ ((⟦ t₁ ⟧ ρ ∎) >>=-cong λ _ → sym $ associative (⟦ t₂ ⟧ ρ)) ⟩
      (⟦ t₁ ⟧ ρ >>= λ v₁ → (⟦ t₂ ⟧ ρ >>= λ v₂ → ⟪ v₁ ∙ v₂ ⟫P) >>= k)  ≅⟨ sym $ associative (⟦ t₁ ⟧ ρ) ⟩
      (⟦ t₁ ⟧ ρ ⟦·⟧ ⟦ t₂ ⟧ ρ >>= k)                                   ≅⟨ sym (·-comp t₁ t₂ >>=-cong λ v → k v ∎) ⟩
      (⟦ t₁ · t₂ ⟧ ρ >>= k)                                           ∎
    correctW (t₁ ∣ t₂) {ρ} {c} {s} {k} hyp =
      exec ⟨ comp t₁ c , s , comp-env ρ ⟩  ≈∈⟨ ∣ˡ (correctW t₁ hyp) ⟩W
      (⟦ t₁ ⟧ ρ >>= k) ∣ (⟦ t₂ ⟧ ρ >>= k)  ∎

    ∙-correctW :
      ∀ {n} v₁ v₂ {ρ : Env n} {c s} {k : Value → D VM.Value} →
      (∀ v → exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≈∈W k v) →
      exec ⟨ app ∷ c , val (comp-val v₂) ∷ val (comp-val v₁) ∷ s , comp-env ρ ⟩ ≈∈W
      ⟪ v₁ ∙ v₂ ⟫P >>= k
    ∙-correctW (con i)   v₂                 _   = ⌈ fail ⌉
    ∙-correctW (ƛ t₁ ρ₁) v₂ {ρ} {c} {s} {k} hyp =
      exec ⟨ app ∷ c , val (comp-val v₂) ∷ val (comp-val (ƛ t₁ ρ₁)) ∷ s , comp-env ρ ⟩  ≈∈⟨ later (

        exec ⟨ comp t₁ [ ret ] , ret c (comp-env ρ) ∷ s , comp-env (v₂ ∷ ρ₁) ⟩                ≈∈⟨ correct t₁ (λ v → laterˡ (hyp v)) ⟩P
        (⟦ t₁ ⟧ (v₂ ∷ ρ₁) >>= k)                                                              ∎) ⟩W

      (⟪ ƛ t₁ ρ₁ ∙ v₂ ⟫P >>= k)                                                         ∎

  whnf : ∀ {x y} → x ≈∈P y → x ≈∈W y
  whnf (x ≈∈⟨ x≈y ⟩P y≅z) = x ≈∈⟨ whnf x≈y ⟩W y≅z
  whnf (correct t hyp)    = correctW t hyp

  mutual

    soundW : ∀ {x y} → x ≈∈W y → x ≈∈ y
    soundW ⌈ x≈y ⌉      = x≈y
    soundW (∣ˡ x≈y₁)    = ∣ˡ (soundW x≈y₁)
    soundW (later  x≈y) = later (♯ soundP x≈y)
    soundW (laterˡ x≈y) = laterˡ (soundW x≈y)

    soundP : ∀ {x y} → x ≈∈P y → x ≈∈ y
    soundP x≈y = soundW (whnf x≈y)

correct : ∀ t →
          exec ⟨ comp t [] , [] , [] ⟩ ≈∈
          ⟦ t ⟧ [] >>= λ v → return (comp-val v)
correct t =
  soundP $ Correctness.correct t (λ _ → ⌈ return ⌉)
  where open Correctness

------------------------------------------------------------------------
-- Type system (following Leroy and Grall)

infix 4 _⊢_∈_

data _⊢_∈_ {n} (Γ : Ctxt n) : Tm n → Ty → Set where
  con : ∀ {i} → Γ ⊢ con i ∈ nat
  var : ∀ {x} → Γ ⊢ var x ∈ lookup Γ x
  ƛ   : ∀ {t σ τ} (t∈ : ♭ σ ∷ Γ ⊢ t ∈ ♭ τ) → Γ ⊢ ƛ t ∈ σ ⇾ τ
  _·_ : ∀ {t₁ t₂ σ τ} (t₁∈ : Γ ⊢ t₁ ∈ σ ⇾ τ) (t₂∈ : Γ ⊢ t₂ ∈ ♭ σ) →
        Γ ⊢ t₁ · t₂ ∈ ♭ τ
  _∣_ : ∀ {t₁ t₂ σ} (t₁∈ : Γ ⊢ t₁ ∈ σ) (t₂∈ : Γ ⊢ t₂ ∈ σ) →
        Γ ⊢ t₁ ∣ t₂ ∈ σ

-- Ω is well-typed.

Ω-well-typed : (τ : Ty) → [] ⊢ Ω ∈ τ
Ω-well-typed τ =
  _·_ {σ = ♯ σ} {τ = ♯ τ} (ƛ (var · var)) (ƛ (var · var))
  where σ = ♯ σ ⇾ ♯ τ

-- The call-by-value fix-point combinator is also well-typed.

fix-well-typed :
  ∀ {σ τ} → [] ⊢ Z ∈ ♯ (♯ (σ ⇾ τ) ⇾ ♯ (σ ⇾ τ)) ⇾ ♯ (σ ⇾ τ)
fix-well-typed =
  ƛ (_·_ {σ = υ} {τ = ♯ _}
         (ƛ (var · ƛ (var · var · var)))
         (ƛ (var · ƛ (var · var · var))))
  where
  υ : ∞ Ty
  υ = ♯ (υ ⇾ ♯ _)

------------------------------------------------------------------------
-- Type soundness

-- WF-Value, WF-Env and WF-DV specify when a
-- value/environment/computation is well-formed with respect to a
-- given context (and type).

mutual

  data WF-Value : Ty → Value → Set where
    con : ∀ {i} → WF-Value nat (con i)
    ƛ   : ∀ {n Γ σ τ} {t : Tm (1 + n)} {ρ}
          (t∈ : ♭ σ ∷ Γ ⊢ t ∈ ♭ τ) (ρ-wf : WF-Env Γ ρ) →
          WF-Value (σ ⇾ τ) (ƛ t ρ)

  infixr 5 _∷_

  data WF-Env : ∀ {n} → Ctxt n → Env n → Set where
    []  : WF-Env [] []
    _∷_ : ∀ {n} {Γ : Ctxt n} {ρ σ v}
          (v-wf : WF-Value σ v) (ρ-wf : WF-Env Γ ρ) →
          WF-Env (σ ∷ Γ) (v ∷ ρ)

data WF-DV (σ : Ty) : D Value → Set where
  return : ∀ {v} (v-wf : WF-Value σ v) → WF-DV σ (return v)
  _∣_    : ∀ {x y}
           (x-wf : WF-DV σ x) (y-wf : WF-DV σ y) → WF-DV σ (x ∣ y)
  later  : ∀ {x} (x-wf : ∞ (WF-DV σ (♭ x))) → WF-DV σ (later x)

-- Variables pointing into a well-formed environment refer to
-- well-formed values.

lookup-wf : ∀ {n Γ ρ} (x : Fin n) → WF-Env Γ ρ →
            WF-Value (lookup Γ x) (lookup ρ x)
lookup-wf zero    (v-wf ∷ ρ-wf) = v-wf
lookup-wf (suc x) (v-wf ∷ ρ-wf) = lookup-wf x ρ-wf

-- If we can prove WF-DV σ x, then x does not "go wrong".

does-not-go-wrong : ∀ {σ x} → WF-DV σ x → ¬ now nothing ≈∈ x
does-not-go-wrong (return v-wf) ()
does-not-go-wrong (x-wf ∣ y-wf) (∣ˡ x↯)     = does-not-go-wrong x-wf x↯
does-not-go-wrong (x-wf ∣ y-wf) (∣ʳ y↯)     = does-not-go-wrong y-wf y↯
does-not-go-wrong (later x-wf)  (laterʳ x↯) =
  does-not-go-wrong (♭ x-wf) x↯

-- A variant of WF-DV, used to please the productivity checker.

infix  3 _⟨_⟩P
infixr 2 _≅⟨_⟩P_

data WF-DVP (σ : Ty) : D Value → Set where
  return      : ∀ {v} (v-wf : WF-Value σ v) → WF-DVP σ (return v)
  _∣_         : ∀ {x y} (x-wf : WF-DVP σ x) (y-wf : WF-DVP σ y) →
                WF-DVP σ (x ∣ y)
  later       : ∀ {x} (x-wf : ∞ (WF-DVP σ (♭ x))) → WF-DVP σ (later x)
  _>>=-congP_ : ∀ {τ x f}
                (x-wf : WF-DVP τ x)
                (f-wf : ∀ {v} → WF-Value τ v → WF-DVP σ (f v)) →
                WF-DVP σ (x >>= f)
  _≅⟨_⟩P_     : ∀ x {y} (x≅y : x ≅ y) (y-wf : WF-DVP σ y) → WF-DVP σ x
  _⟨_⟩P       : ∀ x (x-wf : WF-DVP σ x) → WF-DVP σ x

-- WF-DVP is sound with respect to WF-DV.

private

  -- WHNFs.

  data WF-DVW (σ : Ty) : D Value → Set where
    return : ∀ {v} (v-wf : WF-Value σ v) → WF-DVW σ (return v)
    _∣_    : ∀ {x y} (x-wf : WF-DVW σ x) (y-wf : WF-DVW σ y) →
             WF-DVW σ (x ∣ y)
    later  : ∀ {x} (x-wf : WF-DVP σ (♭ x)) → WF-DVW σ (later x)

  -- Functions which turn programs into WHNFs.

  trans-≅ : ∀ {σ x y} → x ≅ y → WF-DVW σ y → WF-DVW σ x
  trans-≅ fail            ()
  trans-≅ return          (return v-wf)   = return v-wf
  trans-≅ (x₁≅y₁ ∣ x₂≅y₂) (y₁-wf ∣ y₂-wf) = trans-≅ x₁≅y₁ y₁-wf
                                          ∣ trans-≅ x₂≅y₂ y₂-wf
  trans-≅ (later x≅y)     (later y-wf)    = later (_ ≅⟨ ♭ x≅y ⟩P y-wf)

  mutual

    _>>=-congW_ : ∀ {σ τ x f} →
                  WF-DVW σ x →
                  (∀ {v} → WF-Value σ v → WF-DVP τ (f v)) →
                  WF-DVW τ (x >>= f)
    return v-wf   >>=-congW f-wf = whnf (f-wf v-wf)
    (x-wf ∣ y-wf) >>=-congW f-wf = (x-wf >>=-congW f-wf)
                                 ∣ (y-wf >>=-congW f-wf)
    later x-wf    >>=-congW f-wf = later (x-wf >>=-congP f-wf)

    whnf : ∀ {σ x} → WF-DVP σ x → WF-DVW σ x
    whnf (return v-wf)         = return v-wf
    whnf (x-wf ∣ y-wf)         = whnf x-wf ∣ whnf y-wf
    whnf (later x-wf)          = later (♭ x-wf)
    whnf (x-wf >>=-congP f-wf) = whnf x-wf >>=-congW f-wf
    whnf (_ ≅⟨ x≅y ⟩P y-wf)    = trans-≅ x≅y (whnf y-wf)
    whnf (_ ⟨ x-wf ⟩P)         = whnf x-wf

sound : ∀ {σ x} → WF-DVP σ x → WF-DV σ x
sound = λ p → soundW (whnf p)
  where
  soundW : ∀ {σ x} → WF-DVW σ x → WF-DV σ x
  soundW (return v-wf) = return v-wf
  soundW (x-wf ∣ y-wf) = soundW x-wf ∣ soundW y-wf
  soundW (later x-wf)  = later (♯ sound x-wf)

-- Well-typed programs do not "go wrong".

mutual

  ⟦⟧-wf : ∀ {n Γ} (t : Tm n) {σ} → Γ ⊢ t ∈ σ →
          ∀ {ρ} → WF-Env Γ ρ → WF-DVP σ (⟦ t ⟧ ρ)
  ⟦⟧-wf (con i)   con             ρ-wf = return con
  ⟦⟧-wf (var x)   var             ρ-wf = return (lookup-wf x ρ-wf)
  ⟦⟧-wf (ƛ t)     (ƛ t∈)          ρ-wf = return (ƛ t∈ ρ-wf)
  ⟦⟧-wf (t₁ ∣ t₂) (t₁∈ ∣ t₂∈)     ρ-wf = ⟦⟧-wf t₁ t₁∈ ρ-wf
                                       ∣ ⟦⟧-wf t₂ t₂∈ ρ-wf
  ⟦⟧-wf (t₁ · t₂) (t₁∈ · t₂∈) {ρ} ρ-wf =
    ⟦ t₁ · t₂ ⟧ ρ          ≅⟨ ·-comp t₁ t₂ ⟩P
    ⟦ t₁ ⟧ ρ ⟦·⟧ ⟦ t₂ ⟧ ρ   ⟨ (⟦⟧-wf t₁ t₁∈ ρ-wf >>=-congP λ f-wf →
                               ⟦⟧-wf t₂ t₂∈ ρ-wf >>=-congP λ v-wf →
                               ∙-wf f-wf v-wf) ⟩P

  ∙-wf : ∀ {σ τ f v} →
         WF-Value (σ ⇾ τ) f → WF-Value (♭ σ) v →
         WF-DVP (♭ τ) ⟪ f ∙ v ⟫P
  ∙-wf (ƛ t₁∈ ρ₁-wf) v₂-wf = later (♯ ⟦⟧-wf _ t₁∈ (v₂-wf ∷ ρ₁-wf))

type-soundness : ∀ {t : Tm 0} {σ} →
                 [] ⊢ t ∈ σ → ¬ now nothing ≈∈ ⟦ t ⟧ []
type-soundness t∈ = does-not-go-wrong (sound (⟦⟧-wf _ t∈ []))


text:
module plfa.Induction where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)

-- associativity of addition: (m + n) + p ≡ m + (n + p)
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p =
  begin
    (zero + n) + p ≡⟨⟩
    zero + (n + p)
  ∎
+-assoc (suc m) n p =
  begin
    (suc m + n) + p ≡⟨⟩
    suc (m + n) + p ≡⟨⟩
    suc ((m + n) + p) ≡⟨ cong suc (+-assoc m n p) ⟩
    suc (m + (n + p)) ≡⟨⟩
    suc m + (n + p)
  ∎

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = refl
+-assoc′ (suc m) n p rewrite +-assoc′ m n p = refl

{-
  identity: m + 0 ≡ m, analogous to 0 + m ≡ m,
  which is the base case of addition
-}
+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ zero =
  begin
    zero + zero ≡⟨⟩
    zero
  ∎
+-identityʳ (suc m) =
  begin
    suc m + zero ≡⟨⟩
    suc (m + zero) ≡⟨ cong suc (+-identityʳ m) ⟩
    suc m
  ∎

+-identity′ : ∀ (m : ℕ) → m + zero ≡ m
+-identity′ zero = refl
+-identity′ (suc m) rewrite +-identity′ m = refl

{-
  m + suc n ≡ suc (m + n), analogous to suc m + n ≡ suc (m + n),
  which is the inductive case of addition for ∀ (m n :ℕ)
-}
+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n =
  begin
    zero + suc n ≡⟨⟩
    suc (zero + n)
  ∎
+-suc (suc m) n =
  begin
    suc m + suc n ≡⟨⟩
    suc (m + suc n) ≡⟨ cong suc (+-suc m n) ⟩
    suc (suc (m + n)) ≡⟨⟩
    suc (suc m + n)
  ∎

+-suc′ : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc′ zero n = refl
+-suc′ (suc m) n rewrite +-suc′ m n = refl

-- commutativity: m + n ≡ n + m
+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero ≡⟨ +-identityʳ m ⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n ≡⟨ +-suc m n ⟩
    suc (m + n) ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m) ≡⟨⟩
    suc n + m
  ∎

+-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′ m zero rewrite +-identity′ m = refl
+-comm′ m (suc n) rewrite +-suc′ m n | +-comm′ m n = refl

-- rearrange: (m + n) + (p + q) ≡ m + (n + p) + q
+-rearrange : ∀ (m n p q : ℕ) → (m + n) + (p + q) ≡ m + (n + p) + q
+-rearrange m n p q =
  begin
    (m + n) + (p + q) ≡⟨ +-assoc m n (p + q) ⟩
    m + (n + (p + q)) ≡⟨ cong (m +_) (sym (+-assoc n p q)) ⟩
    m + ((n + p) + q) ≡⟨ sym (+-assoc m (n + p) q) ⟩
    m + (n + p) + q
  ∎

-- swap: m + (n + p) ≡ n + (m + p)
+-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap m n p =
  begin
    m + (n + p) ≡⟨ +-comm m (n + p) ⟩
    (n + p) + m ≡⟨ +-assoc n p m ⟩
    n + (p + m) ≡⟨ cong (n +_) (+-comm p m) ⟩
    n + (m + p)
  ∎

+-swap′ : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap′ m n p rewrite +-comm′ m (n + p) | +-assoc′ n p m | +-comm′ p m  = refl

-- distributivity of multiplication over addition: (m + n) * p ≡ m * p + n * p
*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-distrib-+ zero n p =
  begin
    (zero + n) * p ≡⟨⟩
    zero * p + n * p
  ∎
*-distrib-+ (suc m) n p =
  begin
    (suc m + n) * p ≡⟨⟩
    suc (m + n) * p ≡⟨⟩
    p + (m + n) * p ≡⟨ cong (p +_) (*-distrib-+ m n p) ⟩
    p + (m * p + n * p) ≡⟨ sym (+-assoc p (m * p) (n * p)) ⟩
    p + m * p + n * p ≡⟨⟩
    suc m * p + n * p
  ∎

*-distrib-+′ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-distrib-+′ zero n p = refl
*-distrib-+′ (suc m) n p rewrite *-distrib-+′ m n p | sym (+-assoc′ p (m * p) (n * p)) = refl

-- associativity of multiplication: (m * n) * p ≡ m * (n * p)
*-assoc : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
*-assoc zero n p =
  begin
    (zero * n) * p ≡⟨⟩
    zero * (n * p)
  ∎
*-assoc (suc m) n p =
  begin
    (suc m * n) * p ≡⟨⟩
    (n + m * n) * p ≡⟨ *-distrib-+ n (m * n) p ⟩
    n * p + (m * n) * p ≡⟨ cong ((n * p) +_) (*-assoc m n p) ⟩
    n * p + m * (n * p) ≡⟨⟩
    suc m * (n * p)
  ∎

*-assoc′ : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
*-assoc′ zero n p = refl
*-assoc′ (suc m) n p rewrite *-distrib-+′ n (m * n) p | *-assoc′ m n p = refl

-- multiplication by zero, analogous to the base case of multiplication.
n*0≡0 : ∀ (n : ℕ) → n * zero ≡ zero
n*0≡0 zero =
  begin
    zero * zero ≡⟨⟩
    zero
  ∎
n*0≡0 (suc n) =
  begin
    suc n * zero ≡⟨ n*0≡0 n ⟩
    zero
  ∎

n*0≡0′ : ∀ (n : ℕ) → n * zero ≡ zero
n*0≡0′ zero = refl
n*0≡0′ (suc n) rewrite n*0≡0′ n = refl

-- multiplication, analogous to the inductive case of multiplication.
*-suc : ∀ (m n : ℕ) → m * suc n ≡ m + m * n
*-suc zero n =
  begin
    zero * suc n ≡⟨⟩
    zero + zero * n
  ∎
*-suc (suc m) n =
  begin
    suc m * suc n ≡⟨⟩
    suc n + m * suc n ≡⟨ cong (suc n +_) (*-suc m n) ⟩
    suc (n + (m + m * n)) ≡⟨ cong suc (sym (+-assoc n m (m * n))) ⟩
    suc (n + m + m * n) ≡⟨ cong suc (cong (_+ (m * n)) (+-comm n m)) ⟩
    suc (m + n + m * n) ≡⟨ cong suc (+-assoc m n (m * n)) ⟩
    suc m + (n + m * n) ≡⟨⟩
    suc m + suc m * n
  ∎

*-suc′ : ∀ (m n : ℕ) → m * suc n ≡ m + m * n
*-suc′ zero n = refl
*-suc′ (suc m) n rewrite *-suc′ m n | sym (+-assoc′ n m (m * n)) | +-comm n m | +-assoc m n (m * n)= refl

-- commutitavity of multiplication: m * n ≡ n * m
*-comm : ∀ (m n : ℕ) → m * n ≡ n * m
*-comm m zero =
  begin
    m * zero ≡⟨ n*0≡0 m ⟩
    zero * m
  ∎
*-comm m (suc n) =
  begin
    m * suc n ≡⟨ *-suc m n ⟩
    m + m * n ≡⟨ cong (m +_) (*-comm m n) ⟩
    m + n * m ≡⟨⟩
    suc n * m
  ∎

*-comm′ : ∀ (m n : ℕ) → m * n ≡ n * m
*-comm′ m zero rewrite n*0≡0′ m = refl
*-comm′ m (suc n) rewrite *-suc′ m n | *-comm′ m n = refl

-- zero monus (n : ℕ)
0∸n≡0 : ∀ (n : ℕ) → zero ∸ n ≡ zero
0∸n≡0 zero =
  begin
    zero ∸ zero ≡⟨⟩
    zero
  ∎
0∸n≡0 (suc n) =
  begin
    zero ∸ suc n ≡⟨⟩
    zero
  ∎

0∸n≡0′ : ∀ (n : ℕ) → zero ∸ n ≡ zero
0∸n≡0′ zero = refl
0∸n≡0′ (suc n) = refl

-- associativity of monus: m ∸ n ∸ p ≡ m ∸ (n + p)
∸-+-assoc : ∀ (m n p : ℕ) → m ∸ n ∸ p ≡ m ∸ (n + p)
∸-+-assoc zero n p =
  begin
    zero ∸ n ∸ p ≡⟨ cong (_∸ p) (0∸n≡0 n) ⟩
    zero ∸ p ≡⟨ 0∸n≡0 p ⟩
    zero ≡⟨ sym (0∸n≡0 (n + p)) ⟩
    zero ∸ (n + p)
  ∎
∸-+-assoc (suc m) zero p =
  begin
    suc m ∸ zero ∸ p ≡⟨⟩
    suc m ∸ p ≡⟨⟩
    suc m ∸ (zero + p)
  ∎
∸-+-assoc (suc m) (suc n) p =
  begin
    suc m ∸ suc n ∸ p ≡⟨⟩
    m ∸ n ∸ p ≡⟨ ∸-+-assoc m n p ⟩
    m ∸ (n + p) ≡⟨⟩
    suc m ∸ suc (n + p) ≡⟨⟩
    suc m ∸ (suc n + p)
  ∎

∸-+-assoc′ : ∀ (m n p : ℕ) → m ∸ n ∸ p ≡ m ∸ (n + p)
∸-+-assoc′ zero zero p = refl
∸-+-assoc′ zero (suc n) p rewrite 0∸n≡0 p = refl
∸-+-assoc′ (suc m) zero p = refl
∸-+-assoc′ (suc m) (suc n) p rewrite ∸-+-assoc m n p = refl

max_stars_repo_name: tobal/plfa

max_issues_repo_name: tobal/plfa

max_forks_repo_name: tobal/plfa


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Reflection utilities for Fin
------------------------------------------------------------------------

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

module Data.Fin.Reflection where

open import Data.Nat.Base as ℕ hiding (module ℕ)
open import Data.Fin.Base as Fin hiding (module Fin)
open import Data.List.Base
open import Reflection.Term
open import Reflection.Argument

------------------------------------------------------------------------
-- Term

toTerm : ∀ {n} → Fin n → Term
toTerm zero    = con (quote Fin.zero) (1 ⋯⟅∷⟆ [])
toTerm (suc i) = con (quote Fin.suc)  (1 ⋯⟅∷⟆ toTerm i ⟨∷⟩ [])


text:
module algebra where

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

-- Goals are written as normalised

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + y = y
suc x + y = suc (x + y)

record Semigroup (a : Set) : Set where
  field
    _⊛_ : a → a → a
    assoc : ∀ a b c → (a ⊛ b) ⊛ c ≡ a ⊛ (b ⊛ c)

record Monoid (a : Set) : Set where
  field
    semigroup : Semigroup a
  open Semigroup semigroup
  field
    e : a
    idl : ∀ a → e ⊛ a ≡ a
    idr : ∀ a → a ⊛ e ≡ a

record Group (a : Set) : Set where
  field
    monoid : Monoid a
  open Monoid monoid
  open Semigroup semigroup
  field
  -- TODO [aerben] fix this
    invl : ∀ a ∃ b → a ⊛ b ≡ e
    invr : ∀ a ∃ b → b ⊛ a ≡ e

record AbelianGroup (a : Set) : Set where
  field
    group : Group a
  open Group group
  open Monoid monoid
  open Semigroup semigroup
  field
    commutative : ∀ a b → a ⊛ b ≡ b ⊛ a

record CommutativeSemigroup (a : Set) : Set where
  field
    _⊛_ : a → a → a
    associative : ∀ a b c → (a ⊛ b) ⊛ c ≡ a ⊛ (b ⊛ c)
    commutative : ∀ a b → a ⊛ b ≡ b ⊛ a

plusAssociative : ∀ a b c -> (a + b) + c ≡ a + (b + c)
-- Goal: (b + c) ≡ (b + c)
-- Follows from reflexivity
plusAssociative zero b c = refl
-- Goal: suc ((a + b) + c) ≡ suc (a + (b + c))
-- Inductive step
-- Follows from induction assumption and congruence
plusAssociative (suc a) b c =
  begin
    suc ((a + b) + c)
  ≡⟨ cong suc (plusAssociative a b c) ⟩
    suc (a + (b + c))
  ∎

plusCommutativeLemma : ∀ a b -> a + suc b ≡ suc (a + b)
-- Goal: suc b ≡ suc b
-- Follows from reflexivity
plusCommutativeLemma zero b = refl
-- Goal: suc (a + suc b) ≡ suc (suc (a + b))
-- Inductive step
-- Follows from induction assumption and congruence
plusCommutativeLemma (suc a) b =
  begin
    suc (a + suc b)
  ≡⟨ cong suc (plusCommutativeLemma a b) ⟩
    suc (suc (a + b))
  ∎

plusCommutative : ∀ a b -> a + b ≡ b + a
-- Goal: zero ≡ zero
-- Follows from reflexivity
plusCommutative zero zero = refl
-- Goal: suc (a + zero) ≡ suc a
-- One-sided inductive step
-- Follows from induction assumption and congruence
plusCommutative (suc a) zero =
  begin
    suc (a + zero)
  ≡⟨ cong suc (plusCommutative a zero) ⟩
    suc a
  ∎
-- Goal: suc b ≡ suc (b + zero)
-- One-sided inductive step
-- Follows from induction assumption and congruence
plusCommutative zero (suc b) =
  begin
    suc b
  ≡⟨ cong suc (plusCommutative zero b) ⟩
    suc (b + zero)
  ∎
-- plusCommutative (suc a) (suc b) rewrite plusCommutativeAux a b | plusCommutativeAux b a = cong suc (cong suc (plusCommutative a b))
-- Goal: suc (a + suc b) ≡ suc (b + suc a)
plusCommutative (suc a) (suc b) =
  begin
    suc (a + suc b)
  ≡⟨ cong suc (plusCommutativeLemma a b) ⟩
    suc (suc (a + b))
  ≡⟨ cong suc (cong suc (plusCommutative a b)) ⟩
    suc (suc (b + a))
    -- Need to invoke symmetry since definitional equivalence does not guarantee it
  ≡⟨ cong suc (sym (plusCommutativeLemma b a)) ⟩
    suc (b + suc a)
  ∎

plusSemigroup : CommutativeSemigroup ℕ
plusSemigroup = record
  { _⊛_ = _+_
  ; associative = plusAssociative
  ; commutative = plusCommutative
  }

max_stars_repo_name: aronerben/agda-playground

max_issues_repo_name: aronerben/agda-playground

max_forks_repo_name: aronerben/agda-playground


text:
open import Type
open import Structure.Relator
open import Structure.Setoid renaming (_≡_ to _≡ₑ_)

module Structure.Sets.ZFC.Oper {ℓₛ ℓₗ ℓₑ} {S : Type{ℓₛ}} ⦃ equiv : Equiv{ℓₑ}(S) ⦄ (_∈_ : S → S → Type{ℓₗ}) ⦃ [∈]-binaryRelator : BinaryRelator(_∈_) ⦄ where

open import Functional using (id ; _∘₂_)
open import Functional.Dependent using (_∘_)
import      Lvl
open import Logic.Predicate
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Properties
open import Structure.Relator.Proofs renaming ([≡]-binaryRelator to [≡ₑ]-binaryRelator)
open import Structure.Sets.ZFC(_∈_) ⦃ [∈]-binaryRelator ⦄
import      Structure.Sets.Names
open import Syntax.Function
open import Syntax.Implication

open        Structure.Sets.Names.From-[∈] (_∈_)
open        Structure.Sets.Names.Relations (_∈_)
open        Structure.Sets.Names.One                     (_∈_)
open        Structure.Sets.Names.Two                     (_∈_)(_∈_)
open        Structure.Sets.Names.TwoDifferent            (_∈_)(_∈_)
open        Structure.Sets.Names.TwoSame                 (_∈_)(_∈_)
open        Structure.Sets.Names.Three                   (_∈_)(_∈_)(_∈_)
open        Structure.Sets.Names.ThreeNestedTwoDifferent (_∈_)
open        Structure.Sets.Names.ThreeTwoNested          (_∈_)(_∈_)(_∈_)
open import Structure.Sets.Quantifiers(_∈_)
open import Structure.Sets.Quantifiers.Proofs(_∈_) ⦃ [∈]-binaryRelator ⦄

private variable ℓ : Lvl.Level
private variable A B C D E N a b c d e x y z As : S
private variable P : S → Type{ℓ}

module _ ⦃ zfc : ZFC ⦄ where
  open ZFC(zfc)

  infixl 3001 _∩_
  infixl 3002 _⨯_ _∖_

  -- Intersection operator.
  -- Constructs a set which consists of elements which are in both LHS and RHS.
  _∩_ : S → S → S
  a ∩ b = filter(_∈ b) ⦃ binary-unaryRelatorᵣ ⦄ a

  -- "Without"-operator.
  -- Constructs a set which consists of elements which are in LHS, but not RHS.
  _∖_ : S → S → S
  a ∖ b = filter(_∉ b) ⦃ [¬]-unaryRelator ⦃ rel-P = binary-unaryRelatorᵣ ⦄ ⦄ a

  -- Intersection over arbitrary sets.
  -- Constructs a set which consists of elements which are in all of the specified sets.
  ⋂ : S → S
  ⋂(As) = filter(a ↦ (∀ₛ(As) (a ∈_))) ⦃ [∀]-unaryRelator ⦃ rel-P = [→]-unaryRelator ⦃ rel-Q = binary-unaryRelatorᵣ ⦄ ⦄ ⦄ (⋃(As))

  -- Tuple value.
  -- An ordered pair of values.
  _,_ : S → S → S
  (a , b) = pair(singleton a) (pair a b)

  -- Set product (Set of tuples) (Cartesian product).
  _⨯_ : S → S → S
  A ⨯ B = filter(t ↦ ∃ₛ(A)(a ↦ ∃ₛ(B)(b ↦ t ≡ₑ (a , b)))) ⦃ [∃ₛ]-unaryRelator ⦃ rel-P = [∃ₛ]-unaryRelator ⦃ rel-P = binary-unaryRelatorᵣ ⦃ rel-P = [≡ₑ]-binaryRelator ⦄ ⦄ ⦄ ⦄ (℘(℘(A ∪ B)))

  identityPair : S → S
  identityPair(D) = filter(xy ↦ ∃(a ↦ xy ≡ₑ (a , a))) ⦃ [∃]-unaryRelator ⦃ rel-P = binary-unaryRelatorᵣ ⦃ rel-P = [≡ₑ]-binaryRelator ⦄ ⦄ ⦄ (D ⨯ D)

  -- Quotient set.
  -- The set of equivalence classes.
  _/_ : S → (_▫_ : S → S → Type{ℓ}) ⦃ rel : BinaryRelator(_▫_) ⦄ → S
  (a / (_▫_)) ⦃ rel ⦄ = filter(aₛ ↦ ∀ₛ(aₛ)(x ↦ ∀ₛ(aₛ)(x ▫_))) ⦃ binary-unaryRelatorᵣ ⦃ rel-P = [∀ₛ]-binaryRelator {P = \x A _ → ∀ₛ(A) (x ▫_)} ⦃ rel-P = [∀ₛ]-binaryRelator ⦃ rel-P = const-binaryRelator ⦄ ⦄ ⦄ {∅} ⦄ (℘(a))

  -- Equivalence class.
  -- The set of elements which are equivalent to the specified one.
  [_of_,_] : S → S → (_▫_ : S → S → Type{ℓ}) ⦃ rel : BinaryRelator(_▫_) ⦄ → S
  [ x of a , (_▫_) ] = filter(x ▫_) ⦃ binary-unaryRelatorₗ ⦄ a

  -- The unmap of a set.
  -- The set of elements in the domain X when applied to a function gives an element in Y.
  -- Or: The inverse image of the function on the set.
  -- Or: The pre-image of the function on the set.
  -- Note:
  --   The domain is neccessary because a class function's domain is not neccesarily a set.
  --   For example: `const(x): Domain → Domain` for any (x: Domain) is a class function for which its domain is not a set.
  --   This is because const is defined for all objects in `Domain`, so if a set would have to have all objects in `Domain`, it has to be the universal set, but there is no universal set.
  unmap : S → (f : S → S) ⦃ func : Function(f) ⦄ → S → S
  unmap(X) f(Y) = filter(x ↦ f(x) ∈ Y) ⦃ [∘]-unaryRelator {P = _∈ Y} ⦃ binary-unaryRelatorᵣ ⦄ ⦄ X

  [∩]-inclusion : IntersectMembership(_∩_)
  [∩]-inclusion {A = A}{B = B}{x = x} =
    (x ∈ (A ∩ B))                     ⇔-[]
    x ∈ filter(_∈ B) ⦃ _ ⦄ A          ⇔-[ restricted-comprehension ⦃ _ ⦄ ]
    (x ∈ A) ∧ (x ∈ B)                 ⇔-end

  [∖]-inclusion : WithoutMembership(_∖_)
  [∖]-inclusion {A = A}{B = B}{x = x} =
    (x ∈ (A ∖ B))                     ⇔-[]
    x ∈ filter(_∉ B) ⦃ _ ⦄ A          ⇔-[ restricted-comprehension ⦃ _ ⦄ ]
    (x ∈ A) ∧ (x ∉ B)                 ⇔-end

  intersection : BigIntersectionMembershipWithEmpty(⋂)
  intersection {A = A}{x = x} =
    (x ∈ filter(a ↦ ∀ₛ(A)(a ∈_)) ⦃ _ ⦄ (⋃ A)) ⇔-[ restricted-comprehension ⦃ _ ⦄ ]
    (x ∈ ⋃ A) ∧ ∀ₛ(A)(x ∈_)                   ⇔-[ [∧]-map-[↔] union [↔]-reflexivity ]
    ∃(a ↦ (a ∈ A) ∧ (x ∈ a)) ∧ ∀ₛ(A)(x ∈_)    ⇔-end

  [⨯]-inclusion : (x ∈ (A ⨯ B)) ↔ ∃ₛ(A)(a ↦ ∃ₛ(B)(b ↦ x ≡ₑ (a , b)))
  [⨯]-inclusion {x = x}{A = A}{B = B} =
    (x ∈ (A ⨯ B))                                                          ⇔-[]
    x ∈ filter(t ↦ ∃ₛ(A)(a ↦ ∃ₛ(B)(b ↦ t ≡ₑ (a , b)))) ⦃ _ ⦄ (℘(℘(A ∪ B))) ⇔-[ restricted-comprehension ⦃ _ ⦄ ]
    (x ∈ ℘(℘(A ∪ B))) ∧ ∃ₛ(A)(a ↦ ∃ₛ(B)(b ↦ (x ≡ₑ (a , b))))               ⇔-[ [↔]-intro (p ↦ [∧]-intro (l p) p) [∧]-elimᵣ ]
    ∃ₛ(A)(a ↦ ∃ₛ(B)(b ↦ x ≡ₑ (a , b)))                                     ⇔-end
    where
      tuple-superset : (a ∈ A) → (b ∈ B) → ((a , b) ⊆ ℘(A ∪ B))
      tuple-superset pa pb = pair-superset
        ([↔]-to-[←] power (singleton-superset
          ([↔]-to-[←] [∪]-inclusion ([∨]-introₗ pa))
        ))
        ([↔]-to-[←] power (pair-superset
          ([↔]-to-[←] union ([∃]-intro A ⦃ [∧]-intro pair-contains-left  pa ⦄))
          ([↔]-to-[←] union ([∃]-intro B ⦃ [∧]-intro pair-contains-right pb ⦄))
        ))

      l =
        ∃ₛ(A)(a ↦ ∃ₛ(B)(b ↦ x ≡ₑ (a , b)))                     ⇒-[ [∃]-map-proof ([∧]-map id ([∃]-map-proof ([∧]-map id ([↔]-to-[→] set-extensionality)))) ]
        ∃ₛ(A)(a ↦ ∃ₛ(B)(b ↦ x ≡ (a , b)))                      ⇒-[ [∃]-map-proof ([∧]-map id ([∃]-map-proof ([∧]-map id (sub₂(_≡_)(_⊆_))))) ]
        ∃ₛ(A)(a ↦ ∃ₛ(B)(b ↦ x ⊆ (a , b)))                      ⇒-[]
        ∃ₛ(A)(a ↦ ∃ₛ(B)(b ↦ x ⊆ pair(singleton a) (pair a b))) ⇒-[ (\([∃]-intro _ ⦃ [∧]-intro pa ([∃]-intro _ ⦃ [∧]-intro pb sub ⦄) ⦄) {y} → transitivity(_⊆_) sub (tuple-superset pa pb) {y}) ]
        x ⊆ ℘(A ∪ B)                                           ⇒-[ [↔]-to-[←] power ]
        x ∈ ℘(℘(A ∪ B))                                        ⇒-end

  instance
    ⋂-function : Function(⋂)
    Function.congruence ⋂-function {x = As}{y = Bs} AsBs = filter-function ⦃ _ ⦄ ⦃ _ ⦄ p (congruence₁(⋃) AsBs) where
      p : ∀{x} → (∀{A} → (A ∈ As) → (x ∈ A)) ↔ (∀{B} → (B ∈ Bs) → (x ∈ B))
      p = [↔]-intro (_∘ (substitute₂ᵣ(_∈_) AsBs)) (_∘ (substitute₂ᵣ(_∈_) (symmetry(_≡ₑ_) AsBs)))

  instance
    ∪-operator : BinaryOperator(_∪_)
    BinaryOperator.congruence ∪-operator = congruence₁(⋃) ∘₂ congruence₂(pair)

  instance
    ∩-operator : BinaryOperator(_∩_)
    BinaryOperator.congruence ∩-operator xy1 xy2 = filter-function ⦃ _ ⦄ ⦃ _ ⦄ ([↔]-to-[→] set-extensionality xy2) xy1

  instance
    ∖-operator : BinaryOperator(_∖_)
    BinaryOperator.congruence ∖-operator xy1 xy2 = filter-function ⦃ _ ⦄ ⦃ _ ⦄ ([¬]-unaryOperator ([↔]-to-[→] set-extensionality xy2)) xy1

  instance
    [,]-operator : BinaryOperator(_,_)
    BinaryOperator.congruence [,]-operator xy1 xy2 = congruence₂(pair) (congruence₁(singleton) xy1) (congruence₂(pair) xy1 xy2)


text:
module ListMember where

open import Prelude

data Member {A : Set} (x : A) : List A -> Set where
  here : {xs : List A} -> Member x (cons x xs)
  there : forall {y} -> {xs : List A} -> Member x xs -> Member x (cons y xs)

empty-no-member' : forall {A} -> {x : A} -> Member x nil -> Empty
empty-no-member' p = {!!}

empty-no-member : forall {A} -> {x : A} -> Not (Member x nil)
empty-no-member = is-absurd empty-no-member'

neither-here-nor-there' : forall {A} -> {x y : A} {ys : List A} -> (x == y -> Empty) -> (Member x ys -> Empty) -> Member x (cons y ys) -> Empty
neither-here-nor-there' not-here not-there member = {!!}

neither-here-nor-there : forall {A} -> {x y : A} {ys : List A} -> Not (x == y) -> Not (Member x ys) -> Not (Member x (cons y ys))
neither-here-nor-there (is-absurd not-here) (is-absurd not-there) = is-absurd (neither-here-nor-there' not-here not-there)

member : forall {A} -> ((x y : A) -> Dec (x == y)) -> (v : A) -> (vs : List A) -> Dec (Member v vs)
member eq? x nil = no empty-no-member
member eq? x (cons y ys) with eq? x y
member eq? x (cons y ys) | yes p = {!!}
member eq? x (cons y ys) | no pf with member eq? x ys
member eq? x (cons y ys) | no pf | member = {!!}

max_stars_repo_name: carlostome/martin

max_issues_repo_name: carlostome/martin

max_forks_repo_name: carlostome/martin


text:
-- We ban termination pragmas inside `where` clauses.

module Issue1137 where

postulate
  A : Set
  a : A

foo : A
foo = bar
  where
  {-# TERMINATING #-}
  bar : A
  bar = bar


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

module Categories.Diagram.Coend.Properties where

open import Categories.Category.Core using (Category)
open import Categories.Category.Product
import Categories.Category.Construction.Cowedges as Cowedges
open import Categories.Category.Construction.Functors
open import Categories.Category.Equivalence
open import Categories.Category.Equivalence.Preserves
open import Categories.Diagram.Coend
open import Categories.Diagram.Colimit
open import Categories.Diagram.Cowedge
open import Categories.Diagram.Cowedge.Properties
open import Categories.Functor using (Functor)
open import Categories.Functor.Bifunctor using (Bifunctor)
open import Categories.Functor.Instance.Twisted
import Categories.Morphism as M
open import Categories.NaturalTransformation hiding (id)
open import Categories.NaturalTransformation.Dinatural
open import Categories.Object.Initial as Initial

import Categories.Morphism.Reasoning as MR

open import Level
open import Data.Product using (Σ; _,_)
open import Function using (_$_)

module _ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
  (F : Bifunctor (Category.op C) C D) where
  open Cowedges F

  -- Being a Coend is the same as being an Initial object in the category of Cowedges
  Coend⇒Initial : Coend F → Initial Cowedges
  Coend⇒Initial c = record
    { ⊥ = cowedge
    ; ⊥-is-initial = record
      { ! = λ {A} → record { u = factor A ; commute = universal }
      ; !-unique = λ {A} f → unique {A} (Cowedge-Morphism.commute f)
      }
    }
    where
    open Coend c

  Initial⇒Coend : Initial Cowedges → Coend F
  Initial⇒Coend i = record
    { cowedge = ⊥
    ; factor = λ W → u {W₂ = W} !
    ; universal = commute !
    ; unique = λ {_} {g} x → !-unique (record { u = g ; commute = x })
    }
    where
    open Initial.Initial i
    open Cowedge-Morphism

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

module _ (F : Functor E (Functors (Product (Category.op C) C) D)) where
  private
    module C = Category C
    module D = Category D
    module E = Category E
    module NT = NaturalTransformation
  open D
  open HomReasoning

  open MR D
  open Functor F
  open Coend hiding (E)
  open NT using (η)

  CoendF : (∀ X → Coend (F₀ X)) → Functor E D
  CoendF coend = record
    { F₀           = λ X → Coend.E (coend X)
    ; F₁           = F₁′
    ; identity     = λ {A} → unique (coend A) (id-comm-sym ○ ∘-resp-≈ʳ (⟺ identity))
    ; homomorphism = λ {A B C} {f g} → unique (coend A) $ λ {Z} → begin
      (F₁′ g ∘ F₁′ f) ∘ dinatural.α (coend A) Z                         ≈⟨  pullʳ (universal (coend A)) ⟩
      (F₁′ g ∘ (dinatural.α (coend B) Z ∘ η (F₁ f) (Z , Z) )  )         ≈⟨ pullˡ (universal (coend B))  ⟩
      ((dinatural.α (coend C) Z ∘ η (F₁ g) (Z , Z)) ∘ η (F₁ f) (Z , Z)) ≈˘⟨ pushʳ homomorphism ⟩
      dinatural.α (coend C) Z ∘ η (F₁ (g E.∘ f)) (Z , Z)                ∎
    ; F-resp-≈     = λ {A B f g} eq → unique (coend A) $ λ {Z} → begin
      F₁′ g ∘ dinatural.α (coend A) Z                               ≈⟨ universal (coend A) ⟩
      dinatural.α (coend B) Z ∘ η (F₁ g) (Z , Z)                   ≈˘⟨ refl⟩∘⟨ F-resp-≈ eq ⟩
      dinatural.α (coend B) Z ∘ η (F₁ f) (Z , Z)                   ∎
    }
    where F₁′ : ∀ {X Y} → X E.⇒ Y → Coend.E (coend X) ⇒ Coend.E (coend Y)
          F₁′ {X} {Y} f = factor (coend X) $ record
            { E         = Coend.E (coend Y)
            ; dinatural = dinatural (coend Y) ∘> F₁ f
            }

-- A Natural Transformation between two functors induces an arrow between the
-- (object part of) the respective coends.
module _ {P Q : Functor (Product (Category.op C) C) D} (P⇒Q : NaturalTransformation P Q) where
  open Coend renaming (E to coend)
  open Category D

  coend-η : {cp : Coend P} {cq : Coend Q} → coend cp ⇒ coend cq
  coend-η {cp} {cq} = factor cp ((record
    { E = Coend.E cq
    ; dinatural = dtHelper record
      { α = λ c →  dinatural.α cq c ∘ η (c , c)
      ; commute = λ {C} {C′} f → begin
        id ∘ (αq C ∘ η (C , C)) ∘ P.₁ (f , C.id)    ≈⟨ pushʳ assoc ⟩
        (id ∘ αq C) ∘ (η (C , C) ∘ P.₁ (f , C.id))  ≈⟨ refl⟩∘⟨ nt.commute (f , C.id) ⟩
        (id ∘ αq C) ∘ (Q.₁ (f , C.id) ∘ η (C′ , C)) ≈⟨ pullˡ assoc ⟩
        (id ∘ αq C ∘ Q.₁ (f , C.id)) ∘ η (C′ , C)   ≈⟨ αq-comm f ⟩∘⟨refl ⟩
        (id ∘ αq C′ ∘ Q.₁ (C.id , f)) ∘ η (C′ , C)  ≈⟨ pushˡ sym-assoc ⟩
        (id ∘ αq C′) ∘ Q.₁ (C.id , f) ∘ η (C′ , C)  ≈⟨ refl⟩∘⟨ nt.sym-commute (C.id , f) ⟩
        (id ∘ αq C′) ∘ η (C′ , C′) ∘ P.₁ (C.id , f) ≈⟨ pullʳ sym-assoc ⟩
        id ∘ (αq C′ ∘ η (C′ , C′)) ∘ P.₁ (C.id , f) ∎
      }
    }))
    where
    module nt = NaturalTransformation P⇒Q
    open nt using (η)
    open HomReasoning
    module C = Category C
    module P = Functor P
    module Q = Functor Q
    open DinaturalTransformation (dinatural cp) renaming (α to αp; commute to αp-comm)
    open DinaturalTransformation (dinatural cq) renaming (α to αq; commute to αq-comm)
    open Cowedge
    open MR D

module _ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
  (F : Bifunctor (Category.op C) C D) where
  private
    Eq = CoconesTwist≅Cowedges F
    module O = M D
  open M (Cowedges.Cowedges F)
  open Functor

  open StrongEquivalence Eq renaming (F to F⇒)

  -- Coends and Colimits are equivalent, in the category Cowedge F
  Coend-as-Colimit : (coend : Coend F) → (cl : Colimit (Twist′ C D F)) → Coend.cowedge coend ≅ F₀ F⇒ (Colimit.initial.⊥ cl)
  Coend-as-Colimit coend cl = Initial.up-to-iso (Cowedges.Cowedges F) (Coend⇒Initial F coend) (pres-Initial Eq initial)
    where
    open Colimit cl

  -- Which then induces that the objects, in D, are also equivalent.
  Coend-as-Colimit-on-Obj : (coend : Coend F) → (cl : Colimit (Twist′ C D F)) → Coend.E coend O.≅ Colimit.coapex cl
  Coend-as-Colimit-on-Obj coend cl = record
    { from = Cowedge-Morphism.u (M._≅_.from X≅Y)
    ; to = Cowedge-Morphism.u (M._≅_.to X≅Y)
    ; iso = record
      { isoˡ = M._≅_.isoˡ X≅Y
      ; isoʳ = M._≅_.isoʳ X≅Y
      }
    }
    where
      X≅Y = Coend-as-Colimit coend cl
      open Category D

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
-- {-# OPTIONS --without-K                #-}  -- No accepted!

module K-FOTC where

postulate D : Set

data _≡_ (x : D) : D → Set where
  refl : x ≡ x

K : (x : D)(P : x ≡ x → Set) → P refl → (p : x ≡ x) → P p
K x P pr refl = pr

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc