Skip to content

Instantly share code, notes, and snippets.

@clayrat

clayrat/quad.red

Last active November 6, 2018 15:16
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save clayrat/f0d8a463f8047253a0a40a60c1ee2db0 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save clayrat/f0d8a463f8047253a0a40a60c1ee2db0 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
quad.red
def connection/quad (A : type)
(abx : 𝕀 β†’ A)
(aby : [k] A [k=0 β†’ abx 0 | k=1 β†’ abx 1])
(bax : [k] A [k=0 β†’ abx 1 | k=1 β†’ abx 0])
(bay : [k] A [k=0 β†’ abx 1 | k=1 β†’ abx 0])
(abxy : path (𝕀 β†’ A) abx aby)
(baxy : path (𝕀 β†’ A) bax bay)
: [i j] A [
| i=0 β†’ aby j
| i=1 β†’ bay j
| j=0 β†’ abx i
| j=1 β†’ bax i
]
= Ξ» i j β†’ ?wat
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment