<ski> tolarz : hm, you're sortof dividing by the projection
7:32 PM → gb73d, bdonnahue1, jellie, Kasadkad and \Kalascus joined  ⇐ gb73dx, bliminse, CGILightning, Bad_K4rMa, Cherenkov, Nalt| and OEIRIAS quit  ↔ mivan0v popped in  ↔ SwiftMatt and sanbot nipped out
7:52 PM <tolarz> ski: yes
7:52 PM <tolarz> ski: in fact, this (f // relation) is some universal morphism when phrased categorically
7:53 PM <tolarz> but I am sure you know this
7:54 PM → OERIAS joined (~OERIAS@066-214-235-231.res.spectrum.com)
7:56 PM <tolarz> Today I realized, there are multiple ways to formalize quotient types.
7:56 PM ⇐ ski quit (~ski@nc-2504-30.studat.chalmers.se) Ping timeout: 256 seconds
7:56 PM <tolarz> One way gives you an accessor ι: A/~ -> A. That way, you can easily define, say + on Z/NZ, via:  plus(a, b) := π(ιa + ιb)
7:57 PM ⇐ sanbot quit (~sanbot@42.107.84.18) Read error: Connection reset by peer
7:57 PM <tolarz>   where π: A -> A/~ is the projection
7:57 PM <tolarz>   Mathematicians now often want to immediately prove well-definedness. But with such a ι constructor it's not necessary.
7:58 PM ⇐ jellie quit (~zipper@unaffiliated/zipper) Quit: WeeChat 3.0
7:58 PM <tolarz>   However, this ι is not computationally useful: you cannot reduce plus(π 1, π 2)
7:59 PM <tolarz> Another way to do quotient types it to have a constructor, which given f: A -> B and a proof that ∀a a'. a ~ a' => f(a) = f(a'), gives you a function f*: A/~ -> B
7:59 PM <tolarz>   This way can be paired with a computation rule: f* (π x) = f x
8:00 PM <tolarz>   And we can define plus as follows: plus : Z/NZ -> Z/NZ := (λa b: Z. a + b, proof of well-definedness)*
8:00 PM <tolarz>   Then, plus(π 1, π 2) = 1 + 2 by the computation rule
8:00 PM → illustion joined  ⇐ Atque and rubiksdream6 quit
8:01 PM <tolarz> damn, ski left
8:01 PM → moo joined (~wootehfoo@unaffiliated/wootehfoot)
8:02 PM <tolarz> Anyone else knows what I am talking about?
8:02 PM <hammond> is there another way to call a sign?
8:02 PM <tolarz> Any inputs appreciated :)
8:02 PM <hammond> like - +
8:02 PM ⇐ math705 quit (~junior@201.150.126.246) Quit: Leaving.
8:02 PM <hammond> in front of an int. I'm using direction, or ....
8:03 PM ⇐ Newami quit (~Newami@ip70-179-45-125.sd.sd.cox.net) Read error: Connection reset by peer
8:03 PM <mawk> sign
8:03 PM → nummereinsnerd joined  ⇐ SwiftMatt quit
8:03 PM <joel135> i have heard quotienting is problematic
8:03 PM <hammond> mawk other than sign.
8:03 PM <mawk> but sign is perfect
8:04 PM <joel135> in agda's implementation of homotopy type theory  the inductive types support adding equalities between terms
8:04 PM <hammond> sign can be a road sign. depending on the context.
8:04 PM → Newami joined (~Newami@ip70-179-45-125.sd.sd.cox.net)
8:04 PM <mawk> "angle" or "direction" too
8:04 PM ⇐ Newami quit (~Newami@ip70-179-45-125.sd.sd.cox.net) Client Quit
8:05 PM <tolarz> Public Service Announcement: https://q.uiver.app/ is a tool for drawing commutative diagrams. If you know https://tikzcd.yichuanshen.de/, then this is a deluxe variant