namespace latin:/❚
fixmeta ur:?PLF❚
theory OneTyped =
carrier : type❙
❚
theory Relation =
include ?OneTyped❙
rel : carrier ⟶ carrier ⟶ type❘# 1 $ 2 prec 30❘role Judgment❙
❚
theory Reflexivity =
include ?Relation❙
refl : {x} x$x❙
❚
theory Symmetry =
include ?Relation❙
sym : {x,y} x$y ⟶ y$x❙
❚
theory Transitivity =
include ?Relation❙
trans : {x,y,z} x$y ⟶ y$z ⟶ x$z❘# 4 %n 5❙
trans3 : {w,x,y,z} w$x ⟶ x$y ⟶ y$z ⟶ w$z❘
= [w,x,y,z,p,q,r] p trans q trans r❙
trans4 : {v,w,x,y,z} v$w ⟶ w$x ⟶ x$y ⟶ y$z ⟶ v$z❘
= [v,w,x,y,z,p,q,r,s] trans3 (p trans q) r s❙
❚
theory Preorder =
include ?Reflexivity❙
include ?Transitivity❙
❚
theory EquivalenceRelation =
include ?Preorder❙
include ?Symmetry❙
❚
theory Congruence =
include ?Relation❙
congT: {x,y} x$y ⟶ {T: carrier ⟶ carrier} T x $ T y ❘# 3 congT 4❙
❚
theory EquivalenceCongruence =
include ?EquivalenceRelation❙
include ?Congruence❙
❚
/T Equality is an equivalence-congruence.
But semantic equality is even stronger: it allows substitution in objects of any type so that equal objects can never be distinguished.
This is different from the syntactic equality used inside a logic, where equal objets cannot be distinguished by logical formulas but might be distinguishable by other judgments.❚
theory SemanticEquality =
include ?EquivalenceRelation❙
cong : {x,y} x$y ⟶ {A: carrier ⟶ type} A x ⟶ A y❘# 3 cong 4 5❙
// realizes Congruence❙
congT: {x,y} x$y ⟶ {T: carrier ⟶ carrier} T x $ T y ❘# 3 congT 4❘
= [x,y,p,T] p cong ([u]T x $ T u) refl❙
❚
theory EqualityType =
include ?OneTyped❙
structure equalityRel : ?EquivalenceRelation =
include ?OneTyped❙
rel # 1 = 2❙
refl @ refl❙
sym @ sym❙
trans @ trans❙
trans3 @ trans3❙
trans4 @ trans4❙
❚
❚
theory AntiSymmetry =
include ?EqualityType❙
include ?Relation❙
antisym : {x,y} x$y ⟶ y$x ⟶ x = y❙
❚
theory Order =
include ?Preorder❙
include ?AntiSymmetry❙
❚