open import Categories.Category.Core
open import Categories.Object.NaturalNumbers.Parametrized
open import Categories.Category.Distributive
open import Monad.Instance.Delay
open import Monad.Instance.Delay.Quotient

-- Each step of the proof is too computationally expensive, so we had to split them into separate files.
-- This file shall serve as an index.

module Monad.Instance.Delay.Quotient.Theorem.Index {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (DM : DelayM (Distributive.cocartesian distributive)) (PNNO : ParametrizedNNO C (Distributive.cartesian distributive)) (DQ : DelayQ distributive DM PNNO) where

  -- The definitions of the conditions
  open import Monad.Instance.Delay.Quotient.Theorem.Conditions distributive DM PNNO DQ

  -- Step 1 ⇒ 2
  open import Monad.Instance.Delay.Quotient.Theorem.Condition1-2 distributive DM PNNO DQ

  -- Step 2 ⇒ 3
  open import Monad.Instance.Delay.Quotient.Theorem.Condition2-3 distributive DM PNNO DQ

  -- Step 3 ⇒ 1
  open import Monad.Instance.Delay.Quotient.Theorem.Condition3-1 distributive DM PNNO DQ

  -- Step 3 ⇒ 4
  open import Monad.Instance.Delay.Quotient.Theorem.Condition3-4 distributive DM PNNO DQ

  -- Step 4 ⇒ 2
  open import Monad.Instance.Delay.Quotient.Theorem.Condition4-2 distributive DM PNNO DQ