istrunc_self_implies_istrunc #2112
Conversation
| Defined. | ||
|
|
||
| (** If a type [A] implies that it is [n.+1]-truncated, then it is [n.+1]-truncated. **) | ||
| Definition istrunc_self_implies_istrunc {n : trunc_index} {A : Type} (H : A -> IsTrunc n.+1 A) |
There was a problem hiding this comment.
I would call this istrunc_inhabited_istrunc drawing inspiration from HProp.v.
There was a problem hiding this comment.
@ThomatoTomato looks like you missed this comment. I'll rename it in another PR.
There was a problem hiding this comment.
haha, whoops. I totally forgot to do that, sorry 😅 Thank you Ali
Alizter
left a comment
There was a problem hiding this comment.
LGTM. Did you find a nice use of this lemma yet? I couldn't think of any truncation proofs that are simplified by knowing you have an inhabitant.
|
I found one place it could potentially be useful in |
|
My motivation to prove this was originally as a stepping stone to |
Added this cute little lemma about truncations that might come in handy. All it says is that a map (A -> istrunc n.+1 A) is sufficient to deduce that A is n+1 truncated.
I wasn't so sure what to name it, so feel free to make it fit into your mold.