9 lines
170 B
Text
9 lines
170 B
Text
import types.trunc types.arrow_2 types.fiber homotopy.susp homotopy.circle
|
|
|
|
open eq is_trunc is_equiv nat equiv trunc function fiber circle
|
|
|
|
namespace clive
|
|
|
|
|
|
|
|
end clive
|