2015-02-24 22:09:20 +00:00
|
|
|
constant (A : Type₁)
|
|
|
|
|
constant (hom : A → A → Type₁)
|
2015-12-09 05:11:11 +00:00
|
|
|
constant (id' : Πa, hom a a)
|
2015-02-24 22:09:20 +00:00
|
|
|
|
|
|
|
|
structure is_iso [class] {a b : A} (f : hom a b) :=
|
|
|
|
|
(inverse : hom b a)
|
|
|
|
|
open is_iso
|
|
|
|
|
|
|
|
|
|
set_option pp.metavar_args true
|
|
|
|
|
set_option pp.purify_metavars false
|
|
|
|
|
|
2015-12-09 05:11:11 +00:00
|
|
|
definition inverse_id [instance] {a : A} : is_iso (id' a) :=
|
|
|
|
|
is_iso.mk (id' a) (id' a)
|
2015-02-24 22:09:20 +00:00
|
|
|
|
|
|
|
|
definition inverse_is_iso [instance] {a b : A} (f : hom a b) (H : is_iso f) : is_iso (@inverse a b f H) :=
|
|
|
|
|
is_iso.mk (inverse f) f
|
|
|
|
|
|
|
|
|
|
constant a : A
|
|
|
|
|
|
2015-12-08 22:58:08 +00:00
|
|
|
set_option trace.class_instances true
|
2015-02-24 22:09:20 +00:00
|
|
|
|
2015-12-09 05:11:11 +00:00
|
|
|
definition foo := inverse (id' a)
|
2015-02-24 22:09:20 +00:00
|
|
|
|
|
|
|
|
set_option pp.implicit true
|
|
|
|
|
|
|
|
|
|
print definition foo
|
