From 8d4ad591c839f53868261ea16bbf408853f0bbcd Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Mon, 27 Jun 2016 17:19:54 +0200
Subject: [PATCH] feat(hott) add missing pathover lemmas

---
 hott/init/pathover.hlean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean
index 87dd17b7f..8a2e02b6e 100644
--- a/hott/init/pathover.hlean
+++ b/hott/init/pathover.hlean
@@ -216,6 +216,18 @@ namespace eq
   definition tr_pathover_of_eq (q : b₂ = b₂') : p⁻¹ ▸ b₂ =[p] b₂' :=
   by cases q;apply tr_pathover
 
+  definition eq_of_parallel_po_right (q : b =[p] b₂) (q' : b =[p] b₂') : b₂ = b₂' :=
+  begin
+    apply @eq_of_pathover_idp A B, apply change_path (con.left_inv p),
+    exact q⁻¹ᵒ ⬝o q'
+  end
+
+  definition eq_of_parallel_po_left (q : b =[p] b₂) (q' : b' =[p] b₂) : b = b' :=
+  begin
+    apply @eq_of_pathover_idp A B, apply change_path (con.right_inv p),
+    exact q ⬝o q'⁻¹ᵒ
+  end
+
   variable (C)
   definition transporto (r : b =[p] b₂) (c : C b) : C b₂ :=
   by induction r;exact c