search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
362 stars 68 forks source link

Define Lifting Properties #333

Closed TOTBWF closed 2 years ago

TOTBWF commented 2 years ago

Patch Description

This PR defines Lifting Properties, Injective and Projective Morphisms, and also proves a pile of lemmas about them.

Notes

I often find myself looking for the following definition, so I've added it:

record IsIso (from : A ⇒ B) : Set (ℓ ⊔ e) where
  field
    inv : B ⇒ A
    iso : Iso from inv 

  open Iso iso public

This does somewhat violate the naming scheme we use in the library, but it lines up with the literature so I think it's a reasonable name.

I've also been using Retract Arrow for retracts of morphisms, which feels a bit klunky? Perhaps it might make sense to define that notion on it's own.

JacquesCarette commented 2 years ago

Also: I'm fine with IsIso. I don't have a better suggestion for Retract Arrow.

JacquesCarette commented 2 years ago

Sorry to take so long, I've been swamped.

TOTBWF commented 2 years ago

No worries, so have I!