In Chapter 1, there is a proposition named interpret_typed_wiring_diagram which includes the text "which interprets a typed wiring diagram as a lens".
The proof of this proposition incorrectly references prop 1.3.3.7 arity_universal_property. Instead, it should reference the equivalent proposition for typed arities: 1.3.3.11 arity_universal_property_typed.
In Chapter 1, there is a proposition named
interpret_typed_wiring_diagramwhich includes the text "which interprets a typed wiring diagram as a lens".The proof of this proposition incorrectly references prop 1.3.3.7
arity_universal_property. Instead, it should reference the equivalent proposition for typed arities: 1.3.3.11arity_universal_property_typed.