Skip to content

Instantly share code, notes, and snippets.

View TOTBWF's full-sized avatar

Reed Mullanix TOTBWF

204 followers · 12 following
View GitHub Profile
@TOTBWF
TOTBWF / Segal.lagda.md
Last active November 3, 2024 15:12
1-Categories ala Segal
description
Segal conditions.
@TOTBWF
TOTBWF / BCO.lagda.md
Created October 27, 2024 22:51
BCOs and CBPV 
module Blog.BCO where
@TOTBWF
TOTBWF / InversionHell.lagda.md
Created October 1, 2024 14:37
description
Inversion hell.
@TOTBWF
TOTBWF / Dialectica.lagda.md
Last active June 14, 2024 14:55
Dialectica Categories with Valeria
description
Dialectica categories, done representably. June 4th, 2024 at the HIM trimester.
@TOTBWF
TOTBWF / IdempotentSystem.lagda.md
Last active March 15, 2024 20:34
Idempotent systems
description
Idempotent systems. 
open import Cat.Diagram.Monad
open import Cat.Prelude

import Cat.Reasoning
import Cat.Functor.Reasoning
@TOTBWF
TOTBWF / ListHLevels.lagda.md
Created June 21, 2023 16:31
A short proof that lists form a set

A short, self-contained proof that List A has UIP if A has UIP

First, we enable the --without-K flag, which removes UIP as an axiom. We also import Agda.Primitive, which gives us access to the Level type, though this isn't strictly required. We also add a variable block so we don't need to constantly abstract over types and levels.

{-# OPTIONS --without-K --safe #-}
module ListHLevels where
@TOTBWF
TOTBWF / Syntax.lagda.md
Created February 18, 2023 15:44
Encode-decode for indexed terms 
{-# OPTIONS --lossy-unification #-}
open import Cat.Prelude

open import Data.List
open import Data.List.Member
open import Data.Sum

open import Theories.Signature
@TOTBWF
TOTBWF / CNF.lagda.md
Created January 28, 2023 22:44
CNF for classic propositional logic 
open import 1Lab.Prelude

open import Data.Bool
open import Data.Fin
open import Data.List
open import Data.Nat

module Data.Bool.CNF where
@TOTBWF
TOTBWF / day-1.c
Last active December 2, 2022 00:01
Advent of Code 2022 Day 1 with excessive SIMD
#include <fcntl.h>
#include <immintrin.h>
#include <stdio.h>
#include <sys/mman.h>
#include <sys/stat.h>
uint32_t parse_4_digits(const __m128i input) {
const __m128i char_0 = _mm_set1_epi8('0');
// Normalize the '0' char to actually be 0x00.
@TOTBWF
TOTBWF / 1Lab.Reflection.Duh.agda
Created October 4, 2022 22:42
A simple Agda tactic that just uses the first valid thing in scope.
module 1Lab.Reflection.Duh where
open import 1Lab.Reflection
open import 1Lab.Prelude
open import Data.List
open import Data.Nat
private
try-all : Term → Nat → Telescope → TC Term
try-all goal _ [] = typeError $ strErr "Couldn't find anything!" ∷ []