Calle Sönne

> @callesonne, just checking if there's been any progress on this, if there are any blockers, or if you want help with it. No progress sadly, I was busy with...

Okay, I've made some changes now. ~~One thing to note is that the file is significantly slower than before on my computer, but maybe this doesn't matter so much~~ (this...

> > One thought I just had, is that maybe it could be a good idea to add the class `IsObjLift`, which would allow type-class inference to infer `domain_eq` and...

I have now fixed your comments, as well as redefined `IsHomLift` using inductive types as in the zulip thread. I also added a macro `subst_hom_lift` to make the substitution a...

I'm not convinced about using `IsHomLift` as a class anymore, basically for the following two reasons: 1. `IsHomLift p f φ` makes it so that I can leave parameters `p,...

Okay, this makes sense. I think the times I have encountered it has all been in short term-mode proofs, when I had to change the proof from 1 to 2...

I also have a question about design approach @joelriou . In [https://github.com/Paul-Lez/Stacks-project](https://github.com/Paul-Lez/Stacks-project), we have a notion of `BasedCategory` defined as follows: ``` /-- A based category over `𝒮` is a...

Here is an update on this PR. I have split it into 4 smaller PRs. This one now only concerns the definition of a fibered category, defined as in SGA,...

Now that I have added Lax functors, I think this should be rewritten so that Strong natural transformations of Pseudofunctors are not defined to be strong natural tranformations of the...

> Do we agree that `OplaxFunctor.StrongOplaxTrans` and `PseudoFunctor.StrongTrans` are exactly the same structure, up to replacing `OplaxFunctor` with `PseudoFunctor`? > Another equivalent way of defining `StrongTrans` between pseudofunctors would be...