module abelian do
import lib/mathematics/categories/category
import lib/mathematics/homotopy/truncation

-- David Elinder Master Thesis
-- Investigating Abelian categories in univalent type theory
-- Supervisor: Thierry Coquand
-- https://odr.chalmers.se/server/api/core/bitstreams/1e433d84-c3b8-4010-b71f-4fe204ff6cf1/content

def zeroObject (C : precategory) (X: C.C.ob): U₁
 := Σ (bot: isInitial C X) (top: isTerminal C X), U

def hasZeroObject (C: precategory) : U₁
 := Σ (ob: C.C.ob) (zero: zeroObject C ob), unit

def hasAllProducts (C: precategory) : U₁
 := Σ (product: C.C.ob -> C.C.ob -> C.C.ob)
      (π₁: Π (A B : C.C.ob), C.C.hom (product A B) A)
      (π₂: Π (A B : C.C.ob), C.C.hom (product A B) B), U

def hasAllCoproducts (C: precategory) : U₁
 := Σ (coproduct: C.C.ob -> C.C.ob -> C.C.ob)
      (σ₁: Π (A B : C.C.ob), C.C.hom A (coproduct A B))
      (σ₂: Π (A B : C.C.ob), C.C.hom B (coproduct A B)), U

def isMonic (P: precategory) (Y Z : P.C.ob) (f : P.C.hom Y Z) : U
 := Π (X : P.C.ob) (g1 g2 : P.C.hom X Y),
    Path (P.C.hom X Z) (P.P.∘ X Y Z g1 f) (P.P.∘ X Y Z g2 f)
 -> Path (P.C.hom X Y) g1 g2

def isEpic (P : precategory) (X Y : P.C.ob) (f : P.C.hom X Y) : U
 := Π (Z : P.C.ob) (g1 g2 : P.C.hom Y Z),
    Path (P.C.hom X Z) (P.P.∘ X Y Z f g1) (P.P.∘ X Y Z f g2)
 -> Path (P.C.hom Y Z) g1 g2

def kernel (C: precategory) (zero: hasZeroObject C)
    (A B S: C.C.ob) (f: C.C.hom A B) : U₁
 := Σ (k: C.C.hom S A) (monic: isMonic C S A k), unit

def cokernel (C: precategory) (zero: hasZeroObject C)
    (A B S: C.C.ob) (f: C.C.hom A B)  : U₁
 := Σ (k: C.C.hom B S) (epic: isEpic C B S k), unit

def isKernel (C: precategory) (zero: hasZeroObject C)
    (A B S: C.C.ob) (f: C.C.hom A B) (k: C.C.hom S A) : U₁
 := Σ (ker: kernel C zero A B S f), Path (C.C.hom S A) ker.k k

def isCokernel (C: precategory) (zero: hasZeroObject C)
    (A B S: C.C.ob) (f: C.C.hom A B) (k: C.C.hom B S) : U₁
 := Σ (coker: cokernel C zero A B S f), Path (C.C.hom B S) coker.k k

def hasKernel (C: precategory) (zero: hasZeroObject C)
    (A B: C.C.ob) (f: C.C.hom A B) : U₁
 := ‖_‖₋₁ (Σ (monic: isMonic C A B f), unit)

def hasCokernel (C: precategory) (zero: hasZeroObject C)
    (A B: C.C.ob) (f: C.C.hom A B) : U₁
 := ‖_‖₋₁ (Σ (epic: isEpic C A B f), unit)

def hasAllKernels (C : precategory) (zero: hasZeroObject C) : U₁
 := Σ (A B : C.C.ob) (f : C.C.hom A B), hasKernel C zero A B f

def hasAllCokernels (C : precategory) (zero: hasZeroObject C) : U₁
 := Σ (A B : C.C.ob) (f : C.C.hom A B), hasCokernel C zero A B f

def isAbelian (C: precategory): U₁
 := Σ (zero:      hasZeroObject C)
      (prod:     hasAllProducts C)
      (coprod: hasAllCoproducts C)
      (ker:       hasAllKernels C zero)
      (coker:   hasAllCokernels C zero)
      (monicsAreKernels:
         Π (A S: C.C.ob) (k: C.C.hom S A),
         ‖_‖₋₁ (Σ (B: C.C.ob) (f: C.C.hom A B),
                  isKernel C zero A B S f k))
      (epicsAreCoKernels:
         Π (B S: C.C.ob) (k: C.C.hom B S),
         ‖_‖₋₁ (Σ (A: C.C.ob) (f: C.C.hom A B),
                  isCokernel C zero A B S f k)), U