mietek’s gists

mietek / keybase.md

Created July 12, 2019 16:46

Keybase proof

I hereby claim:

To claim this, I am signing this object:

mietek / SystemF.agda

Last active June 30, 2019 21:41 — forked from AndrasKovacs/SystemF.agda

Embedding of predicative polymorphic System F in Agda.


	open import Function
	open import Data.Nat
	open import Data.Fin renaming (_+_ to _f+_)
	open import Data.Unit
	open import Relation.Binary.PropositionalEquality
	open import Data.Product
	open import Data.Sum
	open import Data.Vec
	open import Data.Vec.Properties

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 / 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 / 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 / STLCSemantics.agda

Last active November 10, 2017 03:07

Materials for my Haskell.SG talk on 9 November 2017

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 / 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 / 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 / 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

Miëtek Bak mietek