Murat Kasimov

More about me

Я language (β)

/Я language (β)/Morphisms/field/

Based on provided type this Arrow morphism will try to give you an access to an item within some Product.

> field @i : ( i `P` ii ) `AR___` i `P` ( i `AR___` i `P` ii ) > field @ii : ( i `P` ii ) `AR___` ii `P` ( ii `AR___` i `P` ii )

Since products could be inductively defined, it's also possible to get an access to deeply nested items:

> field @i : ( i `P` ii `P` iii ) `AR___` i `P` ( i `AR___` i `P` ii `P` iii ) > field @ii : ( i `P` ii `P` iii ) `AR___` ii `P` ( ii `AR___` i `P` ii `P` iii ) > field @iii : ( i `P` ii `P` iii ) `AR___` iii `P` ( iii `AR___` i `P` ii `P` iii )

You can subtype this Arrow morphism into Scope:

> Scope `hc` field @i : i `P` ii `AT___` i > Scope `hc` field @ii : i `P` ii `AT__` ii > Scope `hc` field @i : i `P` ii `P` iii `AT___` i > Scope `hc` field @ii : i `P` ii `P` iii `AT__` ii > Scope `hc` field @iii : i `P` ii `P` iii `AT__` iii