Commit 28a04426 authored by Nicola Botta's avatar Nicola Botta
Browse files

Initial.

parent 17894129
> module Isomorphism.Properties
> import Control.Isomorphism
> -- import Isomorphism.Operations
> import Fun.Properties
> import Basic.Operations
> %default total
> %access public export
> |||
> isoEq : {A, B : Type} -> A = B -> Iso A B
> isoEq Refl = isoRefl
> %freeze isoEq
> |||
> isoCong : {A : Type} -> {x : A} -> {y : A} -> {P : A -> Type} -> x = y -> Iso (P x) (P y)
> isoCong {x} {P} prf = replace {P = \ z => Iso (P x) (P z)} prf isoRefl
> %freeze isoCong
Injectivity of to and from
> injectiveFrom : {A, B : Type} -> (iso : Iso A B) -> Injective1 (from iso)
> injectiveFrom {A} {B} (MkIso to from toFrom fromTo) b1 b2 p = s3 where
> s1 : from b1 = from b2
> s1 = p
> s2 : to (from b1) = to (from b2)
> s2 = cong s1
> s3 : b1 = b2
> s3 = replace2 {a = B} {a1 = to (from b1)} {a2 = b1}
> {b = B} {b1 = to (from b2)} {b2 = b2}
> {P = \ a => \b => a = b}
> (toFrom b1) (toFrom b2) s2
> %freeze injectiveFrom
> {-
> ---}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment