# The closed modalities

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-06-08.

module orthogonal-factorization-systems.closed-modalities where
Imports
open import foundation.contractible-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.torsorial-type-families
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import orthogonal-factorization-systems.modal-operators
open import orthogonal-factorization-systems.reflective-subuniverses
open import orthogonal-factorization-systems.sigma-closed-reflective-subuniverses

open import synthetic-homotopy-theory.joins-of-types

## Idea

Given any proposition Q, the join operation _* Q defines a higher modality. We call these the closed modalities.

## Definition

operator-closed-modality :
{l lQ : Level} (Q : Prop lQ)  operator-modality l (l  lQ)
operator-closed-modality Q A = A * type-Prop Q

unit-closed-modality :
{l lQ : Level} (Q : Prop lQ)  unit-modality (operator-closed-modality {l} Q)
unit-closed-modality Q = inl-join

is-closed-modal :
{l lQ : Level} (Q : Prop lQ)  UU l  Prop (l  lQ)
pr1 (is-closed-modal Q B) = type-Prop Q  is-contr B
pr2 (is-closed-modal Q B) = is-prop-function-type is-property-is-contr

## Properties

### The closed modalities define Σ-closed reflective subuniverses

module _
{l lQ : Level} (Q : Prop lQ)
where

is-reflective-subuniverse-closed-modality :
is-reflective-subuniverse {l  lQ} (is-closed-modal Q)
pr1 is-reflective-subuniverse-closed-modality =
operator-closed-modality {l  lQ} Q
pr1 (pr2 is-reflective-subuniverse-closed-modality) =
unit-closed-modality Q
pr1 (pr2 (pr2 is-reflective-subuniverse-closed-modality)) A q =
right-zero-law-join-is-contr
( A)
( type-Prop Q)
( is-proof-irrelevant-is-prop (is-prop-type-Prop Q) q)
pr2 (pr2 (pr2 is-reflective-subuniverse-closed-modality)) B A is-modal-B =
is-equiv-is-contr-map
( λ f
is-contr-equiv
( Σ (A  B) (_＝ f))
( equiv-Σ-equiv-base
( _＝ f)
( right-unit-law-Σ-is-contr
( λ f'
is-contr-Σ
( is-contr-Π is-modal-B)
( center  is-modal-B)
( is-contr-Π
( λ (a , q)
is-prop-is-contr
( is-modal-B q)
( f' a)
( center (is-modal-B q))))) ∘e
( equiv-up-join B)))
( is-torsorial-Id' f))

reflective-subuniverse-closed-modality :
reflective-subuniverse (l  lQ) (l  lQ)
pr1 reflective-subuniverse-closed-modality =
is-closed-modal Q
pr2 reflective-subuniverse-closed-modality =
is-reflective-subuniverse-closed-modality

is-closed-under-Σ-reflective-subuniverse-closed-modality :
is-closed-under-Σ-reflective-subuniverse
( reflective-subuniverse-closed-modality)
is-closed-under-Σ-reflective-subuniverse-closed-modality A B q =
is-contr-Σ
( pr2 A q)
( center (pr2 A q))
( pr2 (B (center (pr2 A q))) q)

closed-under-Σ-reflective-subuniverse-closed-modality :
closed-under-Σ-reflective-subuniverse (l  lQ) (l  lQ)
pr1 closed-under-Σ-reflective-subuniverse-closed-modality =
reflective-subuniverse-closed-modality
pr2 closed-under-Σ-reflective-subuniverse-closed-modality =
is-closed-under-Σ-reflective-subuniverse-closed-modality