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

lemma in colim for spectrification

Browse source
This commit is contained in:
spiceghello 2017-06-08 09:27:57 -06:00
parent 877c740ea9
commit 9f1df6becb
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
colim.hlean
View file

@ -372,7 +372,9 @@ namespace seq_colim
(p : Πn, f n ~* f' n) (n : ℕ) :
pseq_colim_equiv_constant p ∘* pinclusion f n ~* pinclusion f' n :=
begin
sorry
transitivity pinclusion f' n ∘* !pid,
refine phomotopy_of_psquare !pseq_colim_pequiv_pinclusion,
exact !pcompose_pid
end
definition is_equiv_seq_colim_rec (P : seq_colim f → Type) :