From a209f4e085fee0117fc7888cd990705d713fee1f Mon Sep 17 00:00:00 2001 From: Steve Awodey Date: Fri, 30 Jun 2017 13:20:08 +0100 Subject: [PATCH] trivial --- algebra/short_five.hlean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/algebra/short_five.hlean b/algebra/short_five.hlean index af701b9..9fe65a8 100644 --- a/algebra/short_five.hlean +++ b/algebra/short_five.hlean @@ -70,6 +70,9 @@ 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