Enum FiberTyS_ 

pub enum FiberTyS_ {
    TopVar(TopVarName),
    Over(BaseTmS),
    Record(Row<FiberTyS>),
    Id(FiberTyS, FiberTmS, FiberTmS),
}

Inner enum for FiberTyS.

Fiber types type the fiber world — instances of a model and their elements — mirroring how BaseTyS types the base world (models). See crate::tt::toplevel for the comprehension-category picture. The constructors parallel the base world: TopVar references a top-level instance, Over is the atomic fiber-element type, Record assembles them into an instance, and Id imposes a (propositional) equation — just as BaseTyS_::TopVar and BaseTyS_::Id do in the base.

Variants

TopVar(TopVarName)

A reference to a top-level instance declaration, as in a sub-instance import we : Edge. Mirrors BaseTyS_::TopVar: it appears only in syntax and exists to preserve the instance’s name for display — like base top-vars, it is resolved away in the value world (there is no FiberTyV_::TopVar), where it becomes the referenced instance’s Record.

Over(BaseTmS)

The type of a fiber element lying over a codomain object obj.

obj is a base object term (rooted at the codomain model), so it may be a plain generator (self.V), or a modal object such as a list [M, M] or a tensor @tensor [H, M]. Comparing two Over types is comparing their base objects, so modal objects need no special handling. No surface syntax — its inhabitants (FiberTmS) are introduced by set-literal clauses field := [...], projection out of a sub-instance import, fiber list/object -operation literals, and codomain-morphism application.

Record(Row<FiberTyS>)

An instance of a model — an object of the fiber over the codomain model — presented as a record of fiber types. A generator is an Over field, a sub-instance import is a nested Record field, and an equation is an Id field. This is what instance I : X := [...] elaborates to, and also the type of a sub-instance import we : Edge (whose generators are then projected as we.e).

Id(FiberTyS, FiberTmS, FiberTmS)

A propositional equation between two fiber elements of the given fiber type, asserted to hold in the enclosing instance. Mirrors BaseTyS_::Id; like it, these are proof-irrelevant.