From 89118f2a8ebd111de91e48128ae4005c8b64a400 Mon Sep 17 00:00:00 2001 From: Steve Awodey Date: Fri, 16 Jun 2017 14:50:55 -0400 Subject: [PATCH] Merge remote-tracking branch 'origin/new_lean' into new_lean # Conflicts: # algebra/exactness.hlean # homotopy/pushout.hlean # move_to_lib.hlean --- algebra/exact_couple.hlean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean index 4d51500..73dc61f 100644 --- a/algebra/exact_couple.hlean +++ b/algebra/exact_couple.hlean @@ -129,6 +129,9 @@ definition derived_couple_A : AbGroup := definition derived_couple_B : AbGroup := homology (differential EC) (differential_is_differential EC) +print homology + + definition derived_couple_i : derived_couple_A →g derived_couple_A := (image_lift (exact_couple.i EC)) ∘g (image_incl (exact_couple.i EC))