typal equality (changes) in nLab

judgmental equality of termsidentification between terms reflexivity of judgmental equality of termsidentity identification between terms symmetry of judgmental equality of termsinverse identification between terms transitivity of judgmental equality of termsconcatenation of identifications between terms judgmental equality of typesidentification between types reflexivity of judgmental equality of typesidentity identification between types symmetry of judgmental equality of typesinverse identification between types transitivity of judgmental equality of typesconcatenation of identification between types principle of substitutionaction on identifications