{-# OPTIONS --cubical-compatible #-}
module Class.Foldable.Core where

open import Class.Prelude
open import Class.Core
open import Class.Functor
open import Class.Semigroup
open import Class.Monoid

record Foldable (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where
  field fold : ⦃ _ : Semigroup A ⦄ → ⦃ Monoid A ⦄ → F A → A

  foldMap : ⦃ _ : Semigroup B ⦄ → ⦃ Monoid B ⦄ → (A → B) → F A → B
  foldMap f = fold ∘ fmap f

open Foldable ⦃...⦄ public

record Foldable′ (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where
  field foldMap′ : ⦃ _ : Semigroup B ⦄ → ⦃ Monoid B ⦄ → (A → B) → F A → B

  fold′ : ⦃ _ : Semigroup A ⦄ → ⦃ Monoid A ⦄ → F A → A
  fold′ = foldMap′ id

open Foldable′ ⦃...⦄ public

Foldable′⇒Foldable : ⦃ _ : Functor F ⦄ → Foldable′ F → Foldable F
Foldable′⇒Foldable f = let instance _ = f in
  λ where .fold → fold′