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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
|
Notation "'∏' x .. y , P" := (forall x, .. (forall y, P) ..)
(at level 200, x binder, y binder, right associativity) : type_scope.
Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..)
(at level 200, x binder, y binder, right associativity).
Reserved Notation "X ≃ Y" (at level 80, no associativity).
Reserved Notation "g ∘ f" (at level 40, left associativity).
Set Primitive Projections.
Record total2 { T: Type } ( P: T -> Type ) := tpair { pr1 : T; pr2 : P pr1 }.
Arguments tpair {_} _ _ _.
Arguments pr1 {_ _} _.
Arguments pr2 {_ _} _.
Notation "'∑' x .. y , P" := (total2 (λ x, .. (total2 (λ y, P)) ..))
(at level 200, x binder, y binder, right associativity) : type_scope.
Definition funcomp {X Y : Type} {Z:Y->Type} (f : X -> Y) (g : ∏ y:Y, Z y) := λ x, g (f x).
Declare Scope functions.
Open Scope functions.
Notation "g ∘ f" := (funcomp f g) : functions.
Definition isweq {X Y : Type} (f : X -> Y) : Type.
Admitted.
Definition weq (X Y : Type) : Type.
exact (∑ f:X->Y, isweq f).
Defined.
Notation "X ≃ Y" := (weq X%type Y%type) : type_scope.
Definition pr1weq {X Y : Type} := pr1 : X ≃ Y -> (X -> Y).
Coercion pr1weq : weq >-> Funclass.
Definition make_weq {X Y : Type} (f : X -> Y) (is: isweq f) : X ≃ Y.
exact (tpair (λ f : X -> Y, isweq f) f is).
Defined.
Theorem twooutof3c {X Y Z : Type} (f : X -> Y) (g : Y -> Z)
(isf : isweq f) (isg : isweq g) : isweq (g ∘ f).
Admitted.
Definition weqcomp {X Y Z : Type} (w1 : X ≃ Y) (w2 : Y ≃ Z) : X ≃ Z.
exact (make_weq (λ (x : X), w2 (w1 x)) (twooutof3c w1 w2 (pr2 w1) (pr2 w2))).
Defined.
Delimit Scope weq_scope with weq.
Definition weqcomp_to_funcomp {X Y Z : Type} {f : X ≃ Y} {g : Y ≃ Z} :
pr1weq (weqcomp f g) = pr1weq g ∘ pr1weq f.
Admitted.
Definition stn ( n : nat ) : Type.
Admitted.
Definition sequenceToFunction {X} (x:∑ n, stn n -> X) : stn (pr1 x) -> X.
Admitted.
Lemma foo
M
(I : Type)
(m : I -> M)
(n : nat)
(x x' : stn n ≃ I)
(K:stn n -> M) L Z
:
@eq (forall _ : stn n, M) Z
(@sequenceToFunction M
(@tpair nat (fun x0 : nat => forall _ : stn x0, M) n
(fun z : stn n => K (@pr1weq I (stn n) L (@pr1weq (stn n) I x z)))))
.
Proof.
Fail rewrite weqcomp_to_funcomp.
Abort.
|
