dorchard

module OrdersAndEquivClasses where

open import Level
open import Data.Product

-- X is the base
-- S is a set of things drawn from X
record PreOrder {l l' : Level} {X : Set l} {S : X -> Set l'} : Set (Level.suc l ⊔ l') where
 field
  _<_ : Σ X S -> Σ X S -> Set l

dorchard

#!/bin/bash
cp ~/template.tex paper.tex

dorchard

\documentclass[a4paper]{article}

\usepackage[table,x11names]{xcolor}
\usepackage{afterpage}
\usepackage{colortbl}
\usepackage{forloop}
\usepackage{geometry}

\begin{document}

dorchard

Whilst using the Ott tool for defining programming languages and semantics (http://www.cl.cam.ac.uk/~pes20/ott/) I have noticed that I sometimes get the following error when compiling its generated LaTeX:

  ! LaTeX Error: Too many math alphabets used in version normal.

This is a difficult to track down error (but also mildly amusing)! Here are the solutions/reasons I've found so far:

• Using pdflatex? Try switching to xelatex which can support up 256 math fonts.

dorchard

(by Dominic Orchard, School of Computing, University of Kent, 2018)

Disclaimer: this advice is non exhaustive, and every piece of advice might not suit you. At least, I hope it helps you to think about how you can develop your own strategy for exam preparation.

My top tip is to see exams as formative rather than purely about assessment. This is an opportunity to force yourself to learn a topic deeply, which will then benefit you in the future, rather than a box ticking exercise to get a fancy piece of paper at the end. This will orient your attitude to maximising your potential.

Exams are hard. They occupy a short space of time in your whole life but they can have a big impact on the rest of it, so make the most of them. Study well and study wisely.

Exam preparation

dorchard

'.source.idris':
  '∞':
    'prefix': 'Inf'
    'body': '∞'

'.source.haskell':
  '∞':
    'prefix': 'Inf'
    'body': '∞'

dorchard

default: quick

quick:
	pdflatex paper.tex

full:
	pdflatex paper.tex
	bibtex paper
	pdflatex paper.tex
	pdflatex paper.tex

dorchard

{-# LANGUAGE GADTs, TypeFamilies, EmptyDataDecls #-}

{-

A Haskell-based implementation of the monadic semantics for the
simply-typed Call-By-Name computational lambda calculus, following
Moggi's 'Computational lambda-calculus and monads' (1989) (technical report version)
but for the typed calculus (rather than untyped as in this paper).

Category theory seminar, Programming Languages and Systems group,

dorchard

% Highlight comments in darkgreen
\definecolor{darkgreen}{rgb}{0,0.5,0}
\newcommand{\commenthighlight}{\color{darkgreen}\quad-{}- }
\let\onelinecomment=\commenthighlight

% Highlight constructors in darkblue
\definecolor{darkblue}{rgb}{0,0,0.5}
\renewcommand{\Conid}[1]{\textcolor{darkblue}{\textit{#1}}}

dorchard

module Category where

open import Level
open import Relation.Binary.PropositionalEquality

open Level

record Category {lobj : Level} {larr : Level} : Set (suc (lobj ⊔ larr)) where
  field obj : Set lobj
        arr : (src : obj) -> (trg : obj) -> Set larr