case mp
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
⊢ IsIdempotentComplete C → IsIdempotentComplete D

case mpr
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
⊢ IsIdempotentComplete D → IsIdempotentComplete C
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
⊢ IsIdempotentComplete C ↔ IsIdempotentComplete D
constructor
no goals
case mp
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
⊢ IsIdempotentComplete C → IsIdempotentComplete D
exact Equivalence.isIdempotentComplete ε
no goals
case mpr
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
⊢ IsIdempotentComplete D → IsIdempotentComplete C
exact Equivalence.isIdempotentComplete ε.symm