This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Alkanes

module organic-chemistry.alkanes where
Imports 
open import foundation.universe-levels

open import organic-chemistry.hydrocarbons
open import organic-chemistry.saturated-carbons

Idea

An alkane is a hydrocarbon that only has saturated carbons, i.e., it does not have any double or triple carbon-carbon bonds.

Definition

is-alkane-hydrocarbon : {l1 l2 : Level} → hydrocarbon l1 l2 → UU (l1 ⊔ l2)
is-alkane-hydrocarbon H =
  (c : vertex-hydrocarbon H) → is-saturated-carbon-hydrocarbon H c