Skip to content

Commit

Permalink
Run the new autoformatter on all files
Browse files Browse the repository at this point in the history
  • Loading branch information
aabounegm committed Dec 5, 2023
1 parent 7243b19 commit 1622b94
Show file tree
Hide file tree
Showing 24 changed files with 3,530 additions and 3,479 deletions.
8 changes: 4 additions & 4 deletions src/hott/00-common.rzk.md
Original file line number Diff line number Diff line change
Expand Up @@ -90,20 +90,20 @@ The following demonstrates the syntax for constructing terms in Sigma types:
```rzk
#def Map
: U
:= Σ ((A',A) : product U U) , (A' → A)
:= Σ ((A' , A) : product U U) , (A' → A)
#def the-map-Map
( ((A',A),α) : Map)
( ( ( A' , A) , α) : Map)
: A' → A
:= α
#def the-domain-Map
( ((A',_),_) : Map)
( ( ( A' , _) , _) : Map)
: U
:= A'
#def the-codomain-Map
( ((_,A),_) : Map)
( ( ( _ , A) , _) : Map)
: U
:= A
```
Loading

0 comments on commit 1622b94

Please sign in to comment.