• Porting status
• Porting procedure
• High level
• Details
• Some common fixes
• Workarounds for temporary issues
• Equiv to ↑(RelIso.toRelEmbedding e).toEmbedding
• HPow and coersion
• Linting
• Aligning names
• Naming convention
• Examples
• Further conventions
• irreducible_def
• Type Classes
• Categories
• Coercions
• Consequences for porting
• Coercion tag
• Known tactic issues
• change ... with .../change ... at ...
• to_additive issues
• Tips and tricks
• Auto-implicits
• Finding instances
• Reviewing and merging PRs