Connected shapes

In this file we prove that various shapes are connected.

instance CategoryTheory.instIsConnectedWidePullbackShape {J : Type u_1} : CategoryTheory.IsConnected (CategoryTheory.Limits.WidePullbackShape J)

Equations

• ⋯ = ⋯

instance CategoryTheory.instIsConnectedWidePushoutShape {J : Type u_1} : CategoryTheory.IsConnected (CategoryTheory.Limits.WidePushoutShape J)

Equations

• ⋯ = ⋯