Skip to main content

Questions tagged [proof-review]

For questions that ask about possible improvements of a working piece of a proof. Make sure to also include the tag for the language used, and follow that tag's guidance regarding additional version-specific tags.

1 question with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
3 votes
0 answers
100 views

Using crude but effective stratification & cong to implement transitivity of `=`

Suppose I have cong : {A B : Type} (f : A -> B) (p : a = b) : f a = f b coe : (A : I -> Type) -> A 0 -> A 1 It is ...
ice1000's user avatar
  • 6,166