Ethane
module organic-chemistry.ethane where
Imports
open import elementary-number-theory.inequality-natural-numbers open import finite-group-theory.tetrahedra-in-3-space open import foundation.contractible-types open import foundation.coproduct-types open import foundation.decidable-propositions open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.empty-types open import foundation.equality-dependent-pair-types open import foundation.identity-types open import foundation.injective-maps open import foundation.propositional-truncations open import foundation.propositions open import foundation.univalence open import foundation.universe-levels open import foundation.unordered-pairs open import graph-theory.finite-graphs open import graph-theory.walks-undirected-graphs open import organic-chemistry.alkanes open import organic-chemistry.hydrocarbons open import univalent-combinatorics.2-element-types open import univalent-combinatorics.counting open import univalent-combinatorics.finite-types open import univalent-combinatorics.standard-finite-types
Idea
Ethane is the unique alkane with two carbons.
Definition
module _ (t : tetrahedron-in-3-space) (v : vertex-tetrahedron-in-3-space t) where vertex-ethane-𝔽 : 𝔽 lzero vertex-ethane-𝔽 = Fin-𝔽 2 vertex-ethane : UU lzero vertex-ethane = type-𝔽 vertex-ethane-𝔽 edge-ethane-Prop : unordered-pair vertex-ethane → Prop lzero edge-ethane-Prop p = prod-Prop ( is-in-unordered-pair-Prop p (zero-Fin 1)) ( is-in-unordered-pair-Prop p (one-Fin 1)) edge-ethane : unordered-pair vertex-ethane → UU lzero edge-ethane p = type-Prop (edge-ethane-Prop p) abstract is-prop-edge-ethane : (p : unordered-pair vertex-ethane) → is-prop (edge-ethane p) is-prop-edge-ethane p = is-prop-type-Prop (edge-ethane-Prop p) standard-edge-ethane-Prop : (c c' : vertex-ethane) → Prop lzero standard-edge-ethane-Prop c c' = edge-ethane-Prop (standard-unordered-pair c c') standard-edge-ethane : (c c' : vertex-ethane) → UU lzero standard-edge-ethane c c' = type-Prop (standard-edge-ethane-Prop c c') abstract is-prop-standard-edge-ethane : (c c' : vertex-ethane) → is-prop (standard-edge-ethane c c') is-prop-standard-edge-ethane c c' = is-prop-type-Prop (standard-edge-ethane-Prop c c') is-decidable-edge-ethane-eq-Fin-two : (p : unordered-pair vertex-ethane) → type-unordered-pair p ＝ Fin 2 → is-decidable (edge-ethane p) is-decidable-edge-ethane-eq-Fin-two p refl with is-zero-or-one-Fin-two-ℕ (element-unordered-pair p (zero-Fin 1)) | is-zero-or-one-Fin-two-ℕ (element-unordered-pair p (one-Fin 1)) ... | inl is-zero | inl is-zero' = inr ( λ P → apply-universal-property-trunc-Prop (pr2 P) empty-Prop ( λ where (inl (inr star) , is-one) → neq-inl-inr (inv is-zero ∙ is-one) (inr star , is-one) → neq-inl-inr (inv is-zero' ∙ is-one))) ... | inl is-zero | inr is-one' = inl ( pair ( unit-trunc-Prop (zero-Fin 1 , is-zero)) ( unit-trunc-Prop (one-Fin 1 , is-one'))) ... | inr is-one | inl is-zero' = inl ( pair ( unit-trunc-Prop (one-Fin 1 , is-zero')) ( unit-trunc-Prop (zero-Fin 1 , is-one))) ... | inr is-one | inr is-one' = inr ( λ P → apply-universal-property-trunc-Prop (pr1 P) empty-Prop ( λ where (inl (inr star) , is-zero) → neq-inl-inr (inv is-zero ∙ is-one) (inr star , is-zero) → neq-inl-inr (inv is-zero ∙ is-one'))) is-decidable-standard-edge-ethane : (c c' : vertex-ethane) → is-decidable (standard-edge-ethane c c') is-decidable-standard-edge-ethane c c' = is-decidable-edge-ethane-eq-Fin-two (standard-unordered-pair c c') refl abstract is-finite-edge-ethane : (p : unordered-pair vertex-ethane) → is-finite (edge-ethane p) is-finite-edge-ethane p = apply-universal-property-trunc-Prop ( has-two-elements-type-unordered-pair p) ( is-finite-Prop (edge-ethane p)) ( λ e → is-finite-is-decidable-Prop ( edge-ethane-Prop p) ( is-decidable-edge-ethane-eq-Fin-two p ( inv (eq-equiv (Fin 2) (type-unordered-pair p) e)))) edge-ethane-𝔽 : unordered-pair vertex-ethane → 𝔽 lzero pr1 (edge-ethane-𝔽 p) = edge-ethane p pr2 (edge-ethane-𝔽 p) = is-finite-edge-ethane p finite-graph-ethane : Undirected-Graph-𝔽 lzero lzero pr1 finite-graph-ethane = vertex-ethane-𝔽 pr2 finite-graph-ethane = edge-ethane-𝔽 bonding-ethane : (c : vertex-ethane) → Σ (vertex-ethane) (λ c' → standard-edge-ethane c c') → vertex-tetrahedron-in-3-space t bonding-ethane c e = v is-contr-standard-edge-ethane : (c : vertex-ethane) → is-contr (Σ (vertex-ethane) (λ c' → standard-edge-ethane c c')) pr1 (pr1 (is-contr-standard-edge-ethane (inl (inr star)))) = one-Fin 1 pr1 (pr2 (pr1 (is-contr-standard-edge-ethane (inl (inr star))))) = unit-trunc-Prop (zero-Fin 1 , refl) pr2 (pr2 (pr1 (is-contr-standard-edge-ethane (inl (inr star))))) = unit-trunc-Prop (one-Fin 1 , refl) pr2 (is-contr-standard-edge-ethane (inl (inr star))) (inl (inr star) , P) = ex-falso ( apply-universal-property-trunc-Prop (pr2 P) empty-Prop ( λ where (inl (inr star) , is-one) → neq-inl-inr is-one (inr star , is-one) → neq-inl-inr is-one)) pr2 (is-contr-standard-edge-ethane (inl (inr star))) (inr star , P) = eq-pair-Σ refl ( eq-is-prop ( is-prop-edge-ethane ( standard-unordered-pair (inl (inr star)) (inr star)))) pr1 (pr1 (is-contr-standard-edge-ethane (inr star))) = zero-Fin 1 pr1 (pr2 (pr1 (is-contr-standard-edge-ethane (inr star)))) = unit-trunc-Prop (one-Fin 1 , refl) pr2 (pr2 (pr1 (is-contr-standard-edge-ethane (inr star)))) = unit-trunc-Prop (zero-Fin 1 , refl) pr2 (is-contr-standard-edge-ethane (inr star)) (inl (inr star) , P) = eq-pair-Σ refl ( eq-is-prop ( is-prop-edge-ethane ( standard-unordered-pair (inr star) (inl (inr star))))) pr2 (is-contr-standard-edge-ethane (inr star)) (inr star , P) = ex-falso ( apply-universal-property-trunc-Prop (pr1 P) empty-Prop ( λ where (inl (inr star) , is-zero) → neq-inr-inl is-zero (inr star , is-zero) → neq-inr-inl is-zero)) abstract is-emb-bonding-ethane : (c : vertex-ethane) → is-emb (bonding-ethane c) is-emb-bonding-ethane c = is-emb-is-injective ( is-set-type-UU-Fin 4 (pr1 t)) ( is-injective-is-contr (λ e → v) (is-contr-standard-edge-ethane c)) emb-bonding-ethane : (c : vertex-ethane) → Σ (vertex-ethane) (λ c' → standard-edge-ethane c c') ↪ vertex-tetrahedron-in-3-space t pr1 (emb-bonding-ethane c) = bonding-ethane c pr2 (emb-bonding-ethane c) = is-emb-bonding-ethane c count-standard-edge-ethane : (c c' : vertex-ethane) → count (standard-edge-ethane c c') count-standard-edge-ethane c c' = count-is-decidable-Prop ( standard-edge-ethane-Prop c c') ( is-decidable-standard-edge-ethane c c') abstract number-of-elements-count-standard-edge-ethane-leq-3 : (c c' : vertex-ethane) → number-of-elements-count (count-standard-edge-ethane c c') ≤-ℕ 3 number-of-elements-count-standard-edge-ethane-leq-3 (inl (inr star)) (inl (inr star)) = star number-of-elements-count-standard-edge-ethane-leq-3 (inl (inr star)) (inr star) = star number-of-elements-count-standard-edge-ethane-leq-3 (inr star) (inl (inr star)) = star number-of-elements-count-standard-edge-ethane-leq-3 (inr star) (inr star) = star ethane : hydrocarbon lzero lzero pr1 ethane = finite-graph-ethane pr1 (pr2 ethane) c = t pr1 (pr2 (pr2 ethane)) = emb-bonding-ethane pr1 (pr2 (pr2 (pr2 ethane))) (inl (inr star)) P = apply-universal-property-trunc-Prop (pr2 P) empty-Prop ( λ where (inl (inr star) , is-one) → neq-inl-inr is-one (inr star , is-one) → neq-inl-inr is-one) pr1 (pr2 (pr2 (pr2 ethane))) (inr star) P = apply-universal-property-trunc-Prop (pr1 P) empty-Prop ( λ where (inl (inr star) , is-zero) → neq-inr-inl is-zero (inr star , is-zero) → neq-inr-inl is-zero) pr1 (pr2 (pr2 (pr2 (pr2 ethane)))) c c' = concatenate-eq-leq-ℕ 3 ( inv ( compute-number-of-elements-is-finite ( count-standard-edge-ethane c c') ( is-finite-edge-ethane (standard-unordered-pair c c')))) (number-of-elements-count-standard-edge-ethane-leq-3 c c') pr2 (pr2 (pr2 (pr2 (pr2 ethane)))) (inl (inr star)) (inl (inr star)) = unit-trunc-Prop refl-walk-Undirected-Graph pr2 (pr2 (pr2 (pr2 (pr2 ethane)))) (inl (inr star)) (inr star) = unit-trunc-Prop ( tr ( λ x → walk-Undirected-Graph ( undirected-graph-Undirected-Graph-𝔽 finite-graph-ethane) ( zero-Fin 1) ( element-standard-unordered-pair (zero-Fin 1) (one-Fin 1) x)) ( compute-swap-2-Element-Type ( Fin-UU-Fin' 2) ( zero-Fin 1) ( one-Fin 1) ( neq-inl-inr)) ( cons-walk-Undirected-Graph ( standard-unordered-pair (zero-Fin 1) (one-Fin 1)) ( pair ( unit-trunc-Prop (zero-Fin 1 , refl)) ( unit-trunc-Prop (one-Fin 1 , refl))) { zero-Fin 1} ( refl-walk-Undirected-Graph))) pr2 (pr2 (pr2 (pr2 (pr2 ethane)))) (inr star) (inl (inr star)) = unit-trunc-Prop ( tr ( λ x → walk-Undirected-Graph ( undirected-graph-Undirected-Graph-𝔽 finite-graph-ethane) ( one-Fin 1) ( element-standard-unordered-pair (one-Fin 1) (zero-Fin 1) x)) ( compute-swap-2-Element-Type ( Fin-UU-Fin' 2) ( zero-Fin 1) ( one-Fin 1) ( neq-inl-inr)) ( cons-walk-Undirected-Graph ( standard-unordered-pair (one-Fin 1) (zero-Fin 1)) ( pair ( unit-trunc-Prop (one-Fin 1 , refl)) ( unit-trunc-Prop (zero-Fin 1 , refl))) { zero-Fin 1} ( refl-walk-Undirected-Graph))) pr2 (pr2 (pr2 (pr2 (pr2 ethane)))) (inr star) (inr star) = unit-trunc-Prop refl-walk-Undirected-Graph is-alkane-ethane : is-alkane-hydrocarbon ethane is-alkane-ethane = is-prop-standard-edge-ethane