Type constructor for one obj but not the other?

Stream: general

[debord]

Hello. Here's the most MWE I can get from the context I'm working in:

import Mathlib.CategoryTheory.Products.Bifunctor

open CategoryTheory

universe v₁ u₁

variable (𝒞 : Type u₁) [Category.{v₁} 𝒞]

structure CatObj where
  F : 𝒞⥤ 𝒞

structure CatHom (F F' : CatObj 𝒞) where
  θ : NatTrans F.F F'.F

instance Cat : Category (CatObj 𝒞) where
  Hom X Y := CatHom 𝒞 X Y
  id := sorry
  comp := sorry
  id_comp := sorry
  comp_id := sorry
  assoc := sorry

instance TPObj (F F' : CatObj 𝒞) : CatObj 𝒞 where
  F := F'.F ⋙ F.F

instance TPMapTheta (θ : F ⟶ F') (θ' : G ⟶ G') : NatTrans (TPObj 𝒞 F G).F (TPObj 𝒞 F' G').F where
  app A := θ.θ.app (G.F.obj A) ≫ F'.F.map (θ'.θ.app A)
  naturality := sorry

instance TPMap (θ : F ⟶ F') (θ' : G ⟶ G') : (TPObj 𝒞 F G) ⟶ (TPObj 𝒞 F' G') where
  θ := TPMapTheta 𝒞 θ θ'

instance TP : ((CatObj 𝒞) × (CatObj 𝒞)) ⥤ (CatObj 𝒞) where
  obj C := TPObj 𝒞 C.1 C.2
  map F := TPMap 𝒞 F.1 F.2
  map_id X :=  by
    simp
    #check (TPMap 𝒞 (𝟙 X.1) (𝟙 X.2))
    #check 𝟙 (TPObj 𝒞 X.1 X.2)
    #check (TPMap 𝒞 (𝟙 X.1) (𝟙 X.2)).θ
    #check (𝟙 (TPObj 𝒞 X.1 X.2)).θ

In the proof of map_id, why exactly is it the case that (TPMap 𝒞 (𝟙 X.1) (𝟙 X.2)) and 𝟙 (TPObj 𝒞 X.1 X.2) are both objects of type TPObj 𝒞 X.1 X.2 ⟶ TPObj 𝒞 X.1 X.2, and therefore should have the θ constructor from CatHom, and (TPmap 𝒞 (𝟙 X.1) (𝟙 X.2)).θ does indeed correctly check to have type NatTrans (TPObj 𝒞 X.1 X.2).F (TPObj 𝒞 X.1 X.2).F, but (𝟙 (TPObj 𝒞 X.1 X.2)).θ errors with

invalid field 'θ', the environment does not contain 'Quiver.Hom.θ'
  𝟙 (TPObj 𝒞 X.1 X.2)
has type
  TPObj 𝒞 X.1 X.2 ⟶ TPObj 𝒞 X.1 X.2

and

invalid field notation, type is not of the form (C ...) where C is a constant
  𝟙 (TPObj 𝒞 X.1 X.2)
has type
  CategoryStruct.toQuiver.1 (TPObj 𝒞 X.1 X.2) (TPObj 𝒞 X.1 X.2)

They're the same type, so why is the constructor accessible for one but not the other? What is even happening in the second error message, why is it occurring?

[Kim Morrison]

Surely

instance TPObj (F F' : CatObj 𝒞) : CatObj 𝒞 where
  F := F'.F ⋙ F.F

is wrong. This isn't a class, so you shouldn't be defining instances of it.

[Kim Morrison]

The problem is just that dot notation here doesn't know which structures to looking for the theta field in.

    #check CatHom.θ (𝟙 (TPObj 𝒞 X.1 X.2))

works fine.

[debord]

Ah, so it was that simple. Thank you, I managed to prove the theorem now. Thank you also for the tip on the instances, I had them as def at one point but I changed a lot of stuff while just trying things troubleshooting.