ncfavier

open import 1Lab.Prelude
open import Data.Dec
open import Data.Nat

module Goat where

holds : ∀ {ℓ} (A : Type ℓ) ⦃ _ : Dec A ⦄ → Type
holds _ ⦃ yes _ ⦄ = ⊤
holds _ ⦃ no _ ⦄ = ⊥

ncfavier

open import Cat.Functor.Naturality
open import Cat.Functor.Bifunctor
open import Cat.Functor.Coherence
open import Cat.Instances.Product
open import Cat.Functor.Compose
open import Cat.Diagram.Monad
open import Cat.Monoidal.Base
open import Cat.Functor.Base
open import Cat.Prelude

ncfavier

L ⊣ R

adjunct : (L a → b) → (a → R b)
coadjunct : (a → R b) → (L a → b)
unit : a → RL a
counit : LR b → b
Lmap : (a → b) → (L a → L b)
Rmap : (a → b) → (R a → R b)

adjunct f = unit; Rmap f

ncfavier

instance Monoid a => MonadFix ((,) a) where
  mfix :: (b -> (a, b)) -> (a, b)
  mfix f = let (a, b) = f b in (a, b)
  -- or
  mfix f = fix (f . snd)

The laws are proved in section 4.5 of Value Recursion in Monadic Computations

ncfavier

-- Moved to https://agda.monade.li/TangentBundles.html

ncfavier

-- Moved to https://agda.monade.li/FirstGroupCohomology.html

ncfavier

-- Moved to https://agda.monade.li/MonoidalFibres.html

ncfavier

    canonical-elements⇒type-like : is-set Carrier → canonical-elements → type-like c
    canonical-elements⇒type-like set
      record { canon = canon
             ; canon-≈ = canon-≈
             ; canon-≡ = canon-≡ }
      =
      record { type-like-to = Σ _ λ a → canon a ≡ a
             ; type-like-≅ = record { iso = record { _⟨$⟩_ = λ a → canon a , canon-≡ _ _ (canon-≈ a)
                                                   ; cong = λ s → Σ-≡ (canon-≡ _ _ s) set }
                                    ; inv = record { _⟨$⟩_ = fst

ncfavier

-- Moved to https://agda.monade.li/Applicative.html

ncfavier

{-# LANGUAGE LambdaCase, BlockArguments, ViewPatterns #-}
import Data.MemoTrie

count :: [Int] -> Int
count = memoFix \ go -> \case
  [0, 0, 0, 0, 0] -> 1
  [a, b, c, d, e] -> sum $ [go [b, c, d, e, a - n] | n <- [1,3..a]]
                        <> [go [e, d, c, b, a - n] | n <- [2,4..a]]

main = print $ 2 * count (replicate 5 14)