Metamath Proof Explorer


Theorem sectss

Description: The section relation is a relation between morphisms from X to Y and morphisms from Y to X . (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses issect.b B = Base C
issect.h H = Hom C
issect.o · ˙ = comp C
issect.i 1 ˙ = Id C
issect.s S = Sect C
issect.c φ C Cat
issect.x φ X B
issect.y φ Y B
Assertion sectss φ X S Y X H Y × Y H X

Proof

Step Hyp Ref Expression
1 issect.b B = Base C
2 issect.h H = Hom C
3 issect.o · ˙ = comp C
4 issect.i 1 ˙ = Id C
5 issect.s S = Sect C
6 issect.c φ C Cat
7 issect.x φ X B
8 issect.y φ Y B
9 1 2 3 4 5 6 7 8 sectfval φ X S Y = f g | f X H Y g Y H X g X Y · ˙ X f = 1 ˙ X
10 opabssxp f g | f X H Y g Y H X g X Y · ˙ X f = 1 ˙ X X H Y × Y H X
11 9 10 eqsstrdi φ X S Y X H Y × Y H X