Jon Sterling, started 16th Dec 2022

A preduploid is a deductive system in which every object is polarized,
i.e. either positive or negative. Because an object could be both positive *and*
negative, it is necessary to state the preduploid axiom using a propositional
truncation. This definition differs from that of Munch-Maccagnoni (who includes
in the definition of a preduploid a choice of polarization), who has suggested
the modified definition in private communication.

\begin{code}

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

open import UF.PropTrunc
open import UF.FunExt

module Duploids.Preduploid (fe : Fun-Ext) (pt : propositional-truncations-exist) where

open PropositionalTruncation pt

open import MLTT.Spartan
open import UF.Base
open import UF.Equiv
open import UF.Sets-Properties
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Subsingletons-Properties

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

module _ (๐ : deductive-system ๐ค ๐ฅ) where
open deductive-system ๐
open โข-properties ๐
open polarities ๐

is-polarized : (A : ob) โ ๐ค โ ๐ฅ ฬ
is-polarized A = โฅ is-positive A + is-negative A โฅ

being-polarized-is-prop : {A : ob} โ is-prop (is-polarized A)
being-polarized-is-prop = โฅโฅ-is-prop

preduploid-axioms : ๐ค โ ๐ฅ ฬ
preduploid-axioms = (A : ob) โ is-polarized A

preduploid-axioms-is-prop : is-prop preduploid-axioms
preduploid-axioms-is-prop =
ฮ -is-prop fe ฮป _ โ
being-polarized-is-prop

-- TODO: consider flattening the structure
record preduploid (๐ค ๐ฅ : Universe) : (๐ค โ ๐ฅ)โบ ฬ where
constructor make
field
str : deductive-system ๐ค ๐ฅ
ax : preduploid-axioms str

underlying-deductive-system = str

open deductive-system underlying-deductive-system hiding (str ; ax) public

ob-is-polarized : (A : ob) โ is-polarized str A
ob-is-polarized = ax

module preduploid-as-sum (๐ค ๐ฅ : Universe) where
to-sum : preduploid ๐ค ๐ฅ โ ฮฃ str ๊ deductive-system ๐ค ๐ฅ , preduploid-axioms str
to-sum ๐ = let open preduploid ๐ in str , ax

from-sum : (ฮฃ str ๊ deductive-system ๐ค ๐ฅ , preduploid-axioms str) โ preduploid ๐ค ๐ฅ
from-sum ๐ = make (prโ ๐) (prโ ๐)

to-sum-is-equiv : is-equiv to-sum
prโ (prโ to-sum-is-equiv) = from-sum
prโ (prโ to-sum-is-equiv) _ = refl
prโ (prโ to-sum-is-equiv) = from-sum
prโ (prโ to-sum-is-equiv) _ = refl

equiv : preduploid ๐ค ๐ฅ โ (ฮฃ str ๊ deductive-system ๐ค ๐ฅ , preduploid-axioms str)
equiv = to-sum , to-sum-is-equiv
\end{code}

It is currently not totally clear what the correct statement of univalence for a
preduploid is, but one option (inspired by the identification of preduploids
with adjunctions) is to have two univalence conditions: one for thunkable maps
between positive objects and another for linear maps between negative objects.

\begin{code}
module _ (๐ : preduploid ๐ค ๐ฅ) where
open preduploid ๐

module preduploid-univalence where
open polarities underlying-deductive-system
open โข-properties underlying-deductive-system

module _ (A B : ob) where
module _ (f : A โข B) where
is-thunkable-iso : ๐ค โ ๐ฅ ฬ
is-thunkable-iso = is-thunkable f ร (ฮฃ g ๊ (B โข A) , is-inverse f g)

is-linear-iso : ๐ค โ ๐ฅ ฬ
is-linear-iso = is-linear f ร (ฮฃ g ๊ (B โข A) , is-inverse f g)

thunkable-iso : ๐ค โ ๐ฅ ฬ
thunkable-iso = ฮฃ f ๊ A โข B , is-thunkable-iso f

linear-iso : ๐ค โ ๐ฅ ฬ
linear-iso = ฮฃ f ๊ A โข B , is-linear-iso f

๏ผ-to-thunkable-iso : (A B : ob) โ A ๏ผ B โ thunkable-iso A B
๏ผ-to-thunkable-iso A .A refl =
idn A , idn-thunkable A , idn A , idn-L _ _ _ , idn-L _ _ _

๏ผ-to-linear-iso : (A B : ob) โ A ๏ผ B โ linear-iso A B
๏ผ-to-linear-iso A B refl =
idn A , idn-linear A , idn A , idn-L _ _ _ , idn-L _ _ _

is-positively-univalent : ๐ค โ ๐ฅ ฬ
is-positively-univalent =
(A B : ob)
โ is-positive A
โ is-positive B
โ is-equiv (๏ผ-to-thunkable-iso A B)

is-negatively-univalent : ๐ค โ ๐ฅ ฬ
is-negatively-univalent =
(A B : ob)
โ is-negative A
โ is-negative B
โ is-equiv (๏ผ-to-linear-iso A B)

is-univalent : ๐ค โ ๐ฅ ฬ
is-univalent = is-positively-univalent ร is-negatively-univalent
\end{code}

Several *categories* can be obtained from a given preduploid:

1. The category of negative objects and all maps.
2. The category of positive objects and all maps.
3. The category of negative objects and linear maps.
4. The category of positive objects and linear maps.

We define these below, and they will play a role in the structure theorem that
identifies duploids with adjunctions; it is also possible to consider the full
subcategories of a preduploid spanned by linear or thunkable maps. We have not
implemented these yet.

\begin{code}
module NegativesAndAllMaps (๐ : preduploid ๐ค ๐ฅ) where
module ๐ = preduploid ๐
open polarities ๐.underlying-deductive-system

ob : ๐ค โ ๐ฅ ฬ
ob = ฮฃ A ๊ ๐.ob , is-negative A

hom : ob โ ob โ ๐ฅ ฬ
hom A B = prโ A ๐.โข prโ B

idn : (A : ob) โ hom A A
idn A = ๐.idn (prโ A)

seq : (A B C : ob) โ hom A B โ hom B C โ hom A C
seq _ _ _ f g = ๐.cut f g

cat-data : category-structure (๐ค โ ๐ฅ) ๐ฅ
cat-data = ob , hom , idn , seq

module _ (open category-axiom-statements) where
hom-is-set : statement-hom-is-set cat-data
hom-is-set A B = ๐.โข-is-set (prโ A) (prโ B)

idn-L : statement-idn-L cat-data
idn-L A B = ๐.idn-L (prโ A) (prโ B)

idn-R : statement-idn-R cat-data
idn-R A B = ๐.idn-R (prโ A) (prโ B)

assoc : statement-assoc cat-data
assoc A B C D f g h = prโ B (prโ A) f (prโ C) (prโ D) g h โปยน

precat : precategory (๐ค โ ๐ฅ) ๐ฅ
precat = make cat-data (hom-is-set , idn-L , idn-R , assoc)

module PositivesAndAllMaps (๐ : preduploid ๐ค ๐ฅ) where
module ๐ = preduploid ๐
open polarities ๐.underlying-deductive-system

ob : ๐ค โ ๐ฅ ฬ
ob = ฮฃ A ๊ ๐.ob , is-positive A

hom : ob โ ob โ ๐ฅ ฬ
hom A B = prโ A ๐.โข prโ B

idn : (A : ob) โ hom A A
idn A = ๐.idn (prโ A)

seq : (A B C : ob) โ hom A B โ hom B C โ hom A C
seq _ _ _ f g = ๐.cut f g

cat-data : category-structure (๐ค โ ๐ฅ) ๐ฅ
cat-data = ob , hom , idn , seq

module _ (open category-axiom-statements) where
hom-is-set : statement-hom-is-set cat-data
hom-is-set A B = ๐.โข-is-set (prโ A) (prโ B)

idn-L : statement-idn-L cat-data
idn-L A B = ๐.idn-L (prโ A) (prโ B)

idn-R : statement-idn-R cat-data
idn-R A B = ๐.idn-R (prโ A) (prโ B)

assoc : statement-assoc cat-data
assoc A B C D f g h = prโ C (prโ D) h (prโ A) (prโ B) g f โปยน

precat : precategory (๐ค โ ๐ฅ) ๐ฅ
precat = make cat-data (hom-is-set , idn-L , idn-R , assoc)

module NegativesAndLinearMaps (๐ : preduploid ๐ค ๐ฅ) where
module ๐ = preduploid ๐
open polarities ๐.underlying-deductive-system
open โข-properties ๐.underlying-deductive-system

ob : ๐ค โ ๐ฅ ฬ
ob = ฮฃ A ๊ ๐.ob , is-negative A

hom : ob โ ob โ ๐ค โ ๐ฅ ฬ
hom A B = ฮฃ f ๊ (prโ A ๐.โข prโ B) , is-linear f

idn : (A : ob) โ hom A A
prโ (idn A) = ๐.idn (prโ A)
prโ (idn A) = idn-linear (prโ A)

seq : (A B C : ob) โ hom A B โ hom B C โ hom A C
prโ (seq _ _ _ f g) = ๐.cut (prโ f) (prโ g)
prโ (seq _ _ _ f g) = cut-linear (prโ f) (prโ g) (prโ f) (prโ g)

cat-data : category-structure (๐ค โ ๐ฅ) (๐ค โ ๐ฅ)
cat-data = ob , hom , idn , seq

open category-axiom-statements

module _ (A B : ob) (f g : hom A B) where
to-hom-๏ผ : prโ f ๏ผ prโ g โ f ๏ผ g
to-hom-๏ผ h = to-ฮฃ-๏ผ (h , being-linear-is-prop _ _)

hom-is-set : statement-hom-is-set cat-data
hom-is-set A B =
ฮฃ-is-set (๐.โข-is-set (prโ A) (prโ B)) ฮป _ โ
props-are-sets being-linear-is-prop

idn-L : statement-idn-L cat-data
idn-L A B f = to-hom-๏ผ A B _ _ (๐.idn-L (prโ A) (prโ B) (prโ f))

idn-R : statement-idn-R cat-data
idn-R A B f = to-hom-๏ผ A B _ _ (๐.idn-R (prโ A) (prโ B) (prโ f))

assoc : statement-assoc cat-data
assoc A B C D f g h =
to-hom-๏ผ A D _ _
(prโ B (prโ A) (prโ f) (prโ C) (prโ D) (prโ g) (prโ h) โปยน)

precat : precategory (๐ค โ ๐ฅ) (๐ค โ ๐ฅ)
precat = make cat-data (hom-is-set , idn-L , idn-R , assoc)

module PositivesAndThunkableMaps (๐ : preduploid ๐ค ๐ฅ) where
module ๐ = preduploid ๐
open polarities ๐.underlying-deductive-system
open โข-properties ๐.underlying-deductive-system

ob : ๐ค โ ๐ฅ ฬ
ob = ฮฃ A ๊ ๐.ob , is-positive A

hom : ob โ ob โ ๐ค โ ๐ฅ ฬ
hom A B = ฮฃ f ๊ (prโ A ๐.โข prโ B) , is-thunkable f

idn : (A : ob) โ hom A A
prโ (idn A) = ๐.idn (prโ A)
prโ (idn A) = idn-thunkable (prโ A)

seq : (A B C : ob) โ hom A B โ hom B C โ hom A C
prโ (seq _ _ _ f g) = ๐.cut (prโ f) (prโ g)
prโ (seq _ _ _ f g) = cut-thunkable (prโ f) (prโ g) (prโ f) (prโ g)

cat-data : category-structure (๐ค โ ๐ฅ) (๐ค โ ๐ฅ)
cat-data = ob , hom , idn , seq

open category-axiom-statements

module _ (A B : ob) (f g : hom A B) where
to-hom-๏ผ : prโ f ๏ผ prโ g โ f ๏ผ g
to-hom-๏ผ h = to-ฮฃ-๏ผ (h , being-thunkable-is-prop _ _)

hom-is-set : statement-hom-is-set cat-data
hom-is-set A B =
ฮฃ-is-set (๐.โข-is-set (prโ A) (prโ B)) ฮป _ โ
props-are-sets being-thunkable-is-prop

idn-L : statement-idn-L cat-data
idn-L A B f = to-hom-๏ผ A B _ _ (๐.idn-L (prโ A) (prโ B) (prโ f))

idn-R : statement-idn-R cat-data
idn-R A B f = to-hom-๏ผ A B _ _ (๐.idn-R (prโ A) (prโ B) (prโ f))

assoc : statement-assoc cat-data
assoc A B C D f g h =
to-hom-๏ผ A D _ _
(prโ C (prโ D) (prโ h) (prโ A) (prโ B) (prโ g) (prโ f) โปยน)

precat : precategory (๐ค โ ๐ฅ) (๐ค โ ๐ฅ)
precat = make cat-data (hom-is-set , idn-L , idn-R , assoc)

\end{code}