2-element decidable subtypes

module univalent-combinatorics.2-element-decidable-subtypes where
Imports
open import elementary-number-theory.equality-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.well-ordering-principle-standard-finite-types

open import foundation.automorphisms
open import foundation.booleans
open import foundation.coproduct-types
open import foundation.decidable-equality
open import foundation.decidable-propositions
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.functions
open import foundation.functoriality-coproduct-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-propositional-truncation
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.logical-equivalences
open import foundation.mere-equivalences
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.subtypes
open import foundation.type-arithmetic-coproduct-types
open import foundation.univalence
open import foundation.universe-levels

open import univalent-combinatorics.2-element-subtypes
open import univalent-combinatorics.2-element-types
open import univalent-combinatorics.decidable-subtypes
open import univalent-combinatorics.dependent-function-types
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.standard-finite-types

Idea

A 2-element decidable subtype of a type A is a decidable subtype of A of which the underlying type has 2 elements.

Definition

The type of 2-element decidable subtypes

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

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

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

  subtype-2-Element-Decidable-Subtype : subtype l2 X
  subtype-2-Element-Decidable-Subtype =
    subtype-decidable-subtype decidable-subtype-2-Element-Decidable-Subtype

  is-decidable-subtype-subtype-2-Element-Decidable-Subtype :
    is-decidable-subtype subtype-2-Element-Decidable-Subtype
  is-decidable-subtype-subtype-2-Element-Decidable-Subtype =
    is-decidable-decidable-subtype
      decidable-subtype-2-Element-Decidable-Subtype

  is-in-2-Element-Decidable-Subtype : X  UU l2
  is-in-2-Element-Decidable-Subtype =
    is-in-decidable-subtype decidable-subtype-2-Element-Decidable-Subtype

  is-prop-is-in-2-Element-Decidable-Subtype :
    (x : X)  is-prop (is-in-2-Element-Decidable-Subtype x)
  is-prop-is-in-2-Element-Decidable-Subtype =
    is-prop-is-in-decidable-subtype
      decidable-subtype-2-Element-Decidable-Subtype

  eq-is-in-2-Element-Decidable-Subtype :
    {x : X} {y z : is-in-2-Element-Decidable-Subtype x}  Id y z
  eq-is-in-2-Element-Decidable-Subtype {x} =
    eq-is-prop (is-prop-is-in-2-Element-Decidable-Subtype x)

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

  inclusion-2-Element-Decidable-Subtype : type-2-Element-Decidable-Subtype  X
  inclusion-2-Element-Decidable-Subtype =
    inclusion-decidable-subtype decidable-subtype-2-Element-Decidable-Subtype

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

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

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

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

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

The standard 2-element decidable subtypes in a type with decidable equality

module _
  {l : Level} {X : UU l} (d : has-decidable-equality X) {x y : X}
  (np : ¬ (Id x y))
  where

  type-prop-standard-2-Element-Decidable-Subtype : X  UU l
  type-prop-standard-2-Element-Decidable-Subtype =
    type-prop-standard-2-Element-Subtype
      ( pair X (is-set-has-decidable-equality d))
      ( np)

  is-prop-type-prop-standard-2-Element-Decidable-Subtype :
    (z : X)  is-prop (type-prop-standard-2-Element-Decidable-Subtype z)
  is-prop-type-prop-standard-2-Element-Decidable-Subtype =
    is-prop-type-prop-standard-2-Element-Subtype
      ( pair X (is-set-has-decidable-equality d))
      ( np)

  is-decidable-type-prop-standard-2-Element-Decidable-Subtype :
    (z : X)  is-decidable (type-prop-standard-2-Element-Decidable-Subtype z)
  is-decidable-type-prop-standard-2-Element-Decidable-Subtype z =
    is-decidable-coprod (d x z) (d y z)

  subtype-standard-2-Element-Decidable-Subtype : subtype l X
  subtype-standard-2-Element-Decidable-Subtype =
    subtype-standard-2-Element-Subtype
      ( pair X (is-set-has-decidable-equality d))
      ( np)

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

  type-standard-2-Element-Decidable-Subtype : UU l
  type-standard-2-Element-Decidable-Subtype =
    type-standard-2-Element-Subtype
      ( pair X (is-set-has-decidable-equality d))
      ( np)

  equiv-type-standard-2-Element-Decidable-Subtype :
    Fin 2  type-standard-2-Element-Decidable-Subtype
  equiv-type-standard-2-Element-Decidable-Subtype =
    equiv-type-standard-2-Element-Subtype
      ( pair X (is-set-has-decidable-equality d))
      ( np)

  has-two-elements-type-standard-2-Element-Decidable-Subtype :
    has-two-elements type-standard-2-Element-Decidable-Subtype
  has-two-elements-type-standard-2-Element-Decidable-Subtype =
    has-two-elements-type-standard-2-Element-Subtype
      ( pair X (is-set-has-decidable-equality d))
      ( np)

  2-element-type-standard-2-Element-Decidable-Subtype : 2-Element-Type l
  pr1 2-element-type-standard-2-Element-Decidable-Subtype =
    type-standard-2-Element-Decidable-Subtype
  pr2 2-element-type-standard-2-Element-Decidable-Subtype =
    has-two-elements-type-standard-2-Element-Decidable-Subtype

  standard-2-Element-Decidable-Subtype : 2-Element-Decidable-Subtype l X
  pr1 standard-2-Element-Decidable-Subtype =
    decidable-subtype-standard-2-Element-Decidable-Subtype
  pr2 standard-2-Element-Decidable-Subtype =
    has-two-elements-type-standard-2-Element-Decidable-Subtype

module _
  {l : Level} {X : UU l} (d : has-decidable-equality X) {x y : X}
  (np : ¬ (Id x y))
  where

  is-commutative-standard-2-Element-Decidable-Subtype :
    Id
      ( standard-2-Element-Decidable-Subtype d np)
      ( standard-2-Element-Decidable-Subtype d  p  np (inv p)))
  is-commutative-standard-2-Element-Decidable-Subtype =
    eq-pair-Σ
      ( eq-htpy
         z 
          eq-pair-Σ
            ( eq-equiv
              ( (Id x z) + (Id y z))
              ( (Id y z) + (Id x z))
              ( pair
                ( map-commutative-coprod (Id x z) (Id y z))
                ( is-equiv-map-commutative-coprod (Id x z) (Id y z))))
            ( eq-pair-Σ
              ( eq-is-prop
                ( is-prop-is-prop
                  ( type-Decidable-Prop
                    ( pr1
                      ( standard-2-Element-Decidable-Subtype d
                        ( λ p  np (inv p)))
                      ( z)))))
              ( eq-is-prop
                ( is-prop-is-decidable
                  ( is-prop-type-Decidable-Prop
                    ( pr1
                      ( standard-2-Element-Decidable-Subtype d
                        ( λ p  np (inv p)))
                      ( z))))))))
      ( eq-is-prop is-prop-type-trunc-Prop)

module _
  {l : Level} {X : UU l} (d : has-decidable-equality X) {x y z w : X}
  (np : ¬ (Id x y)) (nq : ¬ (Id z w)) (r : Id x z) (s : Id y w)
  where

  eq-equal-elements-standard-2-Element-Decidable-Subtype :
    Id
      ( standard-2-Element-Decidable-Subtype d np)
      ( standard-2-Element-Decidable-Subtype d nq)
  eq-equal-elements-standard-2-Element-Decidable-Subtype =
    eq-pair-Σ
      ( eq-htpy
        ( λ v 
          eq-pair-Σ
            ( eq-equiv
              ( (Id x v) + (Id y v))
              ( (Id z v) + (Id w v))
              ( equiv-coprod
                ( equiv-concat (inv r) v)
                ( equiv-concat (inv s) v)))
            ( eq-pair-Σ
              ( eq-is-prop
                ( is-prop-is-prop
                  ( type-Decidable-Prop
                    ( pr1
                      ( standard-2-Element-Decidable-Subtype d nq)
                      ( v)))))
              ( eq-is-prop
                ( is-prop-is-decidable
                  ( is-prop-type-Decidable-Prop
                    ( pr1
                      ( standard-2-Element-Decidable-Subtype d nq)
                      ( v))))))))
      ( eq-is-prop is-prop-type-trunc-Prop)

Swapping the elements in a 2-element subtype

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

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

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

  compute-swap-2-Element-Decidable-Subtype :
    (x y : type-2-Element-Decidable-Subtype P)  ¬ (Id x y) 
    Id (map-swap-2-Element-Decidable-Subtype x) y
  compute-swap-2-Element-Decidable-Subtype =
    compute-swap-2-Element-Type (2-element-type-2-Element-Decidable-Subtype P)

module _
  {l1 l2 : Level} (n : ) (X : UU-Fin l1 n)
  where

  is-finite-2-Element-Decidable-Subtype :
    is-finite (2-Element-Decidable-Subtype l2 (type-UU-Fin n X))
  is-finite-2-Element-Decidable-Subtype =
    is-finite-type-decidable-subtype
       P 
        pair
          ( has-cardinality 2
            ( Σ (type-UU-Fin n X) (type-Decidable-Prop  P)))
          ( pair
            ( is-prop-type-trunc-Prop)
            ( is-decidable-equiv
              ( equiv-has-cardinality-id-number-of-elements-is-finite
                ( Σ (type-UU-Fin n X) (type-Decidable-Prop  P))
                ( is-finite-type-decidable-subtype P
                  ( is-finite-type-UU-Fin n X))
                ( 2))
              ( has-decidable-equality-ℕ
                ( number-of-elements-is-finite
                  ( is-finite-type-decidable-subtype P
                    ( is-finite-type-UU-Fin n X)))
                ( 2)))))
      ( is-finite-Π
        ( is-finite-type-UU-Fin n X)
        ( λ x 
          is-finite-equiv
            ( inv-equiv equiv-bool-Decidable-Prop ∘e equiv-bool-Fin-two-ℕ)
            ( is-finite-Fin 2)))

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

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

preserves-comp-precomp-equiv-2-Element-Decidable-Subtype :
  { l1 l2 l3 l4 : Level} {X : UU l1} {Y : UU l2} {Z : UU l3} (e : X  Y) 
  ( f : Y  Z) 
  Id
    ( precomp-equiv-2-Element-Decidable-Subtype {l3 = l4} (f ∘e e))
    ( ( precomp-equiv-2-Element-Decidable-Subtype e) 
      ( precomp-equiv-2-Element-Decidable-Subtype f))
preserves-comp-precomp-equiv-2-Element-Decidable-Subtype e f =
  eq-htpy
    ( λ (pair P H) 
      eq-pair-Σ
        ( refl)
        ( eq-is-prop is-prop-type-trunc-Prop))

Properties

Any 2-element decidable subtype of a standard finite type is a standard 2-element decidable subtype

module _
  {l : Level} {n : } (P : 2-Element-Decidable-Subtype l (Fin n))
  where

  element-subtype-2-element-decidable-subtype-Fin :
    type-2-Element-Decidable-Subtype P
  element-subtype-2-element-decidable-subtype-Fin =
    ε-operator-decidable-subtype-Fin n
      ( decidable-subtype-2-Element-Decidable-Subtype P)
      ( is-inhabited-type-2-Element-Decidable-Subtype P)

  element-2-element-decidable-subtype-Fin : Fin n
  element-2-element-decidable-subtype-Fin =
    pr1 element-subtype-2-element-decidable-subtype-Fin

  in-subtype-element-2-element-decidable-subtype-Fin :
    is-in-2-Element-Decidable-Subtype P
      element-2-element-decidable-subtype-Fin
  in-subtype-element-2-element-decidable-subtype-Fin =
    pr2 element-subtype-2-element-decidable-subtype-Fin

  other-element-subtype-2-element-decidable-subtype-Fin :
    type-2-Element-Decidable-Subtype P
  other-element-subtype-2-element-decidable-subtype-Fin =
    map-swap-2-Element-Type
      ( 2-element-type-2-Element-Decidable-Subtype P)
      ( element-subtype-2-element-decidable-subtype-Fin)

  other-element-2-element-decidable-subtype-Fin : Fin n
  other-element-2-element-decidable-subtype-Fin =
    pr1 other-element-subtype-2-element-decidable-subtype-Fin

  in-subtype-other-element-2-element-decidable-subtype-Fin :
    is-in-2-Element-Decidable-Subtype P
      other-element-2-element-decidable-subtype-Fin
  in-subtype-other-element-2-element-decidable-subtype-Fin =
    pr2 other-element-subtype-2-element-decidable-subtype-Fin

  abstract
    unequal-elements-2-element-decidable-subtype-Fin :
      ¬ ( Id
          ( element-2-element-decidable-subtype-Fin)
          ( other-element-2-element-decidable-subtype-Fin))
    unequal-elements-2-element-decidable-subtype-Fin p =
      has-no-fixed-points-swap-2-Element-Type
        ( 2-element-type-2-Element-Decidable-Subtype P)
        { element-subtype-2-element-decidable-subtype-Fin}
        ( eq-type-subtype
          ( subtype-2-Element-Decidable-Subtype P)
          ( inv p))

Types of decidable subtypes of any universe level are equivalent

module _
  {l1 : Level} (X : UU l1)
  where

  equiv-universes-2-Element-Decidable-Subtype :
    (l l' : Level) 
    2-Element-Decidable-Subtype l X  2-Element-Decidable-Subtype l' X
  equiv-universes-2-Element-Decidable-Subtype l l' =
    equiv-subtype-equiv
      ( equiv-universes-decidable-subtype X l l')
      ( λ P 
        pair
          ( has-two-elements (type-decidable-subtype P))
          ( is-prop-type-trunc-Prop))
      ( λ P 
        pair
          ( has-two-elements (type-decidable-subtype P))
          ( is-prop-type-trunc-Prop))
      ( λ S 
        pair
          ( λ h 
            map-trunc-Prop
              ( λ h' 
                equiv-Σ
                  ( λ x 
                    type-Decidable-Prop
                      ( map-equiv
                        ( equiv-universes-decidable-subtype X l l')
                        ( S)
                        ( x)))
                  ( id-equiv)
                  ( λ x 
                    equiv-iff'
                      ( prop-Decidable-Prop (S x))
                      ( prop-Decidable-Prop
                        ( map-equiv
                          ( equiv-universes-decidable-subtype X l l')
                          ( S)
                          ( x)))
                      ( iff-universes-decidable-subtype X l l' S x)) ∘e
                  ( h'))
              ( h))
          ( λ h 
            map-trunc-Prop
              ( λ h' 
                equiv-Σ
                  ( λ x  type-Decidable-Prop (S x))
                  ( id-equiv)
                  ( λ x 
                    inv-equiv
                      ( equiv-iff'
                        ( prop-Decidable-Prop (S x))
                        ( prop-Decidable-Prop
                          ( map-equiv
                            ( equiv-universes-decidable-subtype X l l')
                            ( S)
                            ( x)))
                        ( iff-universes-decidable-subtype X l l' S x))) ∘e
                  ( h'))
              ( h)))