michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(hott) add missing pathover lemmas

Browse source
This commit is contained in:
Jakob von Raumer 2016-06-27 17:19:54 +02:00 committed by Leonardo de Moura
parent a5fe82f177
commit 8d4ad591c8
1 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
hott/init/pathover.hlean
View file

@ -216,6 +216,18 @@ namespace eq
definition tr_pathover_of_eq (q : b₂ = b₂') : p⁻¹ ▸ b₂ =[p] b₂' := definition tr_pathover_of_eq (q : b₂ = b₂') : p⁻¹ ▸ b₂ =[p] b₂' :=
by cases q;apply tr_pathover 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) variable (C)
definition transporto (r : b =[p] b₂) (c : C b) : C b₂ := definition transporto (r : b =[p] b₂) (c : C b) : C b₂ :=
by induction r;exact c by induction r;exact c