Documentation

InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.CoherentIso

This is the free-living isomorphism as a category with objects called zero and one. Perhaps these should have different names?

Instances For

    The free isomorphism is the codiscrete category on two objects. Can we make this a special case of the other definition?

    Equations
    • One or more equations did not get rendered due to their size.

    Functors out of WalkingIso define isomorphisms in the target category.

    Equations
    Instances For

      From an isomorphism in a category, one can build a functor out of WalkingIso to that category.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For