As an application of the dependent Yoneda lemma, one could give a direct (re-)proof of
#def [associative-is-segal](https://rzk-lang.github.io/sHoTT/simplicial-hott/05-segal-types.rzk/#define:associative-is-segal) uses (extext)
( A : U)
( is-segal-A : is-segal A)
( w x y z : A)
( f : hom A w x)
( g : hom A x y)
( h : hom A y z)
: ( comp-is-segal A is-segal-A w y z (comp-is-segal A is-segal-A w x y f g) h)
= ( comp-is-segal A is-segal-A w x z f (comp-is-segal A is-segal-A x y z g h))
by interpreting the type
( y z : A) ->
( g : hom A x y) ->
( h : hom A y z) ->
( comp-is-segal A is-segal-A w y z (comp-is-segal A is-segal-A w x y f g) h)
= ( comp-is-segal A is-segal-A w x z f (comp-is-segal A is-segal-A x y z g h))
as a covariant family over the type coslice A w; here the pair (x , f) is a term of type coslice A w.
As an application of the dependent Yoneda lemma, one could give a direct (re-)proof of
by interpreting the type
as a covariant family over the type
coslice A w; here the pair(x , f)is a term of typecoslice A w.