Navigation Menu

Skip to content

Instantly share code, notes, and snippets.

View mietek's full-sized avatar

Miëtek Bak mietek

282 followers · 0 following
View GitHub Profile
@mietek
mietek / Proset.agda
Last active February 18, 2018 15:56
Preordered sets using squashed types or explicit uniqueness
module Proset where
open import Agda.Primitive public
using (_⊔_)
open import Agda.Builtin.Equality public
using (_≡_ ; refl)
--------------------------------------------------------------------------------
@mietek
mietek / Category.agda
Last active December 4, 2017 15:40
First meaningful use of irrelevance
module Category where
open import Agda.Primitive public
using (Level ; _⊔_)
renaming (lzero to ℓ₀)
open import Function public
using (id ; flip)
renaming (_∘′_ to _∘_)
@mietek
mietek / EncodeDecode.agda
Created November 30, 2017 14:04
Converting between strings and natural numbers
module EncodeDecode where
open import Agda.Builtin.Char
using (Char)
renaming ( primCharToNat to ord
; primNatToChar to chr
)
open import Agda.Builtin.Equality
using (_≡_ ; refl)
@mietek
mietek / STLCSemantics.agda
Last active November 10, 2017 03:07
Materials for my Haskell.SG talk on 9 November 2017
module STLCSemantics where
--------------------------------------------------------------------------------
-- Types
infixr 7 _⇒_
data Type : Set
where
@mietek
mietek / RenSubFirstDraft.agda
Created September 24, 2017 23:05
-- Inspired by
-- https://github.com/andreasabel/strong-normalization/blob/master/agda/RenamingAndSubstitution.agda
-- and
-- https://github.com/mietek/coquand
{-# OPTIONS --no-positivity-check #-}
module RenSubFirstDraft where
@mietek
mietek / RenSub.agda
Last active September 21, 2017 08:32
-- Inspired by
-- https://github.com/andreasabel/strong-normalization/blob/master/agda/RenamingAndSubstitution.agda
-- and
-- https://github.com/mietek/coquand
{-# OPTIONS --no-positivity-check #-}
module RenSub where
open import Function public
@mietek
mietek / CoTest.agda
Last active July 21, 2019 17:42
Breaking subject reduction in Coq, and not breaking it in Agda (any more)
-- More information:
-- http://coq-club.inria.narkive.com/3zS9pwcc/coinductive-types-and-type-preservation
-- https://lists.chalmers.se/pipermail/agda/2008/000383.html
module CoTest where
open import Prelude public
{-
@mietek
mietek / Category.agda
Last active May 31, 2019 01:44 — forked from dorchard/Category.agda
Definition of a category as an Agda record: level polymorphic in the objects and arrows
module Category where
open import Agda.Primitive public
using (Level ; _⊔_ ; lzero ; lsuc)
open import Agda.Builtin.Equality public
using (_≡_ ; refl)
record Category ℓ ℓ′ : Set (lsuc (ℓ ⊔ ℓ′)) where
@mietek
mietek / Brighton.tmTheme
Last active August 5, 2017 11:52
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
<plist version="1.0">
<dict>
<key>author</key>
<string>Miëtek Bak</string>
<key>gutterSettings</key>
<dict>
<key>background</key>
<string>#F9F9F9</string>
@mietek
mietek / Main.agda
Created July 30, 2017 01:59 — forked from gelisam/Main.agda
cat in Agda using copatterns
{-# OPTIONS --copatterns #-}
module Main where
-- A simple cat program which echoes stdin back to stdout, but implemented using copatterns
-- instead of musical notation, as requested by Miëtek Bak (https://twitter.com/mietek/status/806314271747481600).
open import Data.Nat
open import Data.Unit
open import Data.Bool
open import Data.Char