# 2-element subtypes

Content created by Egbert Rijke, Fredrik Bakke, Eléonore Mangel, Jonathan Prieto-Cubides, Elisabeth Stenholm, Julian KG, fernabnor and louismntnu.

Created on 2022-03-21.

module univalent-combinatorics.2-element-subtypes where

Imports
open import foundation.automorphisms
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-coproduct-types
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.logical-equivalences
open import foundation.mere-equivalences
open import foundation.negated-equality
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.torsorial-type-families
open import foundation.transport-along-identifications
open import foundation.type-arithmetic-coproduct-types
open import foundation.unit-type
open import foundation.universe-levels

open import univalent-combinatorics.2-element-types
open import univalent-combinatorics.standard-finite-types


## Idea

A 2-element subtype of a type A is a subtype P of A of which its underlying type Σ A P has cardinality 2. Such a subtype is said to be decidable if the proposition P x is decidable for every x : A.

## Definitions

### The type of 2-element subtypes of a type

2-Element-Subtype : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2)
2-Element-Subtype l2 X =
Σ (subtype l2 X) (λ P → has-two-elements (type-subtype P))

module _
{l1 l2 : Level} {X : UU l1} (P : 2-Element-Subtype l2 X)
where

subtype-2-Element-Subtype : subtype l2 X
subtype-2-Element-Subtype = pr1 P

type-prop-2-Element-Subtype : X → UU l2
type-prop-2-Element-Subtype x = type-Prop (subtype-2-Element-Subtype x)

is-prop-type-prop-2-Element-Subtype :
(x : X) → is-prop (type-prop-2-Element-Subtype x)
is-prop-type-prop-2-Element-Subtype x =
is-prop-type-Prop (subtype-2-Element-Subtype x)

type-2-Element-Subtype : UU (l1 ⊔ l2)
type-2-Element-Subtype = type-subtype subtype-2-Element-Subtype

inclusion-2-Element-Subtype : type-2-Element-Subtype → X
inclusion-2-Element-Subtype = inclusion-subtype subtype-2-Element-Subtype

is-emb-inclusion-2-Element-Subtype : is-emb inclusion-2-Element-Subtype
is-emb-inclusion-2-Element-Subtype =
is-emb-inclusion-subtype subtype-2-Element-Subtype

is-injective-inclusion-2-Element-Subtype :
is-injective inclusion-2-Element-Subtype
is-injective-inclusion-2-Element-Subtype =
is-injective-inclusion-subtype subtype-2-Element-Subtype

has-two-elements-type-2-Element-Subtype :
has-two-elements type-2-Element-Subtype
has-two-elements-type-2-Element-Subtype = pr2 P

2-element-type-2-Element-Subtype : 2-Element-Type (l1 ⊔ l2)
pr1 2-element-type-2-Element-Subtype = type-2-Element-Subtype
pr2 2-element-type-2-Element-Subtype = has-two-elements-type-2-Element-Subtype

is-inhabited-type-2-Element-Subtype : type-trunc-Prop type-2-Element-Subtype
is-inhabited-type-2-Element-Subtype =
is-inhabited-2-Element-Type 2-element-type-2-Element-Subtype


### The standard 2-element subtype of a pair of distinct elements in a set

module _
{l : Level} (X : Set l) {x y : type-Set X} (np : x ≠ y)
where

type-prop-standard-2-Element-Subtype : type-Set X → UU l
type-prop-standard-2-Element-Subtype z = (x ＝ z) + (y ＝ z)

is-prop-type-prop-standard-2-Element-Subtype :
(z : type-Set X) → is-prop (type-prop-standard-2-Element-Subtype z)
is-prop-type-prop-standard-2-Element-Subtype z =
is-prop-coproduct
( λ p q → np (p ∙ inv q))
( is-set-type-Set X x z)
( is-set-type-Set X y z)

subtype-standard-2-Element-Subtype : subtype l (type-Set X)
pr1 (subtype-standard-2-Element-Subtype z) =
type-prop-standard-2-Element-Subtype z
pr2 (subtype-standard-2-Element-Subtype z) =
is-prop-type-prop-standard-2-Element-Subtype z

type-standard-2-Element-Subtype : UU l
type-standard-2-Element-Subtype =
type-subtype subtype-standard-2-Element-Subtype

equiv-type-standard-2-Element-Subtype :
Fin 2 ≃ type-standard-2-Element-Subtype
equiv-type-standard-2-Element-Subtype =
( inv-equiv
( left-distributive-Σ-coproduct (type-Set X) (Id x) (Id y))) ∘e
( equiv-coproduct
( equiv-is-contr
( is-contr-Fin-one-ℕ)
( is-torsorial-Id x))
( equiv-is-contr
( is-contr-unit)
( is-torsorial-Id y)))

has-two-elements-type-standard-2-Element-Subtype :
has-two-elements type-standard-2-Element-Subtype
has-two-elements-type-standard-2-Element-Subtype =
unit-trunc-Prop equiv-type-standard-2-Element-Subtype


### Morphisms of 2-element-subtypes

A moprhism of 2-element subtypes P and Q is just a family of maps P x → Q x.

{-
module _
{l1 l2 l3 : Level} {X : UU l1}
(P : 2-Element-Subtype l2 X) (Q : 2-Element-Subtype l3 X)
where

hom-2-Element-Subtype : UU (l1 ⊔ l2 ⊔ l3)
hom-2-Element-Subtype =
(x : X) → type-prop-2-Element-Subtype P x → type-prop-2-Element-Subtype Q x

map-hom-2-Element-Subtype :
hom-2-Element-Subtype → type-2-Element-Subtype P → type-2-Element-Subtype Q
map-hom-2-Element-Subtype f = tot f

is-emb-map-hom-2-Element-Subtype :
(f : hom-2-Element-Subtype) → is-emb (map-hom-2-Element-Subtype f)
is-emb-map-hom-2-Element-Subtype f =
is-emb-tot
( λ x →
is-emb-is-prop
( is-prop-type-prop-2-Element-Subtype P x)
( is-prop-type-prop-2-Element-Subtype Q x))

is-surjective-map-hom-2-Element-Subtype :
(f : hom-2-Element-Subtype) → is-surjective (map-hom-2-Element-Subtype f)
is-surjective-map-hom-2-Element-Subtype f (pair x q) = {! type-subtype (P ∘ map-inv-equiv e) !}

is-equiv-map-hom-2-Element-Subtype :
(f : hom-2-Element-Subtype) → is-equiv (map-hom-2-Element-Subtype f)
is-equiv-map-hom-2-Element-Subtype f = {!!}
-}


### Swapping the elements in a 2-element subtype

module _
{l1 l2 : Level} {X : UU l1} (P : 2-Element-Subtype l2 X)
where

swap-2-Element-Subtype : Aut (type-2-Element-Subtype P)
swap-2-Element-Subtype =
swap-2-Element-Type (2-element-type-2-Element-Subtype P)

map-swap-2-Element-Subtype :
type-2-Element-Subtype P → type-2-Element-Subtype P
map-swap-2-Element-Subtype =
map-swap-2-Element-Type (2-element-type-2-Element-Subtype P)

compute-swap-2-Element-Subtype :
(x y : type-2-Element-Subtype P) → x ≠ y →
map-swap-2-Element-Subtype x ＝ y
compute-swap-2-Element-Subtype =
compute-swap-2-Element-Type (2-element-type-2-Element-Subtype P)


### 2-element subtypes are closed under precomposition with an equivalence

precomp-equiv-2-Element-Subtype :
{l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} → X ≃ Y →
2-Element-Subtype l3 X → 2-Element-Subtype l3 Y
pr1 (precomp-equiv-2-Element-Subtype e (pair P H)) =
P ∘ (map-inv-equiv e)
pr2 (precomp-equiv-2-Element-Subtype e (pair P H)) =
transitive-mere-equiv _ _ _
( unit-trunc-Prop
( equiv-subtype-equiv
( e)
( P)
( P ∘ (map-inv-equiv e))
( λ x →
iff-equiv
( tr
( λ g → (type-Prop (P x)) ≃ (type-Prop (P (map-equiv g x))))
( inv (left-inverse-law-equiv e))
( id-equiv)))))
( H)

{-
module _
{l : Level} {A : UU l}
where

is-injective-map-Fin-two-ℕ :
(f : Fin 2 → A) → f zero-Fin ≠ f one-Fin → is-injective f
is-injective-map-Fin-two-ℕ f H {inl (inr star)} {inl (inr star)} p = refl
is-injective-map-Fin-two-ℕ f H {inl (inr star)} {inr star} p = ex-falso (H p)
is-injective-map-Fin-two-ℕ f H {inr star} {inl (inr star)} p =
ex-falso (H (inv p))
is-injective-map-Fin-two-ℕ f H {inr star} {inr star} p = refl

is-injective-element-unordered-pair :
(p : unordered-pair A) →
¬ ( (x y : type-unordered-pair p) →
Id (element-unordered-pair p x) (element-unordered-pair p y)) →
is-injective (element-unordered-pair p)
is-injective-element-unordered-pair (pair X f) H {x} {y} p =
apply-universal-property-trunc-Prop
( has-two-elements-type-unordered-pair (pair X f))
( Id-Prop (set-UU-Fin X) x y)
( λ h → {!!})
where
first-element : (Fin 2 ≃ (type-2-Element-Type X)) →
Σ ( type-2-Element-Type X)
( λ x → ¬ ((y : type-2-Element-Type X) → Id (f x) (f y)))
first-element h =
exists-not-not-for-all-count (λ z → (w : type-2-Element-Type X) →
Id (f z) (f w)) (λ z → {!!})
{!!} {!!}
two-elements-different-image :
Σ ( type-2-Element-Type X)
( λ x → Σ (type-2-Element-Type X) (λ y → f x ≠ f y))
two-elements-different-image = {!!}
-}