Optics¶

Optics and lenses in enriched category theory.

optics ¶

Optics: composable bidirectional transformations in Rel(V).

Optics generalize lenses and prisms to provide composable "accessors" that can get, set, and transform parts of a structure. In a V-enriched setting, optics are formulated via profunctors or as pairs of morphisms with specific laws.

The general optic from (S, T) to (A, B) in a monoidal category is a coend:

Optic(S, T, A, B) = ∫^M S → M ⊗ A  ×  M ⊗ B → T

which factors a transformation through a residual M.

This module provides concrete optic types:

Optic (abstract)
├── Lens     — get/put on product structures
├── Prism    — match/build on coproduct structures
├── Adapter  — invertible optics (isomorphisms)
└── Grate    — closed-structure optics

compose_optics() — compose two optics sequentially

These are V-enriched optics: forward() and backward() return Morphism (tensor-shaped fuzzy relations) and backward() joins over the complement axis using the algebra's join. This is a distinct abstraction from didactic.Lens (instance-level, with an explicit complement value) and from didactic.DependentLens (schema- level, wrapping panproto.ProtolensChain). Didactic 0.15.0 does not expose a V-enriched lens abstraction, so this module retains its own implementation.

Optic ¶

Optic(source: SetObject, target: SetObject, focus_source: SetObject, focus_target: SetObject, algebra: Algebra | None = None)

Bases: ABC

Abstract optic from (S, T) to (A, B).

An optic provides a bidirectional transformation between a "whole" (S/T) and a "part" (A/B). S is the source whole type, T is the target whole type, A is the source part type, and B is the target part type.

For simple (non-polymorphic) optics, S = T and A = B.

PARAMETER	DESCRIPTION
`source`	The source whole S. TYPE: `SetObject`
`target`	The target whole T. TYPE: `SetObject`
`focus_source`	The source part A. TYPE: `SetObject`
`focus_target`	The target part B. TYPE: `SetObject`
`algebra`	The enrichment algebra. TYPE: `Algebra or None` DEFAULT: `None`

Source code in src/quivers/enriched/optics.py

def __init__(
    self,
    source: SetObject,
    target: SetObject,
    focus_source: SetObject,
    focus_target: SetObject,
    algebra: Algebra | None = None,
) -> None:
    self._source = source
    self._target = target
    self._focus_source = focus_source
    self._focus_target = focus_target
    self._algebra = algebra if algebra is not None else PRODUCT_FUZZY

source `property` ¶

source: SetObject

The source whole S.

target `property` ¶

target: SetObject

The target whole T.

focus_source `property` ¶

focus_source: SetObject

The source part A.

focus_target `property` ¶

focus_target: SetObject

The target part B.

algebra `property` ¶

algebra: Algebra

The enrichment algebra.

forward `abstractmethod` ¶

forward() -> Morphism

The forward (get/match) morphism.

RETURNS	DESCRIPTION
`Morphism`	A morphism extracting the focus from the source.

Source code in src/quivers/enriched/optics.py

@abstractmethod
def forward(self) -> Morphism:
    """The forward (get/match) morphism.

    Returns
    -------
    Morphism
        A morphism extracting the focus from the source.
    """
    ...

backward `abstractmethod` ¶

backward() -> Morphism

The backward (put/build) morphism.

RETURNS	DESCRIPTION
`Morphism`	A morphism putting the focus back into the whole.

Source code in src/quivers/enriched/optics.py

@abstractmethod
def backward(self) -> Morphism:
    """The backward (put/build) morphism.

    Returns
    -------
    Morphism
        A morphism putting the focus back into the whole.
    """
    ...

as_profunctor ¶

as_profunctor() -> Profunctor

View this optic as a profunctor S ↛ T.

Computes the profunctor representation by composing forward and backward through the focus.

RETURNS	DESCRIPTION
`Profunctor`	The profunctor representation of this optic.

Source code in src/quivers/enriched/optics.py

def as_profunctor(self) -> Profunctor:
    """View this optic as a profunctor S ↛ T.

    Computes the profunctor representation by composing
    forward and backward through the focus.

    Returns
    -------
    Profunctor
        The profunctor representation of this optic.
    """
    fwd = self.forward()
    bwd = self.backward()

    # the profunctor view depends on the optic type,
    # but generally it's fwd >> bwd or a similar composition
    tensor = self._algebra.compose(fwd.tensor, bwd.tensor, self._focus_source.ndim)

    return Profunctor(
        contra=self._source,
        co=self._target,
        tensor=tensor,
        algebra=self._algebra,
    )

Lens ¶

Lens(whole: ProductSet, focus_index: int, algebra: Algebra | None = None)

Bases: Optic

A lens focusing on a component of a product.

A lens from (S, S) to (A, A) on a ProductSet S = A × C consists of:

get: S → A           (extract the focus)
put: A × C → S       (replace the focus, keeping complement)

In the V-enriched setting, get is a projection morphism and put reconstructs the product.

PARAMETER	DESCRIPTION
`whole`	The whole product S = A × C. TYPE: `ProductSet`
`focus_index`	Index of the focus component A in the product. TYPE: `int`
`algebra`	The enrichment algebra. TYPE: `Algebra or None` DEFAULT: `None`

Source code in src/quivers/enriched/optics.py

def __init__(
    self,
    whole: ProductSet,
    focus_index: int,
    algebra: Algebra | None = None,
) -> None:
    if not isinstance(whole, ProductSet):
        raise TypeError(f"Lens requires ProductSet, got {type(whole).__name__}")

    if not (0 <= focus_index < len(whole.components)):
        raise ValueError(
            f"focus_index {focus_index} out of range [0, {len(whole.components)})"
        )

    focus = whole.components[focus_index]
    super().__init__(
        source=whole,
        target=whole,
        focus_source=focus,
        focus_target=focus,
        algebra=algebra,
    )
    self._focus_index = focus_index

focus_index `property` ¶

focus_index: int

Index of the focus component.

forward ¶

forward() -> Morphism

get: S → A (projection to focus component).

RETURNS	DESCRIPTION
`ObservedMorphism`	The projection morphism.

Source code in src/quivers/enriched/optics.py

def forward(self) -> Morphism:
    """get: S → A (projection to focus component).

    Returns
    -------
    ObservedMorphism
        The projection morphism.
    """
    q = self._algebra
    whole = self._source
    focus = self._focus_source

    data = torch.full((*whole.shape, *focus.shape), q.zero)

    # build projection tensor
    assert isinstance(whole, ProductSet)
    components = whole.components

    # compute dimension offset for focus
    offset = 0

    for i in range(self._focus_index):
        offset += components[i].ndim

    # for each element of the whole, project to the focus
    for idx in itertools.product(*(range(s) for s in whole.shape)):
        focus_idx = idx[offset : offset + focus.ndim]
        data[idx + focus_idx] = q.unit

    return observed(whole, focus, data, algebra=q)

backward ¶

backward() -> Morphism

put: A → S (embed focus back, averaging over complement).

In the V-enriched setting, the "put" creates a morphism A → S where fixing the focus component and joining over the complement gives a fuzzy relation.

RETURNS	DESCRIPTION
`ObservedMorphism`	The embedding morphism.

Source code in src/quivers/enriched/optics.py

def backward(self) -> Morphism:
    """put: A → S (embed focus back, averaging over complement).

    In the V-enriched setting, the "put" creates a morphism
    A → S where fixing the focus component and joining over
    the complement gives a fuzzy relation.

    Returns
    -------
    ObservedMorphism
        The embedding morphism.
    """
    q = self._algebra
    whole = self._source
    focus = self._focus_source

    # put: A → S where S = A × C
    # for each a, put(a, (a', c)) = δ(a, a') for the focus,
    # and the unit for the complement
    assert isinstance(whole, ProductSet)

    data = torch.full((*focus.shape, *whole.shape), q.zero)

    # compute dimension offset for focus
    components = whole.components
    offset = 0

    for i in range(self._focus_index):
        offset += components[i].ndim

    for focus_idx in itertools.product(*(range(s) for s in focus.shape)):
        # for each complement index, set the delta
        complement_shapes: list[tuple[int, ...]] = []

        for i, comp in enumerate(components):
            if i != self._focus_index:
                complement_shapes.append(tuple(s for s in comp.shape))

        # iterate over all whole indices where focus matches
        for whole_idx in itertools.product(*(range(s) for s in whole.shape)):
            w_focus = whole_idx[offset : offset + focus.ndim]

            if w_focus == focus_idx:
                data[focus_idx + whole_idx] = q.unit

    return observed(focus, whole, data, algebra=q)

Prism ¶

Prism(whole: CoproductSet, focus_index: int, algebra: Algebra | None = None)

Bases: Optic

A prism focusing on a component of a coproduct.

A prism from (S, S) to (A, A) on a CoproductSet S = A + C consists of:

match: S → A + C    (attempt to extract the focus)
build: A → S         (embed the focus into the whole)

PARAMETER	DESCRIPTION
`whole`	The whole coproduct S = A + C. TYPE: `CoproductSet`
`focus_index`	Index of the focus component A in the coproduct. TYPE: `int`
`algebra`	The enrichment algebra. TYPE: `Algebra or None` DEFAULT: `None`

Source code in src/quivers/enriched/optics.py

def __init__(
    self,
    whole: CoproductSet,
    focus_index: int,
    algebra: Algebra | None = None,
) -> None:
    if not isinstance(whole, CoproductSet):
        raise TypeError(f"Prism requires CoproductSet, got {type(whole).__name__}")

    if not (0 <= focus_index < len(whole.components)):
        raise ValueError(
            f"focus_index {focus_index} out of range [0, {len(whole.components)})"
        )

    focus = whole.components[focus_index]
    super().__init__(
        source=whole,
        target=whole,
        focus_source=focus,
        focus_target=focus,
        algebra=algebra,
    )
    self._focus_index = focus_index

focus_index `property` ¶

focus_index: int

Index of the focus component.

forward ¶

forward() -> Morphism

match: S → A (partial extraction, zero on non-matching).

RETURNS	DESCRIPTION
`ObservedMorphism`	The matching morphism.

Source code in src/quivers/enriched/optics.py

def forward(self) -> Morphism:
    """match: S → A (partial extraction, zero on non-matching).

    Returns
    -------
    ObservedMorphism
        The matching morphism.
    """
    q = self._algebra
    whole = self._source
    focus = self._focus_source

    assert isinstance(whole, CoproductSet)
    start, end = whole.component_range(self._focus_index)

    data = torch.full((whole.size, focus.size), q.zero)

    for i in range(focus.size):
        data[start + i, i] = q.unit

    return observed(whole, focus, data, algebra=q)

backward ¶

backward() -> Morphism

build: A → S (inject focus into the coproduct).

RETURNS	DESCRIPTION
`ObservedMorphism`	The injection morphism.

Source code in src/quivers/enriched/optics.py

def backward(self) -> Morphism:
    """build: A → S (inject focus into the coproduct).

    Returns
    -------
    ObservedMorphism
        The injection morphism.
    """
    q = self._algebra
    whole = self._source
    focus = self._focus_source

    assert isinstance(whole, CoproductSet)
    start, end = whole.component_range(self._focus_index)

    data = torch.full((focus.size, whole.size), q.zero)

    for i in range(focus.size):
        data[i, start + i] = q.unit

    return observed(focus, whole, data, algebra=q)

Adapter ¶

Adapter(from_morph: Morphism, to_morph: Morphism, algebra: Algebra | None = None)

Bases: Optic

An adapter (isomorphism optic).

An adapter between (S, T) and (A, B) consists of an isomorphism pair from: S → A and to: B → T. Every adapter is both a lens and a prism.

PARAMETER	DESCRIPTION
`from_morph`	The forward isomorphism S → A. TYPE: `Morphism`
`to_morph`	The backward isomorphism B → T. TYPE: `Morphism`
`algebra`	The enrichment algebra. TYPE: `Algebra or None` DEFAULT: `None`

Source code in src/quivers/enriched/optics.py

def __init__(
    self,
    from_morph: Morphism,
    to_morph: Morphism,
    algebra: Algebra | None = None,
) -> None:
    super().__init__(
        source=from_morph.domain,
        target=to_morph.codomain,
        focus_source=from_morph.codomain,
        focus_target=to_morph.domain,
        algebra=algebra,
    )
    self._from_morph = from_morph
    self._to_morph = to_morph

forward ¶

forward() -> Morphism

from: S → A.

Source code in src/quivers/enriched/optics.py

def forward(self) -> Morphism:
    """from: S → A."""
    return self._from_morph

backward ¶

backward() -> Morphism

to: B → T.

Source code in src/quivers/enriched/optics.py

def backward(self) -> Morphism:
    """to: B → T."""
    return self._to_morph

verify_isomorphism ¶

verify_isomorphism(atol: float = 1e-05) -> bool

Verify that forward and backward form an isomorphism.

Checks from >> to ≈ id_S and to >> from ≈ id_A (when S=T, A=B).

PARAMETER	DESCRIPTION
`atol`	Absolute tolerance. TYPE: `float` DEFAULT: `1e-05`

RETURNS	DESCRIPTION
`bool`	True if the adapter is an isomorphism.

Source code in src/quivers/enriched/optics.py

def verify_isomorphism(self, atol: float = 1e-5) -> bool:
    """Verify that forward and backward form an isomorphism.

    Checks from >> to ≈ id_S and to >> from ≈ id_A (when S=T, A=B).

    Parameters
    ----------
    atol : float
        Absolute tolerance.

    Returns
    -------
    bool
        True if the adapter is an isomorphism.
    """
    if self._source != self._target or self._focus_source != self._focus_target:
        return False

    fwd = self._from_morph
    bwd = self._to_morph

    # fwd >> bwd ≈ id_S
    roundtrip_s = (fwd >> bwd).tensor
    id_s = identity(self._source, algebra=self._algebra).tensor

    if not torch.allclose(roundtrip_s, id_s, atol=atol):
        return False

    # bwd >> fwd ≈ id_A
    roundtrip_a = (bwd >> fwd).tensor
    id_a = identity(self._focus_source, algebra=self._algebra).tensor

    return torch.allclose(roundtrip_a, id_a, atol=atol)

Grate ¶

Grate(source: SetObject, focus: SetObject, index: SetObject, cotraverse_tensor: Tensor, algebra: Algebra | None = None)

Bases: Optic

A grate optic for closed/exponential structures.

A grate from S to A through a "coindexing" object I encapsulates the pattern:

cotraverse: (I → A) → S

In the V-enriched setting, the grate is represented by a morphism from the internal hom [I, A] to S.

PARAMETER	DESCRIPTION
`source`	The whole S. TYPE: `SetObject`
`focus`	The focus A. TYPE: `SetObject`
`index`	The coindex I. TYPE: `SetObject`
`cotraverse_tensor`	The tensor for (I → A) → S. TYPE: `Tensor`
`algebra`	The enrichment algebra. TYPE: `Algebra or None` DEFAULT: `None`

Source code in src/quivers/enriched/optics.py

def __init__(
    self,
    source: SetObject,
    focus: SetObject,
    index: SetObject,
    cotraverse_tensor: torch.Tensor,
    algebra: Algebra | None = None,
) -> None:
    super().__init__(
        source=source,
        target=source,
        focus_source=focus,
        focus_target=focus,
        algebra=algebra,
    )
    self._index = index
    self._cotraverse_tensor = cotraverse_tensor

index `property` ¶

index: SetObject

The coindex object I.

forward ¶

forward() -> Morphism

Extract focus by evaluating at each index.

Produces S → A by marginalizing over the index.

Source code in src/quivers/enriched/optics.py

def forward(self) -> Morphism:
    """Extract focus by evaluating at each index.

    Produces S → A by marginalizing over the index.
    """
    q = self._algebra
    source = self._source
    focus = self._focus_source

    # use the cotraverse tensor transposed as the getter
    # simplified: just project
    data = q.identity_tensor(source.shape)

    # if source and focus match, return identity
    if source.shape == focus.shape:
        return observed(source, focus, data, algebra=q)

    # otherwise, use marginalization
    return observed(source, focus, self._cotraverse_tensor, algebra=q)

backward ¶

backward() -> Morphism

Rebuild whole from focus via cotraverse.

Source code in src/quivers/enriched/optics.py

def backward(self) -> Morphism:
    """Rebuild whole from focus via cotraverse."""
    q = self._algebra
    focus = self._focus_target
    source = self._target

    if source.shape == focus.shape:
        data = q.identity_tensor(source.shape)
        return observed(focus, source, data, algebra=q)

    # transpose the cotraverse
    n_src = len(source.shape)
    n_foc = len(focus.shape)
    perm = list(range(n_src, n_src + n_foc)) + list(range(n_src))

    return observed(
        focus,
        source,
        self._cotraverse_tensor.permute(*perm),
        algebra=q,
    )

compose_optics ¶

compose_optics(outer: Optic, inner: Optic) -> Optic

Compose two optics sequentially.

Given outer: (S, T) → (M, N) and inner: (M, N) → (A, B), produces the composed optic (S, T) → (A, B).

The composition is returned as an Adapter wrapping the composed forward and backward morphisms.

PARAMETER	DESCRIPTION
`outer`	The outer optic (S, T) → (M, N). TYPE: `Optic`
`inner`	The inner optic (M, N) → (A, B). TYPE: `Optic`

RETURNS	DESCRIPTION
`Adapter`	The composed optic.

Source code in src/quivers/enriched/optics.py

def compose_optics(outer: Optic, inner: Optic) -> Optic:
    """Compose two optics sequentially.

    Given outer: (S, T) → (M, N) and inner: (M, N) → (A, B),
    produces the composed optic (S, T) → (A, B).

    The composition is returned as an Adapter wrapping the composed
    forward and backward morphisms.

    Parameters
    ----------
    outer : Optic
        The outer optic (S, T) → (M, N).
    inner : Optic
        The inner optic (M, N) → (A, B).

    Returns
    -------
    Adapter
        The composed optic.
    """
    fwd = outer.forward() >> inner.forward()
    bwd = inner.backward() >> outer.backward()

    return Adapter(
        from_morph=fwd,
        to_morph=bwd,
        algebra=outer.algebra,
    )

Optics¶

optics ¶

Optic ¶

source property ¶

target property ¶

focus_source property ¶

focus_target property ¶

algebra property ¶

forward abstractmethod ¶

backward abstractmethod ¶

as_profunctor ¶

Lens ¶

focus_index property ¶

forward ¶

backward ¶

Prism ¶

focus_index property ¶

forward ¶

backward ¶

Adapter ¶

forward ¶

backward ¶

verify_isomorphism ¶

Grate ¶

index property ¶

forward ¶

backward ¶

compose_optics ¶

source `property` ¶

target `property` ¶

focus_source `property` ¶

focus_target `property` ¶

algebra `property` ¶

forward `abstractmethod` ¶

backward `abstractmethod` ¶

focus_index `property` ¶

focus_index `property` ¶

index `property` ¶