blob: 5bee69fcdecfcc12cc03766f6b7c0488d91827da (
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
64
65
66
67
68
69
70
71
72
73
74
75
76
|
Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from 4464 lines to 4137 lines, then from 3683 lines to 118 lines, then from 124 lines to 75 lines. *)
Set Universe Polymorphism.
Definition admit {T} : T.
Admitted.
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.
Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
match p with idpath => u end.
Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
:= match p with idpath => idpath end.
Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
: forall x, f x = g x
:= fun x => match h with idpath => idpath end.
Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
equiv_inv : B -> A ;
eisretr : forall x, f (equiv_inv x) = x
}.
Arguments eisretr {A B} f {_} _.
Record Equiv A B := BuildEquiv {
equiv_fun :> A -> B ;
equiv_isequiv :> IsEquiv equiv_fun
}.
Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope.
Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
Local Open Scope equiv_scope.
Instance isequiv_path {A B : Type} (p : A = B)
: IsEquiv (transport (fun X:Type => X) p) | 0
:= admit.
Definition equiv_path (A B : Type) (p : A = B) : A <~> B
:= BuildEquiv _ _ (transport (fun X:Type => X) p) _.
Class Univalence := {
isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B)
}.
Section Univalence.
Context `{Univalence}.
Definition path_universe_uncurried {A B : Type} (f : A <~> B) : A = B
:= (equiv_path A B)^-1 f.
Definition path_universe {A B : Type} (f : A -> B) {feq : IsEquiv f} : (A = B)
:= path_universe_uncurried (BuildEquiv _ _ f feq).
Set Printing Universes.
Definition transport_path_universe {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : A)
: transport (fun X:Type => X) (path_universe f) z = f z
:= apD10 (ap (equiv_fun A B) (eisretr (equiv_path A B) (BuildEquiv _ _ f feq))) z.
(* Toplevel input, characters 0-231:
Error: Illegal application:
The term "isequiv_equiv_path (* Top.1003 Top.1003 Top.1001 Top.997 *)"
of type
"Univalence (* Top.1003 Top.1003 Top.1001 Top.997 *) ->
forall (A : Type (* Top.1003 *)) (B : Type (* Top.997 *)),
IsEquiv (* Top.1003 Top.1001 *)
(equiv_path (* Top.997 Top.1003 Top.1001 Top.1003 *) A B)"
cannot be applied to the terms
"H" : "Univalence (* Top.934 Top.935 Top.936 Top.937 *)"
"A" : "Type (* Top.996 *)"
"B" : "Type (* Top.997 *)"
The 1st term has type "Univalence (* Top.934 Top.935 Top.936 Top.937 *)"
which should be coercible to
"Univalence (* Top.1003 Top.1003 Top.1001 Top.997 *)".
*)
|
