jcreedcmu

it follows from 4ct that:
[[[
every normal term with one free variable has at least one of these colorings:
0

every normal term with two free variables has at least one of these colorings:
12
21

every normal term with three free variables has at least one of these colorings:

jcreedcmu

module Jq where

{-

functional lenses are neat.

https://medium.com/@dtipson/functional-lenses-d1aba9e52254
https://bartoszmilewski.com/category/lens/
https://bartoszmilewski.com/2015/07/13/from-lenses-to-yoneda-embedding/
https://twanvl.nl/blog/haskell/cps-functional-references

jcreedcmu

{-# OPTIONS --without-K --rewriting #-}

module Contractible where

open import HoTT hiding ( Type ; _$_ )

Type = Type0

idp[] : {A : Type} (a b : A) (path : a == b) → idp == path [ (λ c → a == c) ↓ path ]
idp[] a b idp = idp

jcreedcmu

module Loeb where

postulate
  □ : Set → Set
  L : Set → Set

unpack>t : Set → Set
unpack>t C = □ (□ (L C) → □ (□ (L C) → C))
unpack<t : Set → Set
unpack<t C = □ (□ (□ (L C) → C) → □ (L C))

jcreedcmu

{-# OPTIONS --without-K --rewriting --type-in-type #-}

module Leibniz where

open import HoTT

{- Here's Leibniz equality.
   Two things a and b are equal if for every property P that a satisfies, b satisfies it also. -}
module _ {A : Set} where
  _=#_ : (a b : A) → Set

jcreedcmu

import bpy
import mathutils
import math
from math import radians
from mathutils import Matrix

# When DEBUG = True, this sets up a change-frame callback
# that modifies the scene to be the current state of the animation,
# deleting every object that doesn't have the 'pres' attribute set.

jcreedcmu

;; if the binding at point is implicit, make it explicit, and vice-versa
(defun jcreed-swap-agda-implicit ()
  (interactive)
  (save-excursion
    (if (re-search-backward "[({]" nil t)
        (let ((ms (match-string 0)))
          (cond
           ((equal ms "(")
            (replace-match "{")
            (re-search-forward ")")

jcreedcmu

{-# OPTIONS --without-K --rewriting #-}
module Sharp where

open import HoTT hiding ( O; Path; _*_ )

module WithArity (C : Set) where
  postulate
    𝕀 : Set
    η : C → 𝕀
    Path : ∀ {ℓ} (A : 𝕀 → Set ℓ) (a : (c : C) → A (η c)) → Set ℓ

jcreedcmu

{"message":[144,57,21],"delta_us":0}
{"message":[144,57,0],"delta_us":305940}
{"message":[144,59,30],"delta_us":49327}
{"message":[144,59,0],"delta_us":338871}
{"message":[144,45,28],"delta_us":15964}
{"message":[144,60,39],"delta_us":25149}
{"message":[176,64,127],"delta_us":69250}
{"message":[144,52,31],"delta_us":230901}
{"message":[144,45,0],"delta_us":273879}
{"message":[144,52,0],"delta_us":44989}

jcreedcmu

{-# OPTIONS --without-K #-}
module RtnzDatabase where

open import HoTT

Σ' = Σ -- renaming just so we can make the following syntax decl
syntax Σ' A (λ x → B) = ∃ x ∶ A · B

FinSet = Set -- not really constraining to finite, just conveying intent