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}