I have two theories B and C both including a common theory A. My goal is to specify a view BC: B → C in a convenient way without providing mappings for all constants in A.
fixmeta ur:?LF ❚
theory A =
a : type ❙
❚
theory B =
include ?A ❙
b : type ❙
❚
theory C =
include ?A ❙
c : type ❙
❚
view BC : ?B → ?C =
// do I need to map all constants of A here? ❙
b = c ❙
❚
Currently, BC is not total, e.g. the constant a from A has no mapping.
I would like to not have to care about A when defining BC and just map every constant in the A from B to the identical constant in A from C.
Is this possible? Is there some sort of identity-view from A to A that can just be included into BC?
Solution.
view BC : ?B → ?C =
include ?A ❙
b = c ❙
❚
Explanation. The syntax include ?A ❙ in your theories B and C, besides other things, also acts as a normal declaration in the same way as constant declarations are declarations. For views to be valid, all undefined declarations of the domain theory need to be mapped to something. In particular, include declarations need to be mapped to morphisms, which describe the morphism action to be inherited and applied on for the included part of the domain.
Hence, you can achieve mapping all declarations in A to themselves by mapping include ?A to the identity morphism on A, which exactly represents the desired mapping. In MMT surface syntax, this can be achieved via include ?A ❘ = IDENTITY ?A, or equivalently, by the synactic sugar include ?A.
In general, if you got a view v: B → C and B includes A, then v must map include ?A to a morphism A → C. Above, we mapped it to a morphism A → A (namely, the identity), which is also a morphism of the form A → C since A is included in C.
See the second reference below on gluing inclusions in structures for an example where the assigned morphism is not the identity.
Further references.