blob: ca4d23803ed2d1d852825e1183a1d2bc44effe24 (
plain)
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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
Set Primitive Projections.
Set Implicit Arguments.
Record prod {A} {B}:= pair { fst : A ; snd : B }.
Notation " A * B " := (@prod A B) : type_scope.
Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
Notation pr1 := (@projT1 _ _).
Arguments prod : clear implicits.
Check (@projT1 _ (fun x : nat => x = x)).
Check (fun s : @sigT nat (fun x : nat => x = x) => s.(projT1)).
Record rimpl {b : bool} {n : nat} := { foo : forall {x : nat}, x = n }.
Check (fun r : @rimpl true 0 => r.(foo) (x:=0)).
Check (fun r : @rimpl true 0 => @foo true 0 r 0).
Check (fun r : @rimpl true 0 => foo r (x:=0)).
Check (fun r : @rimpl true 0 => @foo _ _ r 0).
Check (fun r : @rimpl true 0 => r.(@foo _ _)).
Check (fun r : @rimpl true 0 => r.(foo)).
Notation "{ x : T & P }" := (@sigT T P).
Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
(* Notation "{ x : T * U & P }" := (@sigT (T * U) P). *)
Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
Arguments idpath {A a} , [A] a.
Class IsEquiv {A B : Type} (f : A -> B) := {}.
Local Instance isequiv_tgt_compose A B
: @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
(A -> B)
(@compose A {xy : B * B & fst xy = snd xy} B
(@compose {xy : B * B & fst xy = snd xy} _ B (@snd B B) pr1)).
(* Toplevel input, characters 220-223: *)
(* Error: Cannot infer this placeholder. *)
Local Instance isequiv_tgt_compose' A B
: @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
(A -> B)
(@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) pr1)).
(* Toplevel input, characters 221-232: *)
(* Error: *)
(* In environment *)
(* A : Type *)
(* B : Type *)
(* The term "pr1" has type "sigT ?30 -> ?29" while it is expected to have type *)
(* "{xy : B * B & fst xy = snd xy} -> ?27 * B". *)
Local Instance isequiv_tgt_compose'' A B
: @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
(A -> B)
(@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _)
(fun s => s.(projT1)))).
(* Toplevel input, characters 15-241:
Error:
Cannot infer an internal placeholder of type "Type" in environment:
A : Type
B : Type
x : ?32
. *)
|
