Skip to content

Commit

Permalink
formatting+settings
Browse files Browse the repository at this point in the history
  • Loading branch information
thchatzidiamantis committed Jul 15, 2024
1 parent 07bcfee commit 32dd953
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 4 deletions.
3 changes: 1 addition & 2 deletions .vscode/settings.json
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,5 @@
"editor.detectIndentation": false,
"editor.insertSpaces": true
},
"rzk.format.enable": true,
"agdaMode.connection.agdaLanguageServer": true
"rzk.format.enable": true
}
4 changes: 2 additions & 2 deletions src/simplicial-hott/08-covariant.rzk.md
Original file line number Diff line number Diff line change
Expand Up @@ -469,8 +469,8 @@ Segal, then so is `Σ A, C`.

## Dependent composition

In a covariant family over a Segal type, we will define dependent composition
of arrows. We first apply the result that the total type is Segal as follows.
In a covariant family over a Segal type, we will define dependent composition of
arrows. We first apply the result that the total type is Segal as follows.

```rzk
#def is-contr-horn-ext-is-covariant-family-is-segal-base uses (extext)
Expand Down

0 comments on commit 32dd953

Please sign in to comment.