Skip to content

Commit

Permalink
Basics/PathGroupoids: drop concat2_p1 and concat2_1p, which are defin…
Browse files Browse the repository at this point in the history
…itionally true
  • Loading branch information
jdchristensen committed Sep 2, 2023
1 parent bff48d2 commit aad097e
Showing 1 changed file with 0 additions and 9 deletions.
9 changes: 0 additions & 9 deletions theories/Basics/PathGroupoids.v
Original file line number Diff line number Diff line change
Expand Up @@ -1087,15 +1087,6 @@ Proof.
symmetry; refine (concat_p1 _ @ concat_1p _).
Defined.

(* The next two are definitionally true, so maybe can be dropped? *)
Definition concat2_p1 {A : Type} {x y : A} {p q : x = y} (h : p = q) :
h @@ 1 = whiskerR h 1 :> (p @ 1 = q @ 1)
:= idpath.

Definition concat2_1p {A : Type} {x y : A} {p q : x = y} (h : p = q) :
1 @@ h = whiskerL 1 h :> (1 @ p = 1 @ q)
:= idpath.

Definition cancel2L {A : Type} {x y z : A} {p p' : x = y} {q q' : y = z}
(g : p = p') (h k : q = q')
: (g @@ h = g @@ k) -> (h = k).
Expand Down

0 comments on commit aad097e

Please sign in to comment.