JasonGross

let gen_const_list ~is_done:(is_done : 'n -> bool) ~pred:(pred : 'n -> 'n)
    (size : 'n) (v : 'a) : 'a list =
  let rec helper size v =
    if is_done size then [] else v::(helper (pred size) v)
  in helper size v

let const_list : int -> 'a -> 'a list =
  gen_const_list ~is_done:(fun size -> size <= 0) ~pred:(fun n -> n - 1)

module Stupid = struct

JasonGross

Require Import HoTT.

Local Open Scope path_scope.
Local Open Scope equiv_scope.

Section ap.
  Variables A B : Type.
  Variables x y : A.
  Variable f : A -> B.
  Context `{IsEquiv _ _ f}.

JasonGross

Inductive paths A (x : A) : A -> Type := idpath : paths A x x.

Notation "x = y" := (paths _ x y).

Record Contr (A : Type) :=
  {
    center : A;
    contr : forall y, center = y
  }.

JasonGross

Set Implicit Arguments.

Section lim.
  Variable J : Type.
  Variable F : J -> Type.
  Variable L : Type.
  Variable Phi : forall x, L -> F x.
  Definition IsLimit := forall N (Psi : forall x, N -> F x), { u : N -> L & forall x, (fun y => (Phi x) (u y)) = Psi x }.
End lim.

JasonGross

Goal forall T, ~~(T + ~T).
Proof.
  intros T negLEM.
  cut (~T).
  - intro negT.
    apply (negLEM (inr negT)).
  - intro t.
    apply (negLEM (inl t)).
Defined

JasonGross

Require Import Overture Equivalences.

Goal forall A (a : A) (B : forall x, a = x -> Type) (x : A), Equiv (forall x (p : a = x), B x p) (B a (idpath a)).
Proof.
  intros.
  apply (equiv_adjointify
           (fun f => f _ idpath)
           (fun p0 => fun x0 p => match p as p' in (_ = y) return B y p' with
                                    | idpath => p0
                                  end)).

JasonGross

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

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

(* 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

(* 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.