Alkenes

Content created by Jonathan Prieto-Cubides, Fredrik Bakke, Egbert Rijke and Amélia Liao.

Created on 2022-07-05.
Last modified on 2025-10-31.

module organic-chemistry.alkenes where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.universe-levels

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

open import univalent-combinatorics.finite-types

Idea

An -alkene is a hydrocarbon equipped with a choice of carbons, each of which has a double bond. For an -alkene, the embedding from the given type (the first component of the -alkene structure) specifies which carbons have double bonds. For example, 1-butene and but-2-ene have the same geometry, and the embedding is what differentiates them (while the third tautometer, isobutylene, is branched, thus has a different geometry).

Definition

alkene : {l1 l2 : Level} → hydrocarbon l1 l2 → ℕ → UU (lsuc lzero ⊔ l1 ⊔ l2)
alkene H n =
  Σ ( Type-With-Cardinality-ℕ lzero n)
    ( λ carbons →
      Σ ( type-Type-With-Cardinality-ℕ n carbons ↪ vertex-hydrocarbon H)
        ( λ embed-carbons →
          ( c : type-Type-With-Cardinality-ℕ n carbons) →
          has-double-bond-hydrocarbon H (map-emb embed-carbons c)))

Recent changes