Commutative squares #
This file provide an API for commutative squares in categories.
bottom are four morphisms which are the edges
of a square,
CommSq top left right bottom is the predicate that this
square is commutative.
Future work #
Arrow.lean and lifting properties using
The square commutes.
The proposition that a square
W ---f---> X | | g h | | v v Y ---i---> Z
is a commuting square.
The commutative square in the opposite category associated to a commutative square.
The commutative square associated to a commutative square in the opposite category.
- l : B ⟶ X
The upper left triangle commutes.
The lower right triangle commutes.
Now we consider a square:
A ---f---> X | | i p | | v v B ---g---> Y
The datum of a lift in a commutative square, i.e. an up-right-diagonal morphism which makes both triangles commute.
LiftStruct for a square and the corresponding square
in the opposite category.
LiftStruct for a square in the oppositive category and
the corresponding square in the original category.
Square has a
The assertion that a square has a
A choice of a diagonal morphism that is part of a
the square has a lift.