Saizan

module Rev where

open import Data.List.Reverse
open import Relation.Binary.PropositionalEquality as PE
open import Relation.Binary.HeterogeneousEquality
open import Data.List
open import Data.Empty
open import Data.Product
open import Data.List.Properties

Saizan

{-# LANGUAGE UndecidableInstances, OverlappingInstances, MultiParamTypeClasses, FunctionalDependencies, TypeOperators
           , TypeFamilies, EmptyDataDecls, FlexibleInstances, ScopedTypeVariables, KindSignatures, GADTs #-}

module Uncurry where

data Fun :: * -> * -> * -> * where
  Done :: Fun () r r
  Moar :: Fun xs f r -> Fun (x,xs) (x -> f) r

class Uncurry args func result | func -> args, func -> result, args result -> func where

Saizan

{-# LANGUAGE GADTs, EmptyDataDecls#-}

module Calculator where

type Stack = [Double]

data Arity = Unary | Binary
data Associativity = Left | Right

data Operator = Operator Arity Associativity

Saizan

module Impossible where

open import Coinduction
open import Function
open import Data.Empty
open import Data.Conat
open import Data.Bool
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Product
open import Relation.Nullary

Saizan

{-# LANGUAGE KindSignatures #-}
import Bound.Class

{-

What laws should Bound have?

We need at least enough to make sure the typical Monad Exp instances are valid.

Let's start by writing some generic Bound instances.

Saizan

record SP : Set₁ where
  field
    F    : Set → Set

    mon  : ∀{ρ ρ'} → (ρ → ρ') → (Fρ : F ρ) → F ρ'

    Supp : ∀ {ρ} → F ρ → Set

    mon-Supp : ∀ {ρ ρ'} (f : ρ → ρ') (Fρ : F ρ)
               → Supp (mon f Fρ) → Supp Fρ

Saizan

{-# OPTIONS --type-in-type #-}
module Coden (m : Set → Set) where

open import Category.Functor
open RawFunctor {{...}}

Ran : (K : Set → Set) → Set → Set
Ran K a = (c : Set) → (a → K c) → m c

α : ∀ {a}{K} → Ran K (K a) → m a

Saizan

{-# OPTIONS --cubical #-}
module Extension where

open import Agda.Primitive
open import Cubical.Core.Everything
open import Agda.Builtin.Nat

infixr 4 _,,_

record I×_ (A : Setω) : Setω where

Saizan

{-# OPTIONS --cubical #-}
module _ where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.HITs.SetTruncation

elimSetTrunc : ∀ {ℓ} (A : Type ℓ) (B : ∥ A ∥₀ → Type ℓ) →
  (f : (a : A) → B (∣ a ∣₀)) →
  (g : (x y : ∥ A ∥₀) → (p q : x ≡ y) →

Saizan

module Prims where
  primitive
    primLockUniv : Set₁

open Prims renaming (primLockUniv to LockU) public

postulate
  Cl : Set
  k0 : Cl
  Tick : Cl → LockU