A TwoBase is the specification of an internal domain and an internal codomain.

The object A selects the internal domain, the object B selects the internal codomain.

Don't confuse the 2-base of an exponential object with the base of its 2-cone. The 2-base selects the internal domain and internal codomain of the exponential object. The base of the 2-cone selects the power object and the internal domain.

A Tripod is a 2-cone on the power object and the internal domain, and an evaluation map from the apex of the 2-cone to the internal codomain.

Tripod is private, use smart constructor tripod which checks the structure of the Tripod or use unsafeTripod if you know that the evalMap has the apex of the twoCone as a source.

In the base of the cone, the power object should be the image of A and the internal domain should be the image of B.

The evaluation map should go from the apex of the 2-cone to the internal codomain

Return the internal domain leg of a Tripod.

Return the internal codomain leg of a Tripod.

Return the power object leg of a Tripod.

Return the internal domain of a Tripod.

Return the internal codomain of a Tripod.

Return the power object of a Tripod.

Return the category in which a Tripod lives.

Smart constructor of Tripod, checks that the apex of the twoCone is the source of the evalMap.

Construct a Tripod without checking the sructure of the Tripod, use with caution.

For a category to be cartesian closed, we need to construct 2-products.

For a Category parametrized over a type t, the power object of an exponential object of a 2-base will contain ExponentialElement constructions (an exponential element is a mapping). A given mapping has as domain and codomain values Exprojections.

For example, in FinSet, let's consider the 2-base selecting {1,2} and {3,4} as internal domain and codomain. The power object of the 2-base is {{1->3,2->3},{1->3,2->4},{1->4,2->3},{1->4,2->4}}, note that it is not an object of (Finset Int) but an object of (FinSet (Set (Map Int))). The Exponential type allows to construct type (FinSet (Exponential Int)) in which we can consider the original objects with Exprojection and the new mappings with ExponentialElement. Here, instead of mappings, we can construct the type (FinSet (Set (Exponential Int))), a mapping is then (ExponentialElement (weakMap [(1,3),(2,3)])). We can construct exprojections in the same category, for example along A which will map (ExponentialElement (weakMap [(1,3),(2,3)])) to (set [Exprojection 1, Exprojection 2]).

Remove the constructor Exprojection from an original object t, throws an error if an ExponentialElement is given.

For a category to be cartesian closed, we need to construct 2-products of exponential objects with exprojected objects.

Return wether a Tripod is a candidate exponential object or not. A Tripod is a candidate exponential object if its twoCone is a limit. Tests if the 2-cone is a 2-product by computing the limits in the universe category with the function limits : it is slow.

A CandidateExponentialObject is a Tripod such that its twoCone is a limit.

A CandidateExponentialObjectMorphism is a morphism between two CandidateExponentialObjects. It is private, use smart constructors candidateExponentialObjectMorphism and unsafeCandidateExponentialObjectMorphism to instantiate.

Smart constructor for CandidateExponentialObjectMorphism. Checks wether the transpose has valid domain and valid codomain.

Unsafe version of candidateExponentialObjectMorphism, use with caution as it does not check wether the transpose has valid domain and valid codomain.

Return the exponential objects of a given 2-base.