lean2/tests/lean/hott/614.hlean
2016-12-02 16:55:23 -08:00

21 lines
593 B
Text

import homotopy.circle
open circle eq int pi
attribute circle.rec [recursor]
protected definition my_decode {x : circle} (c : circle.code x) : base = x :=
begin
induction x,
{ revert c, exact power loop },
{ apply arrow_pathover_left, intro b, apply concato_eq, apply eq_pathover_r,
rewrite [power_con,transport_code_loop]},
end
protected definition my_decode' {x : circle} : circle.code x → base = x :=
begin
induction x,
{ exact power loop},
{ apply arrow_pathover_left, intro b, apply concato_eq, apply eq_pathover_r,
rewrite [power_con,transport_code_loop]},
end