Skip to content

Latest commit

 

History

History
18 lines (10 loc) · 687 Bytes

ReadingNotes.md

File metadata and controls

18 lines (10 loc) · 687 Bytes

4.2 Subtyping

Binary relation - Wikipedia

is the least reflexive binary relation

Reflexive: for all x in X, xRx. Least?

[Reflexive relation

The reflexive closure ≃ of a binary relation ~ on a set X is the smallest reflexive relation on X that is a superset of . Equivalently, it is the union of ~ and the identity relation on X, formally: (≃) = () ∪ (=). For example, the reflexive closure of (<) is (≤).

largest relation between session types coinductively defined

Chapter 21: Metatheory of Recursive Types

21.1 Induction and Coinduction