Structures vs defs

struct.lean

-- Version with structure

structure spoint (a : Type*) (b : Type*) := (x : a → a) (y : b)

namespace spoint

variables {a : Type*}
variables {b : Type*}
variables (A : spoint a b)

def is_eq (A : spoint a b) : Prop := A.x = id

#check A.is_eq

end spoint

structure spoint_two (a : Type*) extends spoint a a
namespace spoint_two

variables {a : Type*}
variables (A : spoint_two a)

#check A.to_spoint.is_eq

end spoint_two

-- Version with def


def dpoint (a : Type*) := a → a

namespace dpoint

variables (a : Type*)
variables (b : dpoint a)

def is_eq (b : dpoint a) : Prop := b = id

-- #check b.is_eq -- does not type-check

end dpoint

def dpoint_two (a : Type*) := a → a
namespace dpoint_two

variables (a : Type*)
variables (b : dpoint_two a)


end dpoint_two