Skip to content

Instantly share code, notes, and snippets.

View madnight's full-sized avatar
💭
One does not so much learn category theory as absorb it over time.

Fabian Beuke madnight

💭
One does not so much learn category theory as absorb it over time.
229 followers · 238 following
View GitHub Profile
@madnight
madnight / identity_is_isomorphism.v
Created October 7, 2023 21:01
Proof that Identity Morphism is an Isomorphism
Section IdentityIsomorphism.
Variable Obj : Type.
Variable Hom : Obj -> Obj -> Type.
Variable id : forall A : Obj, Hom A A.
Variable composition : forall {X Y Z : Obj}, Hom Y Z -> Hom X Y -> Hom X Z.
Notation "g 'o' f" := (composition g f) (at level 50).
Hypothesis id_left : forall A B : Obj, forall f : Hom A B, (id B) o f = f.
@madnight
madnight / identity_is_unique.v
Created September 19, 2023 18:41
Proof that Identity Morphism is Unique
Section Category.
Variable Obj : Type.
Variable Hom : Obj -> Obj -> Type.
Variable composition : forall {X Y Z : Obj}, Hom Y Z -> Hom X Y -> Hom X Z.
Notation "g 'o' f" := (composition g f) (at level 50).
Variable id : forall {X : Obj}, Hom X X.
Hypothesis id_left : forall {X Y : Obj} (f : Hom X Y), id o f = f.
@madnight
madnight / safeHead_is_natural.v
Created September 12, 2023 18:57
Proof that safeHead is natural
Require Import List.
Import ListNotations.
Require Import FunInd.
Require Import Coq.Init.Datatypes.
Inductive Maybe (A:Type) : Type :=
| Just : A -> Maybe A
| Nothing : Maybe A.
Arguments Just {A} a.
@madnight
madnight / list-monad.py
Last active October 30, 2022 19:19
List Monad in Python
"""A List Monad."""
from __future__ import annotations
from itertools import chain
from typing import Any as b
from typing import Callable as Function
from typing import Iterable as Functor
from typing import List
from typing import TypeVar
@madnight
madnight / envs.md
Created February 27, 2019 07:57

App configuration in environment variables: for and against

For (some of these as per the 12 factor principles)

  1. they are are easy to change between deploys without changing any code

  2. unlike config files, there is little chance of them being checked into the code repo accidentally

@madnight
madnight / profile.log
Created October 8, 2017 20:22
SCRIPT /home/x/.vim/plugged/vim-misc/autoload/xolox/misc/cursorhold.vim
Sourced 1 time
Total time: 0.000191
Self time: 0.000191
count total (s) self (s)
" Rate limiting for Vim's CursorHold event.
"
" Author: Peter Odding <peter@peterodding.com>
" Last Change: June 22, 2014
@madnight
madnight / active-issues.sql
Created September 21, 2017 09:32 — forked from alysonla/active-issues.sql
Queries that power the open source section of the 2016 Octoverse report https://octoverse.github.com/
-- Active issues
-- Count of total active issues in the specified time frame
-- Source: githubarchive public data set via Google BigQuery http://githubarchive.org/
SELECT
COUNT(DISTINCT JSON_EXTRACT_SCALAR(events.payload, '$.issue.id')) AS events_issue_count
FROM (SELECT * FROM TABLE_DATE_RANGE([githubarchive:day.],TIMESTAMP('2015-09-01'),TIMESTAMP('2016-08-31')))
AS events
-- 10,723,492 active issues
@madnight
madnight / hn-aeson.hs
Created September 30, 2016 15:23 — forked from Gonzih/hn-aeson.hs
Aeson HN example of nested JSON (unoptimized binary ~20 mb)
{-# LANGUAGE OverloadedStrings #-}
import Data.Aeson
import Control.Applicative ((<$>), (<*>))
import Control.Monad (mzero)
import Network.HTTP.Conduit
import Data.ByteString.Lazy.Internal (ByteString(..))
data Item = Item { title :: String
, url :: String
@madnight
madnight / restpdf.rb
Last active July 23, 2016 14:49
require 'json'
require 'base64'
require 'tempfile'
require 'sinatra'
require 'pdfkit'
# HTTP Status Codes
OK, BAD_REQUEST, UNAUTHORIZED, INTERNAL_SERVER_ERROR = 200, 400, 401, 500
# service is up and running