This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.
2-element types
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!} -}