myuon

{-# LANGUAGE DeriveFunctor #-}

import Control.Applicative
import Control.Arrow
import qualified Control.Category as C
import Control.Monad

data Process m a b = Process { runProcess :: a -> m (b, Process m a b) }
                   deriving (Functor)

myuon

definition (in Category) Iso where
  "Iso f g ≡ (f ∘ g ≈ id (dom g)) & (g ∘ f ≈ id (dom f))"

definition Iso_on_objects ("_ [ _ ≅ _ ]" 40) where
  "𝒞 [ A ≅ B ] ≡ (∃f∈Arr 𝒞. ∃g∈Arr 𝒞. f ∈ Hom[𝒞][A,B] & g ∈ Hom[𝒞][B,A] & Category.Iso 𝒞 f g)"

record 'c setmap =
  setdom :: "'c set"
  setcod :: "'c set"
  setfunction :: "'c ⇒ 'c"

myuon

theory CommRing
imports Main
begin

no_notation plus (infixl "+" 65)
no_notation minus (infixl "-" 65)
no_notation times (infixl "*" 70)
no_notation zero_class.zero ("0")
no_notation one_class.one ("1")

myuon

module Codensity where

open import Level
open import Function
open import Category.Functor
open import Category.Monad
open import Relation.Binary.PropositionalEquality

record Functor {a b} (F : Set a → Set b) : Set (suc (a ⊔ b)) where
  field

myuon

infix 4 _∈_ _∉_
data _∈_ {f} {A : Set f} (x : A) (B : Set f) : Set (suc f) where
  in-eq : A ≡ B → x ∈ B

_∉_ : {B : Set} → B → Set → Set₁
X ∉ A = (X ∈ A) → ⊥

module elem-lemmas where
  elem-∈ : {A B : Set} → ∀{x : B} → x ∈ A → A
  elem-∈ {x = x} (in-eq ≡-refl) = x

myuon

module Set-Syntax where
  Σ-syntax′ : ∀ {a b} (A : Set a) → (A → Set b) → Set (a ⊔ b)
  Σ-syntax′ = Σ

  syntax Σ-syntax′ A (\x → B) = [ x ∈ A ∣ B ]

  Σ-type : ∀{a b} → Set a → Set b → Set _
  Σ-type A B = Σ A (\_ → B)

  syntax Σ-type A P = P ⊆ A

myuon

module CatScratch where

open import Function hiding (_∘_; id)
open import Level
open import Data.Product
open import Relation.Binary
open import Relation.Binary.Core using (_≡_)
open import Relation.Binary.PropositionalEquality using (setoid)
import Relation.Binary.EqReasoning as EqR
import Relation.Binary.SetoidReasoning as SetR

myuon

Require Import FunctionalExtensionality.

Module Category.

Axiom proof_irrelevance : forall (P : Prop) (u v : P), u = v.

Reserved Notation "a ~> b" (at level 90).
Reserved Notation "a o; b" (at level 45, right associativity).

Class Category : Type :=

myuon

Require Import ssreflect.

Class Monad (M : Type -> Type) :=
{
  mreturn : forall {A}, A -> M A
; mbind : forall {A B}, M A -> (A -> M B) -> M B

; left_return : forall A B (a : A) (k : A -> M B), mbind (mreturn a) k = k a
; right_return : forall A (m : M A), mbind m mreturn = m
; composite : forall A B (m : M A) (k : A -> M A) (h : A -> M B),

myuon

{-# LANGUAGE ExistentialQuantification, PackageImports #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
import Control.Applicative
import Text.Trifecta
import "mtl" Control.Monad.State
import qualified Data.Map as M
import Data.Monoid
import Data.Ratio

newtype Var = Var String deriving (Eq, Ord, Show)