# Pullbacks of subtypes

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-11-24.

module foundation.pullbacks-subtypes where

Imports
open import foundation.logical-equivalences
open import foundation.powersets
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.propositions
open import foundation-core.subtypes

open import order-theory.order-preserving-maps-large-posets
open import order-theory.order-preserving-maps-large-preorders


## Idea

Consider a subtype T of a type B and a map f : A → B. Then the pullback subtype pullback f T of A is defined to be T ∘ f. This fits in a pullback diagram

                 π₂
pullback f T -----> T
| ⌟            |
π₁ |              | i
|              |
∨              ∨
A -----------> B
f


The universal property of pullbacks quite literally returns the definition of the subtype pullback f T, because it essentially asserts that

  (S ⊆ pullback f T) ↔ ((x : A) → is-in-subtype S x → is-in-subtype T (f x)).


The operation pullback f : subtype B → subtype A is an order preserving map between the powersets of B and A.

In the file Images of subtypes we show that the pullback operation on subtypes is the upper adjoint of a Galois connection.

## Definitions

### The predicate of being a pullback of subtypes

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} (f : A → B)
(T : subtype l3 B) (S : subtype l4 A)
where

is-pullback-subtype : UUω
is-pullback-subtype =
{l : Level} (U : subtype l A) →
(U ⊆ S) ↔ ((x : A) → is-in-subtype U x → is-in-subtype T (f x))


### Pullbacks of subtypes

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) (T : subtype l3 B)
where

pullback-subtype : subtype l3 A
pullback-subtype = T ∘ f

is-in-pullback-subtype : A → UU l3
is-in-pullback-subtype = is-in-subtype pullback-subtype

is-prop-is-in-pullback-subtype :
(x : A) → is-prop (is-in-pullback-subtype x)
is-prop-is-in-pullback-subtype = is-prop-is-in-subtype pullback-subtype

type-pullback-subtype : UU (l1 ⊔ l3)
type-pullback-subtype = type-subtype pullback-subtype

inclusion-pullback-subtype : type-pullback-subtype → A
inclusion-pullback-subtype = inclusion-subtype pullback-subtype


### The order preserving pullback operation on subtypes

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
where

preserves-order-pullback-subtype :
preserves-order-map-Large-Poset
( powerset-Large-Poset B)
( powerset-Large-Poset A)
( pullback-subtype f)
preserves-order-pullback-subtype S T H x = H (f x)

pullback-subtype-hom-Large-Poset :
hom-Large-Poset (λ l → l) (powerset-Large-Poset B) (powerset-Large-Poset A)
map-hom-Large-Preorder pullback-subtype-hom-Large-Poset =
pullback-subtype f
preserves-order-hom-Large-Preorder pullback-subtype-hom-Large-Poset =
preserves-order-pullback-subtype