2-element types

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

Created on 2022-02-16.
Last modified on 2024-04-11.

module univalent-combinatorics.2-element-types where
Imports
open import elementary-number-theory.equality-natural-numbers
open import elementary-number-theory.modular-arithmetic-standard-finite-types

open import foundation.action-on-identifications-functions
open import foundation.automorphisms
open import foundation.connected-components-universes
open import foundation.contractible-maps
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.double-negation
open import foundation.empty-types
open import foundation.equivalence-extensionality
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.functoriality-coproduct-types
open import foundation.functoriality-dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.identity-systems
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.involutions
open import foundation.mere-equivalences
open import foundation.negated-equality
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.raising-universe-levels
open import foundation.sets
open import foundation.subuniverses
open import foundation.torsorial-type-families
open import foundation.transport-along-identifications
open import foundation.type-arithmetic-coproduct-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.type-arithmetic-empty-type
open import foundation.type-arithmetic-unit-type
open import foundation.unit-type
open import foundation.universal-property-identity-systems
open import foundation.universe-levels

open import univalent-combinatorics.equality-standard-finite-types
open import univalent-combinatorics.equivalences
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.standard-finite-types

Idea

2-element types are types that are merely equivalent to the standard 2-element type Fin 2.

Definition

The condition that a type has two elements

has-two-elements-Prop : {l : Level}  UU l  Prop l
has-two-elements-Prop X = has-cardinality-Prop 2 X

has-two-elements : {l : Level}  UU l  UU l
has-two-elements X = type-Prop (has-two-elements-Prop X)

is-prop-has-two-elements : {l : Level} {X : UU l}  is-prop (has-two-elements X)
is-prop-has-two-elements {l} {X} = is-prop-type-Prop (has-two-elements-Prop X)

The type of all 2-element types of universe level l

2-Element-Type : (l : Level)  UU (lsuc l)
2-Element-Type l = UU-Fin l 2

type-2-Element-Type : {l : Level}  2-Element-Type l  UU l
type-2-Element-Type = pr1

has-two-elements-type-2-Element-Type :
  {l : Level} (X : 2-Element-Type l)  has-two-elements (type-2-Element-Type X)
has-two-elements-type-2-Element-Type = pr2

is-finite-type-2-Element-Type :
  {l : Level} (X : 2-Element-Type l)  is-finite (type-2-Element-Type X)
is-finite-type-2-Element-Type X =
  is-finite-has-cardinality 2 (has-two-elements-type-2-Element-Type X)

finite-type-2-Element-Type : {l : Level}  2-Element-Type l  𝔽 l
pr1 (finite-type-2-Element-Type X) = type-2-Element-Type X
pr2 (finite-type-2-Element-Type X) = is-finite-type-2-Element-Type X

standard-2-Element-Type : (l : Level)  2-Element-Type l
standard-2-Element-Type l = Fin-UU-Fin l 2

type-standard-2-Element-Type : (l : Level)  UU l
type-standard-2-Element-Type l = type-2-Element-Type (standard-2-Element-Type l)

zero-standard-2-Element-Type :
  {l : Level}  type-standard-2-Element-Type l
zero-standard-2-Element-Type = map-raise (zero-Fin 1)

one-standard-2-Element-Type :
  {l : Level}  type-standard-2-Element-Type l
one-standard-2-Element-Type = map-raise (one-Fin 1)

Properties

The condition of having two elements is closed under equivalences

module _
  {l1 l2 : Level} {X : UU l1} {Y : UU l2}
  where

  has-two-elements-equiv : X  Y  has-two-elements X  has-two-elements Y
  has-two-elements-equiv e H =
    transitive-mere-equiv (Fin 2) X Y (unit-trunc-Prop e) H

  has-two-elements-equiv' : X  Y  has-two-elements Y  has-two-elements X
  has-two-elements-equiv' e H =
    transitive-mere-equiv (Fin 2) Y X (unit-trunc-Prop (inv-equiv e)) H

Any 2-element type is inhabited

is-inhabited-2-Element-Type :
  {l : Level} (X : 2-Element-Type l)  type-trunc-Prop (type-2-Element-Type X)
is-inhabited-2-Element-Type X =
  apply-universal-property-trunc-Prop
    ( has-two-elements-type-2-Element-Type X)
    ( trunc-Prop (type-2-Element-Type X))
    ( λ e  unit-trunc-Prop (map-equiv e (zero-Fin 1)))

Any 2-element type is a set

is-set-has-two-elements :
  {l : Level} {X : UU l}  has-two-elements X  is-set X
is-set-has-two-elements H = is-set-has-cardinality 2 H

is-set-type-2-Element-Type :
  {l : Level} (X : 2-Element-Type l)  is-set (type-2-Element-Type X)
is-set-type-2-Element-Type X =
  is-set-has-cardinality 2 (has-two-elements-type-2-Element-Type X)

set-2-Element-Type :
  {l : Level}  2-Element-Type l  Set l
pr1 (set-2-Element-Type X) = type-2-Element-Type X
pr2 (set-2-Element-Type X) = is-set-type-2-Element-Type X

Characterizing identifications between general 2-element types

equiv-2-Element-Type :
  {l1 l2 : Level}  2-Element-Type l1  2-Element-Type l2  UU (l1  l2)
equiv-2-Element-Type X Y = equiv-UU-Fin 2 X Y

id-equiv-2-Element-Type :
  {l1 : Level} (X : 2-Element-Type l1)  equiv-2-Element-Type X X
id-equiv-2-Element-Type X = id-equiv

equiv-eq-2-Element-Type :
  {l1 : Level} (X Y : 2-Element-Type l1)  X  Y  equiv-2-Element-Type X Y
equiv-eq-2-Element-Type X Y = equiv-eq-component-UU-Level

abstract
  is-torsorial-equiv-2-Element-Type :
    {l1 : Level} (X : 2-Element-Type l1) 
    is-torsorial  (Y : 2-Element-Type l1)  equiv-2-Element-Type X Y)
  is-torsorial-equiv-2-Element-Type X =
    is-torsorial-equiv-component-UU-Level X

abstract
  is-equiv-equiv-eq-2-Element-Type :
    {l1 : Level} (X Y : 2-Element-Type l1) 
    is-equiv (equiv-eq-2-Element-Type X Y)
  is-equiv-equiv-eq-2-Element-Type = is-equiv-equiv-eq-component-UU-Level

eq-equiv-2-Element-Type :
  {l1 : Level} (X Y : 2-Element-Type l1)  equiv-2-Element-Type X Y  X  Y
eq-equiv-2-Element-Type X Y =
  map-inv-is-equiv (is-equiv-equiv-eq-2-Element-Type X Y)

extensionality-2-Element-Type :
  {l1 : Level} (X Y : 2-Element-Type l1)  (X  Y)  equiv-2-Element-Type X Y
pr1 (extensionality-2-Element-Type X Y) = equiv-eq-2-Element-Type X Y
pr2 (extensionality-2-Element-Type X Y) = is-equiv-equiv-eq-2-Element-Type X Y

Characterization the identifications of Fin 2 with a 2-element type X

Evaluating an equivalence and an automorphism at 0 : Fin 2

ev-zero-equiv-Fin-two-ℕ :
  {l1 : Level} {X : UU l1}  (Fin 2  X)  X
ev-zero-equiv-Fin-two-ℕ e = map-equiv e (zero-Fin 1)

ev-zero-aut-Fin-two-ℕ : (Fin 2  Fin 2)  Fin 2
ev-zero-aut-Fin-two-ℕ = ev-zero-equiv-Fin-two-ℕ

Evaluating an automorphism at 0 : Fin 2 is an equivalence

aut-point-Fin-two-ℕ :
  Fin 2  (Fin 2  Fin 2)
aut-point-Fin-two-ℕ (inl (inr star)) = id-equiv
aut-point-Fin-two-ℕ (inr star) = equiv-succ-Fin 2

abstract
  is-section-aut-point-Fin-two-ℕ :
    (ev-zero-aut-Fin-two-ℕ  aut-point-Fin-two-ℕ) ~ id
  is-section-aut-point-Fin-two-ℕ (inl (inr star)) = refl
  is-section-aut-point-Fin-two-ℕ (inr star) = refl

  is-retraction-aut-point-Fin-two-ℕ' :
    (e : Fin 2  Fin 2) (x y : Fin 2) 
    map-equiv e (zero-Fin 1)  x 
    map-equiv e (one-Fin 1)  y  htpy-equiv (aut-point-Fin-two-ℕ x) e
  is-retraction-aut-point-Fin-two-ℕ' e
    (inl (inr star)) (inl (inr star)) p q (inl (inr star)) = inv p
  is-retraction-aut-point-Fin-two-ℕ' e
    (inl (inr star)) (inl (inr star)) p q (inr star) =
    ex-falso (Eq-Fin-eq 2 (is-injective-equiv e (p  inv q)))
  is-retraction-aut-point-Fin-two-ℕ' e
    (inl (inr star)) (inr star) p q (inl (inr star)) = inv p
  is-retraction-aut-point-Fin-two-ℕ' e
    (inl (inr star)) (inr star) p q (inr star) = inv q
  is-retraction-aut-point-Fin-two-ℕ' e
    (inr star) (inl (inr star)) p q (inl (inr star)) = inv p
  is-retraction-aut-point-Fin-two-ℕ' e
    (inr star) (inl (inr star)) p q (inr star) = inv q
  is-retraction-aut-point-Fin-two-ℕ' e
    (inr star) (inr star) p q (inl (inr star)) =
    ex-falso (Eq-Fin-eq 2 (is-injective-equiv e (p  inv q)))
  is-retraction-aut-point-Fin-two-ℕ' e
    (inr star) (inr star) p q (inr star) =
    ex-falso (Eq-Fin-eq 2 (is-injective-equiv e (p  inv q)))

  is-retraction-aut-point-Fin-two-ℕ :
    (aut-point-Fin-two-ℕ  ev-zero-aut-Fin-two-ℕ) ~ id
  is-retraction-aut-point-Fin-two-ℕ e =
    eq-htpy-equiv
      ( is-retraction-aut-point-Fin-two-ℕ' e
        ( map-equiv e (zero-Fin 1))
        ( map-equiv e (one-Fin 1))
        ( refl)
        ( refl))

abstract
  is-equiv-ev-zero-aut-Fin-two-ℕ : is-equiv ev-zero-aut-Fin-two-ℕ
  is-equiv-ev-zero-aut-Fin-two-ℕ =
    is-equiv-is-invertible
      aut-point-Fin-two-ℕ
      is-section-aut-point-Fin-two-ℕ
      is-retraction-aut-point-Fin-two-ℕ

equiv-ev-zero-aut-Fin-two-ℕ : (Fin 2  Fin 2)  Fin 2
pr1 equiv-ev-zero-aut-Fin-two-ℕ = ev-zero-aut-Fin-two-ℕ
pr2 equiv-ev-zero-aut-Fin-two-ℕ = is-equiv-ev-zero-aut-Fin-two-ℕ

If X is a 2-element type, then evaluating an equivalence Fin 2 ≃ X at 0 is an equivalence

module _
  {l1 : Level} (X : 2-Element-Type l1)
  where

  abstract
    is-equiv-ev-zero-equiv-Fin-two-ℕ :
      is-equiv (ev-zero-equiv-Fin-two-ℕ {l1} {type-2-Element-Type X})
    is-equiv-ev-zero-equiv-Fin-two-ℕ =
      apply-universal-property-trunc-Prop
        ( has-two-elements-type-2-Element-Type X)
        ( is-equiv-Prop (ev-zero-equiv-Fin-two-ℕ))
        ( λ α 
          is-equiv-left-factor
            ( ev-zero-equiv-Fin-two-ℕ)
            ( map-equiv (equiv-postcomp-equiv α (Fin 2)))
            ( is-equiv-comp
              ( map-equiv α)
              ( ev-zero-equiv-Fin-two-ℕ)
              ( is-equiv-ev-zero-aut-Fin-two-ℕ)
              ( is-equiv-map-equiv α))
            ( is-equiv-postcomp-equiv-equiv α))

  equiv-ev-zero-equiv-Fin-two-ℕ :
    (Fin 2  type-2-Element-Type X)  type-2-Element-Type X
  pr1 equiv-ev-zero-equiv-Fin-two-ℕ = ev-zero-equiv-Fin-two-ℕ
  pr2 equiv-ev-zero-equiv-Fin-two-ℕ = is-equiv-ev-zero-equiv-Fin-two-ℕ

  equiv-point-2-Element-Type :
    type-2-Element-Type X  Fin 2  type-2-Element-Type X
  equiv-point-2-Element-Type =
    map-inv-equiv equiv-ev-zero-equiv-Fin-two-ℕ

  map-equiv-point-2-Element-Type :
    type-2-Element-Type X  Fin 2  type-2-Element-Type X
  map-equiv-point-2-Element-Type x = map-equiv (equiv-point-2-Element-Type x)

  map-inv-equiv-point-2-Element-Type :
    type-2-Element-Type X  type-2-Element-Type X  Fin 2
  map-inv-equiv-point-2-Element-Type x =
    map-inv-equiv (equiv-point-2-Element-Type x)

  is-section-map-inv-equiv-point-2-Element-Type :
    (x : type-2-Element-Type X) 
    (map-equiv-point-2-Element-Type x  map-inv-equiv-point-2-Element-Type x) ~
    id
  is-section-map-inv-equiv-point-2-Element-Type x =
    is-section-map-inv-equiv (equiv-point-2-Element-Type x)

  is-retraction-map-inv-equiv-point-2-Element-Type :
    (x : type-2-Element-Type X) 
    (map-inv-equiv-point-2-Element-Type x  map-equiv-point-2-Element-Type x) ~
    id
  is-retraction-map-inv-equiv-point-2-Element-Type x =
    is-retraction-map-inv-equiv (equiv-point-2-Element-Type x)

  compute-map-equiv-point-2-Element-Type :
    (x : type-2-Element-Type X) 
    map-equiv-point-2-Element-Type x (zero-Fin 1)  x
  compute-map-equiv-point-2-Element-Type =
    is-section-map-inv-equiv equiv-ev-zero-equiv-Fin-two-ℕ

  is-unique-equiv-point-2-Element-Type :
    (e : Fin 2  type-2-Element-Type X) 
    htpy-equiv (equiv-point-2-Element-Type (map-equiv e (zero-Fin 1))) e
  is-unique-equiv-point-2-Element-Type e =
    htpy-eq-equiv (is-retraction-map-inv-equiv equiv-ev-zero-equiv-Fin-two-ℕ e)

The type of pointed 2-element types of any universe level is contractible

Pointed-2-Element-Type : (l : Level)  UU (lsuc l)
Pointed-2-Element-Type l = Σ (2-Element-Type l) type-2-Element-Type

abstract
  is-contr-pointed-2-Element-Type :
    {l : Level}  is-contr (Pointed-2-Element-Type l)
  is-contr-pointed-2-Element-Type {l} =
    is-contr-equiv'
      ( Σ ( 2-Element-Type l)
          ( equiv-2-Element-Type (standard-2-Element-Type l)))
      ( equiv-tot
        ( λ X 
          ( equiv-ev-zero-equiv-Fin-two-ℕ X) ∘e
          ( equiv-precomp-equiv (compute-raise-Fin l 2) (pr1 X))))
      ( is-torsorial-equiv-subuniverse
        ( has-cardinality-Prop 2)
        ( standard-2-Element-Type l))

Completing the characterization of the identity type of the type of 2-element types of arbitrary universe level

point-eq-2-Element-Type :
  {l : Level} {X : 2-Element-Type l} 
  standard-2-Element-Type l  X  type-2-Element-Type X
point-eq-2-Element-Type refl = map-raise (zero-Fin 1)

abstract
  is-equiv-point-eq-2-Element-Type :
    {l : Level} (X : 2-Element-Type l) 
    is-equiv (point-eq-2-Element-Type {l} {X})
  is-equiv-point-eq-2-Element-Type {l} =
    fundamental-theorem-id
      ( is-contr-pointed-2-Element-Type)
      ( λ X  point-eq-2-Element-Type {l} {X})

equiv-point-eq-2-Element-Type :
  {l : Level} {X : 2-Element-Type l} 
  (standard-2-Element-Type l  X)  type-2-Element-Type X
pr1 (equiv-point-eq-2-Element-Type {l} {X}) =
  point-eq-2-Element-Type
pr2 (equiv-point-eq-2-Element-Type {l} {X}) =
  is-equiv-point-eq-2-Element-Type X

eq-point-2-Element-Type :
  {l : Level} {X : 2-Element-Type l} 
  type-2-Element-Type X  standard-2-Element-Type l  X
eq-point-2-Element-Type =
  map-inv-equiv equiv-point-eq-2-Element-Type

is-identity-system-type-2-Element-Type :
  {l1 : Level} (X : 2-Element-Type l1) (x : type-2-Element-Type X) 
  is-identity-system (type-2-Element-Type {l1}) X x
is-identity-system-type-2-Element-Type X x =
  is-identity-system-is-torsorial X x (is-contr-pointed-2-Element-Type)

dependent-universal-property-identity-system-type-2-Element-Type :
  {l1 : Level} (X : 2-Element-Type l1) (x : type-2-Element-Type X) 
  dependent-universal-property-identity-system
    ( type-2-Element-Type {l1})
    { a = X}
    ( x)
dependent-universal-property-identity-system-type-2-Element-Type X x =
  dependent-universal-property-identity-system-is-torsorial x
    ( is-contr-pointed-2-Element-Type)

For any 2-element type X, the type of automorphisms on X is a 2-element type

module _
  {l : Level} (X : 2-Element-Type l)
  where

  has-two-elements-Aut-2-Element-Type :
    has-two-elements (Aut (type-2-Element-Type X))
  has-two-elements-Aut-2-Element-Type =
    apply-universal-property-trunc-Prop
      ( has-two-elements-type-2-Element-Type X)
      ( has-two-elements-Prop (Aut (type-2-Element-Type X)))
      ( λ e 
        has-two-elements-equiv
          ( ( equiv-postcomp-equiv e (type-2-Element-Type X)) ∘e
            ( equiv-precomp-equiv (inv-equiv e) (Fin 2)))
          ( unit-trunc-Prop (inv-equiv equiv-ev-zero-aut-Fin-two-ℕ)))

  Aut-2-Element-Type : 2-Element-Type l
  pr1 Aut-2-Element-Type = Aut (type-2-Element-Type X)
  pr2 Aut-2-Element-Type = has-two-elements-Aut-2-Element-Type

Evaluating homotopies of equivalences e, e' : Fin 2 ≃ X at 0 is an equivalence

module _
  {l1 : Level} (X : 2-Element-Type l1)
  where

  ev-zero-htpy-equiv-Fin-two-ℕ :
    (e e' : Fin 2  type-2-Element-Type X)  htpy-equiv e e' 
    map-equiv e (zero-Fin 1)  map-equiv e' (zero-Fin 1)
  ev-zero-htpy-equiv-Fin-two-ℕ e e' H = H (zero-Fin 1)

  equiv-ev-zero-htpy-equiv-Fin-two-ℕ' :
    (e e' : Fin 2  type-2-Element-Type X) 
    htpy-equiv e e'  (map-equiv e (zero-Fin 1)  map-equiv e' (zero-Fin 1))
  equiv-ev-zero-htpy-equiv-Fin-two-ℕ' e e' =
    ( equiv-ap (equiv-ev-zero-equiv-Fin-two-ℕ X) e e') ∘e
    ( inv-equiv (extensionality-equiv e e'))

  abstract
    is-equiv-ev-zero-htpy-equiv-Fin-two-ℕ :
      (e e' : Fin 2  type-2-Element-Type X) 
      is-equiv (ev-zero-htpy-equiv-Fin-two-ℕ e e')
    is-equiv-ev-zero-htpy-equiv-Fin-two-ℕ e =
      is-fiberwise-equiv-is-equiv-tot
        ( is-equiv-is-contr
          ( tot (ev-zero-htpy-equiv-Fin-two-ℕ e))
          ( is-torsorial-htpy-equiv e)
          ( is-contr-equiv
            ( fiber (ev-zero-equiv-Fin-two-ℕ) (map-equiv e (zero-Fin 1)))
            ( equiv-tot
              ( λ e' 
                equiv-inv
                  ( map-equiv e (zero-Fin 1))
                  ( map-equiv e' (zero-Fin 1))))
            ( is-contr-map-is-equiv
              ( is-equiv-ev-zero-equiv-Fin-two-ℕ X)
              ( map-equiv e (zero-Fin 1)))))

  equiv-ev-zero-htpy-equiv-Fin-two-ℕ :
    (e e' : Fin 2  type-2-Element-Type X) 
    htpy-equiv e e'  (map-equiv e (zero-Fin 1)  map-equiv e' (zero-Fin 1))
  pr1 (equiv-ev-zero-htpy-equiv-Fin-two-ℕ e e') =
    ev-zero-htpy-equiv-Fin-two-ℕ e e'
  pr2 (equiv-ev-zero-htpy-equiv-Fin-two-ℕ e e') =
    is-equiv-ev-zero-htpy-equiv-Fin-two-ℕ e e'

The canonical type family on the type of 2-element types has no section

abstract
  no-section-type-2-Element-Type :
    {l : Level}  ¬ ((X : 2-Element-Type l)  type-2-Element-Type X)
  no-section-type-2-Element-Type {l} f =
    is-not-contractible-Fin 2
      ( Eq-eq-ℕ)
      ( is-contr-equiv
        ( standard-2-Element-Type l  standard-2-Element-Type l)
        ( ( inv-equiv equiv-point-eq-2-Element-Type) ∘e
          ( compute-raise-Fin l 2))
        ( is-prop-is-contr
          ( pair
            ( standard-2-Element-Type l)
            ( λ X  eq-point-2-Element-Type (f X)))
          ( standard-2-Element-Type l)
          ( standard-2-Element-Type l)))

There is no decidability procedure that proves that an arbitrary 2-element type is decidable

abstract
  is-not-decidable-type-2-Element-Type :
    {l : Level} 
    ¬ ((X : 2-Element-Type l)  is-decidable (type-2-Element-Type X))
  is-not-decidable-type-2-Element-Type {l} d =
    no-section-type-2-Element-Type
      ( λ X 
        map-right-unit-law-coproduct-is-empty
          ( pr1 X)
          ( ¬ (pr1 X))
          ( apply-universal-property-trunc-Prop
            ( pr2 X)
            ( double-negation-type-Prop (pr1 X))
            ( λ e  intro-double-negation {l} (map-equiv e (zero-Fin 1))))
          ( d X))

Any automorphism on Fin 2 is an involution

cases-is-involution-aut-Fin-two-ℕ :
  (e : Fin 2  Fin 2) (x y z : Fin 2) 
  map-equiv e x  y  map-equiv e y  z 
  map-equiv (e ∘e e) x  x
cases-is-involution-aut-Fin-two-ℕ e (inl (inr star)) (inl (inr star)) z p q =
  ap (map-equiv e) p  p
cases-is-involution-aut-Fin-two-ℕ e
  (inl (inr star)) (inr star) (inl (inr star)) p q =
  ap (map-equiv e) p  q
cases-is-involution-aut-Fin-two-ℕ e (inl (inr star)) (inr star) (inr star) p q =
  ex-falso (neq-inr-inl (is-injective-equiv e (q  inv p)))
cases-is-involution-aut-Fin-two-ℕ e
  (inr star) (inl (inr star)) (inl (inr star)) p q =
  ex-falso (neq-inr-inl (is-injective-equiv e (p  inv q)))
cases-is-involution-aut-Fin-two-ℕ e (inr star) (inl (inr star)) (inr star) p q =
  ap (map-equiv e) p  q
cases-is-involution-aut-Fin-two-ℕ e (inr star) (inr star) z p q =
  ap (map-equiv e) p  p

is-involution-aut-Fin-two-ℕ : (e : Fin 2  Fin 2)  is-involution-aut e
is-involution-aut-Fin-two-ℕ e x =
  cases-is-involution-aut-Fin-two-ℕ e x
    ( map-equiv e x)
    ( map-equiv (e ∘e e) x)
    ( refl)
    ( refl)

module _
  {l : Level} (X : 2-Element-Type l)
  where

  is-involution-aut-2-element-type :
    (e : equiv-2-Element-Type X X)  is-involution-aut e
  is-involution-aut-2-element-type e x =
    apply-universal-property-trunc-Prop
      ( has-two-elements-type-2-Element-Type X)
      ( Id-Prop (set-2-Element-Type X) (map-equiv (e ∘e e) x) x)
      ( λ h 
        ( ap (map-equiv (e ∘e e)) (inv (is-section-map-inv-equiv h x))) 
        ( ( ap (map-equiv e) (inv (is-section-map-inv-equiv h _))) 
          ( inv (is-section-map-inv-equiv h _) 
            ( ( ap
                ( map-equiv h)
                ( is-involution-aut-Fin-two-ℕ (inv-equiv h ∘e (e ∘e h)) _)) 
              ( is-section-map-inv-equiv h x)))))

The swapping equivalence on arbitrary 2-element types

module _
  {l : Level} (X : 2-Element-Type l)
  where

  swap-2-Element-Type : equiv-2-Element-Type X X
  swap-2-Element-Type =
    ( equiv-ev-zero-equiv-Fin-two-ℕ X) ∘e
    ( ( equiv-precomp-equiv (equiv-succ-Fin 2) (type-2-Element-Type X)) ∘e
      ( inv-equiv (equiv-ev-zero-equiv-Fin-two-ℕ X)))

  map-swap-2-Element-Type : type-2-Element-Type X  type-2-Element-Type X
  map-swap-2-Element-Type = map-equiv swap-2-Element-Type

  compute-swap-2-Element-Type' :
    (x y : type-2-Element-Type X)  x  y  (z : Fin 2) 
    map-inv-equiv-point-2-Element-Type X x y  z 
    map-swap-2-Element-Type x  y
  compute-swap-2-Element-Type' x y f (inl (inr star)) q =
    ex-falso
      ( f
        ( (inv (compute-map-equiv-point-2-Element-Type X x)) 
          ( ( ap (map-equiv-point-2-Element-Type X x) (inv q)) 
            ( is-section-map-inv-equiv-point-2-Element-Type X x y))))
  compute-swap-2-Element-Type' x y p (inr star) q =
    ( ap (map-equiv-point-2-Element-Type X x) (inv q)) 
    ( is-section-map-inv-equiv-point-2-Element-Type X x y)

  compute-swap-2-Element-Type :
    (x y : type-2-Element-Type X)  x  y 
    map-swap-2-Element-Type x  y
  compute-swap-2-Element-Type x y p =
    compute-swap-2-Element-Type' x y p
      ( map-inv-equiv-point-2-Element-Type X x y)
      ( refl)

  compute-map-equiv-point-2-Element-Type' :
    (x : type-2-Element-Type X) 
    map-equiv-point-2-Element-Type X x (one-Fin 1) 
    map-swap-2-Element-Type x
  compute-map-equiv-point-2-Element-Type' x = refl

compute-swap-Fin-two-ℕ :
  map-swap-2-Element-Type (Fin-UU-Fin' 2) ~ succ-Fin 2
compute-swap-Fin-two-ℕ (inl (inr star)) =
  compute-swap-2-Element-Type
    ( Fin-UU-Fin' 2)
    ( zero-Fin 1)
    ( one-Fin 1)
    ( neq-inl-inr)
compute-swap-Fin-two-ℕ (inr star) =
  compute-swap-2-Element-Type
    ( Fin-UU-Fin' 2)
    ( one-Fin 1)
    ( zero-Fin 1)
    ( neq-inr-inl)

The swapping equivalence is not the identity equivalence

module _
  {l : Level} (X : 2-Element-Type l)
  where

  is-not-identity-equiv-precomp-equiv-equiv-succ-Fin :
    equiv-precomp-equiv (equiv-succ-Fin 2) (type-2-Element-Type X)  id-equiv
  is-not-identity-equiv-precomp-equiv-equiv-succ-Fin p' =
    apply-universal-property-trunc-Prop
      ( has-two-elements-type-2-Element-Type X)
      ( empty-Prop)
      ( λ f 
        neq-inr-inl
          ( is-injective-equiv f
            ( htpy-eq-equiv (htpy-eq-equiv p' f) (zero-Fin 1))))

  is-not-identity-swap-2-Element-Type : swap-2-Element-Type X  id-equiv
  is-not-identity-swap-2-Element-Type p =
    is-not-identity-equiv-precomp-equiv-equiv-succ-Fin
      ( ( ( inv (left-unit-law-equiv equiv1)) 
          ( ap  x  x ∘e equiv1) (inv (left-inverse-law-equiv equiv2)))) 
        ( ( inv
            ( right-unit-law-equiv ((inv-equiv equiv2 ∘e equiv2) ∘e equiv1))) 
          ( ( ap
              ( λ x  ((inv-equiv equiv2 ∘e equiv2) ∘e equiv1) ∘e x)
              ( inv (left-inverse-law-equiv equiv2))) 
          ( ( ( eq-equiv-eq-map-equiv refl) 
              ( ap  x  inv-equiv equiv2 ∘e (x ∘e equiv2)) p)) 
            ( ( ap
                ( λ x  inv-equiv equiv2 ∘e x)
                ( left-unit-law-equiv equiv2)) 
              ( left-inverse-law-equiv equiv2))))))
    where
    equiv1 : (Fin 2  type-2-Element-Type X)  (Fin 2  type-2-Element-Type X)
    equiv1 = equiv-precomp-equiv (equiv-succ-Fin 2) (type-2-Element-Type X)
    equiv2 : (Fin 2  type-2-Element-Type X)  type-2-Element-Type X
    equiv2 = equiv-ev-zero-equiv-Fin-two-ℕ X

The swapping equivalence has no fixpoints

module _
  {l : Level} (X : 2-Element-Type l)
  where

  has-no-fixed-points-swap-2-Element-Type :
    {x : type-2-Element-Type X}  map-equiv (swap-2-Element-Type X) x  x
  has-no-fixed-points-swap-2-Element-Type {x} P =
    apply-universal-property-trunc-Prop
      ( has-two-elements-type-2-Element-Type X)
      ( empty-Prop)
      ( λ h 
        is-not-identity-swap-2-Element-Type X
          (eq-htpy-equiv
             y 
              f
                ( inv-equiv h)
                ( y)
                ( map-inv-equiv h x)
                ( map-inv-equiv h y)
                ( map-inv-equiv h (map-equiv (swap-2-Element-Type X) y))
                ( refl)
                ( refl)
                ( refl))))
    where
    f :
      ( h : type-2-Element-Type X  Fin 2)
      ( y : type-2-Element-Type X) 
      ( k1 k2 k3 : Fin 2) 
        map-equiv h x  k1  map-equiv h y  k2 
        map-equiv h (map-equiv (swap-2-Element-Type X) y)  k3 
        map-equiv (swap-2-Element-Type X) y  y
    f h y (inl (inr star)) (inl (inr star)) k3 p q r =
      tr
        ( λ z  map-equiv (swap-2-Element-Type X) z  z)
        ( is-injective-equiv h (p  inv q))
        ( P)
    f h y (inl (inr star)) (inr star) (inl (inr star)) p q r =
      ex-falso
        ( neq-inl-inr
          ( inv p  (ap (map-equiv h) (inv P) 
            ( ap
              ( map-equiv (h ∘e (swap-2-Element-Type X)))
              ( is-injective-equiv h (p  inv r)) 
              ( ( ap
                  ( map-equiv h)
                  ( is-involution-aut-2-element-type X
                    ( swap-2-Element-Type X) y)) 
                ( q))))))
    f h y (inl (inr star)) (inr star) (inr star) p q r =
      ( is-injective-equiv h (r  inv q))
    f h y (inr star) (inl (inr star)) (inl (inr star)) p q r =
      ( is-injective-equiv h (r  inv q))
    f h y (inr star) (inl (inr star)) (inr star) p q r =
      ex-falso
        ( neq-inr-inl
          ( inv p  (ap (map-equiv h) (inv P) 
            ( ap
              ( map-equiv (h ∘e (swap-2-Element-Type X)))
              ( is-injective-equiv h (p  inv r)) 
              ( ( ap
                  ( map-equiv h)
                  ( is-involution-aut-2-element-type X
                    ( swap-2-Element-Type X)
                    ( y))) 
                ( q))))))
    f h y (inr star) (inr star) k3 p q r =
      tr
        ( λ z  map-equiv (swap-2-Element-Type X) z  z)
        ( is-injective-equiv h (p  inv q))
        ( P)

Evaluating an automorphism at 0 : Fin 2 is a group homomorphism

preserves-add-aut-point-Fin-two-ℕ :
  (a b : Fin 2) 
  aut-point-Fin-two-ℕ (add-Fin 2 a b) 
  ( aut-point-Fin-two-ℕ a ∘e aut-point-Fin-two-ℕ b)
preserves-add-aut-point-Fin-two-ℕ (inl (inr star)) (inl (inr star)) =
  eq-equiv-eq-map-equiv refl
preserves-add-aut-point-Fin-two-ℕ (inl (inr star)) (inr star) =
  eq-equiv-eq-map-equiv refl
preserves-add-aut-point-Fin-two-ℕ (inr star) (inl (inr star)) =
  eq-equiv-eq-map-equiv refl
preserves-add-aut-point-Fin-two-ℕ (inr star) (inr star) =
  eq-htpy-equiv  x  inv (is-involution-aut-Fin-two-ℕ (equiv-succ-Fin 2) x))

Any Σ-type over Fin 2 is a coproduct

is-coproduct-Σ-Fin-two-ℕ :
  {l : Level} (P : Fin 2  UU l) 
  Σ (Fin 2) P  (P (zero-Fin 1) + P (one-Fin 1))
is-coproduct-Σ-Fin-two-ℕ P =
  ( equiv-coproduct
    ( left-unit-law-Σ-is-contr is-contr-Fin-one-ℕ (zero-Fin 0))
    ( left-unit-law-Σ (P  inr))) ∘e
  ( right-distributive-Σ-coproduct (Fin 1) unit P)

For any equivalence e : Fin 2 ≃ X, any element of X is either e 0 or it is e 1

module _
  {l : Level} (X : 2-Element-Type l)
  where

  abstract
    is-contr-decide-value-equiv-Fin-two-ℕ :
      (e : Fin 2  type-2-Element-Type X) (x : type-2-Element-Type X) 
      is-contr
        ( ( x  map-equiv e (zero-Fin 1)) +
          ( x  map-equiv e (one-Fin 1)))
    is-contr-decide-value-equiv-Fin-two-ℕ e x =
      is-contr-equiv'
        ( fiber (map-equiv e) x)
        ( ( is-coproduct-Σ-Fin-two-ℕ  y  x  map-equiv e y)) ∘e
          ( equiv-tot  y  equiv-inv (map-equiv e y) x)))
        ( is-contr-map-is-equiv (is-equiv-map-equiv e) x)

  decide-value-equiv-Fin-two-ℕ :
    (e : Fin 2  type-2-Element-Type X) (x : type-2-Element-Type X) 
    (x  map-equiv e (zero-Fin 1)) + (x  map-equiv e (one-Fin 1))
  decide-value-equiv-Fin-two-ℕ e x =
    center (is-contr-decide-value-equiv-Fin-two-ℕ e x)

There can’t be three distinct elements in a 2-element type

module _
  {l : Level} (X : 2-Element-Type l)
  where

  contradiction-3-distinct-element-2-Element-Type :
    (x y z : type-2-Element-Type X) 
    x  y  y  z  x  z  empty
  contradiction-3-distinct-element-2-Element-Type x y z np nq nr =
    apply-universal-property-trunc-Prop
      ( has-two-elements-type-2-Element-Type X)
      ( empty-Prop)
      ( λ e 
        cases-contradiction-3-distinct-element-2-Element-Type
          ( e)
          ( decide-value-equiv-Fin-two-ℕ X e x)
          ( decide-value-equiv-Fin-two-ℕ X e y)
          ( decide-value-equiv-Fin-two-ℕ X e z))
    where
    cases-contradiction-3-distinct-element-2-Element-Type :
      (e : Fin 2  type-2-Element-Type X) 
      (x  map-equiv e (zero-Fin 1)) + (x  map-equiv e (one-Fin 1)) 
      (y  map-equiv e (zero-Fin 1)) + (y  map-equiv e (one-Fin 1)) 
      (z  map-equiv e (zero-Fin 1)) + (z  map-equiv e (one-Fin 1)) 
      empty
    cases-contradiction-3-distinct-element-2-Element-Type e
      (inl refl) (inl refl) c3 = np refl
    cases-contradiction-3-distinct-element-2-Element-Type e
      (inl refl) (inr refl) (inl refl) = nr refl
    cases-contradiction-3-distinct-element-2-Element-Type e
      (inl refl) (inr refl) (inr refl) = nq refl
    cases-contradiction-3-distinct-element-2-Element-Type e
      (inr refl) (inl refl) (inl refl) = nq refl
    cases-contradiction-3-distinct-element-2-Element-Type e
      (inr refl) (inl refl) (inr refl) = nr refl
    cases-contradiction-3-distinct-element-2-Element-Type e
      (inr refl) (inr refl) c3 = np refl

For any map between 2-element types, being an equivalence is decidable

module _
  {l1 l2 : Level} (X : 2-Element-Type l1) (Y : 2-Element-Type l2)
  where

  is-decidable-is-equiv-2-Element-Type :
    (f : type-2-Element-Type X  type-2-Element-Type Y) 
    is-decidable (is-equiv f)
  is-decidable-is-equiv-2-Element-Type f =
    is-decidable-is-equiv-is-finite f
      ( is-finite-type-2-Element-Type X)
      ( is-finite-type-2-Element-Type Y)

A map between 2-element types is an equivalence if and only if its image is the full subtype of the codomain

This remains to be shown. #743

A map between 2-element types is not an equivalence if and only if its image is a singleton subtype of the codomain

This remains to be shown. #743

Any map between 2-element types that is not an equivalence is constant

This remains to be shown. #743

{-
  is-constant-is-not-equiv-2-Element-Type :
    (f : type-2-Element-Type X → type-2-Element-Type Y) →
    ¬ (is-equiv f) →
    Σ (type-2-Element-Type Y) (λ y → f ~ const _ y)
  pr1 (is-constant-is-not-equiv-2-Element-Type f H) = {!!}
  pr2 (is-constant-is-not-equiv-2-Element-Type f H) = {!!}
  -}

Any map between 2-element types is either an equivalence or it is constant

This remains to be shown. #743

Coinhabited 2-element types are equivalent

{-
equiv-iff-2-Element-Type :
  {l1 l2 : Level} (X : 2-Element-Type l1) (Y : 2-Element-Type l2) →
  (type-2-Element-Type X ↔ type-2-Element-Type Y) →
  (equiv-2-Element-Type X Y)
equiv-iff-2-Element-Type X Y (f , g) = {!is-decidable-is-equiv-is-finite!}
-}

Recent changes