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

add sorry's to make library compile

Browse source
This commit is contained in:
Floris van Doorn 2017-07-07 22:38:06 +01:00
parent 90f4acb3f6
commit 9c271470ca
2 changed files with 16 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
homotopy/fwedge.hlean
View file

@ -221,7 +221,7 @@ namespace fwedge
(f ∘* (pwedge_pmap h k)) w = pwedge_pmap (f ∘* h )(f ∘* k) w := (f ∘* (pwedge_pmap h k)) w = pwedge_pmap (f ∘* h )(f ∘* k) w :=
have H : _, from have H : _, from
(@prod_to_pi_bool_nat_square A B X Y f) ⬝htyh (fwedge_pmap_nat_square f) ⬝htyh (fwedge_to_pwedge_nat_square f), (@prod_to_pi_bool_nat_square A B X Y f) ⬝htyh (fwedge_pmap_nat_square f) ⬝htyh (fwedge_to_pwedge_nat_square f),
proof H qed sorry
-- SA to here 7/5 -- SA to here 7/5

4
homotopy/wedge.hlean
View file

@ -48,7 +48,7 @@ namespace wedge
exact (glue ⋆), exact (glue ⋆),
exact inr (inr a), exact inr (inr a),
-- exact elim_glue _ _ _, -- exact elim_glue _ _ _,
exact sorry
end end
@ -65,5 +65,3 @@ namespace wedge
... ≃* plift.{u v} A ∨ plift.{u v} B : by exact pwedge_pequiv !pequiv_plift !pequiv_plift ... ≃* plift.{u v} A ∨ plift.{u v} B : by exact pwedge_pequiv !pequiv_plift !pequiv_plift
end wedge end wedge