school/type-theory
2
0
Fork 0
Code Issues 11 Pull requests Actions Packages Projects 1 Releases Wiki Activity

Bi-invertible equivalence #3

New issue
Closed
opened 2023-05-15 05:35:04 +00:00 by michael · 2 comments
michael commented 2023-05-15 05:35:04 +00:00
Owner
Copy link

Use bi-invertible maps to prove that Bool-id is an equivalence

Use bi-invertible maps to prove that Bool-id is an equivalence
michael commented 2023-05-15 19:17:43 +00:00
Author
Owner
Copy link
Bool-id : Bool → Bool
Bool-id true = true
Bool-id false = false

Bool-id-pointwise : (b : Bool) → Bool-id (Bool-id b) ≡ b
Bool-id-pointwise true = refl
Bool-id-pointwise false = refl

Bool-id-equiv : Bool-id ∘ Bool-id ≡ id
Bool-id-equiv = funExt Bool-id-pointwise

Bool-linv : linv Bool-id
Bool-linv .fst = Bool-id
Bool-linv .snd = funExt Bool-id-pointwise

Bool-rinv : rinv Bool-id
Bool-rinv .fst = Bool-id
Bool-rinv .snd = funExt Bool-id-pointwise

Bool-id-biinv : BiInvEquiv Bool Bool
Bool-id-biinv = biInvEquiv
  Bool-id
  Bool-id Bool-id-pointwise
  Bool-id Bool-id-pointwise

Bool-id-iso : Iso Bool Bool
Bool-id-iso = iso
  Bool-id
  Bool-id
  Bool-id-pointwise
  Bool-id-pointwise

Bool-id-biinv-equiv : Bool ≃ Bool
Bool-id-biinv-equiv = Bool-id , isoToIsEquiv Bool-id-iso

Bool-id-path : Bool ≡ Bool
Bool-id-path = ua Bool-id-biinv-equiv
```agda Bool-id : Bool → Bool Bool-id true = true Bool-id false = false Bool-id-pointwise : (b : Bool) → Bool-id (Bool-id b) ≡ b Bool-id-pointwise true = refl Bool-id-pointwise false = refl Bool-id-equiv : Bool-id ∘ Bool-id ≡ id Bool-id-equiv = funExt Bool-id-pointwise Bool-linv : linv Bool-id Bool-linv .fst = Bool-id Bool-linv .snd = funExt Bool-id-pointwise Bool-rinv : rinv Bool-id Bool-rinv .fst = Bool-id Bool-rinv .snd = funExt Bool-id-pointwise Bool-id-biinv : BiInvEquiv Bool Bool Bool-id-biinv = biInvEquiv Bool-id Bool-id Bool-id-pointwise Bool-id Bool-id-pointwise Bool-id-iso : Iso Bool Bool Bool-id-iso = iso Bool-id Bool-id Bool-id-pointwise Bool-id-pointwise Bool-id-biinv-equiv : Bool ≃ Bool Bool-id-biinv-equiv = Bool-id , isoToIsEquiv Bool-id-iso Bool-id-path : Bool ≡ Bool Bool-id-path = ua Bool-id-biinv-equiv ```
michael commented 2023-05-15 19:19:19 +00:00
Author
Owner
Copy link

I think this is resolved in 9716b4b69b ?

reason for i think is because the Iso doesn't actually use the BiInvEquiv itself, but i think that's fine for now

I _think_ this is resolved in 9716b4b69b3af70dcab68ed3d5321adb8789dfbd ? reason for i think is because the `Iso` doesn't actually use the `BiInvEquiv` itself, but i think that's fine for now
michael added this to the (deleted) project 2023-05-15 23:26:44 +00:00
michael added the
T-equivalence
 label 2023-05-17 09:55:54 +00:00
Sign in to join this conversation.
No Branch/Tag specified
Branches Tags
master
No results found.
Labels
Clear labels   
asking-favonia

   
exercise

   
questions

Open questions I'm trying to find the answer to

  
T-equivalence

[Topic] Equivalence-related issues

No labels
asking-favonia
exercise
questions
T-equivalence
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference: school/type-theory#3
No description provided.
Delete branch "%!s()"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?