Thm* n:{1...}, A:Type, R:(AAProp). (n ~ A) (EquivRel x,y:A. x R y) (x,y:A. Dec(x R y)) (m:(n+1). m ~ (x,y:A//(x R y))) quotient_of_finite

Thm* (A ~ B) (B ~ C) (A ~ C) one_one_corr_tran

Thm* (A ~ B) (B ~ A) one_one_corr_symm

Thm* A ~ A one_one_corr_refl

Thm* R:(TTProp). (EquivRel x,y:T. x R y) (Q:((x,y:T//(x R y))(x,y:T//(x R y))Prop). (EquivRel u,v:x,y:T//(x R y). u Q v) ((x,y:T//(x Q y)) ~ (u,v:(x,y:T//(x R y))//(u Q v)))) quo_of_quo

Thm* n:{1...}, E:(nnProp). (EquivRel x,y:n. x E y) & (x,y:n. Dec(x E y)) (m:(n+1). m ~ (i,j:n//(i E j))) quotient_of_nsubn

In prior sections: fun 1