Conceptual covers

A conceptual cover is a set of concepts, intensions from an index type to a domain of values, representing an agent's ways of identifying the values: the covers of [Alo01], the acquaintance relations of [Lew79a] and [CvS82] read through the concept that identifies the res, the cover-relative belief of [Dek12], and the time-concepts of [Hei94a] and [Abu97] with contexts as indices and times as values. A value is acquainted at an index when some concept in the cover picks it out there (Cover.Acquainted, membership in an image), and a cover is exhaustive on a domain when every value in it is picked out at every index (Cover.IsExhaustiveOn, Set.SurjOn at each index). The name cover identifies each value of a domain by its constant concept (Cover.names): its concepts are rigid (Cover.isRigid_of_mem_names), it is exhaustive on its domain (Cover.names_isExhaustiveOn), and it acquaints with every value of the domain at every index (Cover.names_acquainted).

References

• [Alo01]
• [Lew79a]
• [CvS82]
• [Hei94a]
• [Abu97]
• [Dek12]

@[reducible, inline]

abbrev Reference.Cover (Idx : Type u_1) (Res : Type u_2) : Type (max u_1 u_2)

A conceptual cover: a set of concepts from indices to values.

Equations

• Reference.Cover Idx Res = Set (Idx → Res)

def Reference.Cover.IsExhaustiveOn {Idx : Type u_1} {Res : Type u_2} (C : Cover Idx Res) (dom : Set Res) : Prop

A cover is exhaustive on dom when at every index every value of dom is picked out by some concept in it.

Equations

• C.IsExhaustiveOn dom = ∀ (p : Idx), Set.SurjOn (fun (x : Idx → Res) => x p) C dom

def Reference.Cover.Acquainted {Idx : Type u_1} {Res : Type u_2} (C : Cover Idx Res) (r : Res) (p : Idx) : Prop

r is acquainted at p through C when some concept in C picks it out at p.

Equations

• C.Acquainted r p = (r ∈ (fun (x : Idx → Res) => x p) '' C)

def Reference.Cover.names {Idx : Type u_1} {Res : Type u_2} (dom : Set Res) : Cover Idx Res

The name cover of a domain: each value identified by its constant concept.

Equations

• Reference.Cover.names dom = (fun (r : Res) (x : Idx) => r) '' dom

theorem Reference.Cover.isRigid_of_mem_names {Idx : Type u_1} {Res : Type u_2} {dom : Set Res} {c : Idx → Res} (h : c ∈ names dom) : IsRigid c

theorem Reference.Cover.names_isExhaustiveOn {Idx : Type u_1} {Res : Type u_2} {dom : Set Res} : (names dom).IsExhaustiveOn dom

theorem Reference.Cover.names_acquainted {Idx : Type u_1} {Res : Type u_2} {dom : Set Res} {r : Res} {p : Idx} (hr : r ∈ dom) : (names dom).Acquainted r p