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 ski: yes 7:52 PM ski: in fact, this (f // relation) is some universal morphism when phrased categorically 7:53 PM but I am sure you know this 7:54 PM → OERIAS joined (~OERIAS@066-214-235-231.res.spectrum.com) 7:56 PM 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 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 where π: A -> A/~ is the projection 7:57 PM 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 However, this ι is not computationally useful: you cannot reduce plus(π 1, π 2) 7:59 PM 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 This way can be paired with a computation rule: f* (π x) = f x 8:00 PM And we can define plus as follows: plus : Z/NZ -> Z/NZ := (λa b: Z. a + b, proof of well-definedness)* 8:00 PM Then, plus(π 1, π 2) = 1 + 2 by the computation rule 8:00 PM → illustion joined ⇐ Atque and rubiksdream6 quit 8:01 PM damn, ski left 8:01 PM → moo joined (~wootehfoo@unaffiliated/wootehfoot) 8:02 PM Anyone else knows what I am talking about? 8:02 PM is there another way to call a sign? 8:02 PM Any inputs appreciated :) 8:02 PM like - + 8:02 PM ⇐ math705 quit (~junior@201.150.126.246) Quit: Leaving. 8:02 PM 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 sign 8:03 PM → nummereinsnerd joined ⇐ SwiftMatt quit 8:03 PM i have heard quotienting is problematic 8:03 PM mawk other than sign. 8:03 PM but sign is perfect 8:04 PM in agda's implementation of homotopy type theory the inductive types support adding equalities between terms 8:04 PM 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 "angle" or "direction" too 8:04 PM ⇐ Newami quit (~Newami@ip70-179-45-125.sd.sd.cox.net) Client Quit 8:05 PM 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