{- Type Sequences
   - Chain Complex;
   - Fiber Sequence;
   - Pointed Map Sequence;
   - Group Sequence;
   - Abelian Group Sequence.
   Copyrigh (c) Groupoid Infinity, 2014-2018. -}

module seq where
import algebra
import pointed
import nat
import fun

-- Cohomology Sequences
data Seq (A: U) (B: A -> A -> U) (X Y: A)
   = seqNil (_: A)
   | seqCons (X Y Z: A) (_: B X Y) (_: Seq A B Y Z)

-- Fiber Sequence
fibSeq: pointed -> pointed -> U = Seq pointed pmap
fibNil (X: pointed): fibSeq X X = seqNil X
fibCons (X Y Z: pointed) (h: pmap X Y) (t: fibSeq Y Z): fibSeq X Z = seqCons X Y Z h t

-- Group Homomorphism Sequence
homSeq: group -> group -> U = Seq group grouphom
homNil (X: group): homSeq X X = seqNil X
homCons (X Y Z: group) (h: grouphom X Y) (t: homSeq Y Z): homSeq X Z = seqCons X Y Z h t

-- Abelian Group Homomorphism Sequence
abSeq: abgroup -> abgroup -> U = Seq abgroup abgrouphom
abNil (X: abgroup): abSeq X X = seqNil X
abCons (X Y Z: abgroup) (h: abgrouphom X Y) (t: abSeq Y Z): abSeq X Z = seqCons X Y Z h t

-- Functor Sequence
catSeq: precategory -> precategory -> U = Seq precategory catfunctor
catNil (X: precategory): catSeq X X = seqNil X
catCons (X Y Z: precategory) (h: catfunctor X Y) (t: catSeq Y Z): catSeq X Z = seqCons X Y Z h t

opaque Seq