Categorical crypto improvements#25

Open

WhatisRT wants to merge 33 commits intomainfrom

andre/monoidal-coherence

Commits on Sep 12, 2025

Commits on Sep 15, 2025

proceeding with the logics on channels

mmontin
authored and
WhatisRT
committed
tmp inference issue

mmontin
authored and
WhatisRT
committed
cleaning up + more properties

mmontin
authored and
WhatisRT
committed
Channels commented and in their own file

mmontin
authored and
WhatisRT
committed
tmp does it solve all problems?

mmontin
authored and
WhatisRT
committed
more refactoring, starting the examples

mmontin
authored and
WhatisRT
committed
CategoricalCrypto/Base.agda to CategoricalCrypto/Machine.agda

mmontin
authored and
WhatisRT
committed
Adapting examples (with injectors)

mmontin
authored and
WhatisRT
committed
basic broadcast updated

mmontin
authored and
WhatisRT
committed
Protocol.agda updated

mmontin
authored and
WhatisRT
committed
everything type checks

mmontin
authored and
WhatisRT
committed
typos

mmontin
authored and
WhatisRT
committed
$ typo

mmontin
authored and
WhatisRT
committed
Adversarial patterin in its own module

mmontin
authored and
WhatisRT
committed
drafting automated channels proofs

mmontin
authored and
WhatisRT
committed
nicer fixity and proofs

mmontin
authored and
WhatisRT
committed
alias for lift

mmontin
authored and
WhatisRT
committed
more operators + example

mmontin
authored and
WhatisRT
committed
small tweak

mmontin
authored and
WhatisRT
committed
Channels form a category

mmontin
authored and
WhatisRT
committed
laying out things nicely

mmontin
authored and
WhatisRT
committed
Using automated generation of proofs everywhere

mmontin
authored and
WhatisRT
committed
Fix Short Leios spec & the trace verified for Linear Leios
WhatisRT
committed
more category elements

mmontin
authored and
WhatisRT
committed
laying out definitions nicely

mmontin
authored and
WhatisRT
committed

Commits on Sep 16, 2025

coproduct of tensorial product

mmontin
authored and
WhatisRT
committed
deducing things for being cocartesian

mmontin
authored and
WhatisRT
committed
deducing bifunctor as well

mmontin
authored and
WhatisRT
committed
Use the new channels in Short Leios
WhatisRT
committed