idk what this progress was but here's progress
This commit is contained in:
parent
3c668bfd02
commit
c7f4ee0708
|
@ -13,11 +13,20 @@ open import Data.Product.Base
|
||||||
id : ∀ {ℓ} {A : Type ℓ} → A → A
|
id : ∀ {ℓ} {A : Type ℓ} → A → A
|
||||||
id x = x
|
id x = x
|
||||||
|
|
||||||
|
linv′ : {A B : Type} (f : A → B) → Type
|
||||||
|
linv′ {A} {B} f = Σ[ g ∈ (B → A) ] (g ∘ f ≡ id)
|
||||||
|
|
||||||
|
rinv′ : {A B : Type} (f : A → B) → Type
|
||||||
|
rinv′ {A} {B} f = Σ[ g ∈ (B → A) ] (f ∘ g ≡ id)
|
||||||
|
|
||||||
|
-- Using this definition will need funExt everywhere
|
||||||
|
-- Use this:
|
||||||
|
|
||||||
linv : {A B : Type} (f : A → B) → Type
|
linv : {A B : Type} (f : A → B) → Type
|
||||||
linv {A} {B} f = Σ[ g ∈ (B → A) ] (g ∘ f ≡ id)
|
linv {A} {B} f = Σ[ g ∈ (B → A) ] ((x : A) → g (f x) ≡ x)
|
||||||
|
|
||||||
rinv : {A B : Type} (f : A → B) → Type
|
rinv : {A B : Type} (f : A → B) → Type
|
||||||
rinv {A} {B} f = Σ[ g ∈ (B → A) ] (f ∘ g ≡ id)
|
rinv {A} {B} f = Σ[ g ∈ (B → A) ] ((y : B) → f (g y) ≡ y)
|
||||||
|
|
||||||
biinv : {A B : Type} (f : A → B) → Type
|
biinv : {A B : Type} (f : A → B) → Type
|
||||||
biinv f = linv f × rinv f
|
biinv f = linv f × rinv f
|
||||||
|
@ -32,12 +41,12 @@ Bool-id-pointwise : (b : Bool) → Bool-id (Bool-id b) ≡ b
|
||||||
Bool-id-pointwise true = refl
|
Bool-id-pointwise true = refl
|
||||||
Bool-id-pointwise false = refl
|
Bool-id-pointwise false = refl
|
||||||
|
|
||||||
Bool-id-equiv : Bool-id ∘ Bool-id ≡ id
|
-- Bool-id-equiv : Bool-id ∘ Bool-id ≡ id
|
||||||
Bool-id-equiv = funExt Bool-id-pointwise
|
-- Bool-id-equiv = funExt Bool-id-pointwise
|
||||||
|
|
||||||
Bool-linv : linv Bool-id
|
Bool-linv : linv Bool-id
|
||||||
Bool-linv .fst = Bool-id
|
Bool-linv .fst = Bool-id
|
||||||
Bool-linv .snd = funExt Bool-id-pointwise
|
Bool-linv .snd = ?
|
||||||
|
|
||||||
Bool-rinv : rinv Bool-id
|
Bool-rinv : rinv Bool-id
|
||||||
Bool-rinv .fst = Bool-id
|
Bool-rinv .fst = Bool-id
|
||||||
|
|
|
@ -34,7 +34,7 @@ convert-fiber Top = true , refl
|
||||||
convert-fiber Bottom = false , refl
|
convert-fiber Bottom = false , refl
|
||||||
|
|
||||||
convert-fiber-is-contr : (y : Other) → (fz : fiber convert y) → convert-fiber y ≡ fz
|
convert-fiber-is-contr : (y : Other) → (fz : fiber convert y) → convert-fiber y ≡ fz
|
||||||
convert-fiber-is-contr y fz i =
|
convert-fiber-is-contr y fz =
|
||||||
let
|
let
|
||||||
fx : fiber convert y
|
fx : fiber convert y
|
||||||
fx = convert-fiber y
|
fx = convert-fiber y
|
||||||
|
@ -71,15 +71,22 @@ convert-fiber-is-contr y fz i =
|
||||||
sfx = snd fx
|
sfx = snd fx
|
||||||
sfz = snd fz
|
sfz = snd fz
|
||||||
|
|
||||||
what : sfx ≡ ?
|
what : sfx ≡ ? -- sfz
|
||||||
what = ?
|
what = ?
|
||||||
in
|
in
|
||||||
|
|
||||||
-- z = fst fz
|
-- z = fst fz
|
||||||
-- convert-fiber y ≡ fz
|
-- convert-fiber y ≡ fz
|
||||||
-- (x , convert x₁ ≡ y) ≡ (z , convert z₁ ≡ y)
|
-- fx ≡ fz
|
||||||
|
-- Look into this more:
|
||||||
|
-- (x , convert x₁ ≡ y) ≡ (z , convert z₁ ≡ y)
|
||||||
|
-- Σ[ x ∈ A ] (convert x ≡ y)
|
||||||
|
-- (x , _)
|
||||||
-- - x ≡ z
|
-- - x ≡ z
|
||||||
-- - (convert x₁ ≡ y) ≡ (convert z₁ ≡ y)
|
-- ------ - (convert x₁ ≡ y) ≡ (convert z₁ ≡ y)
|
||||||
eqv7 i , (λ j → ?)
|
--
|
||||||
|
-- eqv7 ?
|
||||||
|
?
|
||||||
|
|
||||||
convert-is-equiv : isEquiv convert
|
convert-is-equiv : isEquiv convert
|
||||||
convert-is-equiv .equiv-proof y = convert-fiber y , convert-fiber-is-contr y
|
convert-is-equiv .equiv-proof y = convert-fiber y , convert-fiber-is-contr y
|
||||||
|
|
Loading…
Reference in a new issue