Built with Alectryon. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
From HoTT.Basics Require Import Overture Equivalences Tactics.From HoTT.Basics Require Import Overture Equivalences Tactics.From HoTT.WildCat Require Import Core SetoidRewrite AbEnriched EpiStable.From HoTT.Spaces Require Import Nat.Core Finite.Fin.LocalOpen Scope mc_add_scope.(** * Homological algebra *)(** Various "diagram lemmas" are proved, usually assuming the wild category satisfies [IsAbEpiStable]. The proofs use the diagram chasing method provided by WildCat.EpiStable. *)(** We will often use the convention that a map [bc : B $-> C] is named as the juxtaposition of the domain and codomain. When we want to highlight the importance of certain maps, they will be given different names. *)(** ** The weak four lemmas *)SectionFourLemma.Context {A : Type} `{IsAbEpiStable A}.Context {BCDEB'C'D'E' : A}
(bc : B $-> C) (cd : C $-> D) (de : D $-> E)
(bc' : B' $-> C') (cd' : C' $-> D') (de' : D' $-> E')
(g : B $-> B') (h : C $-> C') (i : D $-> D') (j : E $-> E')
(sq2 : h $o bc $== bc' $o g) (sq3 : i $o cd $== cd' $o h)
(sq4 : j $o de $== de' $o i)
`{!CatIsAbExact cd de} `{!CatIsAbExact bc' cd'} `{!Epic g} `{!Monic j}.(** The diagram has the following shape:<< B ---> C ---> D ---> E | | | v |g |h |i |j v | | | v v v v B' --> C' --> D' --> E'>> The common assumptions are that the map [B $-> B'] is epi, the map [E $-> E'] is mono, and the sequences [C $-> D] + [D $-> E] and [B' $-> C'] + [C' $-> D'] are exact. *)(** If in addition the composite of [C' $-> D'] and [D' $-> C'] is zero and the map [D $-> D'] is epi, then the map [C $-> C'] is epi. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_cde': de' $o cd' $== 0 Epic1: Epic i
Epic h
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_cde': de' $o cd' $== 0 Epic1: Epic i
Epic h
(* To show that [h : C $-> C'] is epi, we must show that an arbitrary generalized element [c' : elt P C'] lifts along [h : C $-> C']. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_cde': de' $o cd' $== 0 Epic1: Epic i P: A c': elt P C'
Lift c' h
(* Since the map [i : D $-> D'] is assumed epi, we can lift the element [cd' $o c' : elt P D'] to an element [d : elt _ D]. [ld] will be the name given to the proof that [d] is a lift. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_cde': de' $o cd' $== 0 Epic1: Epic i P: A d: elt P D c': elt P C' ld: i $o d $== cd' $o c'
Lift c' h
(* Using exactness of the top row, we can further lift the element [d] to an element [c : elt _ C]. This step involves verifying that [d] is mapped to zero by [de : D $-> E], which requires the map [j] to be mono. *)(* We clear 2-cells and elements when they are no longer needed, to speed up the lifts. The [using clear] clause is applied *after* the hypothesis is proved. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_cde': de' $o cd' $== 0 Epic1: Epic i P: A d: elt P D c': elt P C' ld: i $o d $== cd' $o c'
de $o d $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j Epic1: Epic i P: A c': elt P C' d: elt P D ld: i $o d $== cd' $o c' c: elt P C lc: cd $o c $== d
Lift c' h
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_cde': de' $o cd' $== 0 Epic1: Epic i P: A d: elt P D c': elt P C' ld: i $o d $== cd' $o c'
de $o d $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_cde': de' $o cd' $== 0 Epic1: Epic i P: A d: elt P D c': elt P C' ld: i $o d $== cd' $o c'
j $o (de $o d) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_cde': de' $o cd' $== 0 Epic1: Epic i P: A d: elt P D c': elt P C' ld: i $o d $== cd' $o c'
de' $o (i $o d) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_cde': de' $o cd' $== 0 Epic1: Epic i P: A d: elt P D c': elt P C' ld: i $o d $== cd' $o c'
de' $o (cd' $o c') $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_cde': de' $o cd' $== 0 Epic1: Epic i P: A d: elt P D c': elt P C' ld: i $o d $== cd' $o c'
de' $o cd' $o c' $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_cde': de' $o cd' $== 0 Epic1: Epic i P: A d: elt P D c': elt P C' ld: i $o d $== cd' $o c'
0 $o c' $== 0
apply precomp_zero.
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j Epic1: Epic i P: A c': elt P C' d: elt P D ld: i $o d $== cd' $o c' c: elt P C lc: cd $o c $== d
Lift c' h
(* The element [c] is not necessarily the correct lift of [c']. We correct this by lifting the element [c' - h $o c] using exactness of the bottom row. This yields an element [b' : elt _ B']. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j Epic1: Epic i P: A c': elt P C' d: elt P D ld: i $o d $== cd' $o c' c: elt P C lc: cd $o c $== d
cd' $o (c' - h $o c) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j Epic1: Epic i P: A b': elt P B' c: elt P C c': elt P C' lb': bc' $o b' $== c' - h $o c
Lift c' h
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j Epic1: Epic i P: A c': elt P C' d: elt P D ld: i $o d $== cd' $o c' c: elt P C lc: cd $o c $== d
cd' $o (c' - h $o c) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j Epic1: Epic i P: A c': elt P C' d: elt P D ld: i $o d $== cd' $o c' c: elt P C lc: cd $o c $== d
cd' $o c' - cd' $o (h $o c) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j Epic1: Epic i P: A c': elt P C' d: elt P D ld: i $o d $== cd' $o c' c: elt P C lc: cd $o c $== d
cd' $o c' - i $o (cd $o c) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j Epic1: Epic i P: A c': elt P C' d: elt P D ld: i $o d $== cd' $o c' c: elt P C lc: cd $o c $== d
cd' $o c' - cd' $o c' $== 0
apply inverse_r_0gpd.
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j Epic1: Epic i P: A b': elt P B' c: elt P C c': elt P C' lb': bc' $o b' $== c' - h $o c
Lift c' h
(* Since we know that the map [g : B $-> B'] is epi, we can lift [b'] to an element [b : elt _ B]. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j Epic1: Epic i P: A c': elt P C' c: elt P C b': elt P B' lb': bc' $o b' $== c' - h $o c b: elt P B lb: g $o b $== b'
Lift c' h
(* We obtain the correct lift by adding together the incorrect lift and its correction. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j Epic1: Epic i P: A c': elt P C' c: elt P C b': elt P B' lb': bc' $o b' $== c' - h $o c b: elt P B lb: g $o b $== b'
h $o (c + bc $o b) $== c'
(* It remains to show that this is indeed a lift of [c']. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j Epic1: Epic i P: A c': elt P C' c: elt P C b': elt P B' lb': bc' $o b' $== c' - h $o c b: elt P B lb: g $o b $== b'
h $o c + h $o (bc $o b) $== c'
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j Epic1: Epic i P: A c': elt P C' c: elt P C b': elt P B' lb': bc' $o b' $== c' - h $o c b: elt P B lb: g $o b $== b'
h $o c + bc' $o (g $o b) $== c'
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j Epic1: Epic i P: A c': elt P C' c: elt P C b': elt P B' lb': bc' $o b' $== c' - h $o c b: elt P B lb: g $o b $== b'
h $o c + (c' - h $o c) $== c'
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j Epic1: Epic i P: A c': elt P C' c: elt P C b': elt P B' lb': bc' $o b' $== c' - h $o c b: elt P B lb: g $o b $== b'
h $o c + (- (h $o c) + c') $== c'
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j Epic1: Epic i P: A c': elt P C' c: elt P C b': elt P B' lb': bc' $o b' $== c' - h $o c b: elt P B lb: g $o b $== b'
h $o c - h $o c + c' $== c'
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j Epic1: Epic i P: A c': elt P C' c: elt P C b': elt P B' lb': bc' $o b' $== c' - h $o c b: elt P B lb: g $o b $== b'
0 + c' $== c'
apply mon_unit_l_0gpd.Defined.(** If, in addition to the common assumptions, the composite of [B $-> C] and [C $-> D] is zero and the map [C $-> C'] is mono, then the map [D $-> D'] is mono. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h
Monic i
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h
Monic i
(* To show that a map is mono, it suffices to show that an arbitrary generalized element [d : elt P D] that goes to [0 : elt P D'] is homotopic to [0 : elt P D]. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D p: i $o d $== 0
d $== 0
(* Using exactness, we lift the element [d] to [c : elt _ C]. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D p: i $o d $== 0
de $o d $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D p: i $o d $== 0 c: elt P C lc: cd $o c $== d
d $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D p: i $o d $== 0
de $o d $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D p: i $o d $== 0
j $o (de $o d) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D p: i $o d $== 0
de' $o (i $o d) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h sq4: j $o de $== de' $o i CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D p: i $o d $== 0
de' $o 0 $== 0
apply postcomp_zero.
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D p: i $o d $== 0 c: elt P C lc: cd $o c $== d
d $== 0
(* Next we lift [h $o c] to [b' : elt _ B']. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D p: i $o d $== 0 c: elt P C lc: cd $o c $== d
cd' $o (h $o c) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A c: elt P C d: elt P D lc: cd $o c $== d b': elt P B' lb': bc' $o b' $== h $o c
d $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D p: i $o d $== 0 c: elt P C lc: cd $o c $== d
cd' $o (h $o c) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D p: i $o d $== 0 c: elt P C lc: cd $o c $== d
i $o (cd $o c) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g sq3: i $o cd $== cd' $o h CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D p: i $o d $== 0 c: elt P C lc: cd $o c $== d
i $o d $== 0
exact p.
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A c: elt P C d: elt P D lc: cd $o c $== d b': elt P B' lb': bc' $o b' $== h $o c
d $== 0
(* We lift [b'] to [b : elt _ B]. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D c: elt P C lc: cd $o c $== d b': elt P B' lb': bc' $o b' $== h $o c b: elt P B lb: g $o b $== b'
d $== 0
(* Since [h] is monic, it follows that [b] is a lift of [c]. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D c: elt P C lc: cd $o c $== d b': elt P B' lb': bc' $o b' $== h $o c b: elt P B lb: g $o b $== b'
bc $o b $== c
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D c: elt P C lc: cd $o c $== d b': elt P B' lb': bc' $o b' $== h $o c b: elt P B lb: g $o b $== b' p': bc $o b $== c
d $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D c: elt P C lc: cd $o c $== d b': elt P B' lb': bc' $o b' $== h $o c b: elt P B lb: g $o b $== b'
bc $o b $== c
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D c: elt P C lc: cd $o c $== d b': elt P B' lb': bc' $o b' $== h $o c b: elt P B lb: g $o b $== b'
h $o (bc $o b) $== h $o c
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D c: elt P C lc: cd $o c $== d b': elt P B' lb': bc' $o b' $== h $o c b: elt P B lb: g $o b $== b'
bc' $o (g $o b) $== h $o c
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D c: elt P C lc: cd $o c $== d b': elt P B' lb': bc' $o b' $== h $o c b: elt P B lb: g $o b $== b'
bc' $o b' $== h $o c
exact lb'.
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D c: elt P C lc: cd $o c $== d b': elt P B' lb': bc' $o b' $== h $o c b: elt P B lb: g $o b $== b' p': bc $o b $== c
d $== 0
(* So [d] lifts all the way to [B]. Since [B -> C -> D] is a complex, [d] is zero. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D c: elt P C lc: cd $o c $== d b': elt P B' lb': bc' $o b' $== h $o c b: elt P B lb: g $o b $== b' p': bc $o b $== c
cd $o c $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D c: elt P C lc: cd $o c $== d b': elt P B' lb': bc' $o b' $== h $o c b: elt P B lb: g $o b $== b' p': bc $o b $== c
cd $o (bc $o b) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D c: elt P C lc: cd $o c $== d b': elt P B' lb': bc' $o b' $== h $o c b: elt P B lb: g $o b $== b' p': bc $o b $== c
cd $o bc $o b $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A B, C, D, E, B', C', D', E': A bc: B $-> C cd: C $-> D de: D $-> E bc': B' $-> C' cd': C' $-> D' de': D' $-> E' g: B $-> B' h: C $-> C' i: D $-> D' j: E $-> E' sq2: h $o bc $== bc' $o g CatIsAbExact0: CatIsAbExact cd de CatIsAbExact1: CatIsAbExact bc' cd' Epic0: Epic g Monic0: Monic j complex_bcd: cd $o bc $== 0 Monic1: Monic h P: A d: elt P D c: elt P C lc: cd $o c $== d b': elt P B' lb': bc' $o b' $== h $o c b: elt P B lb: g $o b $== b' p': bc $o b $== c
0 $o b $== 0
apply precomp_zero.Defined.EndFourLemma.(** ** The 3x3-lemmas as presented in Mac Lane's book "Homology" *)SectionThreeByThree.Context {A : Type} `{Is1Cat A}.Context {X00X01X02X10X11X12X20X21X22 : A}
(f0i : X00 $-> X01) (f0j : X01 $-> X02)
(fi0 : X00 $-> X10) (fi1 : X01 $-> X11) (fi2 : X02 $-> X12)
(f1i : X10 $-> X11) (f1j : X11 $-> X12)
(fj0 : X10 $-> X20) (fj1 : X11 $-> X21) (fj2 : X12 $-> X22)
(f2i : X20 $-> X21) (f2j : X21 $-> X22)
(sq1 : fi1 $o f0i $== f1i $o fi0) (sq2 : fi2 $o f0j $== f1j $o fi1)
(sq3 : fj1 $o f1i $== f2i $o fj0) (sq4 : fj2 $o f1j $== f2j $o fj1).(** The diagram has the following shape:<< X00 ----f0i----> X01 ----f0j----> X02 | | | | | | fi0 sq1 fi1 sq2 fi2 | | | | | | v v v X10 ----f1i----> X11 ----f1j----> X12 | | | | | | fj0 sq3 fj1 sq4 fj2 | | | | | | v v v X20 ----f2i----> X21 ----f2j----> X22>> *)(** If all three columns and the last two rows are short exact, then the top row is short exact. We prove the three parts of the conclusion as separate results, each requiring a different subset of the hypotheses (and in fact not all of the hypotheses are needed). *)
exact (monic_homotopic _ _ sq1^$).Defined.(** For the remaining results, we need this assumption. *)Context `{!IsAbEpiStable A}.(** The hypotheses aren't entirely minimal here. Instead of the two exactness hypotheses, we really only need that the lifting property holds. *)
exact lx11.Defined.(** If every column is exact, the top and bottom rows are short exact, and the middle row is a complex, then the middle row is short exact. Like above, we prove the three parts of this separately, with fewer hypotheses. *)
apply mon_unit_r_0gpd.Defined.EndThreeByThree.(** ** The spider lemma *)SectionSpider.Context {A : Type} `{IsAbEpiStable A}.(** Given a diagram<< A1 -> A2 \ ^ v / X ^ \ / v B1 -> B2>> where the diagonals are exact, if the map [B1 $-> B2] is mono/epi, so is the map [A1 $-> A2]. *)Context {A1A2XB1B2 : A} (a : A1 $-> A2) (ax : A1 $-> X)
(xa : X $-> A2) (b : B1 $-> B2) (bx : B1 $-> X) (xb : X $-> B2)
{tr1 : xa $o ax $== a} {tr2 : xb $o bx $== b}
`{!Monic ax} `{!CatIsAbExact ax xb} `{!Epic xb}
`{!Monic bx} `{!CatIsAbExact bx xa} `{!Epic xa}.
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b
Monic a
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b
Monic a
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b P: A a1: elt P A1 p: a $o a1 $== 0
a1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b P: A a1: elt P A1 p: a $o a1 $== 0
ax $o a1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b P: A a1: elt P A1 p: a $o a1 $== 0
xa $o (ax $o a1) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b P: A b1: elt P B1 a1: elt P A1 lb1: bx $o b1 $== ax $o a1
ax $o a1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b P: A a1: elt P A1 p: a $o a1 $== 0
xa $o (ax $o a1) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b P: A a1: elt P A1 p: a $o a1 $== 0
xa $o ax $o a1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b P: A a1: elt P A1 p: a $o a1 $== 0
a $o a1 $== 0
exact p.
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b P: A b1: elt P B1 a1: elt P A1 lb1: bx $o b1 $== ax $o a1
ax $o a1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b P: A b1: elt P B1 a1: elt P A1 lb1: bx $o b1 $== ax $o a1
b1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b P: A b1: elt P B1 a1: elt P A1 lb1: bx $o b1 $== ax $o a1 b1_is_zero: b1 $== 0
ax $o a1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b P: A b1: elt P B1 a1: elt P A1 lb1: bx $o b1 $== ax $o a1
b1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b P: A b1: elt P B1 a1: elt P A1 lb1: bx $o b1 $== ax $o a1
b $o b1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b P: A b1: elt P B1 a1: elt P A1 lb1: bx $o b1 $== ax $o a1
xb $o bx $o b1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b P: A b1: elt P B1 a1: elt P A1 lb1: bx $o b1 $== ax $o a1
xb $o ax $o a1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b P: A b1: elt P B1 a1: elt P A1 lb1: bx $o b1 $== ax $o a1
0 $o a1 $== 0
apply precomp_zero.
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b P: A b1: elt P B1 a1: elt P A1 lb1: bx $o b1 $== ax $o a1 b1_is_zero: b1 $== 0
ax $o a1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b P: A b1: elt P B1 a1: elt P A1 lb1: bx $o b1 $== ax $o a1 b1_is_zero: b1 $== 0
bx $o b1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Monic2: Monic b P: A b1: elt P B1 a1: elt P A1 lb1: bx $o b1 $== ax $o a1 b1_is_zero: b1 $== 0
bx $o 0 $== 0
apply postcomp_zero.Defined.
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b
Epic a
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b
Epic a
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b P: A a2: elt P A2
Lift a2 a
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b P: A x: elt P X a2: elt P A2 lx: xa $o x $== a2
Lift a2 a
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b P: A a2: elt P A2 x: elt P X lx: xa $o x $== a2 b1: elt P B1 lb1: b $o b1 $== xb $o x
Lift a2 a
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b P: A a2: elt P A2 x: elt P X lx: xa $o x $== a2 b1: elt P B1 lb1: b $o b1 $== xb $o x
xb $o (x - bx $o b1) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b P: A x: elt P X a2: elt P A2 lx: xa $o x $== a2 a1: elt P A1 b1: elt P B1 la1: ax $o a1 $== x - bx $o b1
Lift a2 a
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b P: A a2: elt P A2 x: elt P X lx: xa $o x $== a2 b1: elt P B1 lb1: b $o b1 $== xb $o x
xb $o (x - bx $o b1) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b P: A a2: elt P A2 x: elt P X lx: xa $o x $== a2 b1: elt P B1 lb1: b $o b1 $== xb $o x
xb $o x - xb $o (bx $o b1) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b P: A a2: elt P A2 x: elt P X lx: xa $o x $== a2 b1: elt P B1 lb1: b $o b1 $== xb $o x
xb $o x - b $o b1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a tr2: xb $o bx $== b Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b P: A a2: elt P A2 x: elt P X lx: xa $o x $== a2 b1: elt P B1 lb1: b $o b1 $== xb $o x
b $o b1 - b $o b1 $== 0
apply inverse_r_0gpd.
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b P: A x: elt P X a2: elt P A2 lx: xa $o x $== a2 a1: elt P A1 b1: elt P B1 la1: ax $o a1 $== x - bx $o b1
Lift a2 a
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b P: A x: elt P X a2: elt P A2 lx: xa $o x $== a2 a1: elt P A1 b1: elt P B1 la1: ax $o a1 $== x - bx $o b1
a $o a1 $== a2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b P: A x: elt P X a2: elt P A2 lx: xa $o x $== a2 a1: elt P A1 b1: elt P B1 la1: ax $o a1 $== x - bx $o b1
xa $o ax $o a1 $== a2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b P: A x: elt P X a2: elt P A2 lx: xa $o x $== a2 a1: elt P A1 b1: elt P B1 la1: ax $o a1 $== x - bx $o b1
xa $o (ax $o a1) $== a2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b P: A x: elt P X a2: elt P A2 lx: xa $o x $== a2 a1: elt P A1 b1: elt P B1 la1: ax $o a1 $== x - bx $o b1
xa $o (x - bx $o b1) $== a2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b P: A x: elt P X a2: elt P A2 lx: xa $o x $== a2 a1: elt P A1 b1: elt P B1 la1: ax $o a1 $== x - bx $o b1
xa $o x - xa $o (bx $o b1) $== a2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b P: A x: elt P X a2: elt P A2 lx: xa $o x $== a2 a1: elt P A1 b1: elt P B1 la1: ax $o a1 $== x - bx $o b1
xa $o x - 0 $o b1 $== a2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b P: A x: elt P X a2: elt P A2 lx: xa $o x $== a2 a1: elt P A1 b1: elt P B1 la1: ax $o a1 $== x - bx $o b1
xa $o x - 0 $== a2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, X, B1, B2: A a: A1 $-> A2 ax: A1 $-> X xa: X $-> A2 b: B1 $-> B2 bx: B1 $-> X xb: X $-> B2 tr1: xa $o ax $== a Monic0: Monic ax CatIsAbExact0: CatIsAbExact ax xb Epic0: Epic xb Monic1: Monic bx CatIsAbExact1: CatIsAbExact bx xa Epic1: Epic xa Epic2: Epic b P: A x: elt P X a2: elt P A2 lx: xa $o x $== a2 a1: elt P A1 b1: elt P B1 la1: ax $o a1 $== x - bx $o b1
xa $o x $== a2
exact lx.Defined.EndSpider.(** ** The incomplete snail lemma *)SectionSnail.Context {A : Type} `{IsAbEpiStable A}.(** Here we will prove the incomplete snail lemma. The complete snail lemma was developed as a more general analogue of the snake lemma that holds in certain non-abelian contexts. The incomplete snail lemma is a lemma that one can use to prove the complete snail lemma. In fact, if the incomplete snail lemma is true and if every kernel map in the category has a cokernel, then the complete snail lemma is true. See Janelidze, Vitale; The snail lemma in a pointed regular category. *)Context {W1W2XY1Y2Z : A} (w : W1 $-> W2) (wx : W1 $-> X)
(wz : W2 $-> Z) (xw : X $-> W2) (xy : X $-> Y2)
(y : Y1 $-> Y2) (yx : Y1 $-> X) (yz : Y2 $-> Z)
(tr1 : w $== xw $o wx) (tr2 : y $== xy $o yx)
(sq1 : wz $o xw $== yz $o xy).(** We assume that we have a diagram of shape:<< W1 = = W1 | | | | v v Y1 -> X ---> W2 ---> 0 || | | || | | || v v Y1 -> Y2 --> Z>> Each row and the first column is assumed to be exact. We will show that the last column is exact as well. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx sq1: wz $o xw $== yz $o xy Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz
CatIsAbExact w wz
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx sq1: wz $o xw $== yz $o xy Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz
CatIsAbExact w wz
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx sq1: wz $o xw $== yz $o xy Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz
wz $o w $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx sq1: wz $o xw $== yz $o xy Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz
forall (P : A) (b : elt P W2), wz $o b $== 0 -> Lift b w
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx sq1: wz $o xw $== yz $o xy Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz
wz $o w $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx sq1: wz $o xw $== yz $o xy Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz
wz $o (xw $o wx) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx sq1: wz $o xw $== yz $o xy Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz
yz $o (xy $o wx) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx sq1: wz $o xw $== yz $o xy Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz
yz $o 0 $== 0
apply postcomp_zero.
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx sq1: wz $o xw $== yz $o xy Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz
forall (P : A) (b : elt P W2), wz $o b $== 0 -> Lift b w
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx sq1: wz $o xw $== yz $o xy Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A w2: elt P W2 p: wz $o w2 $== 0
Lift w2 w
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx sq1: wz $o xw $== yz $o xy Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A w2: elt P W2 p: wz $o w2 $== 0 x: elt P X lx: xw $o x $== w2
Lift w2 w
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx sq1: wz $o xw $== yz $o xy Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A w2: elt P W2 p: wz $o w2 $== 0 x: elt P X lx: xw $o x $== w2
yz $o (xy $o x) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A x: elt P X w2: elt P W2 lx: xw $o x $== w2 y1: elt P Y1 ly1: y $o y1 $== xy $o x
Lift w2 w
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx sq1: wz $o xw $== yz $o xy Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A w2: elt P W2 p: wz $o w2 $== 0 x: elt P X lx: xw $o x $== w2
yz $o (xy $o x) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx sq1: wz $o xw $== yz $o xy Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A w2: elt P W2 p: wz $o w2 $== 0 x: elt P X lx: xw $o x $== w2
wz $o (xw $o x) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx sq1: wz $o xw $== yz $o xy Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A w2: elt P W2 p: wz $o w2 $== 0 x: elt P X lx: xw $o x $== w2
wz $o w2 $== 0
exact p.
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A x: elt P X w2: elt P W2 lx: xw $o x $== w2 y1: elt P Y1 ly1: y $o y1 $== xy $o x
Lift w2 w
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A x: elt P X w2: elt P W2 lx: xw $o x $== w2 y1: elt P Y1 ly1: y $o y1 $== xy $o x
xy $o (x - yx $o y1) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A w2: elt P W2 x: elt P X lx: xw $o x $== w2 w1: elt P W1 y1: elt P Y1 lw1: wx $o w1 $== x - yx $o y1
Lift w2 w
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A x: elt P X w2: elt P W2 lx: xw $o x $== w2 y1: elt P Y1 ly1: y $o y1 $== xy $o x
xy $o (x - yx $o y1) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A x: elt P X w2: elt P W2 lx: xw $o x $== w2 y1: elt P Y1 ly1: y $o y1 $== xy $o x
xy $o x - xy $o (yx $o y1) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A x: elt P X w2: elt P W2 lx: xw $o x $== w2 y1: elt P Y1 ly1: y $o y1 $== xy $o x
xy $o x - y $o y1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx tr2: y $== xy $o yx Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A x: elt P X w2: elt P W2 lx: xw $o x $== w2 y1: elt P Y1 ly1: y $o y1 $== xy $o x
xy $o x - xy $o x $== 0
apply inverse_r_0gpd.
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A w2: elt P W2 x: elt P X lx: xw $o x $== w2 w1: elt P W1 y1: elt P Y1 lw1: wx $o w1 $== x - yx $o y1
Lift w2 w
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A w2: elt P W2 x: elt P X lx: xw $o x $== w2 w1: elt P W1 y1: elt P Y1 lw1: wx $o w1 $== x - yx $o y1
w $o w1 $== w2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A w2: elt P W2 x: elt P X lx: xw $o x $== w2 w1: elt P W1 y1: elt P Y1 lw1: wx $o w1 $== x - yx $o y1
xw $o wx $o w1 $== w2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A w2: elt P W2 x: elt P X lx: xw $o x $== w2 w1: elt P W1 y1: elt P Y1 lw1: wx $o w1 $== x - yx $o y1
xw $o (wx $o w1) $== w2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A w2: elt P W2 x: elt P X lx: xw $o x $== w2 w1: elt P W1 y1: elt P Y1 lw1: wx $o w1 $== x - yx $o y1
xw $o (x - yx $o y1) $== w2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A w2: elt P W2 x: elt P X lx: xw $o x $== w2 w1: elt P W1 y1: elt P Y1 lw1: wx $o w1 $== x - yx $o y1
xw $o x - xw $o (yx $o y1) $== w2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A w2: elt P W2 x: elt P X lx: xw $o x $== w2 w1: elt P W1 y1: elt P Y1 lw1: wx $o w1 $== x - yx $o y1
xw $o x - 0 $o y1 $== w2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A w2: elt P W2 x: elt P X lx: xw $o x $== w2 w1: elt P W1 y1: elt P Y1 lw1: wx $o w1 $== x - yx $o y1
xw $o x - 0 $== w2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A W1, W2, X, Y1, Y2, Z: A w: W1 $-> W2 wx: W1 $-> X wz: W2 $-> Z xw: X $-> W2 xy: X $-> Y2 y: Y1 $-> Y2 yx: Y1 $-> X yz: Y2 $-> Z tr1: w $== xw $o wx Epic0: Epic xw CatIsAbExact0: CatIsAbExact wx xy CatIsAbExact1: CatIsAbExact yx xw CatIsAbExact2: CatIsAbExact y yz P: A w2: elt P W2 x: elt P X lx: xw $o x $== w2 w1: elt P W1 y1: elt P Y1 lw1: wx $o w1 $== x - yx $o y1
xw $o x $== w2
exact lx.Defined.EndSnail.(** ** Two-by-three lemmas *)SectionTwoByThree.Context {A : Type} `{IsAbEpiStable A}.(** Here we will show how to transport the structure of an exact sequence across a morphism of composable pairs satisfying some properties. *)Context {A1A2B1B2C1C2 : A}
(f1 : A1 $-> B1) (g1 : B1 $-> C1)
(f2 : A2 $-> B2) (g2 : B2 $-> C2)
(a : A1 $-> A2) (b : B1 $-> B2) (c : C1 $-> C2)
(sq1 : b $o f1 $== f2 $o a) (sq2 : c $o g1 $== g2 $o b)
`{!Epic a} `{!Monic c}.(** In general, the diagrams will be of the shape:<< A1 ---> B1 ---> C1 | | v | | | v | | v v v A2 ---> B2 ---> C2>> In particular the map [A1 $-> A2] is epi and the map [C1 $-> C2] is mono. *)(** If the middle map [B1 $-> B2] is also epi and the upper morphisms [A1 $-> B1] and [B1 $-> C1] form an exact sequence, then the lower morphisms [A2 $-> B2] and [B2 $-> C2] form an exact sequence. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1
CatIsAbExact f2 g2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1
CatIsAbExact f2 g2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1
g2 $o f2 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1
forall (P : A) (b0 : elt P B2), g2 $o b0 $== 0 -> Lift b0 f2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1
g2 $o f2 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1
g2 $o f2 $o a $== 0 $o a
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1
g2 $o f2 $o a $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1
g2 $o b $o f1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1
c $o g1 $o f1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1
c $o (g1 $o f1) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1
c $o 0 $== 0
apply postcomp_zero.
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1
forall (P : A) (b0 : elt P B2), g2 $o b0 $== 0 -> Lift b0 f2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1 P: A b2: elt P B2 p: g2 $o b2 $== 0
Lift b2 f2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1 P: A b2: elt P B2 p: g2 $o b2 $== 0 b1: elt P B1 lb1: b $o b1 $== b2
Lift b2 f2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1 P: A b2: elt P B2 p: g2 $o b2 $== 0 b1: elt P B1 lb1: b $o b1 $== b2
g1 $o b1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1 P: A b2: elt P B2 p: g2 $o b2 $== 0 b1: elt P B1 lb1: b $o b1 $== b2 a1: elt P A1 la1: f1 $o a1 $== b1
Lift b2 f2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1 P: A b2: elt P B2 p: g2 $o b2 $== 0 b1: elt P B1 lb1: b $o b1 $== b2
g1 $o b1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1 P: A b2: elt P B2 p: g2 $o b2 $== 0 b1: elt P B1 lb1: b $o b1 $== b2
c $o (g1 $o b1) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1 P: A b2: elt P B2 p: g2 $o b2 $== 0 b1: elt P B1 lb1: b $o b1 $== b2
g2 $o (b $o b1) $== 0
by lhs' napply (_ $@L lb1).
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1 P: A b2: elt P B2 p: g2 $o b2 $== 0 b1: elt P B1 lb1: b $o b1 $== b2 a1: elt P A1 la1: f1 $o a1 $== b1
Lift b2 f2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1 P: A b2: elt P B2 p: g2 $o b2 $== 0 b1: elt P B1 lb1: b $o b1 $== b2 a1: elt P A1 la1: f1 $o a1 $== b1
f2 $o (a $o a1) $== b2
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a Epic0: Epic a Monic0: Monic c Epic1: Epic b CatIsAbExact0: CatIsAbExact f1 g1 P: A b2: elt P B2 p: g2 $o b2 $== 0 b1: elt P B1 lb1: b $o b1 $== b2 a1: elt P A1 la1: f1 $o a1 $== b1
b $o (f1 $o a1) $== b2
by lhs' napply (_ $@L la1).Defined.(** If the middle map [B1 $-> B2] is now mono and the lower morphisms [A2 $-> B2] and [B2 $-> C2] form an exact sequence, then the upper morphisms [A1 $-> B1] and [B1 $-> C1] form an exact sequence. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2
CatIsAbExact f1 g1
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2
CatIsAbExact f1 g1
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2
g1 $o f1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2
forall (P : A) (b0 : elt P B1), g1 $o b0 $== 0 -> Lift b0 f1
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2
g1 $o f1 $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2
c $o (g1 $o f1) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2
g2 $o (b $o f1) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2
g2 $o (f2 $o a) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2
g2 $o f2 $o a $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2
0 $o a $== 0
apply precomp_zero.
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2
forall (P : A) (b0 : elt P B1), g1 $o b0 $== 0 -> Lift b0 f1
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2 P: A b1: elt P B1 p: g1 $o b1 $== 0
Lift b1 f1
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2 P: A b1: elt P B1 p: g1 $o b1 $== 0
g2 $o (b $o b1) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2 P: A a2: elt P A2 b1: elt P B1 la2: f2 $o a2 $== b $o b1
Lift b1 f1
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2 P: A b1: elt P B1 p: g1 $o b1 $== 0
g2 $o (b $o b1) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2 P: A b1: elt P B1 p: g1 $o b1 $== 0
c $o (g1 $o b1) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a sq2: c $o g1 $== g2 $o b Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2 P: A b1: elt P B1 p: g1 $o b1 $== 0
c $o 0 $== 0
apply postcomp_zero.
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2 P: A a2: elt P A2 b1: elt P B1 la2: f2 $o a2 $== b $o b1
Lift b1 f1
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2 P: A b1: elt P B1 a2: elt P A2 la2: f2 $o a2 $== b $o b1 a1: elt P A1 la1: a $o a1 $== a2
Lift b1 f1
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2 P: A b1: elt P B1 a2: elt P A2 la2: f2 $o a2 $== b $o b1 a1: elt P A1 la1: a $o a1 $== a2
f1 $o a1 $== b1
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2 P: A b1: elt P B1 a2: elt P A2 la2: f2 $o a2 $== b $o b1 a1: elt P A1 la1: a $o a1 $== a2
b $o (f1 $o a1) $== b $o b1
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2 P: A b1: elt P B1 a2: elt P A2 la2: f2 $o a2 $== b $o b1 a1: elt P A1 la1: a $o a1 $== a2
f2 $o (a $o a1) $== b $o b1
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A A1, A2, B1, B2, C1, C2: A f1: A1 $-> B1 g1: B1 $-> C1 f2: A2 $-> B2 g2: B2 $-> C2 a: A1 $-> A2 b: B1 $-> B2 c: C1 $-> C2 sq1: b $o f1 $== f2 $o a Epic0: Epic a Monic0: Monic c Monic1: Monic b CatIsAbExact0: CatIsAbExact f2 g2 P: A b1: elt P B1 a2: elt P A2 la2: f2 $o a2 $== b $o b1 a1: elt P A1 la1: a $o a1 $== a2
f2 $o a2 $== b $o b1
exact la2.Defined.EndTwoByThree.(** ** The diamond lemma *)SectionDiamond.Context {Ae : Type} `{H0 : Is1Cat Ae} `{!IsAbEpiStable Ae}.Context {ABCDEFGH : Ae}
(ab : A $-> B) (bc : B $-> C) (cd : C $-> D) (de : D $-> E)
(ah : A $-> H) (hg : H $-> G) (gf : G $-> F) (fe : F $-> E)
(hb : H $-> B) (bd : B $-> D) (hf : H $-> F) (fd : F $-> D)
(tru : ab $== hb $o ah) (trr : bd $== cd $o bc)
(trd : fe $== de $o fd) (trl : hf $== gf $o hg)
(sq : bd $o hb $== fd $o hf)
`{!CatIsAbExact ab bc} `{!CatIsAbExact cd de}
`{!CatIsAbExact ah hg} `{!CatIsAbExact gf fe}
`{!Epic hg} `{!Monic cd}.(** The diagram has the shape:<< A / \ / \ v v H ----> B /| |\ / | | \ v | | v G | | C \ | | / \ | | / vv vv F ----> D \ / \ / v v E>> where each diagonal is assumed to be exact. *)(** If the map [H $-> B] is mono, then so is [G $-> F]. *)
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah trr: bd $== cd $o bc trd: fe $== de $o fd trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb
Monic gf
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah trr: bd $== cd $o bc trd: fe $== de $o fd trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb
Monic gf
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb
Monic gf
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb
forall (P : Ae) (b : elt P G), gf $o b $== 0 -> b $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae g: elt P G p: gf $o g $== 0
g $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae g: elt P G p: gf $o g $== 0 h: elt P H lh: hg $o h $== g
g $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae g: elt P G p: gf $o g $== 0 h: elt P H lh: hg $o h $== g
bc $o (hb $o h) $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae h: elt P H g: elt P G lh: hg $o h $== g a: elt P A la: ab $o a $== hb $o h
g $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae g: elt P G p: gf $o g $== 0 h: elt P H lh: hg $o h $== g
bc $o (hb $o h) $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae g: elt P G p: gf $o g $== 0 h: elt P H lh: hg $o h $== g
cd $o (bc $o (hb $o h)) $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae g: elt P G p: gf $o g $== 0 h: elt P H lh: hg $o h $== g
cd $o bc $o (hb $o h) $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae g: elt P G p: gf $o g $== 0 h: elt P H lh: hg $o h $== g
bd $o (hb $o h) $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae g: elt P G p: gf $o g $== 0 h: elt P H lh: hg $o h $== g
fd $o (hf $o h) $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae g: elt P G p: gf $o g $== 0 h: elt P H lh: hg $o h $== g
fd $o (gf $o hg $o h) $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae g: elt P G p: gf $o g $== 0 h: elt P H lh: hg $o h $== g
fd $o 0 $== 0
apply postcomp_zero.
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae h: elt P H g: elt P G lh: hg $o h $== g a: elt P A la: ab $o a $== hb $o h
g $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae h: elt P H g: elt P G lh: hg $o h $== g a: elt P A la: ab $o a $== hb $o h
ah $o a $== h
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae h: elt P H g: elt P G lh: hg $o h $== g a: elt P A la: ab $o a $== hb $o h la': ah $o a $== h
g $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae h: elt P H g: elt P G lh: hg $o h $== g a: elt P A la: ab $o a $== hb $o h
ah $o a $== h
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae h: elt P H g: elt P G lh: hg $o h $== g a: elt P A la: ab $o a $== hb $o h
hb $o (ah $o a) $== hb $o h
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae h: elt P H g: elt P G lh: hg $o h $== g a: elt P A la: ab $o a $== hb $o h
hb $o ah $o a $== hb $o h
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae h: elt P H g: elt P G lh: hg $o h $== g a: elt P A la: ab $o a $== hb $o h
ab $o a $== hb $o h
exact la.
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae h: elt P H g: elt P G lh: hg $o h $== g a: elt P A la: ab $o a $== hb $o h la': ah $o a $== h
g $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae h: elt P H g: elt P G lh: hg $o h $== g a: elt P A la: ab $o a $== hb $o h la': ah $o a $== h
hg $o h $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae h: elt P H g: elt P G lh: hg $o h $== g a: elt P A la: ab $o a $== hb $o h la': ah $o a $== h
hg $o (ah $o a) $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae h: elt P H g: elt P G lh: hg $o h $== g a: elt P A la: ab $o a $== hb $o h la': ah $o a $== h
hg $o ah $o a $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Monic1: Monic hb P: Ae h: elt P H g: elt P G lh: hg $o h $== g a: elt P A la: ab $o a $== hb $o h la': ah $o a $== h
0 $o a $== 0
apply precomp_zero.Defined.(** If the map [F $-> D] is epi, then so is the map [B $-> C]. *)
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah trr: bd $== cd $o bc trd: fe $== de $o fd trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd
Epic bc
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D tru: ab $== hb $o ah trr: bd $== cd $o bc trd: fe $== de $o fd trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd
Epic bc
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trd: fe $== de $o fd trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd
Epic bc
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trd: fe $== de $o fd trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae c: elt P C
Lift c bc
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trd: fe $== de $o fd trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae f: elt P F c: elt P C lf: fd $o f $== cd $o c
Lift c bc
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trd: fe $== de $o fd trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae f: elt P F c: elt P C lf: fd $o f $== cd $o c
fe $o f $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae c: elt P C f: elt P F lf: fd $o f $== cd $o c g: elt P G lg: gf $o g $== f
Lift c bc
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trd: fe $== de $o fd trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae f: elt P F c: elt P C lf: fd $o f $== cd $o c
fe $o f $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trd: fe $== de $o fd trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae f: elt P F c: elt P C lf: fd $o f $== cd $o c
de $o fd $o f $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trd: fe $== de $o fd trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae f: elt P F c: elt P C lf: fd $o f $== cd $o c
de $o (fd $o f) $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trd: fe $== de $o fd trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae f: elt P F c: elt P C lf: fd $o f $== cd $o c
de $o (cd $o c) $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trd: fe $== de $o fd trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae f: elt P F c: elt P C lf: fd $o f $== cd $o c
de $o cd $o c $== 0
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trd: fe $== de $o fd trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae f: elt P F c: elt P C lf: fd $o f $== cd $o c
0 $o c $== 0
napply precomp_zero.
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae c: elt P C f: elt P F lf: fd $o f $== cd $o c g: elt P G lg: gf $o g $== f
Lift c bc
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae f: elt P F c: elt P C lf: fd $o f $== cd $o c g: elt P G lg: gf $o g $== f h: elt P H lh: hg $o h $== g
Lift c bc
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae f: elt P F c: elt P C lf: fd $o f $== cd $o c g: elt P G lg: gf $o g $== f h: elt P H lh: hg $o h $== g
bc $o (hb $o h) $== c
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae f: elt P F c: elt P C lf: fd $o f $== cd $o c g: elt P G lg: gf $o g $== f h: elt P H lh: hg $o h $== g
cd $o (bc $o (hb $o h)) $== cd $o c
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae f: elt P F c: elt P C lf: fd $o f $== cd $o c g: elt P G lg: gf $o g $== f h: elt P H lh: hg $o h $== g
cd $o bc $o (hb $o h) $== cd $o c
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae f: elt P F c: elt P C lf: fd $o f $== cd $o c g: elt P G lg: gf $o g $== f h: elt P H lh: hg $o h $== g
bd $o (hb $o h) $== cd $o c
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae f: elt P F c: elt P C lf: fd $o f $== cd $o c g: elt P G lg: gf $o g $== f h: elt P H lh: hg $o h $== g
bd $o hb $o h $== cd $o c
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae f: elt P F c: elt P C lf: fd $o f $== cd $o c g: elt P G lg: gf $o g $== f h: elt P H lh: hg $o h $== g
fd $o hf $o h $== cd $o c
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae f: elt P F c: elt P C lf: fd $o f $== cd $o c g: elt P G lg: gf $o g $== f h: elt P H lh: hg $o h $== g
fd $o (hf $o h) $== cd $o c
Ae: Type IsGraph0: IsGraph Ae Is2Graph0: Is2Graph Ae Is01Cat0: Is01Cat Ae H0: Is1Cat Ae IsAbEpiStable0: IsAbEpiStable Ae A, B, C, D, E, F, G, H: Ae ab: A $-> B bc: B $-> C cd: C $-> D de: D $-> E ah: A $-> H hg: H $-> G gf: G $-> F fe: F $-> E hb: H $-> B bd: B $-> D hf: H $-> F fd: F $-> D trr: bd $== cd $o bc trl: hf $== gf $o hg sq: bd $o hb $== fd $o hf CatIsAbExact0: CatIsAbExact ab bc CatIsAbExact1: CatIsAbExact cd de CatIsAbExact2: CatIsAbExact ah hg CatIsAbExact3: CatIsAbExact gf fe Epic0: Epic hg Monic0: Monic cd Epic1: Epic fd P: Ae f: elt P F c: elt P C lf: fd $o f $== cd $o c g: elt P G lg: gf $o g $== f h: elt P H lh: hg $o h $== g
fd $o (gf $o hg $o h) $== cd $o c
byrewrite cat_assoc, lh, lg, lf.Defined.EndDiamond.(** ** The baby dragon lemmas *)SectionBaby_Dragon.(** The dragon lemmas involve diagrams which in general have the same shape, but can be elongated or shortened. For example, the case [n = 2] below has shape:<< top 0 top 1 top 2 / \ / \ / \ / \ / \ / \ v v v v v v mid 0 mid 1 mid 2 mid 3 \ / \ / \ / \ / \ / \ / v v v v v v bot 0 bot 1 bot 2>> where all the diagonal sequences are exact, the maps [top 0 $-> middle 0], [middle 1 $-> bot 1], and [middle 2 $-> bot 2] are epic, and the maps [top 0 $-> middle 1], [top 1 $-> middle 2], and [middle 3 $-> bot 2] are mono. For general [n], the diagram will have a similar shape, with [n + 1] objects in the top and bottom rows. *)(** The baby dragon lemma has an epi statement and a mono statement. We shall first prove the epi part, then the mono part. To do the epi part, we will show that if the map [middle 0 $-> bot 0] is epi, then so is [top 2 $-> middle 3]. Due to the lack of symmetry at the edges of the diagram, we need to prove a more general statement first to make the induction go through. *)Context {A : Type} `{IsAbEpiStable A}.(** We make a datatype for the above diagram with [n+1] squares. *)RecordBabyDragon {n : nat} := {
top : Fin n.+1 -> A;
mid : Fin n.+2 -> A;
bot : Fin n.+1 -> A;
top_l (k : Fin n.+1) : top k $-> mid (fin_incl k);
top_r (k : Fin n.+1) : top k $-> mid (fsucc k);
bot_l (k : Fin n.+1) : mid (fin_incl k) $-> bot k;
bot_r (k : Fin n.+1) : mid (fsucc k) $-> bot k;
sq (k : Fin n.+1) : (bot_l k) $o (top_l k) $== (bot_r k) $o (top_r k);
exact_r (k : Fin n) :: CatIsAbExact (top_r (fin_incl k)) (bot_l (fsucc k));
exact_l (k : Fin n) :: CatIsAbExact (top_l (fsucc k)) (bot_r (fin_incl k))
}.(** Note that [bot_l k] refers to the bottom-left map in the [k]th square, which points down and to the *right*. *)Arguments BabyDragon : clear implicits.(** In order to make an inductive argument, we need two ways of truncating a diagram. This one drops the right-hand square, keeping the left [n+1] squares. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1
BabyDragon n
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1
BabyDragon n
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n.+1
A
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n.+2
A
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n.+1
A
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n.+1
?Goal $-> ?Goal0@{k:=fin_incl k}
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n.+1
?Goal $->
?Goal0@{k:=match k with
| inl i' => inl (fsucc i')
| inr tt => inr tt
end}
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n.+1
?Goal0@{k:=fin_incl k} $-> ?Goal1
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n.+1
?Goal0@{k:=match k with
| inl i' => inl (fsucc i')
| inr tt => inr tt
end} $->
?Goal1
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n.+1
?Goal4 $o ?Goal2 $== ?Goal5 $o ?Goal3
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n.+1
A
exact (top D (fsucc k)).
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n.+2
A
exact (mid D (fsucc k)).
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n.+1
A
exact (bot D (fsucc k)).
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n.+1
top D (fsucc k) $-> mid D (fsucc (fin_incl k))
exact (top_l _ (fsucc k)).
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n.+1
top D (fsucc k) $->
mid D (fsucc match k with
| inl i' => inl (fsucc i')
| inr tt => inr tt
end)
exact (top_r _ (fsucc k)).
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n.+1
mid D (fsucc (fin_incl k)) $-> bot D (fsucc k)
exact (bot_l _ (fsucc k)).
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n.+1
mid D (fsucc match k with
| inl i' => inl (fsucc i')
| inr tt => inr tt
end) $->
bot D (fsucc k)
exact (bot_r _ (fsucc k)).
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n.+1
bot_l D (fsucc k) $o top_l D (fsucc k) $==
bot_r D (fsucc k) $o top_r D (fsucc k)
exact (sq _ (fsucc k)).
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n
CatIsAbExact (top_r D (fsucc (fin_incl k))) (bot_l D (fsucc (fsucc k)))
exact (exact_r _ (fsucc k)).
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 k: Fin n
CatIsAbExact (top_l D (fsucc (fsucc k))) (bot_r D (fsucc (fin_incl k)))
exact (exact_l _ (fsucc k)).Defined.(** This is a helper lemma that can be proved by induction. The epi part of the dragon lemma follows immediately. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n H1: forallk : Fin n.+1, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero)
Epic (bot_r D fin_last $o top_r D fin_last)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n H1: forallk : Fin n.+1, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero)
Epic (bot_r D fin_last $o top_r D fin_last)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A D: BabyDragon 0 H1: forallk : Fin 1, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero)
Epic (bot_r D fin_last $o top_r D fin_last)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Epic (bot_l D0 k)) ->
Epic (top_l D0 fin_zero) -> Epic (bot_r D0 fin_last $o top_r D0 fin_last)
Epic (bot_r D fin_last $o top_r D fin_last)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A D: BabyDragon 0 H1: forallk : Fin 1, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero)
Epic (bot_r D fin_last $o top_r D fin_last)
rapply (epic_homotopic _ _ (sq _ fin_zero)).
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Epic (bot_l D0 k)) ->
Epic (top_l D0 fin_zero) -> Epic (bot_r D0 fin_last $o top_r D0 fin_last)
Epic (bot_r D fin_last $o top_r D fin_last)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Epic (bot_l D0 k)) ->
Epic (top_l D0 fin_zero) -> Epic (bot_r D0 fin_last $o top_r D0 fin_last) P: A b_last: elt P (bot D fin_last)
Lift b_last (bot_r D fin_last $o top_r D fin_last)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Epic (bot_l D0 k)) ->
Epic (top_l D0 fin_zero) -> Epic (bot_r D0 fin_last $o top_r D0 fin_last) P: A m_last: elt P (mid D (fin_incl fin_last)) b_last: elt P (bot D fin_last) lm_last: bot_l D fin_last $o m_last $== b_last
Lift b_last (bot_r D fin_last $o top_r D fin_last)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Epic (bot_l D0 k)) ->
Epic (top_l D0 fin_zero) -> Epic (bot_r D0 fin_last $o top_r D0 fin_last) P: A m_last: elt P (mid D (fin_incl fin_last)) b_last: elt P (bot D fin_last) lm_last: bot_l D fin_last $o m_last $== b_last D':= baby_dragon_trunc_left n D: BabyDragon n
Lift b_last (bot_r D fin_last $o top_r D fin_last)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Epic (bot_l D0 k)) ->
Epic (top_l D0 fin_zero) -> Epic (bot_r D0 fin_last $o top_r D0 fin_last) P: A b_last: elt P (bot D fin_last) m_last: elt P (mid D (fin_incl fin_last)) lm_last: bot_l D fin_last $o m_last $== b_last D':= baby_dragon_trunc_left n D: BabyDragon n t_penult: elt P (top D' fin_last) lt_penult: bot_r D' fin_last $o top_r D' fin_last $o t_penult $==
bot_r D' fin_last $o m_last
Lift b_last (bot_r D fin_last $o top_r D fin_last)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Epic (bot_l D0 k)) ->
Epic (top_l D0 fin_zero) -> Epic (bot_r D0 fin_last $o top_r D0 fin_last) P: A b_last: elt P (bot D fin_last) m_last: elt P (mid D (fin_incl fin_last)) lm_last: bot_l D fin_last $o m_last $== b_last t_penult: elt P (top (baby_dragon_trunc_left n D) fin_last) lt_penult: bot_r (baby_dragon_trunc_left n D) fin_last $o
top_r (baby_dragon_trunc_left n D) fin_last $o t_penult $==
bot_r (baby_dragon_trunc_left n D) fin_last $o m_last
Lift b_last (bot_r D fin_last $o top_r D fin_last)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Epic (bot_l D0 k)) ->
Epic (top_l D0 fin_zero) -> Epic (bot_r D0 fin_last $o top_r D0 fin_last) P: A b_last: elt P (bot D fin_last) m_last: elt P (mid D (fin_incl fin_last)) lm_last: bot_l D fin_last $o m_last $== b_last t_penult: elt P (top (baby_dragon_trunc_left n D) fin_last) lt_penult: bot_r (baby_dragon_trunc_left n D) fin_last $o
top_r (baby_dragon_trunc_left n D) fin_last $o t_penult $==
bot_r (baby_dragon_trunc_left n D) fin_last $o m_last
bot_r D (fin_incl fin_last) $o
(m_last - top_r D (fin_incl fin_last) $o t_penult) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) P: A m_last: elt P (mid D (fin_incl fin_last)) b_last: elt P (bot D fin_last) lm_last: bot_l D fin_last $o m_last $== b_last t_last: elt P (top D (fsucc fin_last)) t_penult: elt P (top (baby_dragon_trunc_left n D) fin_last) lt_last: top_l D (fsucc fin_last) $o t_last $==
m_last - top_r D (fin_incl fin_last) $o t_penult
Lift b_last (bot_r D fin_last $o top_r D fin_last)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Epic (bot_l D0 k)) ->
Epic (top_l D0 fin_zero) -> Epic (bot_r D0 fin_last $o top_r D0 fin_last) P: A b_last: elt P (bot D fin_last) m_last: elt P (mid D (fin_incl fin_last)) lm_last: bot_l D fin_last $o m_last $== b_last t_penult: elt P (top (baby_dragon_trunc_left n D) fin_last) lt_penult: bot_r (baby_dragon_trunc_left n D) fin_last $o
top_r (baby_dragon_trunc_left n D) fin_last $o t_penult $==
bot_r (baby_dragon_trunc_left n D) fin_last $o m_last
bot_r D (fin_incl fin_last) $o
(m_last - top_r D (fin_incl fin_last) $o t_penult) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Epic (bot_l D0 k)) ->
Epic (top_l D0 fin_zero) -> Epic (bot_r D0 fin_last $o top_r D0 fin_last) P: A b_last: elt P (bot D fin_last) m_last: elt P (mid D (fin_incl fin_last)) lm_last: bot_l D fin_last $o m_last $== b_last t_penult: elt P (top (baby_dragon_trunc_left n D) fin_last) lt_penult: bot_r (baby_dragon_trunc_left n D) fin_last $o
top_r (baby_dragon_trunc_left n D) fin_last $o t_penult $==
bot_r (baby_dragon_trunc_left n D) fin_last $o m_last
bot_r D (fin_incl fin_last) $o m_last -
bot_r D (fin_incl fin_last) $o (top_r D (fin_incl fin_last) $o t_penult) $==
0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Epic (bot_l D0 k)) ->
Epic (top_l D0 fin_zero) -> Epic (bot_r D0 fin_last $o top_r D0 fin_last) P: A b_last: elt P (bot D fin_last) m_last: elt P (mid D (fin_incl fin_last)) lm_last: bot_l D fin_last $o m_last $== b_last t_penult: elt P (top (baby_dragon_trunc_left n D) fin_last) lt_penult: bot_r (baby_dragon_trunc_left n D) fin_last $o
top_r (baby_dragon_trunc_left n D) fin_last $o t_penult $==
bot_r (baby_dragon_trunc_left n D) fin_last $o m_last
bot_r D (fin_incl fin_last) $o m_last -
bot_r D (fin_incl fin_last) $o top_r D (fin_incl fin_last) $o t_penult $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Epic (bot_l D0 k)) ->
Epic (top_l D0 fin_zero) -> Epic (bot_r D0 fin_last $o top_r D0 fin_last) P: A b_last: elt P (bot D fin_last) m_last: elt P (mid D (fin_incl fin_last)) lm_last: bot_l D fin_last $o m_last $== b_last t_penult: elt P (top (baby_dragon_trunc_left n D) fin_last) lt_penult: bot_r (baby_dragon_trunc_left n D) fin_last $o
top_r (baby_dragon_trunc_left n D) fin_last $o t_penult $==
bot_r (baby_dragon_trunc_left n D) fin_last $o m_last
bot_r (baby_dragon_trunc_left n D) fin_last $o
top_r (baby_dragon_trunc_left n D) fin_last $o t_penult -
bot_r D (fin_incl fin_last) $o top_r D (fin_incl fin_last) $o t_penult $== 0
apply inverse_r_0gpd.
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) P: A m_last: elt P (mid D (fin_incl fin_last)) b_last: elt P (bot D fin_last) lm_last: bot_l D fin_last $o m_last $== b_last t_last: elt P (top D (fsucc fin_last)) t_penult: elt P (top (baby_dragon_trunc_left n D) fin_last) lt_last: top_l D (fsucc fin_last) $o t_last $==
m_last - top_r D (fin_incl fin_last) $o t_penult
Lift b_last (bot_r D fin_last $o top_r D fin_last)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) P: A m_last: elt P (mid D (fin_incl fin_last)) b_last: elt P (bot D fin_last) lm_last: bot_l D fin_last $o m_last $== b_last t_last: elt P (top D (fsucc fin_last)) t_penult: elt P (top (baby_dragon_trunc_left n D) fin_last) lt_last: top_l D (fsucc fin_last) $o t_last $==
m_last - top_r D (fin_incl fin_last) $o t_penult
bot_r D fin_last $o top_r D fin_last $o t_last $== b_last
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) P: A m_last: elt P (mid D (fin_incl fin_last)) b_last: elt P (bot D fin_last) lm_last: bot_l D fin_last $o m_last $== b_last t_last: elt P (top D (fsucc fin_last)) t_penult: elt P (top (baby_dragon_trunc_left n D) fin_last) lt_last: top_l D (fsucc fin_last) $o t_last $==
m_last - top_r D (fin_incl fin_last) $o t_penult
bot_l D fin_last $o top_l D fin_last $o t_last $== b_last
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) P: A m_last: elt P (mid D (fin_incl fin_last)) b_last: elt P (bot D fin_last) lm_last: bot_l D fin_last $o m_last $== b_last t_last: elt P (top D (fsucc fin_last)) t_penult: elt P (top (baby_dragon_trunc_left n D) fin_last) lt_last: top_l D (fsucc fin_last) $o t_last $==
m_last - top_r D (fin_incl fin_last) $o t_penult
bot_l D fin_last $o (top_l D fin_last $o t_last) $== b_last
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) P: A m_last: elt P (mid D (fin_incl fin_last)) b_last: elt P (bot D fin_last) lm_last: bot_l D fin_last $o m_last $== b_last t_last: elt P (top D (fsucc fin_last)) t_penult: elt P (top (baby_dragon_trunc_left n D) fin_last) lt_last: top_l D (fsucc fin_last) $o t_last $==
m_last - top_r D (fin_incl fin_last) $o t_penult
bot_l D fin_last $o (m_last - top_r D (fin_incl fin_last) $o t_penult) $==
b_last
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) P: A m_last: elt P (mid D (fin_incl fin_last)) b_last: elt P (bot D fin_last) lm_last: bot_l D fin_last $o m_last $== b_last t_last: elt P (top D (fsucc fin_last)) t_penult: elt P (top (baby_dragon_trunc_left n D) fin_last) lt_last: top_l D (fsucc fin_last) $o t_last $==
m_last - top_r D (fin_incl fin_last) $o t_penult
bot_l D fin_last $o m_last -
bot_l D fin_last $o (top_r D (fin_incl fin_last) $o t_penult) $== b_last
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) P: A m_last: elt P (mid D (fin_incl fin_last)) b_last: elt P (bot D fin_last) lm_last: bot_l D fin_last $o m_last $== b_last t_last: elt P (top D (fsucc fin_last)) t_penult: elt P (top (baby_dragon_trunc_left n D) fin_last) lt_last: top_l D (fsucc fin_last) $o t_last $==
m_last - top_r D (fin_incl fin_last) $o t_penult
bot_l D fin_last $o m_last -
bot_l D fin_last $o top_r D (fin_incl fin_last) $o t_penult $== b_last
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) P: A m_last: elt P (mid D (fin_incl fin_last)) b_last: elt P (bot D fin_last) lm_last: bot_l D fin_last $o m_last $== b_last t_last: elt P (top D (fsucc fin_last)) t_penult: elt P (top (baby_dragon_trunc_left n D) fin_last) lt_last: top_l D (fsucc fin_last) $o t_last $==
m_last - top_r D (fin_incl fin_last) $o t_penult
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) P: A m_last: elt P (mid D (fin_incl fin_last)) b_last: elt P (bot D fin_last) lm_last: bot_l D fin_last $o m_last $== b_last t_last: elt P (top D (fsucc fin_last)) t_penult: elt P (top (baby_dragon_trunc_left n D) fin_last) lt_last: top_l D (fsucc fin_last) $o t_last $==
m_last - top_r D (fin_incl fin_last) $o t_penult
bot_l D fin_last $o m_last - 0 $== b_last
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Epic (bot_l D k) Epic0: Epic (top_l D fin_zero) P: A m_last: elt P (mid D (fin_incl fin_last)) b_last: elt P (bot D fin_last) lm_last: bot_l D fin_last $o m_last $== b_last t_last: elt P (top D (fsucc fin_last)) t_penult: elt P (top (baby_dragon_trunc_left n D) fin_last) lt_last: top_l D (fsucc fin_last) $o t_last $==
m_last - top_r D (fin_incl fin_last) $o t_penult
bot_l D fin_last $o m_last $== b_last
exact lm_last.Defined.(** The epi form of the baby dragon lemma states that the map [top fin_last $-> middle fin_last] is epic. *)Definitionbaby_dragon_epi (n : nat) (D : BabyDragon n)
`{!forallk : Fin (n.+1), Epic (bot_l D k)}
`{!Epic (top_l D fin_zero)} `{!Monic (bot_r D fin_last)}
: Epic (top_r D fin_last)
:= epic_cancel_monic _ _.(** This is a helper lemma that can be proved by induction. The mono part of the dragon lemma follows immediately. *)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n H1: forallk : Fin n.+1, Monic (top_r D k) Monic0: Monic (bot_r D fin_last)
Monic (bot_l D fin_zero $o top_l D fin_zero)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n H1: forallk : Fin n.+1, Monic (top_r D k) Monic0: Monic (bot_r D fin_last)
Monic (bot_l D fin_zero $o top_l D fin_zero)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A D: BabyDragon 0 H1: forallk : Fin 1, Monic (top_r D k) Monic0: Monic (bot_r D fin_last)
Monic (bot_l D fin_zero $o top_l D fin_zero)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero)
Monic (bot_l D fin_zero $o top_l D fin_zero)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A D: BabyDragon 0 H1: forallk : Fin 1, Monic (top_r D k) Monic0: Monic (bot_r D fin_last)
Monic (bot_l D fin_zero $o top_l D fin_zero)
rapply (monic_homotopic _ _ (sq _ _)^$).
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero)
Monic (bot_l D fin_zero $o top_l D fin_zero)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t: elt P (top D fin_zero) zero_t: bot_l D fin_zero $o top_l D fin_zero $o t $== 0
t $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t: elt P (top D fin_zero) zero_t: bot_l D fin_zero $o top_l D fin_zero $o t $== 0
bot_r D fin_zero $o (top_r D fin_zero $o t) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t': elt P (top D (fsucc fin_zero)) t: elt P (top D fin_zero) lift_t': top_l D (fsucc fin_zero) $o t' $== top_r D fin_zero $o t
t $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t: elt P (top D fin_zero) zero_t: bot_l D fin_zero $o top_l D fin_zero $o t $== 0
bot_r D fin_zero $o (top_r D fin_zero $o t) $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t: elt P (top D fin_zero) zero_t: bot_l D fin_zero $o top_l D fin_zero $o t $== 0
bot_r D fin_zero $o top_r D fin_zero $o t $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t: elt P (top D fin_zero) zero_t: bot_l D fin_zero $o top_l D fin_zero $o t $== 0
bot_l D fin_zero $o top_l D fin_zero $o t $== 0
exact zero_t.
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t': elt P (top D (fsucc fin_zero)) t: elt P (top D fin_zero) lift_t': top_l D (fsucc fin_zero) $o t' $== top_r D fin_zero $o t
t $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t': elt P (top D (fsucc fin_zero)) t: elt P (top D fin_zero) lift_t': top_l D (fsucc fin_zero) $o t' $== top_r D fin_zero $o t
top_r D fin_zero $o t $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t': elt P (top D (fsucc fin_zero)) t: elt P (top D fin_zero) lift_t': top_l D (fsucc fin_zero) $o t' $== top_r D fin_zero $o t
top_l D (fsucc fin_zero) $o t' $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t': elt P (top D (fsucc fin_zero)) t: elt P (top D fin_zero) lift_t': top_l D (fsucc fin_zero) $o t' $== top_r D fin_zero $o t
top_l D (fsucc fin_zero) $o t' $== top_l D (fsucc fin_zero) $o 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t': elt P (top D (fsucc fin_zero)) t: elt P (top D fin_zero) lift_t': top_l D (fsucc fin_zero) $o t' $== top_r D fin_zero $o t
t' $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t': elt P (top D (fsucc fin_zero)) t: elt P (top D fin_zero) lift_t': top_l D (fsucc fin_zero) $o t' $== top_r D fin_zero $o t D':= baby_dragon_trunc_right n D: BabyDragon n
t' $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t': elt P (top D (fsucc fin_zero)) t: elt P (top D fin_zero) lift_t': top_l D (fsucc fin_zero) $o t' $== top_r D fin_zero $o t D':= baby_dragon_trunc_right n D: BabyDragon n
Monic (bot_r D' fin_zero $o top_r D' fin_zero)
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t': elt P (top D (fsucc fin_zero)) t: elt P (top D fin_zero) lift_t': top_l D (fsucc fin_zero) $o t' $== top_r D fin_zero $o t D':= baby_dragon_trunc_right n D: BabyDragon n
bot_r D' fin_zero $o top_r D' fin_zero $o t' $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t': elt P (top D (fsucc fin_zero)) t: elt P (top D fin_zero) lift_t': top_l D (fsucc fin_zero) $o t' $== top_r D fin_zero $o t D':= baby_dragon_trunc_right n D: BabyDragon n
Monic (bot_r D' fin_zero $o top_r D' fin_zero)
rapply (monic_homotopic _ _ (sq _ _)).
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t': elt P (top D (fsucc fin_zero)) t: elt P (top D fin_zero) lift_t': top_l D (fsucc fin_zero) $o t' $== top_r D fin_zero $o t D':= baby_dragon_trunc_right n D: BabyDragon n
bot_r D' fin_zero $o top_r D' fin_zero $o t' $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t': elt P (top D (fsucc fin_zero)) t: elt P (top D fin_zero) lift_t': top_l D (fsucc fin_zero) $o t' $== top_r D fin_zero $o t D':= baby_dragon_trunc_right n D: BabyDragon n
bot_l D' fin_zero $o top_l D' fin_zero $o t' $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t': elt P (top D (fsucc fin_zero)) t: elt P (top D fin_zero) lift_t': top_l D (fsucc fin_zero) $o t' $== top_r D fin_zero $o t
bot_l (baby_dragon_trunc_right n D) fin_zero $o
top_l (baby_dragon_trunc_right n D) fin_zero $o t' $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t': elt P (top D (fsucc fin_zero)) t: elt P (top D fin_zero) lift_t': top_l D (fsucc fin_zero) $o t' $== top_r D fin_zero $o t
bot_l (baby_dragon_trunc_right n D) fin_zero $o top_r D fin_zero $o t $== 0
A: Type IsGraph0: IsGraph A Is2Graph0: Is2Graph A Is01Cat0: Is01Cat A H: Is1Cat A H0: IsAbEpiStable A n: nat D: BabyDragon n.+1 H1: forallk : Fin n.+2, Monic (top_r D k) Monic0: Monic (bot_r D fin_last) IHn: forallD0 : BabyDragon n,
(forallk : Fin n.+1, Monic (top_r D0 k)) ->
Monic (bot_r D0 fin_last) -> Monic (bot_l D0 fin_zero $o top_l D0 fin_zero) P: A t': elt P (top D (fsucc fin_zero)) t: elt P (top D fin_zero) lift_t': top_l D (fsucc fin_zero) $o t' $== top_r D fin_zero $o t
0 $o t $== 0
apply precomp_zero.Defined.(** The mono form of the baby dragon lemma states that the map [middle fin_zero $-> bot fin_zero] is monic. *)Definitionbaby_dragon_mono (n : nat) (D : BabyDragon n)
`{!forallk : Fin (n.+1), Monic (top_r D k)}
`{!Monic (bot_r D fin_last)} `{!Epic (top_l D fin_zero)}
: Monic (bot_l D fin_zero)
:= monic_cancel_epic _ _.EndBaby_Dragon.