---

Step * 1 of Lemma perm_morph_wf


1. S : Type
2. T : Type
3. s2t : S ⟶ T
4. t2s : T ⟶ S
5. InvFuns(S;T;s2t;t2s)
6. p : Perm(S)
⊢ InvFuns(T;T;s2t o (p.f o t2s);s2t o (p.b o t2s))
BY
{ ((AddProperties 6 THENA Auto) THEN (D 7 THEN D 5) THEN D 0) }

1
1. S : Type
2. T : Type
3. s2t : S ⟶ T
4. t2s : T ⟶ S
5. (t2s o s2t) = Id{S} ∈ (S ⟶ S)
6. (s2t o t2s) = Id{T} ∈ (T ⟶ T)
7. p : Perm(S)
8. (p.b o p.f) = Id{S} ∈ (S ⟶ S)
9. (p.f o p.b) = Id{S} ∈ (S ⟶ S)
⊢ ((s2t o (p.b o t2s)) o (s2t o (p.f o t2s))) = Id{T} ∈ (T ⟶ T)

2
1. S : Type
2. T : Type
3. s2t : S ⟶ T
4. t2s : T ⟶ S
5. (t2s o s2t) = Id{S} ∈ (S ⟶ S)
6. (s2t o t2s) = Id{T} ∈ (T ⟶ T)
7. p : Perm(S)
8. (p.b o p.f) = Id{S} ∈ (S ⟶ S)
9. (p.f o p.b) = Id{S} ∈ (S ⟶ S)
⊢ ((s2t o (p.f o t2s)) o (s2t o (p.b o t2s))) = Id{T} ∈ (T ⟶ T)

---

Latex:

---

Latex:

1.  S  :  Type
2.  T  :  Type
3.  s2t  :  S  {}\mrightarrow{}  T
4.  t2s  :  T  {}\mrightarrow{}  S
5.  InvFuns(S;T;s2t;t2s)
6.  p  :  Perm(S)
\mvdash{}  InvFuns(T;T;s2t  o  (p.f  o  t2s);s2t  o  (p.b  o  t2s))


By

---

Latex:
((AddProperties  6  THENA  Auto)  THEN  (D  7  THEN  D  5)  THEN  D  0)

---

Home Index