blob: 206df23bce8088833f4043cb4f8674ae5c6e5692 (
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
|
(* Issue caused and fixed during the lifetime of #6775: unification
failing on partially applied cumulative inductives. *)
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Unset Elimination Schemes.
Inductive paths@{i} {A : Type@{i}} (a : A) : A -> Type@{i} :=
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 inverse {A : Type} {x y : A} (p : x = y) : y = x
:= match p with idpath => idpath end.
Arguments inverse {A x y} p : simpl nomatch.
Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
match p, q with idpath, idpath => idpath end.
Arguments concat {A x y z} p q : simpl nomatch.
Notation "1" := idpath.
Reserved Notation "p @ q" (at level 20).
Notation "p @ q" := (concat p q).
Reserved Notation "p ^" (at level 3, format "p '^'").
Notation "p ^" := (inverse p).
Definition concat_pV_p {A} {x y z : A} (p : x = z) (q : y = z) :
(p @ q^) @ q = p
:=
(match q as i return forall p, (p @ i^) @ i = p with
idpath =>
fun p =>
match p with idpath => 1 end
end) p.
|
