A kind of type theory without: Equality reflection or Uniqueness of Identy Proofs See also Axiom of Extensionality Source https://www.youtube.com/watch?v=u92V0OMgvhM&list=PL1-2D_rCQBarjdqnM21sOsx09CtFSVO6Z