Skip to content

Instantly share code, notes, and snippets.

View JasonGross's full-sized avatar

Jason Gross JasonGross

186 followers · 11 following
View GitHub Profile
@JasonGross
JasonGross / finite_choice.v
Created January 30, 2014 19:40
Proof that finite sets have choice
Require Import HoTT.HoTT.
Require Import HoTT.hit.minus1Trunc.
Generalizable All Variables.
Set Implicit Arguments.
Local Notation "|| T ||" := (minus1Trunc T).
(*Local Notation "| x |" := (min1 x).*)
Fixpoint Fin (n : nat) : Type :=
@JasonGross
JasonGross / pi_homogenous.v
Created January 31, 2014 00:43
Pi types can be homogenous
Require Import HoTT.HoTT.
Require Import HoTT.hit.minus1Trunc HoTT.hit.Truncations.
Generalizable All Variables.
Set Implicit Arguments.
Class IsHomogenous X (x : X) := is_homogenous : forall y, existT idmap X y = existT idmap X x.
Lemma path_forall_type `{Funext, Univalence} X (Y Y' : X -> Type)
: Y == Y' -> (forall x, Y x) = (forall x, Y' x).
@JasonGross
JasonGross / split_sig_ltac.v
Created February 5, 2014 19:47
Ltac + typeclasses implementation of a partial split_sig tactic
(* Coq's build in tactics don't work so well with things like [iff]
so split them up into multiple hypotheses *)
Ltac split_in_context ident funl funr :=
repeat match goal with
| [ H : context p [ident] |- _ ] =>
let H0 := context p[funl] in let H0' := eval simpl in H0 in assert H0' by (apply H);
let H1 := context p[funr] in let H1' := eval simpl in H1 in assert H1' by (apply H);
clear H
end.
@JasonGross
JasonGross / hott_ltac_split_sig.v
Last active August 29, 2015 13:56
HoTT + Ltac + typeclasses implementation of a split_sig tactic
(* Coq's build in tactics don't work so well with things like [iff]
so split them up into multiple hypotheses *)
Ltac split_in_context ident funl funr :=
repeat match goal with
| [ H : context p [ident] |- _ ] =>
let H0 := context p[funl] in let H0' := eval simpl in H0 in assert H0' by (apply H);
let H1 := context p[funr] in let H1' := eval simpl in H1 in assert H1' by (apply H);
clear H
end.
@JasonGross
JasonGross / slow_record_eta.v
Last active August 29, 2015 13:56
Example of eta for records being slow in coq
(* File reduced by coq-bug-finder from 7411 lines to 2271 lines. *)
Generalizable All Variables.
Definition relation (A : Type) := A -> A -> Type.
Class Reflexive {A} (R : relation A) := reflexivity : forall x : A, R x x.
Class Symmetric {A} (R : relation A) := symmetry : forall x y, R x y -> R y x.
Class Transitive {A} (R : relation A) := transitivity : forall x y z, R x y -> R y z -> R x z.
Notation "( x ; y )" := (existT _ x y) : fibration_scope.
Open Scope fibration_scope.
@JasonGross
JasonGross / Nicolai.v
Created February 18, 2014 04:11
The Truncation Map |_| : ℕ -> ‖ℕ‖ is nearly Invertible - in Coq - http://homotopytypetheory.org/2013/10/28/the-truncation-map-_-%E2%84%95-%E2%80%96%E2%84%95%E2%80%96-is-nearly-invertible/
Require Import Overture types.Universe hit.minus1Trunc Contractible types.Sigma Equivalences.
Set Implicit Arguments.
Local Open Scope path_scope.
Section invert.
Context `{Univalence}.
Definition pathto (T : Type) (x : T) := { y : T & x = y }.
Local Instance trunc_pathto T x : Contr (@pathto T x)
@JasonGross
JasonGross / bool_extract_info.v
Last active August 29, 2015 13:56
We have [a = b], but [f a ≠ f b], because [f] is a dependent function which just happens to land in the same type for [a] and [b].
Require Import Overture types.Universe hit.minus1Trunc Equivalences types.Bool types.Sigma.
Set Implicit Arguments.
Local Open Scope path_scope.
Definition negb (b : Bool) : Bool
:= if b then false else true.
Instance isequiv_negb : IsEquiv negb.
Proof.
@JasonGross
JasonGross / not_nearly.v
Last active August 29, 2015 13:56
Composition is not what you think it is! Why "nearly invertible" isn't.
Require Import Overture hit.Interval hit.minus1Trunc types.Bool types.Universe Tactics types.Sigma Equivalences PathGroupoids types.Forall.
Set Implicit Arguments.
Local Open Scope equiv_scope.
Local Open Scope path.
Definition Q `{Univalence} : interval -> Type
:= interval_rectnd
Type Bool Bool
(path_universe negb).
@JasonGross
JasonGross / W.v
Created February 28, 2014 05:50
W-types
Require Import Overture types.Bool types.Unit.
Set Implicit Arguments.
Inductive W A (B : A -> Type) :=
sup : forall a, (B a -> W B) -> W B.
Definition WNat := @W Bool (fun b => if b then Empty else Unit).
Definition WNat0 : WNat := sup true (fun x => match x : Empty with end).
Definition WNatS : WNat -> WNat := fun n => sup false (fun x => n).
@JasonGross
JasonGross / lift_univ.v
Created March 4, 2014 17:00
(A = B) -> (Lift A = Lift B)
Definition lift_eq_down {A B : Type} (p : @paths Type A B) : @paths Type (A : Type) (B : Type)
:= match p in (@paths _ _ B) return (@paths Type (A : Type) B) with
| idpath => idpath
end.
Set Printing All.
Check @lift_eq_down.
(*
lift_eq_down (* Top.1226 Top.1227 Top.1229 Top.1229 Top.1230 Top.1231