Add discrete categories

[barrettj12]

I've defined discrete categories using Hom[ x , y ] = x ≡ y.

I'm now trying to show that a function f : A → ob C determines a Functor (Discrete A) C, but I'm having trouble showing that this preserves composition. Maybe someone else can help.

[kangxyz]

I think you can use J-rule twice, so you only need to treat composition of identity morphisms.

[barrettj12]

Makes sense, but I'm not quite sure how to apply J here.

I think the problem might be that given p : x ≡ y and q : y ≡ z

• F p and F (p ∙ q) are obtained by transport from id {F x}
• F q is obtained from id {F y}

so it's not clear how to compose them.

[mortberg]

Just a name change suggestion