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

chore(hott/cubical/square): remove unnecessary annotations added in previous commit

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-29 12:25:31 -07:00
parent b790ca9806
commit e384894f7a
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
hott/cubical/square.hlean
View file

@ -103,8 +103,8 @@ namespace cubical
from eq.rec_on p (by cases r; cases t; exact H), from eq.rec_on p (by cases r; cases t; exact H),
left_inv (to_fun !square_equiv_eq) s ▹ !con_inv_cancel_right ▹ H2 left_inv (to_fun !square_equiv_eq) s ▹ !con_inv_cancel_right ▹ H2
definition rec_on_t.{l} {A : Type.{l}} {a₁₀ : A} definition rec_on_t {a₁₀ : A}
{P : Π {a₀₂ a₂₂ : A} {b : a₀₂ = a₂₂} {l : a₁₀ = a₀₂} {r : a₁₀ = a₂₂}, square idp b l r → Type.{l}} {P : Π {a₀₂ a₂₂ : A} {b : a₀₂ = a₂₂} {l : a₁₀ = a₀₂} {r : a₁₀ = a₂₂}, square idp b l r → Type}
{a₀₂ a₂₂ : A} {b : a₀₂ = a₂₂} {l : a₁₀ = a₀₂} {r : a₁₀ = a₂₂} {a₀₂ a₂₂ : A} {b : a₀₂ = a₂₂} {l : a₁₀ = a₀₂} {r : a₁₀ = a₂₂}
(s : square idp b l r) (H : P ids) : P s := (s : square idp b l r) (H : P ids) : P s :=
let p : l ⬝ b = r := (eq_of_square s)⁻¹ ⬝ !idp_con in let p : l ⬝ b = r := (eq_of_square s)⁻¹ ⬝ !idp_con in