HomSet
Posted on March 1, 2020
Tags: typetheory
HomSet in programming terms are simply the types of the functions.
Nested HomSets are simply the types of curried functions.
0.0.1 Translate Homset to function type notation
\[ f :: A \rightarrow B := f \in Hom(A, B) \] \[ f :: A \rightarrow (B \rightarrow C) := f \in Hom(A, Hom(B,C)) \] \[ f :: (A \rightarrow B) \rightarrow C := f \in Hom(Hom(A,B),C) \]
0.0.2 Free Monoid
- object : T
- Morphism : Alphabet = {a,b,c…} map T –> T
- Composition : Append
The Free Monoid on the alphabet results in the set of all possible words/strings created from the alphabet.
0.0.2.0.1 Free monoid on number
Addition mod 2 group is a category
- 1+1 = 0
- 1+0 = 1
Category
- object : T
- morphisms: numbers {0,1}
- composition: addition
- Identity morphism: 0
Checking composition: (1+1)+1 = 1+(1+1)
1 Cubical Type Theory
Interval : Typeis a point on a PathPath (A: Type) (x: A) (y: A) : Type
