1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
(* Testing 8.5 regression with type classes not solving evars
redefined while trying to solve them with the type class mechanism *)
Global Set Universe Polymorphism.
Monomorphic Universe i.
Inductive paths {A : Type} (a : A) : A -> Type :=
idpath : paths a a.
Arguments idpath {A a} , [A] a.
Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.
Inductive trunc_index : Type :=
| minus_two : trunc_index
| trunc_S : trunc_index -> trunc_index.
Notation "-1" := (trunc_S minus_two) (at level 0).
Class IsPointed (A : Type) := point : A.
Arguments point A {_}.
Record pType :=
{ pointed_type : Type ;
ispointed_type : IsPointed pointed_type }.
Coercion pointed_type : pType >-> Sortclass.
#[export] Existing Instance ispointed_type.
Private Inductive Trunc (n : trunc_index) (A :Type) : Type :=
tr : A -> Trunc n A.
Arguments tr {n A} a.
Record ooGroup :=
{ classifying_space : pType@{i} }.
Definition group_loops (X : pType)
: ooGroup.
Proof.
(** This works: *)
pose (x0 := point X).
pose (H := existT (fun x:X => Trunc -1 (x = point X)) x0 (tr idpath)).
clear H x0.
(** But this doesn't: *)
pose (existT (fun x:X => Trunc -1 (x = point X)) (point X) (tr idpath)).
Abort.
|
