Merge pull request #1758 from jdchristensen/fix-HITs

HITs: fix inconsistencies from several HITs

test/bugs/github1758.v

@@ -0,0 +1,44 @@
+From HoTT Require Import Basics.Overture HIT.Interval HIT.Flattening Colimits.GraphQuotient
+          Spaces.Torus.Torus Cubical.
+
+(* Test that various higher inductive types are defined correctly.  If they are defined in the most naive way, two uses of the induction principle that are definitionally equal on the point constructors will be considered definitionally equal, which is inconsistent.  There is an idiom that must be used in order to force Coq to regard the supplementary data as being required as well.  See, for example, Colimits/GraphQuotient.v for the idiom. *)
+
+Fail Definition test_interval (P : interval -> Type) (a : P zero) (b : P one)
+  (p p' : seg # a = b) :
+  interval_ind P a b p = interval_ind P a b p'
+  := 1.
+
+Fail Definition test_wtil {A B f g C D} (Q : Wtil A B f g C D -> Type)
+  (cct' : forall a x, Q (cct a x))
+  (ppt' : forall b y, (ppt b y) # (cct' (f b) y) = cct' (g b) (D b y))
+  (ppt'' : forall b y, (ppt b y) # (cct' (f b) y) = cct' (g b) (D b y))
+  : Wtil_ind Q cct' ppt' = Wtil_ind Q cct' ppt''
+  := 1.
+
+Section GraphQuotient_bug.
+  Local Definition R : Unit -> Unit -> Type := fun x y => Unit.
+
+  (* This should be the circle. *)
+  Local Definition Q := GraphQuotient R.
+
+  (* This is the identity map. *)
+  Local Definition id : Q -> Q := GraphQuotient_rec gq (fun a b r => gqglue r).
+
+  (* This is the constant map. *)
+  Local Definition cst : Q -> Q.
+  Proof.
+    refine (GraphQuotient_rec gq _).
+    intros [] [] r.
+    reflexivity.
+  Defined.
+
+  Fail Definition test_graphquotient : id = cst := 1.
+End GraphQuotient_bug.
+
+Fail Definition test_torus (P : Torus -> Type) (pb : P tbase)
+  (pla pla' : DPath P loop_a pb pb)
+  (plb : DPath P loop_b pb pb)
+  (ps : DPathSquare P surf pla pla plb plb)
+  (ps' : DPathSquare P surf pla' pla' plb plb)
+  : Torus_ind P pb pla plb ps = Torus_ind P pb pla' plb ps'
+  := 1.

theories/Colimits/GraphQuotient.v

@@ -22,8 +22,8 @@ Module Export GraphQuotient.
     (gqglue' : forall a b (s : R a b), gqglue@{i j u} s # gq' a = gq' b)
     : forall x, P x := fun x =>
     match x with
-    | gq a => gq' a
-    end.
+    | gq a => fun _ => gq' a
+    end gqglue'.
 
   Axiom GraphQuotient_ind_beta_gqglue@{i j u k}
   : forall  {A : Type@{i}} {R : A -> A -> Type@{j}}

theories/HIT/Flattening.v

@@ -29,7 +29,7 @@ Definition Wtil_ind {A B f g C D} (Q : Wtil A B f g C D -> Type)
   (cct' : forall a x, Q (cct a x))
   (ppt' : forall b y, (ppt b y) # (cct' (f b) y) = cct' (g b) (D b y))
   : forall w, Q w
-  := fun w => match w with cct a x => cct' a x end.
+  := fun w => match w with cct a x => fun _ => cct' a x end ppt'.
 
 Axiom Wtil_ind_beta_ppt
   : forall {A B f g C D} (Q : Wtil A B f g C D -> Type)

theories/HIT/Interval.v

@@ -30,14 +30,6 @@ Axiom interval_ind_beta_seg : forall (P : interval -> Type)
 
 End Interval.
 
-(*   Should fail:
-Lemma test (P : interval -> Type) (a : P zero) (b : P one)
-      (p p' : seg # a = b) :
-    interval_ind P a b p = interval_ind P a b p'.
-reflexivity.
-*)
-
-
 Definition interval_rec (P : Type) (a b : P) (p : a = b)
   : interval -> P
   := interval_ind (fun _ => P) a b (transport_const _ _ @ p).

theories/HIT/README.txt

@@ -1,10 +1,5 @@
-The files in this directory require Yves Bertot's "private types"
-extension to Coq in order to implement higher inductive types (HITs).
-The "private types" extension is included in the stable branch of the
-HoTT/coq repository, so if you followed the INSTALL instructions you
-should be okay.
+The files in this directory use "private inductive types" in order to
+implement higher inductive types (HITs).
 
-The files which use HITs are currently segregated into this directory
-because the "private types" extension is a hack whose details may
-change in the future, and we are still hoping to one day have an
-actual implementation of HITs.
+Many of the files which use HITs are currently segregated into this
+directory, but they can also be found in other directories.

theories/Spaces/Torus/Torus.v

@@ -19,10 +19,8 @@ Module Export Torus.
   (* We define the induction principle for Torus *)
   Definition Torus_ind (P : Torus -> Type) (pb : P tbase)
     (pla : DPath P loop_a pb pb) (plb : DPath P loop_b pb pb)
-    (ps : DPathSquare P surf pla pla plb plb) (x : Torus) : P x.
-  Proof.
-    by destruct x.
-  Defined.
+    (ps : DPathSquare P surf pla pla plb plb) (x : Torus) : P x
+  := (match x with tbase => fun _ _ _ => pb end) pla plb ps.
 
   (* We declare propsitional computational rules for loop_a and loop_b *)
   Axiom Torus_ind_beta_loop_a : forall (P : Torus -> Type) (pb : P tbase)