Pullback properties

[frederikgebert]

I proved the pasting law for pullbacks and added it to Pullback/Properties.agda.
I'm new to agda, so any feedback is much appreciated. I hope this fits into this library!

[JacquesCarette]

This is generally very nice. Just a few minor comments.

There might be a second round, as some thing might become more obvious once these clean-ups are down.

[frederikgebert]

Thank you for your feedback. I removed all implicit arguments and everything still works. I'm very impressed by Agda's ability to fill in those arguments! I also implemented the other changes you proposed. Everything is so much cleaner now.. :O
I will go through the proof again in the next days to see if I can shorten it by removing unnecessary definitions.

[JacquesCarette]

Don't go overboard on shortening. Sometimes some intermediate definitions are useful for conceptual clarity. But in general, yes, shorter is better.

[frederikgebert]

I removed some definitions that seemed redundant and moved intermediate equations to the definitions that use them. This increases clarity because the typing judgements are much shorter.
I also removed some lines by using pull, push and extend reasoning.
Sorry for basically rewriting the whole proof but I think it makes more sense now.