From bf3a132e9935db928a2c809bbf3b9694a7aabcc1 Mon Sep 17 00:00:00 2001 From: Steve Awodey Date: Fri, 30 Jun 2017 13:21:49 +0100 Subject: [PATCH] fixed --- algebra/short_five.hlean | 2 -- 1 file changed, 2 deletions(-) diff --git a/algebra/short_five.hlean b/algebra/short_five.hlean index 9fe65a8..bc371f6 100644 --- a/algebra/short_five.hlean +++ b/algebra/short_five.hlean @@ -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