{-# OPTIONS --safe --lossy-unification #-}
module Cubical.Algebra.GradedRing.Instances.CohomologyRingFun where

open import Cubical.Foundations.Prelude

open import Cubical.Relation.Nullary

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat renaming (_+_ to _+ℕ_)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Sigma

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Ring
open import Cubical.Algebra.GradedRing.Base
open import Cubical.Algebra.GradedRing.DirectSumFun

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.RingStructure.CupProduct
open import Cubical.ZCohomology.RingStructure.RingLaws
open import Cubical.ZCohomology.RingStructure.GradedCommutativity

private variable
  ℓ : Level

open PlusBis

module _ (A : Type ℓ) where

  CohomologyRingFun-GradedRing : GradedRing ℓ-zero ℓ
  CohomologyRingFun-GradedRing =
      ⊕Fun-GradedRing
      _+'_ (makeIsMonoid isSetℕ +'-assoc +'-rid +'-lid)
      +'≡+
      (λ k → coHom k A)
      (λ k → snd (coHomGroup k A))
      1⌣
      _⌣_
      (λ {k} {l} → 0ₕ-⌣ k l)
      (λ {k} {l} → ⌣-0ₕ k l)
      (λ _ _ _ → sym (ΣPathTransport→PathΣ _ _ ((sym (+'-assoc _ _ _)) , (sym (assoc-⌣ _ _ _ _ _ _)))))
      (λ _ → sym (ΣPathTransport→PathΣ _ _ (sym (+'-rid _) , sym (lUnit⌣ _ _))))
      (λ _ → ΣPathTransport→PathΣ _ _ (refl , transportRefl _ ∙ rUnit⌣ _ _))
      (λ _ _ _ → leftDistr-⌣ _ _ _ _ _)
      λ _ _ _ → rightDistr-⌣ _ _ _ _ _