Add code for generating and working with quotients

statebox / idris-ct

formally verified category theory library

GNU Affero General Public License v3.0

259 stars 23 forks source link

Add code for generating and working with quotients #43

Open WhatisRT opened 5 years ago

WhatisRT commented 5 years ago

This adds some generic code for dealing with (extensional) quotients

clayrat commented 5 years ago

I'm not sure where are you using Singleton, but there's an interface for such things in contrib: https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Interfaces/Proposition.idr

WhatisRT commented 5 years ago

Oh, Singleton is a leftover from a previous try. Good to know that Proposition is a thing!

WhatisRT commented 5 years ago

I'm not sure what you mean by 'the commuting triangle in exists would commute pointwise'.

As for the dependent pair, do you mean that it would be nicer if we didn't have to write fst $ exists ...? In that case, I'd just define another function.