13 lines
497 B
Agda
13 lines
497 B
Agda
module 1FundamentalGroup.Preambles.P0 where
|
||
|
||
open import Cubical.Data.Empty using (⊥) public
|
||
open import Cubical.Data.Unit renaming ( Unit to ⊤ ) public
|
||
open import Cubical.Data.Bool hiding (elim) public
|
||
open import Cubical.Foundations.Prelude
|
||
renaming ( subst to endPt
|
||
; transport to pathToFun
|
||
) public
|
||
open import Cubical.Foundations.Isomorphism renaming ( Iso to _≅_ ) public
|
||
open import Cubical.Foundations.Path public
|
||
open import Cubical.HITs.S1 public
|