This commit is contained in:
Steve Awodey 2017-06-30 13:21:49 +01:00
parent a209f4e085
commit bf3a132e99

View file

@ -70,8 +70,6 @@ section short_exact
(is_exact_at_3 : is_exact_at_m C (S (S n)))
(is_contr_4 : is_contr (C (S (S (S (S n))))))
print is_exact_at_m C n
/- TODO: show that this gives rise to a short exact sequence in the sense above -/
end short_exact