# Impredicative encodings of the logical operations

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Elisabeth Stenholm.

Created on 2022-02-09.

module foundation.impredicative-encodings where
Imports
open import foundation.conjunction
open import foundation.dependent-pair-types
open import foundation.disjunction
open import foundation.existential-quantification
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.universe-levels

open import foundation-core.coproduct-types
open import foundation-core.empty-types
open import foundation-core.equivalences
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.sets

## Idea

By quantifying over all propositions in a universe, we can define all the logical operations. The idea is to use the fact that any proposition P is equivalent to the proposition (Q : Prop l) → (P ⇒ Q) ⇒ Q, which can be thought of as the least proposition Q containing P.

### The impredicative encoding of the propositional truncation

impredicative-trunc-Prop :
{l : Level}  UU l  Prop (lsuc l)
impredicative-trunc-Prop {l} A =
Π-Prop
( Prop l)
( λ Q  function-Prop (A  type-Prop Q) Q)

type-impredicative-trunc-Prop :
{l : Level}  UU l  UU (lsuc l)
type-impredicative-trunc-Prop {l} A =
type-Prop (impredicative-trunc-Prop A)

map-impredicative-trunc-Prop :
{l : Level} (A : UU l)
type-trunc-Prop A  type-impredicative-trunc-Prop A
map-impredicative-trunc-Prop {l} A =
map-universal-property-trunc-Prop
( impredicative-trunc-Prop A)
( λ x Q f  f x)

map-inv-impredicative-trunc-Prop :
{l : Level} (A : UU l)
type-impredicative-trunc-Prop A  type-trunc-Prop A
map-inv-impredicative-trunc-Prop A H =
H (trunc-Prop A) unit-trunc-Prop

equiv-impredicative-trunc-Prop :
{l : Level} (A : UU l)
type-trunc-Prop A  type-impredicative-trunc-Prop A
equiv-impredicative-trunc-Prop A =
equiv-iff
( trunc-Prop A)
( impredicative-trunc-Prop A)
( map-impredicative-trunc-Prop A)
( map-inv-impredicative-trunc-Prop A)

### The impredicative encoding of conjunction

impredicative-conjunction-Prop :
{l1 l2 : Level}  Prop l1  Prop l2  Prop (lsuc (l1  l2))
impredicative-conjunction-Prop {l1} {l2} P1 P2 =
Π-Prop
( Prop (l1  l2))
( λ Q  function-Prop (type-Prop P1  (type-Prop P2  type-Prop Q)) Q)

type-impredicative-conjunction-Prop :
{l1 l2 : Level}  Prop l1  Prop l2  UU (lsuc (l1  l2))
type-impredicative-conjunction-Prop P1 P2 =
type-Prop (impredicative-conjunction-Prop P1 P2)

map-impredicative-conjunction-Prop :
{l1 l2 : Level} (P1 : Prop l1) (P2 : Prop l2)
type-conjunction-Prop P1 P2  type-impredicative-conjunction-Prop P1 P2
map-impredicative-conjunction-Prop {l1} {l2} P1 P2 (pair p1 p2) Q f =
f p1 p2

map-inv-impredicative-conjunction-Prop :
{l1 l2 : Level} (P1 : Prop l1) (P2 : Prop l2)
type-impredicative-conjunction-Prop P1 P2  type-conjunction-Prop P1 P2
map-inv-impredicative-conjunction-Prop P1 P2 H =
H (conjunction-Prop P1 P2)  p1 p2  pair p1 p2)

equiv-impredicative-conjunction-Prop :
{l1 l2 : Level} (P1 : Prop l1) (P2 : Prop l2)
type-conjunction-Prop P1 P2  type-impredicative-conjunction-Prop P1 P2
equiv-impredicative-conjunction-Prop P1 P2 =
equiv-iff
( conjunction-Prop P1 P2)
( impredicative-conjunction-Prop P1 P2)
( map-impredicative-conjunction-Prop P1 P2)
( map-inv-impredicative-conjunction-Prop P1 P2)

### The impredicative encoding of disjunction

impredicative-disjunction-Prop :
{l1 l2 : Level}  Prop l1  Prop l2  Prop (lsuc (l1  l2))
impredicative-disjunction-Prop {l1} {l2} P1 P2 =
Π-Prop
( Prop (l1  l2))
( λ Q
function-Prop
( type-implication-Prop P1 Q)
( function-Prop (type-implication-Prop P2 Q) Q))

type-impredicative-disjunction-Prop :
{l1 l2 : Level}  Prop l1  Prop l2  UU (lsuc (l1  l2))
type-impredicative-disjunction-Prop P1 P2 =
type-Prop (impredicative-disjunction-Prop P1 P2)

map-impredicative-disjunction-Prop :
{l1 l2 : Level} (P1 : Prop l1) (P2 : Prop l2)
type-disjunction-Prop P1 P2  type-impredicative-disjunction-Prop P1 P2
map-impredicative-disjunction-Prop {l1} {l2} P1 P2 =
map-universal-property-trunc-Prop
( impredicative-disjunction-Prop P1 P2)
( rec-coproduct
( λ x Q f1 f2  f1 x)
( λ y Q f1 f2  f2 y))

map-inv-impredicative-disjunction-Prop :
{l1 l2 : Level} (P1 : Prop l1) (P2 : Prop l2)
type-impredicative-disjunction-Prop P1 P2  type-disjunction-Prop P1 P2
map-inv-impredicative-disjunction-Prop P1 P2 H =
H ( disjunction-Prop P1 P2)
( inl-disjunction-Prop P1 P2)
( inr-disjunction-Prop P1 P2)

equiv-impredicative-disjunction-Prop :
{l1 l2 : Level} (P1 : Prop l1) (P2 : Prop l2)
type-disjunction-Prop P1 P2  type-impredicative-disjunction-Prop P1 P2
equiv-impredicative-disjunction-Prop P1 P2 =
equiv-iff
( disjunction-Prop P1 P2)
( impredicative-disjunction-Prop P1 P2)
( map-impredicative-disjunction-Prop P1 P2)
( map-inv-impredicative-disjunction-Prop P1 P2)

### The impredicative encoding of negation

impredicative-neg-Prop :
{l : Level}  UU l  Prop (lsuc l)
impredicative-neg-Prop {l} A =
Π-Prop (Prop l)  Q  function-Prop A Q)

type-impredicative-neg-Prop :
{l : Level}  UU l  UU (lsuc l)
type-impredicative-neg-Prop A =
type-Prop (impredicative-neg-Prop A)

map-impredicative-neg-Prop :
{l : Level} (A : UU l)
¬ A  type-impredicative-neg-Prop A
map-impredicative-neg-Prop A f Q a = ex-falso (f a)

map-inv-impredicative-neg-Prop :
{l : Level} (A : UU l)
type-impredicative-neg-Prop A  ¬ A
map-inv-impredicative-neg-Prop A H a = H (neg-Prop' A) a a

equiv-impredicative-neg-Prop :
{l : Level} (A : UU l)
¬ A  type-impredicative-neg-Prop A
equiv-impredicative-neg-Prop A =
equiv-iff
( neg-Prop' A)
( impredicative-neg-Prop A)
( map-impredicative-neg-Prop A)
( map-inv-impredicative-neg-Prop A)

### The impredicative encoding of existential quantification

impredicative-exists-Prop :
{l1 l2 : Level} {A : UU l1} (P : A  Prop l2)  Prop (lsuc (l1  l2))
impredicative-exists-Prop {l1} {l2} {A} P =
Π-Prop
( Prop (l1  l2))
( λ Q  function-Prop ((x : A)  type-Prop (P x)  type-Prop Q) Q)

type-impredicative-exists-Prop :
{l1 l2 : Level} {A : UU l1} (P : A  Prop l2)  UU (lsuc (l1  l2))
type-impredicative-exists-Prop P =
type-Prop (impredicative-exists-Prop P)

map-impredicative-exists-Prop :
{l1 l2 : Level} {A : UU l1} (P : A  Prop l2)
exists A P  type-impredicative-exists-Prop P
map-impredicative-exists-Prop {l1} {l2} {A} P =
map-universal-property-trunc-Prop
( impredicative-exists-Prop P)
( ind-Σ  x y Q h  h x y))

map-inv-impredicative-exists-Prop :
{l1 l2 : Level} {A : UU l1} (P : A  Prop l2)
type-impredicative-exists-Prop P  exists A P
map-inv-impredicative-exists-Prop {A = A} P H =
H ( exists-Prop A P)
( λ x y  unit-trunc-Prop (pair x y))

equiv-impredicative-exists-Prop :
{l1 l2 : Level} {A : UU l1} (P : A  Prop l2)
exists A P  type-impredicative-exists-Prop P
equiv-impredicative-exists-Prop {A = A} P =
equiv-iff
( exists-Prop A P)
( impredicative-exists-Prop P)
( map-impredicative-exists-Prop P)
( map-inv-impredicative-exists-Prop P)

### The impredicative encoding of the based identity type of a set

impredicative-based-id-Prop :
{l : Level} (A : Set l) (a x : type-Set A)  Prop (lsuc l)
impredicative-based-id-Prop {l} A a x =
Π-Prop (type-Set A  Prop l)  Q  hom-Prop (Q a) (Q x))

type-impredicative-based-id-Prop :
{l : Level} (A : Set l) (a x : type-Set A)  UU (lsuc l)
type-impredicative-based-id-Prop A a x =
type-Prop (impredicative-based-id-Prop A a x)

map-impredicative-based-id-Prop :
{l : Level} (A : Set l) (a x : type-Set A)
a  x  type-impredicative-based-id-Prop A a x
map-impredicative-based-id-Prop A a .a refl Q p = p

map-inv-impredicative-based-id-Prop :
{l : Level} (A : Set l) (a x : type-Set A)
type-impredicative-based-id-Prop A a x  a  x
map-inv-impredicative-based-id-Prop A a x H =
H  x  pair (a  x) (is-set-type-Set A a x)) refl

equiv-impredicative-based-id-Prop :
{l : Level} (A : Set l) (a x : type-Set A)
(a  x)  type-impredicative-based-id-Prop A a x
equiv-impredicative-based-id-Prop A a x =
equiv-iff
( pair (a  x) (is-set-type-Set A a x))
( impredicative-based-id-Prop A a x)
( map-impredicative-based-id-Prop A a x)
( map-inv-impredicative-based-id-Prop A a x)

### The impredicative encoding of Martin-Löf's identity type of a set

impredicative-id-Prop :
{l : Level} (A : Set l) (x y : type-Set A)  Prop (lsuc l)
impredicative-id-Prop {l} A x y =
Π-Prop (type-Set A  type-Set A  Prop l)
Q  function-Prop ((a : type-Set A)  type-Prop (Q a a)) (Q x y))

type-impredicative-id-Prop :
{l : Level} (A : Set l) (x y : type-Set A)  UU (lsuc l)
type-impredicative-id-Prop A x y =
type-Prop (impredicative-id-Prop A x y)

map-impredicative-id-Prop :
{l : Level} (A : Set l) (x y : type-Set A)
x  y  type-impredicative-id-Prop A x y
map-impredicative-id-Prop A x .x refl Q r = r x

map-inv-impredicative-id-Prop :
{l : Level} (A : Set l) (x y : type-Set A)
type-impredicative-id-Prop A x y  x  y
map-inv-impredicative-id-Prop A x y H =
H  a b  pair (a  b) (is-set-type-Set A a b))  a  refl)

equiv-impredicative-id-Prop :
{l : Level} (A : Set l) (x y : type-Set A)
(x  y)  type-impredicative-id-Prop A x y
equiv-impredicative-id-Prop A x y =
equiv-iff
( pair (x  y) (is-set-type-Set A x y))
( impredicative-id-Prop A x y)
( map-impredicative-id-Prop A x y)
( map-inv-impredicative-id-Prop A x y)