| λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 . λ x5 : ι → ι . λ x6 x7 . λ x8 : ι → ι → ι → ι . λ x9 : ι → ι → ι → ι → ι → ι → ι . and (and (and (MetaCat_terminal_p x0 x1 x2 x3 x4 x5) (x0 x6)) (x1 x4 x6 x7)) (∀ x10 x11 x12 . MetaCat_monic_p x0 x1 x2 x3 x10 x11 x12 ⟶ and (x1 x11 x6 (x8 x10 x11 x12)) (MetaCat_pullback_p x0 x1 x2 x3 x4 x11 x6 x7 (x8 x10 x11 x12) x10 (x5 x10) x12 (x9 x10 x11 x12))) |
|
| type |
|---|
| (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ι → ι → (ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο |
|
|
| name |
|---|
| MetaCat_subobject_classifier_p |
|
|
|
|
|
|
|