Skip to main content
Proof Assistants Beta

All Questions

Ask Question
Tagged with
1 question
Newest Active Bountied Unanswered
3 votes
0 answers
102 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
ice1000♦
  • 6,306