Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Alice Laroche and Egbert Rijke.

Created on 2022-08-16.
Last modified on 2023-05-01.

module organic-chemistry.methane where
open import elementary-number-theory.inequality-natural-numbers

open import finite-group-theory.tetrahedra-in-3-space

open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.unit-type
open import foundation.universe-levels

open import graph-theory.walks-undirected-graphs

open import organic-chemistry.alkanes
open import organic-chemistry.hydrocarbons

open import univalent-combinatorics.counting
open import univalent-combinatorics.finite-types
## Idea

Methane is the simpliest hydrocarbon, and the first alkane.


module _
  (t : tetrahedron-in-3-space)

  methane : hydrocarbon lzero lzero
  methane =
    ( unit-𝔽 ,  x  empty-𝔽)) ,
    ( λ c  t) ,
    ( λ c   e  ex-falso (pr2 e)) , λ e _  ex-falso (pr2 e)) ,
    ( λ c x  x) ,
    ( λ c c' 
        ( 3)
        ( inv
          ( compute-number-of-elements-is-finite count-empty is-finite-empty))
        ( star)) ,
    ( λ {star star  unit-trunc-Prop refl-walk-Undirected-Graph})

  is-alkane-methane : is-alkane-hydrocarbon methane
  is-alkane-methane c c' e e' = is-prop-empty e e'

Recent changes