Formalization of the Univalence Axiom

Formalizes the HoTT univalence axiom (A ≃ B) ≃ (A = B) in the MBSE design space.

Since Lean 4 is not a cubical type theory, full univalence does not hold intrinsically. Instead, we use a setoid quotient to construct the design space DesignSpace as PartDef / ComponentEquiv. On this quotient type, the following hold:

• Sound (ua): ComponentEquiv a b → ⟦a⟧ = ⟦b⟧
• Complete (ua⁻¹): ⟦a⟧ = ⟦b⟧ → ComponentEquiv a b
• Transport: ⟦a⟧ = ⟦b⟧ → P ⟦a⟧ → P ⟦b⟧
• Path induction: Induction on the quotient type
• Fiber: Lifting of design space points

References

• HoTT Book §2.10 (Universes and the univalence axiom)
• Setoid model of HoTT (Altenkirch, Boulier, Kaposi, Tabareau 2019)

theorem VerifiedMBSE.Equivalence.componentEquiv_equivalence : Equivalence ComponentEquiv

Proof that ComponentEquiv is an equivalence relation.

@[implicit_reducible]

instance VerifiedMBSE.Equivalence.componentSetoid : Setoid Core.PartDef

Setoid instance on PartDef. Uses ComponentEquiv as the equivalence relation.

Equations

• VerifiedMBSE.Equivalence.componentSetoid = { r := VerifiedMBSE.Equivalence.ComponentEquiv, iseqv := VerifiedMBSE.Equivalence.componentEquiv_equivalence }

def VerifiedMBSE.Equivalence.DesignSpace : Type

DesignSpace: quotient type of PartDef by ComponentEquiv. Corresponds to the HoTT universe U. Equal elements are mutually substitutable.

Equations

• VerifiedMBSE.Equivalence.DesignSpace = Quotient VerifiedMBSE.Equivalence.componentSetoid

def VerifiedMBSE.Equivalence.DesignSpace.mk (pd : Core.PartDef) : DesignSpace

Embedding from PartDef into DesignSpace.

Equations

• VerifiedMBSE.Equivalence.DesignSpace.mk pd = Quotient.mk VerifiedMBSE.Equivalence.componentSetoid pd

def VerifiedMBSE.Equivalence.«term⟦_⟧» : Lean.ParserDescr

Notation: ⟦pd⟧ denotes DesignSpace.mk pd.

Equations

• One or more equations did not get rendered due to their size.

theorem VerifiedMBSE.Equivalence.ua {a b : Core.PartDef} (h : ComponentEquiv a b) : DesignSpace.mk a = DesignSpace.mk b

ua (Univalence axiom, sound direction): ComponentEquiv a b → ⟦a⟧ = ⟦b⟧. Automatically holds via Quotient.sound in the setoid quotient.

theorem VerifiedMBSE.Equivalence.ua_inv {a b : Core.PartDef} (h : DesignSpace.mk a = DesignSpace.mk b) : ComponentEquiv a b

ua_inv (Univalence axiom, complete direction): ⟦a⟧ = ⟦b⟧ → ComponentEquiv a b. Holds via Quotient.exact.

theorem VerifiedMBSE.Equivalence.ua_iff {a b : Core.PartDef} : ComponentEquiv a b ↔ DesignSpace.mk a = DesignSpace.mk b

ua and ua_inv are mutual inverses. This gives the equivalence (ComponentEquiv a b) ≃ (⟦a⟧ = ⟦b⟧).

theorem VerifiedMBSE.Equivalence.transport {P : DesignSpace → Prop} {a b : Core.PartDef} (h : ComponentEquiv a b) : P (DesignSpace.mk a) → P (DesignSpace.mk b)

transport: transports a predicate on DesignSpace along an equality. MBSE version of HoTT transport: (p : a = b) → P a → P b.

theorem VerifiedMBSE.Equivalence.transport_symm {P : DesignSpace → Prop} {a b : Core.PartDef} (h : ComponentEquiv a b) : P (DesignSpace.mk b) → P (DesignSpace.mk a)

transport_symm: transport in the reverse direction.

theorem VerifiedMBSE.Equivalence.transport_refl {P : DesignSpace → Prop} (a : Core.PartDef) (pa : P (DesignSpace.mk a)) : ⋯ = pa

transport_refl: transport along reflexive equivalence is the identity.

def VerifiedMBSE.Equivalence.DesignSpace.liftProp (P : Core.PartDef → Prop) (resp : ∀ (a b : Core.PartDef), ComponentEquiv a b → (P a ↔ P b)) : DesignSpace → Prop

Lift for defining predicates on DesignSpace. Only predicates respecting ComponentEquiv can be lifted.

Equations

• VerifiedMBSE.Equivalence.DesignSpace.liftProp P resp = Quotient.lift P ⋯

theorem VerifiedMBSE.Equivalence.DesignSpace.liftProp_mk (P : Core.PartDef → Prop) (resp : ∀ (a b : Core.PartDef), ComponentEquiv a b → (P a ↔ P b)) (pd : Core.PartDef) : liftProp P resp (mk pd) = P pd

liftProp is consistent with the original predicate.

def VerifiedMBSE.Equivalence.DesignSpace.liftBool (f : Core.PartDef → Bool) (resp : ∀ (a b : Core.PartDef), ComponentEquiv a b → f a = f b) : DesignSpace → Bool

Lift for Bool-valued functions on DesignSpace.

Equations

• VerifiedMBSE.Equivalence.DesignSpace.liftBool f resp = Quotient.lift f resp

theorem VerifiedMBSE.Equivalence.DesignSpace.ind {P : DesignSpace → Prop} (h : ∀ (pd : Core.PartDef), P (mk pd)) (d : DesignSpace) : P d

Induction on DesignSpace (universal quantification). MBSE version of HoTT path induction.

theorem VerifiedMBSE.Equivalence.DesignSpace.ind₂ {P : DesignSpace → DesignSpace → Prop} (h : ∀ (a b : Core.PartDef), P (mk a) (mk b)) (d₁ d₂ : DesignSpace) : P d₁ d₂

Binary induction on DesignSpace.

def VerifiedMBSE.Equivalence.Fiber (d : DesignSpace) : Type

Fiber: fiber over a point d in the design space. The set of all concrete PartDefs equivalent to d. HoTT homotopy fiber fib(f, b) = Σ(a:A). f(a) = b.

Equations

• VerifiedMBSE.Equivalence.Fiber d = { pd : VerifiedMBSE.Core.PartDef // VerifiedMBSE.Equivalence.DesignSpace.mk pd = d }

theorem VerifiedMBSE.Equivalence.fiber_nonempty (d : DesignSpace) : Nonempty (Fiber d)

Every fiber is nonempty (every DesignSpace point has a representative).

theorem VerifiedMBSE.Equivalence.fiber_equiv {d : DesignSpace} (x y : Fiber d) : ComponentEquiv ↑x ↑y

Any two elements of a fiber are ComponentEquiv.

theorem VerifiedMBSE.Equivalence.groupoid_left_id {a b : Core.PartDef} (h : ComponentEquiv a b) : ⋯ = h

ComponentEquiv has a groupoid structure (strict category with invertible morphisms). refl = id, trans = comp, symm = inv.

theorem VerifiedMBSE.Equivalence.groupoid_right_id {a b : Core.PartDef} (h : ComponentEquiv a b) : ⋯ = h

theorem VerifiedMBSE.Equivalence.groupoid_left_inv {a b : Core.PartDef} (h : ComponentEquiv a b) : ⋯ = ⋯

theorem VerifiedMBSE.Equivalence.groupoid_right_inv {a b : Core.PartDef} (h : ComponentEquiv a b) : ⋯ = ⋯

theorem VerifiedMBSE.Equivalence.system_component_ua {a b : Core.PartDef} (h : ComponentEquiv a b) (f : DesignSpace → Prop) : f (DesignSpace.mk a) ↔ f (DesignSpace.mk b)

Replacing a component in a system with an equivalent one does not change its representation in the design space.

theorem VerifiedMBSE.Equivalence.invariant_respects_equiv {a b : Core.PartDef} (h : ComponentEquiv a b) : a.invariant ↔ b.invariant

Invariants are well-defined on the design space (respect ComponentEquiv).

def VerifiedMBSE.Equivalence.designInvariant : DesignSpace → Prop

Lifting the invariant to DesignSpace.

Equations

• VerifiedMBSE.Equivalence.designInvariant = VerifiedMBSE.Equivalence.DesignSpace.liftProp (fun (pd : VerifiedMBSE.Core.PartDef) => pd.invariant) ⋯

theorem VerifiedMBSE.Equivalence.designInvariant_mk (pd : Core.PartDef) : designInvariant (DesignSpace.mk pd) = pd.invariant

designInvariant is consistent with the original invariant.