Nuprl Lemma : pscm-comp_wf

∀[C:SmallCategory]. ∀[A,B,E:ps_context{j:l}(C)]. ∀[F:psc_map{j:l}(C; A; B)]. ∀[G:psc_map{j:l}(C; B; E)].
  (G o F ∈ psc_map{j:l}(C; A; E))


Proof

Error : references
Latex:
\mforall{}[C:SmallCategory].  \mforall{}[A,B,E:ps\_context\{j:l\}(C)].  \mforall{}[F:psc\_map\{j:l\}(C;  A;  B)].  \mforall{}[G:psc\_map\{j:l\}(C;
                                                                                                                                                                                            B;
                                                                                                                                                                                            E)].
    (G  o  F  \mmember{}  psc\_map\{j:l\}(C;  A;  E))


Date html generated: 2020_05_21-AM-10_29_39
Last ObjectModification: 2020_04_01-AM-10_47_47

Theory : presheaf!models!of!type!theory


Home Index