I've declared a certain locale which fixes multiple things and am trying to declare a new locale for morphisms of the first. Here's the first locale:
locale presheaf = topology + Ring +
fixes
opcatopensets ::" ('a) PosetalCategory" and
objectsmap :: "'a set ⇒ ('a, 'm) Ring_scheme" and
restrictionsmap:: "('a set ×'a set) ⇒ ('a ⇒ 'a)"
assumes
"opcatopensets ≡ ⦇ Obj = {x. x ∈ T} , Mor = {(x,y)| x y. (x,y) ∈ revpo} ,
Dom = psheafdom , Cod = psheafcod , Id = psheafid , Comp = psheafcomp ⦈" and
"∀y w. w ≠ y ⟶ (psheafcomp (x,y) (w,z) = undefined)" and
"∀x. x ∉ T ⟶ (objectsmap x = undefined)" and
"∀x y.(restrictionsmap (x,y)) ∈ rHom (objectsmap x) (objectsmap y)" and
"∀ x y . (restrictionsmap (x,x) y = y) " and
"∀ x y z . ( (restrictionsmap (y,z))∘(restrictionsmap (x,y)) = restrictionsmap(x,z) )"
At the end of this declaration, I get the following output:
locale presheaf =
fixes T :: "'a set set"
and R :: "('b, 'c) Ring_scheme"
and opcatopensets :: "'a PosetalCategory"
and objectsmap :: "'a set ⇒ ('a, 'm) Ring_scheme"
and restrictionsmap :: "'a set × 'a set ⇒ 'a ⇒ 'a"
assumes "presheaf T R opcatopensets objectsmap restrictionsmap"
So I thought I could extract from the last line what I needed in order to define a new locale involving two instances of the locale "presheaf". This is what I tried:
locale sheafmorphism =
F: presheaf T R opcatopensets F restrictionsmap + G: presheaf T R opcatopensets
G restrictionsmap
for F and G +
fixes morphism :: "'a set ⇒ ('a ⇒ 'a)"
assumes (things)
In short, I want to fix two presheaves F and G and then fix this parameter "morphism" and assume things involving "morphism" and the "restrictionsmap" and "objectsmap" of F and G. This attempt of mine led to:
Illegal free variables in expression: "T", "R", "opcatopensets", "restrictionsmap"
I suppose I don't understand how to do this when the locale you want to instantiate fixes more than one thing. What is causing this error and how could I do what I'd like?