useronym

open import Data.Empty

-- Intuition: We have objects (Struct) which consist of a bunch of fields (Atomic)
-- which can be in different states (state).

record Struct : Set₁ where
  field
    Atomic : Set
    State  : Atomic → Set
open Struct

useronym

data State = St Int ((Int, State) -> (Int, State))


unfold2 :: (State, State) -> [Int]
unfold2 (St x f, St y g) = let (x', St y' g') = f (x, St y g) in
                             x : (unfold2 (St y' g', St x' f))


-- Some examples.

useronym

open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Product
open import Data.Empty
open import Function


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

useronym

module Delay
%default total


codata Partial : Type -> Type where
  Now   : a -> Partial a
  Later : Partial a -> Partial a


Functor Partial where

useronym

module Coalgebra where

open import Coinduction
open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Nat


data List (A : Set) : Set where
  ∅ˡ   : List A

useronym

module Topology where

import Level
open import Function
open import Data.Empty
open import Data.Unit
open import Data.Nat hiding (_⊔_)
open import Data.Fin
open import Data.Product
open import Relation.Nullary

useronym

module K.Semantics.Algebra where
open import K.Syntax
open import Common
open import Algebra.Structures using (IsBooleanAlgebra)
open import Relation.Binary using (Preorder; IsEquivalence)


record ModalAlgebra : Set₁ where
  infix 6 _≃_
  infix 7 _∧_

useronym

open import Function                              using (_$_) renaming (_∘′_ to _∘_) public
open import Category.Monad public
open import Data.Empty                            using (⊥) public
open import Data.Unit                             using (⊤) renaming (tt to •) public
open import Data.Fin                              using (Fin) renaming (zero to zeroᶠ; suc to sucᶠ) public
open import Data.Product                          using (_×_) renaming (_,_ to ⟨_,_⟩; proj₁ to π₁; proj₂ to π₂) public
open import Data.Bool                             using (Bool; true; false; if_then_else_; not) renaming (_∧_ to _and_; _∨_ to _or_) public
open import Data.Maybe                            using (Maybe; just; nothing) renaming (monad to Mmonad) public
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst₂; cong₂) public

useronym

module BCI.Hilbert.Definition where
open import Common

-- A tree variant of a Hilbert-style proof system with "BCI" as axioms.


data Form : Set where
  var : Atom → Form
  _⇒_ : Form → Form → Form
infixr 10 _⇒_

useronym

module test1 where
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong₂) public


data List (A : Set) : Set where
  ∅   : List A
  _,_ : List A → A → List A
infixl 10 _,_

data _⊆_ {A} : List A → List A → Set where