Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Define Dagger categories #1201

Open
wants to merge 35 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
35 commits
Select commit Hold shift + click to select a range
c744da6
Create folder for Dagger Categories
anshwad10 Mar 2, 2025
5c8fb22
Add files via upload
anshwad10 Mar 2, 2025
c6f6978
Update Base.agda
anshwad10 Mar 2, 2025
5d787ae
Add files via upload
anshwad10 Mar 2, 2025
10a563e
Update Properties.agda
anshwad10 Mar 2, 2025
35c2601
add syntax for dagger, fix whitespace, other minor improvements
anshwad10 Mar 2, 2025
30658a5
fix whitespace, add more lemmas for univalence
anshwad10 Mar 2, 2025
0bf35c1
Add files via upload
anshwad10 Mar 2, 2025
97dd20e
Dagger functors
anshwad10 Mar 2, 2025
8083a73
`areInv` is a proposition
anshwad10 Mar 2, 2025
3a41cf4
Update Properties.agda
anshwad10 Mar 2, 2025
3f1e345
fix whitespace
anshwad10 Mar 2, 2025
a3daeed
fix whitespace
anshwad10 Mar 2, 2025
f35dca3
remove trailing newlines
anshwad10 Mar 2, 2025
c5e0208
Update Morphism.agda
anshwad10 Mar 2, 2025
b57d802
fix type error
anshwad10 Mar 2, 2025
127a1c7
fix import
anshwad10 Mar 2, 2025
4cd983f
Create Dagger.agda
anshwad10 Mar 2, 2025
c220ad1
Update Properties.agda
anshwad10 Mar 3, 2025
f3bd6f1
undo Update Properties.agda
anshwad10 Mar 3, 2025
bbaa94f
Update Functor.agda
anshwad10 Mar 3, 2025
7d12126
add binary products of dagger categories
anshwad10 Mar 3, 2025
0fd5bb7
Add files via upload
anshwad10 Mar 3, 2025
62ab610
Update Functors.agda
anshwad10 Mar 3, 2025
a82cb33
Update BinProduct.agda
anshwad10 Mar 3, 2025
87678c8
fix whitespace
anshwad10 Mar 3, 2025
251aa71
fix whitespace
anshwad10 Mar 3, 2025
ee66405
fix whitespace
anshwad10 Mar 3, 2025
4327fef
Update Functor.agda
anshwad10 Mar 4, 2025
a76600a
Update Functor.agda
anshwad10 Mar 4, 2025
a5faa06
import Functors.Constant
anshwad10 Mar 4, 2025
c79c8c0
import natural transformations
anshwad10 Mar 4, 2025
9711894
add hidden argument puns
anshwad10 Mar 4, 2025
40f1026
Update Properties.agda
anshwad10 Mar 4, 2025
0a3bbf0
Update Properties.agda
anshwad10 Mar 4, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Create Dagger.agda
anshwad10 authored Mar 2, 2025
commit 4cd983f4e0949f29d0f27ebe0b049c7ee3b772e6
8 changes: 8 additions & 0 deletions Cubical/Categories/Dagger.agda
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
-- Dagger categories
{-# OPTIONS --safe #-}

module Cubical.Categories.Dagger where

open import Cubical.Categories.Dagger.Base public
open import Cubical.Categories.Dagger.Properties public
open import Cubical.Categories.Dagger.Functor public