Jon Sterling, started 17th Dec 2022

We could consider three forms of depolarization for a deductive system:
1. All objects have positive polarity
2. All objects have negative polarity
3. Either (1) or (2).

It will happen that all three forms of depolarization are equivalent; moreover,
a depolarized deductive system is the same thing as a precategory.

\begin{code}

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

open import UF.FunExt

module Duploids.Depolarization (fe : Fun-Ext) where

open import MLTT.Spartan
open import UF.Base
open import UF.Equiv
open import UF.PropTrunc
open import UF.Retracts
open import UF.HLevels
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

open import Categories.Category fe
open import Duploids.DeductiveSystem fe

module _ (๐““ : deductive-system ๐“ค ๐“ฅ) where
 module ๐““ = deductive-system ๐““
 open ๐““
 open polarities ๐““

 is-pos-depolarized : ๐“ค โŠ” ๐“ฅ ฬ‡
 is-pos-depolarized = (A : ob) โ†’ is-positive A

 is-neg-depolarized : ๐“ค โŠ” ๐“ฅ ฬ‡
 is-neg-depolarized = (A : ob) โ†’ is-negative A

 being-pos-depolarized-is-prop : is-prop is-pos-depolarized
 being-pos-depolarized-is-prop =
  ฮ -is-prop fe ฮป _ โ†’
  being-positive-is-prop

 being-neg-depolarized-is-prop : is-prop is-neg-depolarized
 being-neg-depolarized-is-prop =
  ฮ -is-prop fe ฮป _ โ†’
  being-negative-is-prop
\end{code}

The positive and negative depolarizations are equivalent.

\begin{code}
 is-pos-depolarized-gives-is-neg-depolarized
  : is-pos-depolarized
  โ†’ is-neg-depolarized
 is-pos-depolarized-gives-is-neg-depolarized pos A B f C D g h =
  pos C D h B A g f

 is-neg-depolarized-gives-is-pos-depolarized
  : is-neg-depolarized
  โ†’ is-pos-depolarized
 is-neg-depolarized-gives-is-pos-depolarized neg A B f U V g h =
  neg V U h A B g f
\end{code}

A depolarized deductive system enjoys the full associativity axiom and therefore
gives rise to a precategory.

\begin{code}
 module depolarization-and-precategories (H : is-pos-depolarized) where
  depolarization-gives-assoc : category-axiom-statements.statement-assoc ๐““.str
  depolarization-gives-assoc A B C D f g h = H C D h A B g f โปยน

  depolarization-gives-precategory-axioms : precategory-axioms ๐““.str
  depolarization-gives-precategory-axioms =
   โŠข-is-set ,
   idn-L ,
   idn-R ,
   depolarization-gives-assoc

  precategory-of-depolarized-deductive-system : precategory ๐“ค ๐“ฅ
  precategory-of-depolarized-deductive-system =
   make ๐““.str depolarization-gives-precategory-axioms
\end{code}

Conversely, any deductive system enjoying the axioms of a precategory is
depolarized.

\begin{code}
 module _ (ax : precategory-axioms ๐““.str) where
  module ax = precategory-axioms ๐““.str ax

  precategory-gives-pos-depolarized : is-pos-depolarized
  precategory-gives-pos-depolarized A B f U V g h =
   ax.assoc U V A B h g f โปยน
\end{code}

For the sake of symmetry, we may considered an equivalent "unbiased" form of
depolarization, which requires propositional truncation.

\begin{code}
 module unbiased-depolarization (pt : propositional-truncations-exist) where
  open PropositionalTruncation pt

  depolarization : ๐“ค โŠ” ๐“ฅ ฬ‡
  depolarization = is-pos-depolarized + is-neg-depolarized

  is-depolarized : ๐“ค โŠ” ๐“ฅ ฬ‡
  is-depolarized = โˆฅ depolarization โˆฅ
\end{code}

When a deductive system is depolarized in the unbiased sense, it is both
positively and negatively depolarized. Hence, all notions of depolarization are
equivalent.

\begin{code}
  module _ (H : is-depolarized) where
   is-depolarized-gives-is-pos-depolarized : is-pos-depolarized
   is-depolarized-gives-is-pos-depolarized A B f U V g h =
    โˆฅโˆฅ-rec (โŠข-is-set _ _) case H
    where
     case : depolarization โ†’ cut (cut h g) f ๏ผ cut h (cut g f)
     case (inl pos) =
      pos A B f U V g h
     case (inr neg) =
      is-neg-depolarized-gives-is-pos-depolarized
       neg
       A B f U V g h

   is-depolarized-gives-is-neg-depolarized : is-neg-depolarized
   is-depolarized-gives-is-neg-depolarized =
    is-pos-depolarized-gives-is-neg-depolarized
     is-depolarized-gives-is-pos-depolarized


depolarized-deductive-system : (๐“ค ๐“ฅ : Universe) โ†’ (๐“ค โŠ” ๐“ฅ)โบ ฬ‡
depolarized-deductive-system ๐“ค ๐“ฅ =
 ฮฃ ๐““ ๊ž‰ deductive-system ๐“ค ๐“ฅ ,
 is-pos-depolarized ๐““

depolarized-deductive-system-to-precategory
 : depolarized-deductive-system ๐“ค ๐“ฅ
 โ†’ precategory ๐“ค ๐“ฅ
depolarized-deductive-system-to-precategory (๐““ , H) =
 let open depolarization-and-precategories in
 precategory-of-depolarized-deductive-system ๐““ H

precategory-to-depolarized-deductive-system
 : precategory ๐“ค ๐“ฅ
 โ†’ depolarized-deductive-system ๐“ค ๐“ฅ
precategory-to-depolarized-deductive-system ๐“’ =
 ๐““ , precategory-gives-pos-depolarized ๐““ (precategory.ax ๐“’)
 where
  open precategory ๐“’
  open depolarization-and-precategories
  ๐““ : deductive-system _ _
  ๐““ = make (precategory.str ๐“’) (hom-is-set , idn-L , idn-R)

depolarized-deductive-system-to-precategory-is-equiv
 : is-equiv (depolarized-deductive-system-to-precategory {๐“ค} {๐“ฅ})
depolarized-deductive-system-to-precategory-is-equiv = H
 where
  H : is-equiv (depolarized-deductive-system-to-precategory {๐“ค} {๐“ฅ})
  prโ‚ H =
   precategory-to-depolarized-deductive-system , ฮป ๐“’ โ†’
    equivs-are-lc
     precategory-as-sum.to-sum
     precategory-as-sum.to-sum-is-equiv
     (to-ฮฃ-๏ผ (refl , precategory-axioms-is-prop (precategory.str ๐“’) _ _))
  prโ‚‚ H =
   precategory-to-depolarized-deductive-system ,
   ฮป (๐““ , _) โ†’ to-ฮฃ-๏ผ (refl , being-pos-depolarized-is-prop ๐““ _ _)
\end{code}