{- 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