This module defines tactic/meta infrastructure for displaying commutative diagrams in the infoview.
Metaprogramming utilities for breaking down category theory expressions #
@[inline, reducible]
Expressions to display as labels in a diagram.
Instances For
Widget for general commutative diagrams #
Construct a commutative diagram from a Penrose sub
stance program and expressions embeds
to
display as labels in the diagram.
Instances For
Commutative triangles #
Triangle with homs = [f,g,h]
and objs = [A,B,C]
A f B
h g
C
Instances For
Given a commutative triangle f ≫ g = h
or e ≡ h = f ≫ g
, return a triangle diagram.
Otherwise none
.
Instances For
Commutative squares #
Square with homs = [f,g,h,i]
and objs = [A,B,C,D]
A f B
i g
D h C
Instances For
Given a commutative square f ≫ g = i ≫ h
, return a square diagram. Otherwise none
.