gistfile1.txt

import analysis.topology.continuity 

universes u v 

local attribute [class] topological_space.is_open 

structure presheaf_of_types (α : Type*) [T : topological_space α] := 
(F : Π U : set α, T.is_open U → Type*)
(res : ∀ (U V : set α) (OU : T.is_open U) (OV : T.is_open V) (H : V ⊆ U), 
  (F U OU) → (F V OV))
(Hcomp : ∀ (U V W : set α) (OU : T.is_open U) (OV : T.is_open V) (OW : T.is_open W)
  (HUV : V ⊆ U) (HVW : W ⊆ V),
  (res U W OU OW (set.subset.trans HVW HUV)) = (res V W OV _ HVW) ∘ (res U V _ _ HUV) )

definition presheaf_of_types_pushforward
  {α : Type*} [Tα : topological_space α]
  {β : Type*} [Tβ : topological_space β]
  (f : α → β)
  (fcont: continuous f)
  (FPT : presheaf_of_types α)
  : presheaf_of_types β :=
  { F := λ V OV, FPT.F (f ⁻¹' V) (fcont V OV),
    res := λ V₁ V₂ OV₁ OV₂ H, 
    FPT.res (f ⁻¹' V₁) (f⁻¹' V₂) (fcont V₁ OV₁) (fcont V₂ OV₂) (λ x Hx,H Hx),
    Hcomp := λ Uβ Vβ Wβ OUβ OVβ OWβ HUV HVW,rfl -- assertion violation
  }