Session 2: Sets, maps, and composition
1. Review of Article I
Excerpt (p. 23)
If we recall that a point of a set A is a map from a singleton set \mathbf{1} to A, we see that there is a simple test for equality of maps of sets {A \xrightarrow{f} B} and {A \xrightarrow{g} B}:
\text{If for each \textit{point}}\; \mathbf{1} \xrightarrow{a} A, f \circ a = g \circ a, \;\text{then}\; f = g.
We generalise to types here.
example {A B : Type} {f g : A ⟶ B}
: (∀ a : Point A, f ⊚ a = g ⊚ a) → f = g := A:TypeB:Typef:A ⟶ Bg:A ⟶ B⊢ (∀ (a : Point A), f ⊚ a = g ⊚ a) → f = g
A:TypeB:Typef:A ⟶ Bg:A ⟶ Bh:∀ (a : Point A), f ⊚ a = g ⊚ a⊢ f = g
A:TypeB:Typef:A ⟶ Bg:A ⟶ Bh:∀ (a : Point A), f ⊚ a = g ⊚ aa':A⊢ f a' = g a'
All goals completed! 🐙