------------------------------------------------------------------------
-- Eliminators and initiality
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

module Partiality-algebra.Eliminators where

open import Equality.Propositional
open import Interval using (⟨ext⟩; cong-ext)
open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J using (_↔_)
import Equivalence equality-with-J as Eq
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J hiding (Type)
open import H-level.Closure equality-with-J
open import Surjection equality-with-J using (_↠_)

open import Partiality-algebra as PA hiding (id; _∘_)
open import Partiality-algebra.Category

------------------------------------------------------------------------
-- Eliminators

-- I (NAD) have tried to follow the spirit of the rules for HITs
-- specified in the HoTT-Agda library
-- (https://github.com/HoTT/HoTT-Agda/blob/master/core/lib/types/HIT_README.txt).
-- However, at the time of writing those rules don't apply to indexed
-- types.

-- A specification of a given partiality algebra's eliminator
-- arguments (for given motive sizes).

record Arguments {a p′ q′} {A : Set a} p q
                 (PA : Partiality-algebra p′ q′ A) :
                 Set (a  lsuc (p  q)  p′  q′) where

  open Partiality-algebra PA

  -- Predicate transformer related to increasing sequences.

  Inc : (P : Type  Set p)
        (Q :  {x y}  P x  P y  x  y  Set q) 
        Increasing-sequence  Set (p  q)
  Inc P Q s =
     λ (p :  n  P (s [ n ])) 
       n  Q (p n) (p (suc n)) (increasing s n)

  field
    P  : Type  Set p
    Q  :  {x y}  P x  P y  x  y  Set q
    pe : P never
    po :  x  P (now x)
    pl :  s (pq : Inc P Q s)  P ( s)
    pa :  {x y} (x⊑y : x  y) (x⊒y : x  y)
         (p-x : P x) (p-y : P y)
         (q-x⊑y : Q p-x p-y x⊑y) (q-x⊒y : Q p-y p-x x⊒y) 
         subst P (antisymmetry x⊑y x⊒y) p-x  p-y
    pp :  {x}  Uniqueness-of-identity-proofs (P x)
    qr :  x (p : P x)  Q p p (⊑-refl x)
    qt :  {x y z} (x⊑y : x  y) (y⊑z : y  z) 
         (px : P x) (py : P y) (pz : P z) 
         Q px py x⊑y  Q py pz y⊑z  Q px pz (⊑-trans x⊑y y⊑z)
    qe :  x (p : P x)  Q pe p (never⊑ x)
    qu :  s (pq : Inc P Q s) n 
         Q (proj₁ pq n) (pl s pq) (upper-bound s n)
    ql :  s ub is-ub (pq : Inc P Q s) (pu : P ub)
         (qu :  n  Q (proj₁ pq n) pu (is-ub n)) 
         Q (pl s pq) pu (least-upper-bound s ub is-ub)
    qp :  {x y} (p-x : P x) (p-y : P y) (x⊑y : x  y) 
         Proof-irrelevant (Q p-x p-y x⊑y)

-- A specification of a given partiality algebra's eliminators.

record Eliminators {a p q p′ q′} {A : Set a}
                   {PA : Partiality-algebra p′ q′ A}
                   (args : Arguments p q PA) :
                   Set (a  p  q  p′  q′) where
  open Partiality-algebra PA
  open Arguments args

  field
    ⊥-rec : (x : Type)  P x
    ⊑-rec :  {x y} (x⊑y : x  y)  Q (⊥-rec x) (⊥-rec y) x⊑y

  inc-rec : (s : Increasing-sequence)  Inc P Q s
  inc-rec = λ { (s , inc)  (  n  ⊥-rec (s   n))
                            ,  n  ⊑-rec (inc n))
                            ) }

  field

    -- Some "computation" rules.

    ⊥-rec-never : ⊥-rec never  pe
    ⊥-rec-now   :  x  ⊥-rec (now x)  po x
    ⊥-rec-⨆     :  s  ⊥-rec ( s)  pl s (inc-rec s)

-- A specification of the elimination principle for a given partiality
-- algebra (for motives of certain sizes).

Elimination-principle :
   {a p′ q′} {A : Set a} 
   p q  Partiality-algebra p′ q′ A  Set (a  lsuc (p  q)  p′  q′)
Elimination-principle p q P =
  (args : Arguments p q P)  Eliminators args

------------------------------------------------------------------------
-- Initiality

-- The statement that a given partiality algebra is homotopy-initial.

Initial :  {a p q} p′ q′ {A : Set a}  Partiality-algebra p q A 
          Set (a  p  q  lsuc (p′  q′))
Initial p′ q′ {A} P =
  (P′ : Partiality-algebra p′ q′ A)  Contractible (Morphism P P′)

-- If a partiality algebra is initial at certain sizes, then it is
-- also initial at smaller sizes.

lower-initiality :
   {a p q p₁ q₁} p₂ q₂ {A : Set a}
  (P : Partiality-algebra p q A)
  (initial : Initial (p₁  p₂) (q₁  q₂) P) 
  Initial p₁ q₁ P
lower-initiality {p₁ = p₁} {q₁} p₂ q₂ {A} P initial P′ =
  Σ-map lower-morphism lemma (initial P″)
  where
  open Partiality-algebra P′

  P″ : Partiality-algebra (p₁  p₂) (q₁  q₂) A
  P″ = record
    { Type                    =  p₂ Type
    ; partiality-algebra-with = record
      { _⊑_                = λ x y   q₂ (lower x  lower y)
      ; never              = lift never
      ; now                = lift  now
      ;                   = lift    Σ-map (lower ∘_) (lower ∘_)
      ; antisymmetry       = λ x⊑y y⊑x 
                               cong lift (antisymmetry (lower x⊑y)
                                                       (lower y⊑x))
      ; Type-UIP-unused    = λ _ _ 
                               _⇔_.to set⇔UIP
                                 (↑-closure 2 Type-is-set) _ _
      ; ⊑-refl             = lift  ⊑-refl  lower
      ; ⊑-trans            = λ x⊑y y⊑z 
                               lift (⊑-trans (lower x⊑y)
                                             (lower y⊑z))
      ; never⊑             = lift  never⊑  lower
      ; upper-bound        = λ _  lift  upper-bound _
      ; least-upper-bound  = λ _ _ 
                               lift 
                               least-upper-bound _ _ 
                               (lower ∘_)
      ; ⊑-proof-irrelevant = _⇔_.to propositional⇔irrelevant
                               (↑-closure 1 ⊑-propositional)
      }
    }

  lower-morphism : Morphism P P″  Morphism P P′
  lower-morphism m = record
    { function     = lower  function
    ; monotone     = lower  monotone
    ; strict       = cong lower strict
    ; now-to-now   = cong lower  now-to-now
    ; ω-continuous = cong lower  ω-continuous
    }
    where
    open Morphism m

  lift-morphism : Morphism P P′  Morphism P P″
  lift-morphism m = record
    { function     = lift  function
    ; monotone     = lift  monotone
    ; strict       = cong lift strict
    ; now-to-now   = cong lift  now-to-now
    ; ω-continuous = cong lift  ω-continuous
    }
    where
    open Morphism m

  lemma : {m : Morphism P P″} 
          (∀ m′  m  m′) 
          (∀ m′  lower-morphism m  m′)
  lemma {m} hyp m′ = _↔_.to equality-characterisation-Morphism
    (lower  Morphism.function m  ≡⟨ cong ((lower ∘_)  Morphism.function) (hyp (lift-morphism m′)) ⟩∎
     Morphism.function m′         )

------------------------------------------------------------------------
-- Specifying the partiality monad using eliminators is logically
-- equivalent (at the meta-level) to specifying it using initiality

-- Any partiality algebra with eliminators (at certain sizes) is
-- initial (at the same sizes).

eliminators→initiality :
   {a p q p′ q′} {A : Set a} 
  (P : Partiality-algebra p′ q′ A) 
  Elimination-principle p q P 
  Initial p q P
eliminators→initiality {p = p} {q} P elims P′ = morphism , unique
  where
  module P  = Partiality-algebra P
  module P′ = Partiality-algebra P′

  args : Arguments p q P
  args = record
    { P  = λ _  P′.Type
    ; Q  = λ x y _  x P′.⊑ y
    ; pe = P′.never
    ; po = P′.now
    ; pl = λ _  P′.⨆
    ; pa = λ x⊑y y⊑x u v u⊑v v⊑u 
             let eq = Partiality-algebra.antisymmetry P x⊑y y⊑x in

             subst (const P′.Type) eq u  ≡⟨ subst-const eq 
             u                           ≡⟨ P′.antisymmetry u⊑v v⊑u ⟩∎
             v                           
    ; pp = _⇔_.to set⇔UIP P′.Type-is-set
    ; qr = λ _  P′.⊑-refl
    ; qt = λ _ _ _ _ _  P′.⊑-trans
    ; qe = λ _  P′.never⊑
    ; qu = λ _  P′.upper-bound
    ; ql = λ _ _ _  P′.least-upper-bound
    ; qp = λ _ _ _  _⇔_.to propositional⇔irrelevant P′.⊑-propositional
           -- If the expression above is replaced by
           -- P′.⊑-proof-irrelevant, then
           -- Partiality-monad.Inductive.Monad.Adjunction.join-correct
           -- no longer type-checks.
    }

  module E = Eliminators (elims args)

  morphism : Morphism P P′
  morphism = record
    { function     = E.⊥-rec
    ; monotone     = E.⊑-rec
    ; strict       = E.⊥-rec-never
    ; now-to-now   = E.⊥-rec-now
    ; ω-continuous = E.⊥-rec-⨆
    }

  open Morphism

  function-unique : (f : Morphism P P′) 
                    E.⊥-rec  function f
  function-unique f = sym $ ⟨ext⟩ $ Eliminators.⊥-rec (elims (record
    { Q  = λ _ _ _   _ 
    ; pe = function f P.never  ≡⟨ strict f 
           P′.never            ≡⟨ sym $ E.⊥-rec-never ⟩∎
           E.⊥-rec P.never     
    ; po = λ x 
             function f (P.now x)  ≡⟨ now-to-now f x 
             P′.now x              ≡⟨ sym $ E.⊥-rec-now x ⟩∎
             E.⊥-rec (P.now x)     
    ; pl = λ s hyp 
             function f (P.⨆ s)            ≡⟨ ω-continuous f s 
             P′.⨆ (sequence-function f s)  ≡⟨ cong P′.⨆ $ _↔_.to P′.equality-characterisation-increasing (proj₁ hyp) 
             P′.⨆ (E.inc-rec s)            ≡⟨ sym $ E.⊥-rec-⨆ s 
             E.⊥-rec (P.⨆ s)               
    ; pa = λ _ _ _ _ _ _  _⇔_.to set⇔UIP P′.Type-is-set _ _
    ; pp = λ _ _  _⇔_.to set⇔UIP (mono₁ 1 (P′.Type-is-set _ _)) _ _
    ; qp = λ _ _ _ _ _  refl
    }))

  unique :  f  morphism  f
  unique f =
    _↔_.to equality-characterisation-Morphism (function-unique f)

-- Any partiality algebra with initiality (at certain sufficiently
-- large sizes) has eliminators (at certain sizes).

initiality→eliminators :
   {a p q p′ q′} {A : Set a} {P : Partiality-algebra p′ q′ A}
  (initial : Initial (p  p′) (q  q′) P) 
  Elimination-principle p q P
initiality→eliminators {p = p} {q} {p′} {q′} {A} {PA} initial args =
  record
    { ⊥-rec       = ⊥-rec
    ; ⊑-rec       = ⊑-rec
    ; ⊥-rec-never = ⊥-rec-never
    ; ⊥-rec-now   = ⊥-rec-now
    ; ⊥-rec-⨆     = ⊥-rec-⨆
    }
  where
  open Partiality-algebra PA

  open Arguments args

  private

    -- A partiality algebra with ∃ P as the carrier type.

    ∃PA : Partiality-algebra (p  p′) (q  q′) A
    ∃PA = record
      { Type                    =  P
      ; partiality-algebra-with = record
        { _⊑_                = λ { (_ , p) (_ , q)   (Q p q) }
        ; never              = never , pe
        ; now                = λ x  now x , po x
        ;                   = λ s   (Σ-map (proj₁ ∘_) (proj₁ ∘_) s)
                                   , pl _ ( proj₂  proj₁ s
                                          , proj₂  proj₂ s
                                          )
        ; antisymmetry       = λ { {x = (x , p)} {y = (y , q)}
                                   (x⊑y , Qx⊑y) (y⊑x , Qy⊑x) 
                                   Σ-≡,≡→≡
                                     (antisymmetry x⊑y y⊑x)
                                     (pa x⊑y y⊑x p q Qx⊑y Qy⊑x)
                                 }
        ; Type-UIP-unused    = _⇔_.to propositional⇔irrelevant
                                 (Σ-closure 2
                                    Type-is-set
                                     _  _⇔_.from set⇔UIP pp)
                                    _ _)
        ; ⊑-refl             = λ _  _ , qr _ _
        ; ⊑-trans            = Σ-zip ⊑-trans (qt _ _ _ _ _)
        ; never⊑             = λ _  _ , qe _ _
        ; upper-bound        = λ _ _  upper-bound _ _ , qu _ _ _
        ; least-upper-bound  = λ _ _ ⊑qs 
                                   least-upper-bound _ _ (proj₁  ⊑qs)
                                 , ql _ _ _ _ _ (proj₂  ⊑qs)
        ; ⊑-proof-irrelevant = _⇔_.to propositional⇔irrelevant
                                 (Σ-closure 1 ⊑-propositional λ _ 
                                    _⇔_.from propositional⇔irrelevant
                                      (qp _ _ _))
        }
      }

    -- Initiality gives us a morphism from PA to ∃PA.

    eliminator-morphism : Morphism PA ∃PA
    eliminator-morphism = proj₁ (initial ∃PA)

    open Morphism eliminator-morphism

    -- We can construct a morphism from ∃PA to PA directly.

    proj₁-morphism : Morphism ∃PA PA
    proj₁-morphism = record
      { function     = proj₁
      ; monotone     = proj₁
      ; strict       = refl
      ; now-to-now   = λ _  refl
      ; ω-continuous = λ _  refl
      }

    -- By composing the two morphisms we get an endomorphism on PA.

    id′ : Morphism PA PA
    id′ = proj₁-morphism PA.∘ eliminator-morphism

    -- Due to initiality this morphism must be equal to id.

    id′≡id : id′  PA.id
    id′≡id =
      let m , unique = lower-initiality p q PA initial PA in

      id′    ≡⟨ sym $ unique id′ 
      m      ≡⟨ unique PA.id ⟩∎
      PA.id  

    abstract

      -- This provides us with a key lemma used to define the
      -- eliminators.

      lemma :  x  proj₁ (function x)  x
      lemma x = cong  m  Morphism.function m x) id′≡id

    -- As an aside this means that there is a split surjection from
    -- ∃ P to Type.

    ↠Type :  P  Type
    ↠Type = record
      { logical-equivalence = record
        { to   = Morphism.function proj₁-morphism
        ; from = function
        }
      ; right-inverse-of = lemma
      }

  -- The eliminators.

  ⊥-rec :  x  P x
  ⊥-rec x =                 $⟨ proj₂ (function x) 
    P (proj₁ (function x))  ↝⟨ subst P (lemma x) ⟩□
    P x                     

  ⊑-rec :  {x y} (x⊑y : x  y)  Q (⊥-rec x) (⊥-rec y) x⊑y
  ⊑-rec {x} {y} x⊑y =                                                   $⟨ proj₂ (monotone x⊑y) 
    Q (proj₂ (function x)) (proj₂ (function y)) (proj₁ (monotone x⊑y))  ↝⟨ subst Q′ $
                                                                             Σ-≡,≡→≡ (cong₂ _,_ (lemma x) (lemma y)) (
        subst  xy  P (proj₁ xy) × P (proj₂ xy) ×
                      proj₁ xy  proj₂ xy)
              (cong₂ _,_ (lemma x) (lemma y))
              ( proj₂ (function x)
              , proj₂ (function y)
              , proj₁ (monotone x⊑y)
              )                                                                 ≡⟨ push-subst-, {y≡z = cong₂ _,_ (lemma x) (lemma y)}
                                                                                                 xy  P (proj₁ xy))
                                                                                                 xy  P (proj₂ xy) × proj₁ xy  proj₂ xy)
                                                                                                {p = ( proj₂ (function x)
                                                                                                     , proj₂ (function y)
                                                                                                     , proj₁ (monotone x⊑y)
                                                                                                     )} 
        ( subst  xy  P (proj₁ xy))
                (cong₂ _,_ (lemma x) (lemma y))
                (proj₂ (function x))
        , subst  xy  P (proj₂ xy) × proj₁ xy  proj₂ xy)
                (cong₂ _,_ (lemma x) (lemma y))
                ( proj₂ (function y)
                , proj₁ (monotone x⊑y)
                )
        )                                                                       ≡⟨ cong₂ _,_
                                                                                     (subst-∘ P proj₁ (cong₂ _,_ (lemma x) (lemma y))
                                                                                              {p = proj₂ (function x)})
                                                                                     (push-subst-, {y≡z = cong₂ _,_ (lemma x) (lemma y)}
                                                                                                    xy  P (proj₂ xy))
                                                                                                    xy  proj₁ xy  proj₂ xy)
                                                                                                   {p = ( proj₂ (function y)
                                                                                                        , proj₁ (monotone x⊑y)
                                                                                                        )}) 
        ( subst P (cong proj₁ $ cong₂ _,_ (lemma x) (lemma y))
                (proj₂ (function x))
        , subst  xy  P (proj₂ xy))
                (cong₂ _,_ (lemma x) (lemma y))
                (proj₂ (function y))
        , subst  xy  proj₁ xy  proj₂ xy)
                (cong₂ _,_ (lemma x) (lemma y))
                (proj₁ (monotone x⊑y))
        )                                                                       ≡⟨ cong₂ _,_
                                                                                     (cong  p  subst P p (proj₂ (function x))) $
                                                                                        cong-proj₁-cong₂-, (lemma x) (lemma y))
                                                                                     (cong₂ _,_
                                                                                        (subst-∘ P proj₂ (cong₂ _,_ (lemma x) (lemma y))
                                                                                                 {p = proj₂ (function y)})
                                                                                        (_⇔_.to propositional⇔irrelevant
                                                                                           ⊑-propositional
                                                                                           _ _)) 
        ( subst P (lemma x) (proj₂ (function x))
        , subst P (cong proj₂ $ cong₂ _,_ (lemma x) (lemma y))
                (proj₂ (function y))
        , x⊑y
        )                                                                       ≡⟨ cong  p  ⊥-rec x , subst P p (proj₂ (function y)) , x⊑y) $
                                                                                     cong-proj₂-cong₂-, (lemma x) (lemma y) ⟩∎
        (⊥-rec x , ⊥-rec y , x⊑y)                                               ) ⟩□

    Q (⊥-rec x) (⊥-rec y) x⊑y                                           
    where
    Q′ :
      ( λ xy  P (proj₁ xy) × P (proj₂ xy) × proj₁ xy  proj₂ xy) 
      Set q
    Q′ (_ , px , py , x⊑y) = Q px py x⊑y

  inc-rec :  s  Inc P Q s
  inc-rec (s , inc) = ⊥-rec  s , ⊑-rec  inc

  -- "Computation" rules.

  private

    -- A lemma.

    ⊥-rec-lemma′ :
       {a b} {A : Set a} {B : A  Set b} {x y : Σ A B} 
      Is-set A 
      x  y  (p : proj₁ x  proj₁ y) 
      subst B p (proj₂ x)  proj₂ y
    ⊥-rec-lemma′ {B = B} A-set =
      elim  {x y} _  (p : proj₁ x  proj₁ y) 
                        subst B p (proj₂ x)  proj₂ y)
            { (_ , x₂) p 
                subst B p x₂     ≡⟨ cong  p  subst B p _) $
                                      _⇔_.to set⇔UIP A-set p refl 
                subst B refl x₂  ≡⟨⟩

                x₂               
              })

    -- A specific instance of the lemma above.

    ⊥-rec-lemma :  {x y}  function x  (x , y)  ⊥-rec x  y
    ⊥-rec-lemma {x} {y} eq =
      ⊥-rec x                                 ≡⟨⟩
      subst P (lemma x) (proj₂ (function x))  ≡⟨ ⊥-rec-lemma′ Type-is-set eq (lemma x) ⟩∎
      y                                       

  ⊥-rec-never : ⊥-rec never  pe
  ⊥-rec-never = ⊥-rec-lemma strict

  ⊥-rec-now :  x  ⊥-rec (now x)  po x
  ⊥-rec-now x = ⊥-rec-lemma (now-to-now x)

  ⊥-rec-⨆ :  s  ⊥-rec ( s)  pl s (inc-rec s)
  ⊥-rec-⨆ s = ⊥-rec-lemma
    (function ( s)                                           ≡⟨ ω-continuous s 

      (Σ-map (proj₁ ∘_) (proj₁ ∘_) (sequence-function s)) ,
     pl _ ( proj₂  proj₁ (sequence-function s)
          , proj₂  proj₂ (sequence-function s)
          )                                                   ≡⟨⟩

      ( proj₁  function  proj₁ s
       , proj₁  monotone  proj₂ s
       ) ,
     pl _ ( proj₂  function  proj₁ s
          , proj₂  monotone  proj₂ s
          )                                                   ≡⟨ Σ-≡,≡→≡ (cong  lemma₁) lemma₂ 

      s , pl s ( ⊥-rec  proj₁ s
                , ⊑-rec  proj₂ s
                )                                             ≡⟨⟩

      s , pl s (inc-rec s)                                   )
     where
     lemma₁ =
       ( proj₁  function  proj₁ s
       , proj₁  monotone  proj₂ s
       )                             ≡⟨ _↔_.to equality-characterisation-increasing  n 
                                          lemma (s [ n ])) ⟩∎
       s                             

     lemma₂ =
       subst P (cong  lemma₁)
         (pl _ ( proj₂  function  proj₁ s
               , proj₂  monotone  proj₂ s
               ))                                         ≡⟨ sym $ subst-∘ P  lemma₁ 

       subst (P  ) lemma₁
         (pl _ ( proj₂  function  proj₁ s
               , proj₂  monotone  proj₂ s
               ))                                         ≡⟨ elim
                                                                {s′ s} eq   {i′ i} 
                                                                              subst  s   n  P (s [ n ])) eq (proj₁ i′)  proj₁ i 
                                                                              subst (P  ) eq (pl s′ i′)  pl s i)
                                                                s {i′ i} eq 
                                                                  pl s i′  ≡⟨ cong (pl s) (Σ-≡,≡→≡ eq (⟨ext⟩ λ _  qp _ _ _ _ _)) ⟩∎
                                                                  pl s i   )
                                                               lemma₁
                                                               (⟨ext⟩ λ n 
           let lemma₃ =
                 cong _[ n ] lemma₁                               ≡⟨ sym $ cong-∘ (_$ n) proj₁ lemma₁ 
                 cong (_$ n) (cong proj₁ lemma₁)                  ≡⟨ cong (cong (_$ n)) $ proj₁-Σ-≡,≡→≡ (⟨ext⟩ (lemma  proj₁ s)) _ 
                 cong (_$ n) (⟨ext⟩ (lemma  proj₁ s))            ≡⟨ cong-ext (lemma  proj₁ s) ⟩∎
                 lemma (s [ n ])                                  
           in
           subst  s   n  P (s [ n ])) lemma₁
                 (proj₂  function  proj₁ s) n                   ≡⟨ sym $ push-subst-application lemma₁  s n  P (s [ n ])) 

           subst  s  P (s [ n ])) lemma₁
                 (proj₂ (function (s [ n ])))                     ≡⟨ subst-∘ P _[ n ] lemma₁ 

           subst P (cong _[ n ] lemma₁)
                 (proj₂ (function (s [ n ])))                     ≡⟨ cong  eq  subst P eq (proj₂ (function (s [ n ])))) lemma₃ ⟩∎

           subst P (lemma (s [ n ]))
                 (proj₂ (function (s [ n ])))                     ) 

       pl s (  n  subst P (lemma (s [ n ]))
                           (proj₂ (function (s [ n ]))))
            , ⊑-rec  proj₂ s
            )                                             ≡⟨⟩

       pl s ( ⊥-rec  proj₁ s
            , ⊑-rec  proj₂ s
            )                                             

-- For any partiality algebra (with certain levels) initiality (at
-- possibly larger levels) is logically equivalent to having
-- eliminators (at the same possibly larger levels).

initiality⇔eliminators :
   {a p q p′ q′} {A : Set a} 
  (P : Partiality-algebra p′ q′ A) 
  Initial (p  p′) (q  q′) P
    
  Elimination-principle (p  p′) (q  q′) P
initiality⇔eliminators P = record
  { to   = initiality→eliminators
  ; from = eliminators→initiality P
  }

-- For any partiality algebra initiality at all levels is logically
-- equivalent (at the meta-level) to having eliminators at all levels.

∀initiality→∀eliminators :
   {a p q} {A : Set a} 
  (P : Partiality-algebra p q A) 
  (∀ p q  Initial p q P) 
  (∀ p q  Elimination-principle p q P)
∀initiality→∀eliminators {p = p′} {q = q′} P initial p q =
  initiality→eliminators (initial (p  p′) (q  q′))

∀eliminators→∀initiality :
   {a p q} {A : Set a} 
  (P : Partiality-algebra p q A) 
  (∀ p q  Elimination-principle p q P) 
  (∀ p q  Initial p q P)
∀eliminators→∀initiality P elim p q =
  eliminators→initiality P (elim p q)