型理論における型が同じと同型は同じかどうか

型理論における型と代数学で言う同型は同じかどうか

Martin-Löf型理論からいろいろ引っ張ってくれば良さそう

同型射も使いそう

圏論も交えると上手いこと言えそう

同型射は圏論の言葉だった

圏論を交える場合、型と圏論における、同値関係とか同型を確認しないといけない？

同型

$ a ≅ b である$ f : a → b，g : b → a が存在して $ g \circ f = 1_a かつ f \circ g = 1_b

code:Haskell

i2i_f :: Int -> Int

i2i_g :: Int -> Int

f :: a -> b

g :: b -> a

-- h1 = g ◯ f

h1 = g . f

-- h2 = f ◯ g

h2 = f . g