Skip to content

Instantly share code, notes, and snippets.

View jcmckeown's full-sized avatar

Jesse C. McKeown jcmckeown

3 followers · 0 following
View GitHub Profile
@jcmckeown
jcmckeown / subterms.v
Last active August 29, 2015 14:02
Some trivial coq tactics whose purpose is to automagically extract/fold particular subterms of the goal type. The idea is to reduce ambiguity in human/coq interactions.
Require Import HoTT.
(* or your favourite source for the needed arrithmetic types *)
Open Scope list_scope.
(**
These are tactics to aid human consumption/production of terms compatible
with the goal type --- sometimes coq prettyprinting produces ambiguous
appearances, while refine fails unless you fill in more holes --- which is
@jcmckeown
jcmckeown / CoherentCategoriesModulo.v
Last active August 29, 2015 14:01
Trying to get at a definition of Categories internal to coq/HoTT, with all the compositions and their equations and Nothing Else; the gist of this gist is: do not assume equations before you need them, and prove them if possible! Third revision: added some comments, removed some NOP proof lines. Maybe some other tweaks?
Require Import HoTT.
Open Scope path_scope.
Open Scope type_scope.
Section Categories.
(** Everyone knows a category has an underlying graph, so we should
mention them *)
@jcmckeown
jcmckeown / Cofiber.v
Last active December 19, 2015 09:09
Coq 8.4 has module-local inductive types; the idea is that you can't see why the underlying type can't work, because you're not allowed to do destructuring on the local inductive. This has the nifty side-effect (not "computational effects") that you can define (obstructed) functions that "compute" the way we want, but that have meaningful obstru…
Require Import HoTT.
Local Open Scope path_scope.
Local Open Scope equiv_scope.
Module Export Cofiber.
Local Inductive cofiber {A B : Type} (f : A -> B) : Type :=
| apex : cofiber f
| ground : B -> cofiber f.
@jcmckeown
jcmckeown / nCkAnomaly.v
Created June 23, 2013 04:27
Producing an "Anomaly: please report" Sat June 22. 2013; anomaly arises whether using the @HoTT or standard coq library (with minor changes in nCkComp)
Inductive nCk : nat -> nat -> Type :=
|zz : nCk 0 0
| incl { m n : nat } : nCk m n -> nCk (S m) (S n)
| excl { m n : nat } : nCk m n -> nCk (S m) n.
Definition nCkComp { l m n : nat } :
nCk l m -> nCk m n -> nCk l n.
Proof.
intro.
revert n.
@jcmckeown
jcmckeown / nCk_Eq.v
Last active December 18, 2015 16:59 — forked from anonymous/nCk_Eq.v
(see header comment)
(** Approximating decidable equality for the type nCk.
As with GlobSet and DeltaSet, we implement locally the needed homotopy theory (which is trivial);
`Require Import Homotopy` will do as well, modulo some notation, some names. I'd also bet some
disappointment that the rhyming staves at the end of `nCk_uniq` are encapsulated in some named
Lemma in `Homotopy`. Since the path arguments to `trans` in the concluding Lemma are cases of
`@path nat`, which is a proposition in the sense of Voevodsky, it should be straight-forward (if
tedious) to produce decidable equality in `nCk` by using those in `(list bool)` and `nat`.
*)
@jcmckeown
jcmckeown / DeltaSets.v
Last active December 18, 2015 12:59
Very nearly how to describe delta-sets by the "dependent type" trick. It isn't quite right, because of Stuff... but never mind that for now. Among other things, it's rather difficult to extract what data a DeltaSkeleton actually involves. That is, coq can `eval cbv` the expressions `projT1 (DeltaSkeleton 0)`, and produces exactly what we want, `…
(** A 0-skeletal filling of an l-simplex is (S l) vertices.
A (S k)-skeletal filling of an l-simplex has (S l) C (S k) (S k)-cells
matching their boundaries in a k-skeletal filling of an l-simplex;
where to say the (S k)-cell matches its boundary is to say that its boundary
is the underlying k-skeletal filling of its underlying (S k)-simplex.
*)
(** I don't know why coq makes its type system so rich and its proof system so comparatively strict.
possibly (almost certainly) because the reverse combination would be too difficult/inconsistent?
for instance, it makes intuitive sense that this next Fixpoint should be equivalent (as a type over nat * nat)
@jcmckeown
jcmckeown / GlobSets.v
Created June 13, 2013 01:15
Roughly, ordinary globular sets, by the dependent type trick described for n-skeletal simplicial sets during the IAS Univalent Foundations programme year. It was remarked that getting a good notion of "simplicial set", with all degrees occupied, elluded codification, but the trick in the following should adapt trivially; that is, a Δ-set with ce…
(** Define the types we need. Checked in version Trunk of April 2013 *)
Polymorphic Inductive eqv { X : Type } : X -> X -> Type :=
reflect (x : X) : eqv x x.
(** and assume the simplification we want *)
Polymorphic Axiom funextT :
forall (X : Type) (P : X -> Type) (f g : forall x , P x) (s :
forall x, eqv (f x) (g x)) , eqv f g.