JasonGross

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

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

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

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

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

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

Module Bug.
  Axiom A : Set.
  Axiom I : Set.

  Module Type IWrapper.
    Axiom i : I.
  End IWrapper.

  Module R (i : IWrapper).
    Axiom f : A.

JasonGross

Module Bug.  

  Module Type M.
  End M.

  Module Type FT.
  End FT.

  Module F (m : M) <: FT.
  End F.

JasonGross

---------- Forwarded message ----------
From: Michael Shulman 
Date: Sunday, October 13, 2013
Subject: Generalizing Higher Inductive Types
To: Jason Gross <jasongross9@gmail.com>
Cc: Peter LeFanu Lumsdaine <p.l.lumsdaine@gmail.com>

JasonGross

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))