Skip to content

Instantly share code, notes, and snippets.

View JasonGross's full-sized avatar

Jason Gross JasonGross

263 followers · 15 following
View GitHub Profile
@JasonGross
JasonGross / funext.v
Created July 16, 2013 21:47
judgemental funext out of HITs
Parameter A : Type.
Parameter B : A -> Type.
Parameters f g : forall a : A, B a.
Axiom p : forall x, f x = g x.
Inductive I :=
| zero : I
| one : I
| seg : zero = one.
@JasonGross
JasonGross / test.hs
Created August 2, 2013 23:29
ghc -XMultiParamTypeClasses -XFunctionalDependencies -XUndecidableInstances ~/test.hsghc -XMultiParamTypeClasses -XFunctionalDependencies -XUndecidableInstances ~/test.hs
main :: IO Int
main = main
class Key k m | k -> m where
empty :: m v
lookup' :: k -> m v -> Maybe v
data MB t = MB (Maybe t) (Maybe t)
instance Key Bool MB where
@JasonGross
JasonGross / test.hs
Created August 2, 2013 23:30
ghc -XMultiParamTypeClasses -XFunctionalDependencies -XUndecidableInstances ~/test.hsghc -XMultiParamTypeClasses -XFunctionalDependencies -XUndecidableInstances ~/test.hs
main :: IO Int
main = main
class Key k m | k -> m where
empty :: m v
lookup' :: k -> m v -> Maybe v
data MB t = MB (Maybe t) (Maybe t)
instance Key Bool MB where
@JasonGross
JasonGross / Pseudofunctor.v
Created August 3, 2013 17:29
Require Export Category.Core Category.Morphisms Cat FunctorCategory.
Require Import Common.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Universe Polymorphism.
Local Open Scope morphism_scope.
@JasonGross
JasonGross / theorem2_6_5.v
Created August 7, 2013 22:48
Require Import HoTT.
Theorem theorem2_6_5' {A A'} {P : A -> Type} {P' : A' -> Type} (g : A -> A') (h : forall a, P a -> P' (g a)) (x y : sigT P) (p : x.1 = y.1)\
(q : transport _ p x.2 = y.2) : Type.
pose (fun z => (g z.1 ; h z.1 z.2)) as f.
refine (ap f (path_sigma P x y p q) = path_sigma P' (f x) (f y) (ap g p) _).
subst f; simpl.
destruct q.
destruct p.
@JasonGross
JasonGross / funext_interval.v
Created August 12, 2013 05:29
Proof of funext from the interval.
Require Import HoTT.
Axiom Interval : Type.
Axioms zero one : Interval.
Axiom seg : zero = one.
Axiom Interval_rect_nodep : forall P
(Pzero Pone : P)
(H : Pzero = Pone),
Interval -> P.
@JasonGross
JasonGross / 886.v
Created September 3, 2013 20:11
https://code.google.com/p/agda/issues/detail?id=886&q=Display in Coq
Module Bug.
Axiom A : Set.
Axiom I : Set.
Module Type IWrapper.
Axiom i : I.
End IWrapper.
Module R (i : IWrapper).
Axiom f : A.
@JasonGross
JasonGross / foo.v
Created September 3, 2013 20:36
Module Bug.
Module Type M.
End M.
Module Type FT.
End FT.
Module F (m : M) <: FT.
End F.
@JasonGross
JasonGross / gist:7093588
Created October 22, 2013 01:04
Email about higher inductive types.
---------- Forwarded message ----------
From: Michael Shulman
Date: Sunday, October 13, 2013
Subject: Generalizing Higher Inductive Types
To: Jason Gross <[email protected]>
Cc: Peter LeFanu Lumsdaine <[email protected]>
@JasonGross
JasonGross / gist:7103651
Created October 22, 2013 16:21
log of attempt at makefile verbosity
jgross@cagnode17:/tmp/fooo/bar$ ls
foo.c foo.h Makefile
jgross@cagnode17:/tmp/fooo/bar$ cat foo.c
jgross@cagnode17:/tmp/fooo/bar$ cat foo.h
jgross@cagnode17:/tmp/fooo/bar$ cat Makefile
V = 0
CC_0 := @echo -t "Compiling $<..."; $(CC)
CC_1 := $(CC)
CC = $(CC_$(V))