HoTT-Inspired Component Equivalence

Defines PortEquiv (port interface equivalence), ComponentEquiv (component equivalence), Substitutable (substitutability), and transport_wellFormed (design-space transport).

Correspondence with HoTT

• Equivalence (A ≃ B) → ComponentEquiv
• Univalence (A ≃ B → A = B) → Substitutability principle
• Transport → transport_wellFormed

def VerifiedMBSE.Equivalence.PortCompatible (p q : Core.PortDef) : Prop

PortCompatible: two ports are compatible (flowType and direction match).

Equations

• VerifiedMBSE.Equivalence.PortCompatible p q = (p.flowType = q.flowType ∧ p.feature.direction = q.feature.direction)

structure VerifiedMBSE.Equivalence.PortEquiv (ports₁ ports₂ : List Core.PortDef) : Prop

PortEquiv: two port lists are structurally equivalent. In HoTT terms, PortBundle(A) ≃ PortBundle(B).

• length_eq : ports₁.length = ports₂.length

  Port counts match

• forward (p : Core.PortDef) : p ∈ ports₁ → ∃ (q : Core.PortDef), q ∈ ports₂ ∧ PortCompatible p q

  Forward compatible mapping ports₁ → ports₂

• backward (q : Core.PortDef) : q ∈ ports₂ → ∃ (p : Core.PortDef), p ∈ ports₁ ∧ PortCompatible q p

  Backward compatible mapping ports₂ → ports₁

theorem VerifiedMBSE.Equivalence.PortEquiv.refl (ports : List Core.PortDef) : PortEquiv ports ports

PortEquiv is reflexive.

theorem VerifiedMBSE.Equivalence.PortEquiv.symm {p₁ p₂ : List Core.PortDef} (h : PortEquiv p₁ p₂) : PortEquiv p₂ p₁

PortEquiv is symmetric.

theorem VerifiedMBSE.Equivalence.PortEquiv.trans {p₁ p₂ p₃ : List Core.PortDef} (h₁₂ : PortEquiv p₁ p₂) (h₂₃ : PortEquiv p₂ p₃) : PortEquiv p₁ p₃

PortEquiv is transitive.

structure VerifiedMBSE.Equivalence.ComponentEquiv (a b : Core.PartDef) : Prop

ComponentEquiv: two PartDefs are equivalent. Port interfaces are equivalent and invariants are biconditional.

• portEquiv : PortEquiv a.ports b.ports

  Port interface equivalence

• invariantIff : a.invariant ↔ b.invariant

  Invariant biconditional

theorem VerifiedMBSE.Equivalence.ComponentEquiv.refl (pd : Core.PartDef) : ComponentEquiv pd pd

ComponentEquiv is reflexive.

theorem VerifiedMBSE.Equivalence.ComponentEquiv.symm {a b : Core.PartDef} (h : ComponentEquiv a b) : ComponentEquiv b a

ComponentEquiv is symmetric.

theorem VerifiedMBSE.Equivalence.ComponentEquiv.trans {a b c : Core.PartDef} (hab : ComponentEquiv a b) (hbc : ComponentEquiv b c) : ComponentEquiv a c

ComponentEquiv is transitive.

structure VerifiedMBSE.Equivalence.Substitutable (a b : Core.PartDef) : Prop

Substitutable: A can substitute for B (upward compatible). A weaker condition than ComponentEquiv.

• invariantStronger : b.invariant → a.invariant

  b's invariant implies a's invariant

• portsSubset (p : Core.PortDef) : p ∈ a.ports → ∃ (q : Core.PortDef), q ∈ b.ports ∧ PortCompatible p q

  All ports of a exist in b

theorem VerifiedMBSE.Equivalence.ComponentEquiv.toSubstitutable {a b : Core.PartDef} (h : ComponentEquiv a b) : Substitutable a b

ComponentEquiv → Substitutable (special case of bidirectional equivalence).

theorem VerifiedMBSE.Equivalence.Substitutable.trans {a b c : Core.PartDef} (hab : Substitutable a b) (hbc : Substitutable b c) : Substitutable a c

Substitutable is transitive.

theorem VerifiedMBSE.Equivalence.transport_wellFormed (sys : Core.System) (a b : Core.PartDef) (hmem : a ∈ sys.parts) (hequiv : ComponentEquiv a b) : (∀ (p : Core.PartDef), p ∈ sys.parts → p.invariant) → b.invariant

Replacing a component with an equivalent one preserves invariants. MBSE version of HoTT transport: (A = B) → P(A) → P(B).