Update chapters 4 and 5

UniMath / SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.

Creative Commons Attribution Share Alike 4.0 International

378 stars 22 forks source link

Update chapters 4 and 5 #61

Open UlrikBuchholtz opened 4 years ago

UlrikBuchholtz commented 4 years ago

I've now closed issue #45 as settled. This means we should now go through Ch. 4+5 and update the exposition where needed. (Dan already fixed a lot of the formulas.)

DanGrayson commented 4 years ago

Yes.

One at a time, I guess, starting with the assignee.

marcbezem commented 4 years ago

For example, we now need to define composition of homomorphisms. A good place would be after Remark 4.3.2. Something like: For f: Hom(F,G) and g: Hom(G,H) we define the composition gf by induction, setting (\mkhom\Bg)(\mkhom\Bf) \defeq \mkhom(\Bg\Bf). Here \Bg\Bf is the composition of pointed maps defined in \cref{def:pointedtypes}.